*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] structured induction*From*: Makarius <makarius at sketis.net>*Date*: Tue, 5 Aug 2008 19:05:05 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <18584.28607.357728.841943@locatelli.inf.ed.ac.uk>*References*: <18584.28607.357728.841943@locatelli.inf.ed.ac.uk>

On Tue, 5 Aug 2008, Randy Pollack wrote: > lemma > assumes h:"R M" --"R is an inductively defined relation" > shows "P M = {}" "Q M" --"P and Q are any properties" > using h proof (induct) > case (constr1 X) --"constr1 is a single argument constructor of R" > show ?case > > The last line will fail: > > *** Unbound schematic variable: ?case > > The ProofGeneral drop down for cases shows something about > "subcases: 1 2" How do I get ?case to work in this setting? You first need to enter the particular sub cases before the ?case binding show up. See the end of src/HOL/Induct/Common_Patterns.thy for examples for induction with multiple goals. > Please give pointers to some examples of well-founded induction over a > measure function in Isabelle 2008. I know of Makarius' note "Structured > Induction Proofs ...", but I still can't get things to work in the > structured way (as opposed to using the object language to give an > explicit induction predicate ...). Maybe you did not use the proper rule, which is wf_induct_rule as opposed to the old wf_induct (the correct rule is already declared as canonical induction scheme for `wf r` facts). Here is an example pattern involving both an extra parameter x and premise "A x a", apart from the induction argument a: lemma fixes a :: 'a and r :: "('a * 'a) set" and x :: 'b assumes "wf r" and "A x a" shows "B x a" using assms proof (induct a arbitrary: x) case (less a) note prem = `A x a` -- {* cf. @{thm less.prems} *} note hyp = `!!x y. (y, a) : r ==> A x y ==> B x y` -- {* cf. @{thm less.hyps} *} show ?case sorry qed The example from the "Structured Induction Proofs ..." paper is in src/HOL/Isar_examples/Puzzle.thy (it uses the less_induct rule). Makarius

**References**:**[isabelle] structured induction***From:*Randy Pollack

- Previous by Date: [isabelle] structured induction
- Next by Date: [isabelle] LAST CALL FOR PARTICIPATION (TPHOLs'2008)
- Previous by Thread: [isabelle] structured induction
- Next by Thread: [isabelle] LAST CALL FOR PARTICIPATION (TPHOLs'2008)
- Cl-isabelle-users August 2008 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