Re: [isabelle] exception THM 0 raised (line 737 of "thm.ML")



OK, here are some bits of information, none of which are a satisfactory
answer.

1) It's clear the problem comes from the extra meta-quantified "x" and
"xa" in super.induct.

2) You can use super.induct[simplified] as an induction rule. That gets
rid of the pointless quantification and essentially gives you
nat.induct. Then the cases can be proven.

3) If you turn ML's debugging trace on, you get this explanation:

Here's the full trace:
Exception trace - exception THM 0 raised (line 737 of "thm.ML"): assume:
variables
Assumption.assume_hyps(2)
Basics.fold_map(3)()
Assumption.add_assms(3)
Proof.gen_assume(8)(1)
Proof.gen_assume(8)
Proof.gen_case(5)
Library.oo(1)(1)(1)
Toplevel.gen_proofs'(2)(1)(1)(1)
exception THM 0 raised (line 737 of "thm.ML"): assume: variables

So, the problem is, the "case" mechanism is trying to depend on an
assumption involving more variables. I'm guessing those variables were
invented by the "fun" package to handle the *two* binders of "x" created
by the syntax "{x | x . x : super n}". I think the package is then
getting confused, because these variables don't actually get involved in
the induction principle.

I would suspect that for more involved recursive functions, the
variables involved will be connected to the induction principle for it
to be useful. But you might have to fiddle a bit to get that to be true.

Cheers,
    Thomas.

On 09/03/16 03:47, Daniel StÃwe wrote:
Hi all,

in my bachelor's thesis I was working with functions calling
themselves in a set comprehension.
But while using induction and Isar with the induction rules for these
functions I got an unexpected exception in the case of the induction
step. I guess some unnecessary fixed variables in the rule are causing
this.

I created a minimal example showing the exception at last:


theory Super
imports Main
begin

fun super where
"super 0 = {}" |
"super (Suc n) = { x | x . x â super n}"

lemma "x â super n â P x"
by (induction n rule: super.induct) auto

lemma "x â super n â P x"
proof (induction n)
case 0
  thus ?case by simp
next
  case (Suc n)
  thus ?case by auto
qed

thm super.induct nat.induct
(*
  â?P 0; ân. (âx xa. ?P n) â ?P (Suc n)â â ?P ?a0.0
  â?P 0; ânat. ?P nat â ?P (Suc nat)â â ?P ?nat
*)

lemma "x â super n â P x"
proof (induction n rule: super.induct)
print_cases
  case 1
  thus ?case by simp
next
  case 2
  (* exception THM 0 raised (line 661 of "thm.ML") - Isabelle 2015 *)
  (* exception THM 0 raised (line 737 of "thm.ML") - Isabelle 2016 *)
oops

end


Greetings,
Daniel




________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.