*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] structured induction proofs using customized induction scheme*From*: Bianca Lutz <bianca.lutz at gmx.net>*Date*: Wed, 3 Feb 2010 22:04:44 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1265201904.2234.97.camel@macbroy12.informatik.tu-muenchen.de>*References*: <5002b9521001260735x47fbe207ueb0dea8877c73695@mail.gmail.com> <1265201904.2234.97.camel@macbroy12.informatik.tu-muenchen.de>*Reply-to*: bianca.lutz at gmx.net*Sender*: bialut at googlemail.com

Hi Johannes, thanks for your advice. Now I see that my posting was misleading. I'm sorry about that. What I tried to describe was Isabelle's interpretation of my induction scheme to highlight the two schematic variables. The actual lemma statement involves no question marks: lemma R_induct: [[ R t1 t2; /\t1 t2. [[P2 t1 t2]] ==> P1 (T1 t1) (T1 t2); /\t1 t2. [[P2 t1 t2]] ==> P1 (T2 t1) (T2 t2); /\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & P1 (op t1 x) (op t2 x)]] ==> P2 t1 t2; ... ]] ==> P1 t1 t2 Just as you suggested. I should make things a bit clearer, I guess. I have an inductively defined predicate on terms inductive lc :: term => bool and I want to prove lemma R_lc: fixes t1 t2 assumes "R t1 t2" shows "lc t1 & lc t2" proof (induct rule: R_induct[of t1 t2 "%t1 t2. (ALL x. Q x --> lc (op t1 x) & lc (op t2 x))" "%t1 t2. lc t1 & lc t2"]) case 2 As I mentioned in the last post Isabelle fails at the last line *** Illegal schematic variable(s) in case "2" *** At command "case". According to Isabelle->Show me...->cases case "2" is defined as 2: fix t1 t2 let "?case" = "lc (T1 t1) & lc (T2 t2)" assume 2.hyps: "ALL x. Q x --> lc (op t1 x) & lc (op t2 x)" and 2.prems: Whereas the subgoal corresponding to case "2" is /\t1 t2. [[ ALL x. Q x --> lc (op t1 x) & lc (op t2 x) ]] ==> lc (T1 t1) & lc (T1 t2) Yet, I don't understand Isabelle's failure ... > By the way you can provide names to the cases with: > > lemma R_induct[case_names Name1 Name2 Name3]: > .... Thanks, this will make some of my proofs a lot more readable. Bianca.

**Follow-Ups**:**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Andreas Lochbihler

**References**:**Re: [isabelle] structured induction proofs using customized induction scheme***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] structured induction proofs using customized induction scheme
- Next by Date: Re: [isabelle] structured induction proofs using customized induction scheme
- Previous by Thread: Re: [isabelle] structured induction proofs using customized induction scheme
- Next by Thread: Re: [isabelle] structured induction proofs using customized induction scheme
- Cl-isabelle-users February 2010 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