[isabelle] More problems with induction



Again considering the same recdef, that defines some advanced shuffle
operator:

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 {})"

lemma [simp]: "w\<otimes>\<^bsub>\<alpha>\<^esub>[] = {w}" by (cases w,
auto)

Now I want to prove the following lemma:
lemma cil_contains_empty[simp]: "[] \<in>
wa\<otimes>\<^bsub>\<alpha>\<^esub>wb \<longrightarrow> wa=[] \<and> wb=[]"
  apply (induct rule: cil.induct)
this leaves me with some odd subgoals of the form:
2. \<And>\<alpha> ad ae. ad # ae \<in> wa
\<otimes>\<^bsub>\<alpha>\<^esub> [] \<longrightarrow> wa = ad # ae
\<and> [] = ad # ae
  (Consider the last conjunct, []=ad#ae). It obviously does not the same
case distinction as in the definition, but fixes wa.

I have no idea how to get the right unification automatically, my
current workaround is instantiating the induction rule by hand:
  apply (rule cil.induct[where P="\<lambda>\<alpha> wa wb. [] \<in>
wa\<otimes>\<^bsub>\<alpha>\<^esub>wb \<longrightarrow> wa=[] \<and>
wb=[]"])
  apply auto

this works, but is many writing overhead and makes the proof look confusing.

Is there any documentation/tutorial information on how the induct method
works and what all the parameters mean (e.g. arbitrary). The
Isabelle/HOL Tutorial only covers induct_tac.

Many thanks for any hints again,
  yours Peter










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