Re: [isabelle] structured induction proofs using customized induction scheme



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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.