*To*: bianca.lutz at gmx.net*Subject*: Re: [isabelle] structured induction proofs using customized induction scheme*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 03 Feb 2010 13:58:24 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5002b9521001260735x47fbe207ueb0dea8877c73695@mail.gmail.com>*Organization*: Technische Universität München*References*: <5002b9521001260735x47fbe207ueb0dea8877c73695@mail.gmail.com>

Hi Bianca, Am Dienstag, den 26.01.2010, 16:35 +0100 schrieb Bianca Lutz: [..] > The induction scheme R.induct has the following shape: > [[ R t1 t2; > /\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P (op t1 x) (op t2 x)]] > ==> ?P (T1 t1) (T1 t2); > /\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P (op t1 x) (op t2 x)]] > ==> ?P (T2 t1) (T2 t2); > ... > ]] ==> ?P t1 t2 Here ?P is an quantified variable which can be arbitrary instantiated when R.induct is used. > Usually there is some predicate P2 t1 t2 following from > ALL x. Q x --> R (op t1 x) (op t2 x) & P (op t1 x) (op t2 x) > that solves both R1 and R2. > > Therefore, I proved the following customized induction scheme > 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 When Isabelle reads variables with question marks in theorems they are interpreted as existentially quantified variables. Just don't write them with question marks, Isabelle interprets each identifier which is not defined as constant as all quantified variable. So write: 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" unfortunately when Isabelle writes theorems (like "thm R_induct") the all quantified variables are shown with question marks. By the way you can provide names to the cases with: lemma R_induct[case_names Name1 Name2 Name3]: .... > Unfortunately, when I use this as shown below Isabelle fails at the last line: > *** Illegal schematic variable(s) in case "2" > *** at command "case" I hope this solves your problem, Johannes

**Follow-Ups**:

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