[isabelle] structured induction proofs using customized induction scheme



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.





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