*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] structured induction proofs using customized induction scheme*From*: Bianca Lutz <bianca.lutz at gmx.net>*Date*: Tue, 26 Jan 2010 16:35:46 +0100*Reply-to*: bianca.lutz at gmx.net*Sender*: bialut at googlemail.com

Hello, I have some problems concerning customized induction schemes in conjunction with structured induction proofs using the induct method. Consider the following two datatypes: term = T1 term | T2 term | ... var = string a primrec function op :: [term, var] => term and an inductively defined relation R :: [term, term] => bool where R1: [[ ALL x. Q x --> R (op t1 x) (op t2 x) ]] ==> R (T1 t1) (T1 t2) | R2: [[ ALL x. Q x --> R (op t1 x) (op t2 x) ]] ==> R (T2 t1) (T2 t2) | ... whereas Q is a rather long statement concerning elements of type var. 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 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 Unfortunately, when I use this as shown below Isabelle fails at the last line: *** Illegal schematic variable(s) in case "2" *** at command "case" although there is no schematic variable in case "2" (at least according to Isabelle->Show me...->cases), since I instantiated ?P2 with some appropriate predicate beforehand ... lemma assumes "R t1 t2" shows "P1 t1 t2" proof (induct rule: R_induct[of t1 t2 P2 P1]) case 1 thus ?case by (simp add: assms) (* R t1 t2 *) next case 2 I have no idea how to avoid this. Any suggestions? Thanks, Bianca.

- Previous by Date: Re: [isabelle] Word32/64 ?
- Next by Date: [isabelle] Order of type parameters in record definition
- Previous by Thread: Re: [isabelle] Word32/64 ?
- Next by Thread: [isabelle] Order of type parameters in record definition
- Cl-isabelle-users January 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