Email Gateway (Aug 18 2022 at 10:55): Email Gateway (Aug 18 2022 at 10:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 10:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
I found the second problem myself: I left placeholders (?X, etc) in the
lemma, that probably got instantiated to some special values ...
But the first problem is still there: How to generate an appropriate
induction theorem for fixed parameter \<alpha> ?
Peter Lammich wrote:
Last updated: Nov 21 2024 at 12:39 UTC