[isabelle] Problems with induction



I've defined some extended interleaving operator, that has a parameter
\<alpha>. I used recdef:

consts cil :: "('a \<Rightarrow> ('m set \<times> 'm set)) \<times> ('a
list) \<times> ('a list) \<Rightarrow> 'a list set"

syntax
  cons_interleave :: "'a list \<Rightarrow> ('a \<Rightarrow> ('m set
\<times> 'm set)) \<Rightarrow> 'a list \<Rightarrow> 'a list set" ("_
\<otimes>\<^bsub>_\<^esub> _" [64,64,64] 64)
translations
  "a\<otimes>\<^bsub>\<alpha>\<^esub>b" == "cil (\<alpha>,a,b)"

recdef "cil" "measure (\<lambda>(\<alpha>,x,y). length x + length y)"
  "[] \<otimes>\<^bsub>\<alpha> \<^esub> w = {w}"
  "w \<otimes>\<^bsub>\<alpha>\<^esub> [] = {w}"
  "e1#w1 \<otimes>\<^bsub>\<alpha>\<^esub> e2#w2 = (if fst (\<alpha> e1)
\<inter> foldl (op \<union>) {} (map (\<lambda>e. fst (\<alpha> e)
\<union> snd (\<alpha> e)) (e2#w2)) = {} then e1\<cdot>(w1
\<otimes>\<^bsub>\<alpha>\<^esub> e2#w2) else {}) \<union>
                     (if fst (\<alpha> e2) \<inter> foldl (op \<union>)
{} (map (\<lambda>e. fst (\<alpha> e) \<union> snd (\<alpha> e))
(e1#w1)) = {} then e2\<cdot>(e1#w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2)
else {})"


This generates an induction theorem:
thm cil.induct
(*
\<lbrakk>\<And>\<alpha>. ?P \<alpha> [] []; \<And>\<alpha> ad ae. ?P
\<alpha> [] (ad # ae); \<And>\<alpha> z aa. ?P \<alpha> (z # aa) [];
 \<And>\<alpha> e1 w1 e2 w2.
    \<lbrakk>fst (\<alpha> e2) \<inter>
     foldl op \<union> {} (map (\<lambda>e. fst (\<alpha> e) \<union>
snd (\<alpha> e)) (e1 # w1)) =
     {} \<longrightarrow>
     ?P \<alpha> (e1 # w1) w2;
     fst (\<alpha> e1) \<inter>
     foldl op \<union> {} (map (\<lambda>e. fst (\<alpha> e) \<union>
snd (\<alpha> e)) (e2 # w2)) =
     {} \<longrightarrow>
     ?P \<alpha> w1 (e2 # w2)\<rbrakk>
    \<Longrightarrow> ?P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk>
\<Longrightarrow> ?P ?u ?v ?w
*)
This induction theorem is too general for my intended use, where the
parameter \<alpha> is always fixed. My first question is:
Can I automatically generate an induction theorem where \<alpha> is
fixed (or tell induct to fix \<alpha>) ?

I tried to work around, and thought some theorem like the one below
might do (I simply removed \<alpha> from the \<And>-quantifier binding):

lemma "\<lbrakk>?P \<alpha> [] []; \<And>ad ae. ?P \<alpha> [] (ad #
ae); \<And>z aa. ?P \<alpha> (z # aa) [];
 \<And>e1 w1 e2 w2.
    \<lbrakk>fst (\<alpha> e2) \<inter>
     foldl op \<union> {} (map (\<lambda>e. fst (\<alpha> e) \<union>
snd (\<alpha> e)) (e1 # w1)) =
     {} \<longrightarrow>
     ?P \<alpha> (e1 # w1) w2;
     fst (\<alpha> e1) \<inter>
     foldl op \<union> {} (map (\<lambda>e. fst (\<alpha> e) \<union>
snd (\<alpha> e)) (e2 # w2)) =
     {} \<longrightarrow>
     ?P \<alpha> w1 (e2 # w2)\<rbrakk>
    \<Longrightarrow> ?P \<alpha> (e1 # w1) (e2 # w2)\<rbrakk>
\<Longrightarrow> ?P \<alpha> ?v ?w"

I tried to prove this with auto:

apply (auto elim: cil.induct)

and isabelle prints: No subgoals.
but when I issue a done:
done

I get the following error message:

(*
*** Proved a different theorem: \<lbrakk>True; \<And>ad ae. True;
\<And>z aa. True;
***  \<And>e1 w1 e2 w2.
***     \<lbrakk>fst (\<alpha> e2) \<inter>
***      foldl op \<union> {} (map (\<lambda>e. fst (\<alpha> e)
\<union> snd (\<alpha> e)) (e1 # w1)) =
***      {} \<longrightarrow>
***      True;
***      fst (\<alpha> e1) \<inter>
***      foldl op \<union> {} (map (\<lambda>e. fst (\<alpha> e)
\<union> snd (\<alpha> e)) (e2 # w2)) =
***      {} \<longrightarrow>
***      True\<rbrakk>
***     \<Longrightarrow> True\<rbrakk>
*** \<Longrightarrow> True
*** At command "done".
*)

Now I'm completely confused. I neither understand how to do induction
nicely when the parameter \<alpha> is fixed. (Probably I can always
rewrite my goal and add a "\<alpha>=fixedExp", where fixedExp is my
fixed parameter. But is this writing overhead necessary?) nor do I
understand what this error message about proving a different theorem means ?

Thanks in advance for any help/explanations
  Peter











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