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

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
 fix t1 t2
 let "?case" = "lc (T1 t1) & lc (T2 t2)"
   "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.


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