Email Gateway (Aug 18 2022 at 10:48): Email Gateway (Aug 18 2022 at 10:48):From: Andreas Lochbihler <lochbihl@infosun.fim.uni-passau.de>
Hi Peter,
if you look in the original TransitiveClosure theory of HOL, you also
find an extra rule for pairs.
However, you do not have to prove the induction rule by hand, but you
can have Isabelle generate it for you:
In TransitiveClosure.thy:
lemmas rtrancl_induct2 =
rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
consumes 1, case_names refl step]
So, your trcl_pair_induct could be written as
lemmas trcl_pair_induct =
trcl_induct[of "(xc1,xc2)" "xb" "(xa1,xa2)", split_format (complete),
consumes 1, case names empty cons]
Induction over inductive sets where the element to be in the set in the
premises is not of the most general form is always a problem because
induct discards everything like pairs, a fixed parameter and the like.
An alternative would be to reformulate the lemma you want to prove, but
this is very tedious if you have to do it multiple times.
lemma preserves_cl: "[| (c,w,c') : trcl T; c = (a, b); c' = (a', b') |]
\<Longrightarrow> Prop a b \<Longrightarrow> Prop a' b'"
Regards,
Andreas
Email Gateway (Aug 18 2022 at 10:51):From: Peter Lammich <peter.lammich@uni-muenster.de>
I have the following problem with set induction and pair datatypes,
illustrated in the pice of code below:
-- "Defining transitive closure of labeled transition system as
inductive set"
types ('c,'a) LTS = "('c \<times> 'a \<times> 'c) set"
text {* Transitive closure of LTS *}
consts trcl :: "('c,'a) LTS \<Rightarrow> ('c,'a list) LTS"
inductive "trcl t"
intros
empty[simp]: "(c,[],c) \<in> trcl t"
cons[simp]: "\<lbrakk> (c,a,c') \<in> t; (c',w,c'') \<in> trcl t
\<rbrakk> \<Longrightarrow> (c,a#w,c'') \<in> trcl t"
-- "Now do some very simple inductive proof, using trcl.induct"
consts T':: "(nat \<times> bool \<times> nat) set"
consts Prop':: "nat \<Rightarrow> bool"
lemma preserves': "(a,e,a')\<in>T' \<Longrightarrow> Prop' a
\<Longrightarrow> Prop' a'" sorry
lemma preserves_trcl': "(a,w,a')\<in>trcl T' \<Longrightarrow> Prop' a
\<Longrightarrow> Prop' a'"
apply (induct rule: trcl.induct)
apply (auto simp add: preserves')
done
-- "Ok, this works fine !"
-- "Now we want to do the same for states that are pairs: "
consts T:: "((nat \<times> nat) \<times> bool \<times> (nat \<times>
nat)) set"
consts Prop:: "nat \<Rightarrow> nat \<Rightarrow> bool"
lemma preserves: "((a,b),e,(a',b'))\<in>T \<Longrightarrow> Prop a b
\<Longrightarrow> Prop a' b'" sorry
lemma preserves_cl: "((a,b),w,(a',b'))\<in>trcl T \<Longrightarrow> Prop
a b \<Longrightarrow> Prop a' b'"
apply (induct rule: trcl.induct)
oops
This did not get the induction correctly, there are the following
subgoals:
1. \<And>c. Prop a b \<Longrightarrow> Prop a' b'
2. \<And>aa c c' c'' w. \<lbrakk>(c, aa, c') \<in> T; (c', w, c'')
\<in> trcl T; Prop a b \<Longrightarrow> Prop a' b'; Prop a b\<rbrakk>
\<Longrightarrow> Prop a' b'
the first one is obviously not provable
What can I do about this ? Currently I'm working around by providing a
specialized induction rule for pairs:
lemma trcl_pair_induct[induct set]:
"\<lbrakk>((xc1,xc2), xb, (xa1,xa2)) \<in> trcl t; \<And>c1 c2. P c1
c2 [] c1 c2; \<And>a c1 c2 c1' c2' c1'' c2'' w. \<lbrakk>((c1,c2), a,
(c1',c2')) \<in> t; ((c1',c2'), w, (c1'',c2'')) \<in> trcl t; P c1' c2'
w c1'' c2''\<rbrakk> \<Longrightarrow> P c1 c2 (a # w) c1'' c2''\<rbrakk>
\<Longrightarrow> P xc1 xc2 xb xa1 xa2"
using trcl.induct[of "(xc1,xc2)" xb "(xa1,xa2)" t "\<lambda>c w c'.
let (c1,c2)=c in let (c1',c2')=c' in P c1 c2 w c1' c2'"] by auto
Is this the way to go, or is there another (nicer) possibility, i.e. one
generic scheme that can handle pairs, triples and so on
Many thanks in advance, yours
Peter
Last updated: May 03 2024 at 04:19 UTC