# HG changeset patch
# User Chengsong
# Date 1648635531 -3600
# Node ID 10fd25fba2bade1e37b514d585fb5cfef2aa8900
# Parent  37d14cbce020202c094d13aa65096d1f3706762e
identities

diff -r 37d14cbce020 -r 10fd25fba2ba thys2/BasicIdentities.thy
--- 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)"
diff -r 37d14cbce020 -r 10fd25fba2ba thys2/ClosedForms.thy
--- 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>