*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] exception THM 0 raised (line 737 of "thm.ML")*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Thu, 10 Mar 2016 11:49:45 +1100*In-reply-to*: <2fe0b39b925591513b8710f3b904a24d@in.tum.de>*References*: <2fe0b39b925591513b8710f3b904a24d@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

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.

**References**:**[isabelle] exception THM 0 raised (line 737 of "thm.ML")***From:*Daniel StÃwe

- Previous by Date: [isabelle] New AFP article: The Cartan Fixed Point Theorems
- Next by Date: [isabelle] using and simp add:
- Previous by Thread: [isabelle] exception THM 0 raised (line 737 of "thm.ML")
- Next by Thread: [isabelle] New AFP article: The Cartan Fixed Point Theorems
- Cl-isabelle-users March 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list