Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] More problems with induction

Email Gateway (Aug 18 2022 at 10:55):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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

Email Gateway (Aug 18 2022 at 10:55):

From: Makarius <makarius@sketis.net>
See the isar-ref manual. Some common patterns are given in
HOL/Induct/Common_Patterns.thy

Makarius

Last updated: May 03 2024 at 12:27 UTC