Re: [isabelle] structured induction proofs using customized induction scheme
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:
[[ 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
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"])
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)"
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