--- a/thys2/BasicIdentities.thy Tue Mar 29 10:57:02 2022 +0100
+++ b/thys2/BasicIdentities.thy Wed Mar 30 11:18:51 2022 +0100
@@ -53,6 +53,16 @@
(if x \<in> acc then rdistinct xs acc
else x # (rdistinct xs ({x} \<union> acc)))"
+lemma rdistinct_concat:
+ shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
+ apply(induct rs)
+ apply simp+
+ done
+
+lemma rdistinct_concat2:
+ shows "\<forall>r \<in> set rs. r \<in> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
+ by (simp add: rdistinct_concat subsetI)
+
lemma distinct_not_exist:
shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)"
--- a/thys2/ClosedForms.thy Tue Mar 29 10:57:02 2022 +0100
+++ b/thys2/ClosedForms.thy Wed Mar 30 11:18:51 2022 +0100
@@ -544,11 +544,34 @@
by (meson fr_in_rstar freal_trans)
+lemma gr_in_rstar : "r1 \<leadsto>g r2 \<Longrightarrow> r1 \<leadsto>g* r2"
+ using grewrites.intros(1) grewrites.intros(2) by blast
+
+lemma greal_trans[trans]:
+ assumes a1: "r1 \<leadsto>g* r2" and a2: "r2 \<leadsto>g* r3"
+ shows "r1 \<leadsto>g* r3"
+ using a2 a1
+ apply(induct r2 r3 arbitrary: r1 rule: grewrites.induct)
+ apply(auto)
+ done
+
+
+lemma gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"
+ by (meson gr_in_rstar greal_trans)
+
+
+
lemma frewrite_append:
shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
apply(induct rs)
apply simp+
using frewrite.intros(3) by blast
+
+lemma grewrite_append:
+ shows "\<lbrakk> rsa \<leadsto>g rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>g rs @ rsb"
+ apply(induct rs)
+ apply simp+
+ using grewrite.intros(3) by blast
@@ -559,12 +582,25 @@
using frewrite.intros(3) by blast
+lemma grewrites_cons:
+ shows "\<lbrakk> rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>g* r # rsb"
+ apply(induct rsa rsb rule: grewrites.induct)
+ apply simp
+ using grewrite.intros(3) by blast
+
+
lemma frewrites_append:
shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"
apply(induct rs)
apply simp
by (simp add: frewrites_cons)
+lemma grewrites_append:
+ shows " \<lbrakk>rsa \<leadsto>g* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>g* (rs @ rsb)"
+ apply(induct rs)
+ apply simp
+ by (simp add: grewrites_cons)
+
lemma frewrites_concat:
@@ -580,6 +616,37 @@
apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later)
using frewrites_cons by auto
+lemma grewrites_concat:
+ shows "\<lbrakk>rs1 \<leadsto>g rs2; rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>g* (rs2 @ rsb)"
+ apply(induct rs1 rs2 rule: grewrite.induct)
+ apply(simp)
+ apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>g (rs @ rsa)")
+ prefer 2
+ using grewrite.intros(1) apply blast
+ apply(subgoal_tac "(rs @ rsa) \<leadsto>g* (rs @ rsb)")
+ using gmany_steps_later apply blast
+ apply (simp add: grewrites_append)
+ apply (metis append.assoc append_Cons grewrite.intros(2) grewrites_append gmany_steps_later)
+ using grewrites_cons apply auto
+ apply(subgoal_tac "rsaa @ a # rsba @ a # rsc @ rsa \<leadsto>g* rsaa @ a # rsba @ a # rsc @ rsb")
+ using grewrite.intros(4) grewrites.intros(2) apply force
+ using grewrites_append by auto
+
+
+lemma grewritess_concat:
+ shows "\<lbrakk>rsa \<leadsto>g* rsb; rsc \<leadsto>g* rsd \<rbrakk> \<Longrightarrow> (rsa @ rsc) \<leadsto>g* (rsb @ rsd)"
+ apply(induct rsa rsb rule: grewrites.induct)
+ apply(case_tac rs)
+ apply simp
+ using grewrites_append apply blast
+ by (meson greal_trans grewrites.simps grewrites_concat)
+
+lemma grewrites_equal_rsimp:
+ shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+ apply simp
+ sorry
+
+
lemma frewrites_middle:
shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)"
by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3))
@@ -588,11 +655,6 @@
shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2"
by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later)
-lemma many_steps_later1:
- shows " \<lbrakk>rs1 \<leadsto>f* rs2\<rbrakk>
- \<Longrightarrow> (RONE # rs1) \<leadsto>f* (RONE # rs2)"
- oops
-
lemma early_late_der_frewrites:
shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)"
apply(induct rs)
@@ -620,23 +682,9 @@
lemma rd_flts_set:
- shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 (insert RZERO (rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f*
- rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))"
-
- oops
-
-
-
-lemma rd_flts_set2:
- shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ((rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f*
- rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))"
- oops
-
-
-
-lemma flts_does_rewrite:
- shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rflts rs1 = rflts rs2"
- oops
+ shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset))) \<leadsto>g*
+ rdistinct rs2 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset)))"
+ sorry
lemma with_wo0_distinct:
shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
@@ -663,15 +711,6 @@
apply (simp add: frewrites_cons)
done
-lemma rdistinct_concat:
- shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
- apply(induct rs)
- apply simp+
- done
-
-lemma rdistinct_concat2:
- shows "\<forall>r \<in> set rs. r \<in> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
- by (simp add: rdistinct_concat subsetI)
lemma frewrite_with_distinct:
shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk>