# [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.