# HG changeset patch
# User Chengsong
# Date 1649020347 -3600
# Node ID 51af5f882350eea3a4b69572803a97363069580a
# Parent  ab6aaf8d7649de4dc7b8610825fbc509f902f3f1
fun

diff -r ab6aaf8d7649 -r 51af5f882350 thys2/BasicIdentities.thy
--- a/thys2/BasicIdentities.thy	Fri Apr 01 23:18:00 2022 +0100
+++ b/thys2/BasicIdentities.thy	Sun Apr 03 22:12:27 2022 +0100
@@ -53,6 +53,14 @@
      (if x \<in> acc then rdistinct xs  acc 
       else x # (rdistinct xs  ({x} \<union> acc)))"
 
+lemma rdistinct_does_the_job:
+  shows "distinct (rdistinct rs s)"
+  apply(induct rs arbitrary: s)
+   apply simp
+  apply simp
+  sorry
+
+
 lemma rdistinct_concat:
   shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
   apply(induct rs)
@@ -76,6 +84,38 @@
   apply simp
   done
 
+lemma rdistinct_on_distinct:
+  shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"
+  apply(induct rs)
+   apply simp
+  apply(subgoal_tac "rdistinct rs {} = rs")
+   prefer 2
+  apply simp
+  using distinct_not_exist by fastforce
+
+lemma distinct_rdistinct_append:
+  shows "distinct rs1 \<Longrightarrow> rdistinct (rs1 @ rsa) {} = rs1 @ (rdistinct rsa (set rs1))"
+  sorry
+
+lemma rdistinct_concat_general:
+  shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+  sorry
+
+lemma rdistinct_set_equality:
+  shows "set (rdistinct rs {}) = set rs"
+  sorry
+
+lemma distinct_once_enough:
+  shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
+  apply(subgoal_tac "distinct (rdistinct rs {})")
+   apply(subgoal_tac 
+" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
+  apply(simp only:)
+  using rdistinct_concat_general apply blast
+  apply (simp add: distinct_rdistinct_append rdistinct_set_equality)
+  by (simp add: rdistinct_does_the_job)
+  
+
 
 fun rflts :: "rrexp list \<Rightarrow> rrexp list"
   where 
@@ -84,6 +124,29 @@
 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"
 | "rflts (r1 # rs) = r1 # rflts rs"
 
+lemma rflts_def_idiot:
+  shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk>
+       \<Longrightarrow> rflts (a # rs) = a # rflts rs"
+  apply(case_tac a)
+       apply simp_all
+  done
+
+lemma rflts_def_idiot2:
+  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
+  apply(induct rs)
+   apply simp
+  by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+
+
+lemma flts_append:
+  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+  apply(induct rs1)
+   apply simp
+  apply(case_tac a)
+       apply simp+
+  done
+
 
 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"
   where
@@ -187,12 +250,7 @@
   shows "rsize (RALTS rs) \<le> Suc ( sum_list (map rsize rs)) "
   by simp
 
-lemma rflts_def_idiot:
-  shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk>
-       \<Longrightarrow> rflts (a # rs) = a # rflts rs"
-  apply(case_tac a)
-       apply simp_all
-  done
+
 
 
 lemma rflts_mono:
@@ -318,12 +376,7 @@
   by force
 
 
-lemma rdistinct_does_the_job:
-  shows "distinct (rdistinct rs s)"
-  apply(induct rs arbitrary: s)
-   apply simp
-  apply simp
-  sorry
+
 
 lemma rders_simp_same_simpders:
   shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
@@ -417,17 +470,280 @@
 
 
 
+lemma idem_after_simp1:
+  shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
+  apply(case_tac "rsimp aa")
+  apply simp+
+  apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
+  by simp
+
+lemma identity_wwo0:
+  shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
+  by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+
+
+lemma distinct_removes_last:
+  shows "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
+  apply(induct as arbitrary: rset ab rset1 a)
+     apply simp
+    apply simp
+  apply(case_tac "aa \<in> rset")
+   apply(case_tac "a = aa")
+  apply (metis append_Cons)
+    apply simp
+   apply(case_tac "a \<in> set as")
+  apply (metis append_Cons rdistinct.simps(2) set_ConsD)
+   apply(case_tac "a = aa")
+    prefer 2
+    apply simp
+   apply (metis append_Cons)
+  apply(case_tac "ab \<in> rset1")
+  prefer 2
+   apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 
+               ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
+  prefer 2
+  apply force
+  apply(simp only:)
+     apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
+    apply(simp only:)
+    apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
+     apply blast
+    apply(case_tac "a \<in> insert ab rset1")
+     apply simp
+     apply (metis insertI1)
+    apply simp
+    apply (meson insertI1)
+   apply simp
+  apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
+   apply simp
+  by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
+
+
+lemma distinct_removes_middle:
+  shows  "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
+and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
+   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
+     apply simp
+    apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp
+    apply metis
+   apply simp
+   apply (metis insertI1)
+  apply(case_tac "a = ab")
+   apply simp
+   apply(case_tac "ab \<in> rset")
+    apply simp
+    apply presburger
+   apply (meson insertI1)
+  apply(case_tac "a \<in> rset")
+  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+  apply(case_tac "ab \<in> rset")
+  apply simp
+   apply (meson insert_iff)
+  apply simp
+  by (metis insertI1)
+
+
+lemma distinct_removes_middle3:
+  shows  "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
+  using distinct_removes_middle(1) by fastforce
+
+lemma distinct_removes_last2:
+  shows "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+  by (simp add: distinct_removes_last(1))
+
+lemma distinct_removes_middle2:
+  shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}"
+  by (metis distinct_removes_middle(1))
+
+lemma distinct_removes_list:
+  shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
+  apply(induct rs)
+   apply simp+
+  apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
+   prefer 2
+  apply (metis append_Cons append_Nil distinct_removes_middle(1))
+  by presburger
+
+
+lemma spawn_simp_rsimpalts:
+  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
+  apply(cases rs)
+   apply simp
+  apply(case_tac list)
+   apply simp
+   apply(subst rsimp_idem[symmetric])
+   apply simp
+  apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
+   apply(simp only:)
+   apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
+    apply(simp only:)
+  prefer 2
+  apply simp
+   prefer 2
+  using rsimp_ALTs.simps(3) apply presburger
+  apply auto
+  apply(subst rsimp_idem)+
+  by (metis comp_apply rsimp_idem)
 
 
 
 
+inductive good1 :: "rrexp \<Rightarrow> bool"
+  where
+"\<lbrakk>RZERO \<notin> set rs; \<nexists>rs1. RALTS rs1 \<in> set rs\<rbrakk> \<Longrightarrow> good1 (RALTS rs)"
+|"good1 RZERO"
+|"good1 RONE"
+|"good1 (RCHAR c)"
+|"good1 (RSEQ r1 r2)"
+|"good1 (RSTAR r0)"
 
+inductive goods :: "rrexp list \<Rightarrow> bool"
+  where
+ "goods []"
+|"\<lbrakk>goods rs; r \<noteq> RZERO; \<nexists>rs1. RALTS rs1 = r\<rbrakk> \<Longrightarrow> goods (r # rs)"
+
+lemma goods_good1:
+  shows "goods rs = good1 (RALTS rs)"
+  apply(induct rs)
+  apply (simp add: good1.intros(1) goods.intros(1))
+  apply(case_tac "goods rs")
+   apply(case_tac a)
+        apply simp
+  using good1.simps goods.cases apply auto[1]
+  apply (simp add: good1.simps goods.intros(2))
+  apply (simp add: good1.simps goods.intros(2))
+     apply (simp add: good1.simps goods.intros(2))
+  using good1.simps goods.cases apply auto[1]
+  apply (metis good1.cases good1.intros(1) goods.intros(2) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.distinct(9) rrexp.inject(3) set_ConsD)
+  apply simp
+  by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30))
+
+lemma rsimp_good1:
+  shows "rsimp r = r1 \<Longrightarrow> good1 r1"
+
+  sorry
+
+lemma rsimp_no_dup:
+  shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs"
+  sorry
+
+
+lemma rsimp_good1_2:
+  shows "map rsimp rsa = [RALTS rs] \<Longrightarrow> good1 (RALTS rs)"
+  by (metis Cons_eq_map_D rsimp_good1)
+  
+
+
+lemma simp_singlealt_flatten:
+  shows "rsimp (RALTS [RALTS rsa]) = rsimp (RALTS (rsa @ []))"
+  apply(induct rsa)
+   apply simp
+  apply simp
+  by (metis idem_after_simp1 list.simps(9) rsimp.simps(2))
+
+
+lemma good1_rsimpalts:
+  shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+  by (metis no_alt_short_list_after_simp) 
+  
+
+lemma good1_flts:
+  shows "good1 (RALTS rs1) \<Longrightarrow> rflts rs1 = rs1"
+  apply(induct rs1)
+   apply simp 
+  by (metis good1.cases good1.intros(1) list.set_intros(1) rflts_def_idiot rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.inject(3) rsimp.simps(3) rsimp.simps(4) rsimp_inner_idem4 set_subset_Cons subsetD)
+ 
+
+
+lemma good1_flatten:
+  shows "\<lbrakk> rsimp r =  (RALTS rs1)\<rbrakk>
+       \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)"
+  apply(subst good1_rsimpalts)
+   apply simp+
+  apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)")
+   apply simp
+  apply(subgoal_tac "good1 (RALTS rs1)")
+  prefer 2
+  using rsimp_good1 apply blast
+  using flts_append good1_flts by presburger
+
+lemma flatten_rsimpalts:
+  shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = 
+         rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)"
+  apply(case_tac "map rsimp rsa")
+   apply simp
+  apply(case_tac "list")
+   apply simp
+   apply(case_tac a)
+        apply simp+
+    apply(rename_tac rs1)
+    apply(subgoal_tac "good1 (RALTS rs1)")
+     apply(subgoal_tac "distinct rs1")
+  apply(subst rdistinct_on_distinct)
+  apply blast
+  apply(subst rdistinct_on_distinct)
+       apply blast
+  using good1_flatten apply blast
+ 
+  using rsimp_no_dup apply force
+  
+  using rsimp_good1_2 apply presburger
+
+   apply simp+
+  apply(case_tac "rflts (a # aa # lista)")
+   apply simp
+  by (smt (verit) append_Cons append_Nil empty_iff good1_flatten list.distinct(1) rdistinct.simps(2) rsimp.simps(2) rsimp_ALTs.elims rsimp_good1)
+
+
+lemma flts_good_good:
+  shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> good1 (RALTS (rflts rs ))"
+  apply(induct rs)
+   apply simp
+  using goods.intros(1) goods_good1 apply auto[1]
+  apply(case_tac  "a")
+  apply simp
+  apply (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(4) rrexp.distinct(1) rrexp.distinct(15))
+     apply simp
+  using goods.intros(2) goods_good1 apply blast
+  using goods.intros(2) goods_good1 apply auto[1]
+   apply(subgoal_tac "good1 a")
+  apply (metis Un_iff good1.cases good1.intros(1) list.set_intros(2) rflts.simps(3) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) set_append)
+  apply simp
+  by (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(7) rrexp.distinct(29) rrexp.distinct(9))
+
+
+lemma simp_flatten_aux1:
+  shows "\<forall>r \<in> set (map rsimp rsa). good1 r"
+  apply(induct rsa)
+   apply(simp add: goods.intros)
+  using rsimp_good1 by auto
+
+
+
+lemma simp_flatten_aux:
+  shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})"
+  sorry
 
 
 
 lemma simp_flatten:
   shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"
+  apply simp
+  apply(subst flatten_rsimpalts)
+  apply(simp add: flts_append)
+  apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good1 r")
+  apply (metis distinct_once_enough simp_flatten_aux)
+  using simp_flatten_aux1 by blast
 
+lemma simp_flatten3:
+  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
   sorry
 
 
@@ -455,7 +771,105 @@
 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
 
 
+lemma distinct_flts_no0:
+  shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =
+           rflts (map rsimp (rdistinct rs rset))  "
+  
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac a)
+  apply simp+
+    apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+  prefer 2
+  apply simp  
+  by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7))
 
+lemma flts_removes0:
+  shows "  rflts (rs @ [RZERO])  =
+           rflts rs"
+  apply(induct rs)
+   apply simp
+  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+  
+
+lemma rflts_spills_last:
+  shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs"
+  apply (induct rs1)
+  apply simp
+  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma flts_keeps1:
+  shows " rflts (rs @ [RONE]) = 
+          rflts  rs @ [RONE] "
+  apply (induct rs)
+   apply simp
+  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma flts_keeps_others:
+  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
+  apply(induct rs)
+   apply simp
+  apply (simp add: rflts_def_idiot)
+  apply(case_tac a)
+       apply simp
+  using flts_keeps1 apply blast
+     apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+  apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+  apply blast
+  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma spilled_alts_contained:
+  shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
+  apply(induct rs1)
+   apply simp 
+  apply(case_tac "a = aa")
+   apply simp
+  apply(subgoal_tac " a \<in> set rs1")
+  prefer 2
+   apply (meson set_ConsD)
+  apply(case_tac aa)
+  using rflts.simps(2) apply presburger
+      apply fastforce
+  apply fastforce
+  apply fastforce
+  apply fastforce
+  by fastforce
+
+
+lemma distinct_removes_duplicate_flts:
+  shows " a \<in> set rsa
+       \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+           rdistinct (rflts (map rsimp rsa)) {}"
+  apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
+  prefer 2
+  apply simp
+  apply(induct "rsimp a")
+       apply simp
+  using flts_removes0 apply presburger
+      apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
+                          rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
+      apply (simp only:)
+       apply(subst flts_keeps1)
+  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
+      apply presburger
+        apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
+                            rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
+      apply (simp only:)
+      prefer 2
+      apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
+  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
+
+    apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
+   prefer 2
+   apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
+  apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
+  prefer 2
+  apply (simp add: rflts_spills_last)
+  apply(simp only:)
+  apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
+  prefer 2
+  using spilled_alts_contained apply presburger
+  using distinct_removes_list by blast
 
 
 
diff -r ab6aaf8d7649 -r 51af5f882350 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Fri Apr 01 23:18:00 2022 +0100
+++ b/thys2/ClosedForms.thy	Sun Apr 03 22:12:27 2022 +0100
@@ -2,129 +2,6 @@
 "BasicIdentities"
 begin
 
-
-lemma idem_after_simp1:
-  shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
-  apply(case_tac "rsimp aa")
-  apply simp+
-  apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
-  by simp
-
-lemma identity_wwo0:
-  shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
-  by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
-
-
-lemma distinct_removes_last:
-  shows "\<lbrakk>a \<in> set as\<rbrakk>
-    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
-and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
-  apply(induct as arbitrary: rset ab rset1 a)
-     apply simp
-    apply simp
-  apply(case_tac "aa \<in> rset")
-   apply(case_tac "a = aa")
-  apply (metis append_Cons)
-    apply simp
-   apply(case_tac "a \<in> set as")
-  apply (metis append_Cons rdistinct.simps(2) set_ConsD)
-   apply(case_tac "a = aa")
-    prefer 2
-    apply simp
-   apply (metis append_Cons)
-  apply(case_tac "ab \<in> rset1")
-  prefer 2
-   apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 
-               ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
-  prefer 2
-  apply force
-  apply(simp only:)
-     apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
-    apply(simp only:)
-    apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
-     apply blast
-    apply(case_tac "a \<in> insert ab rset1")
-     apply simp
-     apply (metis insertI1)
-    apply simp
-    apply (meson insertI1)
-   apply simp
-  apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
-   apply simp
-  by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
-
-
-lemma distinct_removes_middle:
-  shows  "\<lbrakk>a \<in> set as\<rbrakk>
-    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
-and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
-   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
-     apply simp
-    apply simp
-   apply(case_tac "a \<in> rset")
-    apply simp
-    apply metis
-   apply simp
-   apply (metis insertI1)
-  apply(case_tac "a = ab")
-   apply simp
-   apply(case_tac "ab \<in> rset")
-    apply simp
-    apply presburger
-   apply (meson insertI1)
-  apply(case_tac "a \<in> rset")
-  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
-  apply(case_tac "ab \<in> rset")
-  apply simp
-   apply (meson insert_iff)
-  apply simp
-  by (metis insertI1)
-
-
-lemma distinct_removes_middle3:
-  shows  "\<lbrakk>a \<in> set as\<rbrakk>
-    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
-  using distinct_removes_middle(1) by fastforce
-
-lemma distinct_removes_last2:
-  shows "\<lbrakk>a \<in> set as\<rbrakk>
-    \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
-  by (simp add: distinct_removes_last(1))
-
-lemma distinct_removes_middle2:
-  shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}"
-  by (metis distinct_removes_middle(1))
-
-lemma distinct_removes_list:
-  shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
-  apply(induct rs)
-   apply simp+
-  apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
-   prefer 2
-  apply (metis append_Cons append_Nil distinct_removes_middle(1))
-  by presburger
-
-
-lemma spawn_simp_rsimpalts:
-  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
-  apply(cases rs)
-   apply simp
-  apply(case_tac list)
-   apply simp
-   apply(subst rsimp_idem[symmetric])
-   apply simp
-  apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
-   apply(simp only:)
-   apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
-    apply(simp only:)
-  prefer 2
-  apply simp
-   prefer 2
-  using rsimp_ALTs.simps(3) apply presburger
-  apply auto
-  apply(subst rsimp_idem)+
-  by (metis comp_apply rsimp_idem)
-
 lemma map_concat_cons:
   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
   by simp
@@ -133,98 +10,14 @@
   shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
   by simp
 
-lemma flts_removes0:
-  shows "  rflts (rs @ [RZERO])  =
-           rflts rs"
-  apply(induct rs)
-   apply simp
-  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-  
-lemma flts_keeps1:
-  shows " rflts (rs @ [RONE]) = 
-          rflts  rs @ [RONE] "
-  apply (induct rs)
-   apply simp
-  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-
-lemma flts_keeps_others:
-  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
-  apply(induct rs)
-   apply simp
-  apply (simp add: rflts_def_idiot)
-  apply(case_tac a)
-       apply simp
-  using flts_keeps1 apply blast
-     apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-  apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-  apply blast
-  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
 
-lemma rflts_def_idiot2:
-  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
-  apply(induct rs)
-   apply simp
-  by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-
-lemma rflts_spills_last:
-  shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs"
-  apply (induct rs1)
-  apply simp
-  by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
 
 
-lemma spilled_alts_contained:
-  shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
-  apply(induct rs1)
-   apply simp 
-  apply(case_tac "a = aa")
-   apply simp
-  apply(subgoal_tac " a \<in> set rs1")
-  prefer 2
-   apply (meson set_ConsD)
-  apply(case_tac aa)
-  using rflts.simps(2) apply presburger
-      apply fastforce
-  apply fastforce
-  apply fastforce
-  apply fastforce
-  by fastforce
+
 
-lemma distinct_removes_duplicate_flts:
-  shows " a \<in> set rsa
-       \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
-           rdistinct (rflts (map rsimp rsa)) {}"
-  apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
-  prefer 2
-  apply simp
-  apply(induct "rsimp a")
-       apply simp
-  using flts_removes0 apply presburger
-      apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
-                          rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
-      apply (simp only:)
-       apply(subst flts_keeps1)
-  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
-      apply presburger
-        apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
-                            rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
-      apply (simp only:)
-      prefer 2
-      apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
-  apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
 
-    apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
-   prefer 2
-   apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
-  apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
-  prefer 2
-  apply (simp add: rflts_spills_last)
-  apply(simp only:)
-  apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
-  prefer 2
-  using spilled_alts_contained apply presburger
-  by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust)
+
 
 lemma flts_middle0:
   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
@@ -246,13 +39,7 @@
        apply simp+
   done
 
-lemma flts_append:
-  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
-  apply(induct rs1)
-   apply simp
-  apply(case_tac a)
-       apply simp+
-  done
+
 
 lemma simp_removes_duplicate1:
   shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
@@ -351,18 +138,6 @@
 
 
 
-lemma distinct_flts_no0:
-  shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =
-           rflts (map rsimp (rdistinct rs rset))  "
-  
-  apply(induct rs arbitrary: rset)
-   apply simp
-  apply(case_tac a)
-  apply simp+
-    apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-  prefer 2
-  apply simp  
-  by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7))
 
 
 
@@ -387,12 +162,20 @@
 | "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"
 | "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 
 
+lemma grewrite_variant1:
+  shows "a \<in> set rs1 \<Longrightarrow> rs1 @ a # rs \<leadsto>g rs1 @ rs"
+  apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)
+  done
+
 
 inductive 
   grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)
 where 
   [intro, simp]:"rs \<leadsto>g* rs"
 | [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"
+
+
+
 (*
 inductive 
   frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)
@@ -431,6 +214,26 @@
 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 gstar_rdistinct_general:
+  shows "rs1 @  rs \<leadsto>g* rs1 @ (rdistinct rs (set rs1))"
+  apply(induct rs arbitrary: rs1)
+   apply simp
+  apply(case_tac " a \<in> set rs1")
+   apply simp
+  apply(subgoal_tac "rs1 @ a # rs \<leadsto>g rs1 @ rs")
+  using gmany_steps_later apply auto[1]
+  apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)
+  apply simp
+  apply(drule_tac x = "rs1 @ [a]" in meta_spec)
+  by simp
+
+
+lemma gstar_rdistinct:
+  shows "rs \<leadsto>g* rdistinct rs {}"
+  apply(induct rs)
+   apply simp
+  by (metis append.left_neutral empty_set gstar_rdistinct_general)
+
 
 
 lemma frewrite_append:
@@ -540,29 +343,27 @@
      apply simp
   oops
 
+lemma grewrite_cases_middle:
+  shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
+(\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>
+(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>
+(\<exists>rsa rsb rsc a. rs1 = rsa @ [a] @ rsb @ [a] @ rsc \<and> rs2 = rsa @ [a] @ rsb @ rsc)"
+  apply( induct rs1 rs2 rule: grewrite.induct)
+     apply simp
+  apply blast
+  apply (metis append_Cons append_Nil)
+  apply (metis append_Cons)
+  by blast
 
 
 lemma grewrite_equal_rsimp:
   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
-  apply(induct rs1 rs2 rule: grewrite.induct)
-  apply simp
-  using simp_flatten apply blast
-   prefer 2
-   apply (smt (verit) append.assoc append_Cons in_set_conv_decomp simp_removes_duplicate2)
-  apply simp
-  apply(case_tac "rdistinct (rflts (map rsimp rs1)) {}")
-  apply(case_tac "rsimp r = RZERO")
-    apply simp
-   apply(case_tac "\<exists>rs. rsimp r = RALTS rs")
-    prefer 2
-   
-    apply(subgoal_tac "rdistinct (rflts (rsimp r # map rsimp rs1)) {} = 
-                    rsimp r # rdistinct (rflts (map rsimp rs1)) {rsimp r}")
-  prefer 2
-  apply (simp add: list.inject rflts_def_idiot)
-    apply(simp only:)
-
-  sorry
+  apply(frule grewrite_cases_middle)
+  apply(case_tac "(\<exists>rsa rsb rsc. rs1 = rsa @ [RALTS rsb] @ rsc \<and> rs2 = rsa @ rsb @ rsc)")  
+  using simp_flatten3 apply auto[1]
+  apply(case_tac "(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc)")
+  apply (metis (mono_tags, opaque_lifting) append_Cons append_Nil list.set_intros(1) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) simp_removes_duplicate3)
+  by (smt (verit) append.assoc append_Cons append_Nil in_set_conv_decomp simp_removes_duplicate3)
 
 
 lemma grewrites_equal_rsimp:
@@ -576,7 +377,10 @@
 
 lemma grewrites_equal_simp_2:
   shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2"
-  sorry
+  oops
+
+
+
 
 lemma grewrites_last:
   shows "r # [RALTS rs] \<leadsto>g*  r # rs"
@@ -615,7 +419,6 @@
 
 
 
-
 lemma with_wo0_distinct:
   shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
   apply(induct rs arbitrary: rset)
@@ -661,93 +464,391 @@
 r = +rs
 [] \<leadsto>g* rs which is wrong
 *)
-lemma frewrite_with_distinct:
-  shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk>
-       \<Longrightarrow> rdistinct rs2
-            (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>g* 
-           rdistinct rs3 
-            (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"
-  apply(induct rs2 rs3  arbitrary: rset rule: frewrite.induct)
-    apply(case_tac "RZERO \<in>  (rset \<union> \<Union> (alt_set ` rset))")
-  apply simp
-    apply simp
-
-
-  oops
 
 
 
-lemma frewrites_with_distinct:
-  shows "\<lbrakk>rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow>
-( (rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g* 
- rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))))
-\<or> ( rs1 @ (rdistinct rsb (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>g*
-    rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))))  
- )
-"
-  apply(induct rsa rsb arbitrary: rs1 rule: frewrite.induct)
-    apply simp
-   apply(case_tac "RALTS rs \<in> set rs1")
-    apply(subgoal_tac "set rs \<subseteq> \<Union> (alt_set `set rs1)")
-     apply (metis (full_types) Un_iff Un_insert_left 
-Un_insert_right grewrites.intros(1) le_supI2 rdistinct.simps(2) rdistinct_concat)
-  apply (metis Un_subset_iff Union_upper alt_set.simps(1) imageI)
-
-   apply(case_tac "RALTS rs \<in> \<Union> (alt_set ` set rs1)")
-  apply simp
-  apply (smt (z3) UN_insert Un_iff alt_set.simps(1) alt_set_has_all dual_order.trans grewrites.intros(1) insert_absorb rdistinct_concat subset_insertI)
-  
-
-  oops
 
 
 
-lemma rd_flts_set:
-  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)))"
-  apply(induct rs1 rs2 rule: frewrites.induct)
-   apply simp
-  oops
 
 lemma frewrite_simpeq:
   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
   apply(induct rs1 rs2 rule: frewrite.induct)
     apply simp
   using simp_flatten apply presburger
-  by (meson grewrites_cons grewrites_equal_rsimp grewrites_equal_simp_2)
+  by (metis (no_types, opaque_lifting) grewrites_equal_rsimp grewrites_last list.simps(9) rsimp.simps(2))
+
+lemma gstar0:
+  shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))"
+  apply(induct rs arbitrary: rsa)
+   apply simp
+  apply(case_tac "a = RZERO")
+   apply simp
+  
+  using gr_in_rstar grewrite.intros(1) grewrites_append apply presburger
+  apply(case_tac "a \<in> set rsa")
+   apply simp+
+  apply(drule_tac x = "rsa @ [a]" in meta_spec)
+  by simp
+  
+lemma gstar01:
+  shows "rdistinct rs {} \<leadsto>g* rdistinct rs {RZERO}"
+  by (metis empty_set gstar0 self_append_conv2)
+
+
+lemma grewrite_rdistinct_aux:
+  shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"
+  sorry
+
+lemma grewrite_rdistinct_worth1:
+  shows "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)"
+  by (metis append.assoc empty_set grewrite_rdistinct_aux grewrites_append inf_sup_aci(5) insert_is_Un list.simps(15))
+
+lemma grewrite_rdisitinct:
+  shows "rs @ rdistinct rsa {RALTS rs} \<leadsto>g* rs @ rdistinct rsa (insert (RALTS rs) (set rs))"
+  apply(induct rsa arbitrary: rs)
+   apply simp
+  apply(case_tac "a = RALTS rs")
+  apply simp
+  apply(case_tac "a \<in> set rs")
+   apply simp
+  apply(subgoal_tac "rs @
+           a # rdistinct rsa {RALTS rs, a} \<leadsto>g rs @ rdistinct rsa {RALTS rs, a}")
+    apply(subgoal_tac 
+"rs @ rdistinct rsa {RALTS rs, a} \<leadsto>g* rs @ rdistinct rsa (insert (RALTS rs) (set rs))")
+  using gmany_steps_later apply blast
+    apply(subgoal_tac 
+" rs @ rdistinct rsa {RALTS rs, a} \<leadsto>g* rs @ rdistinct rsa ({RALTS rs, a} \<union> set rs)")
+     apply (simp add: insert_absorb)
+  using grewrite_rdistinct_aux apply blast
+  using grewrite_variant1 apply blast
+  by (metis grewrite_rdistinct_aux insert_is_Un)
+
+  
+lemma frewrite_rd_grewrites_general:
+  shows "\<lbrakk>rs1 \<leadsto>f rs2; \<And>rs. \<exists>rs3. 
+(rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3)\<rbrakk>
+       \<Longrightarrow> 
+\<exists>rs3. (rs @ (r # rdistinct rs1 (set rs \<union> {r})) \<leadsto>g* rs3) \<and> (rs @ (r # rdistinct rs2 (set rs \<union> {r})) \<leadsto>g* rs3)"
+  apply(drule_tac x = "rs @ [r]" in meta_spec )
+  by simp
+
+
+lemma grewrites_middle_distinct:
+  shows "RALTS rs \<in> set rsb \<Longrightarrow> 
+         rsb @
+       rdistinct ( rs @ rsa)
+        (set rsb) \<leadsto>g* rsb @ rdistinct rsa (set rsb)"
+  sorry
+
+
+
+lemma frewrite_rd_grewrites_aux:
+  shows     "  rsb @
+       rdistinct (RALTS rs # rsa)
+        (set rsb) \<leadsto>g* rsb @
+                       rdistinct rs (set rsb) @ rdistinct rsa (insert (RALTS rs) (set rs) \<union> set rsb)"
+
+  
+  sorry
+
+lemma flts_gstar:
+  shows "rs \<leadsto>g* rflts rs"
+  sorry
+
+lemma list_dlist_union:
+  shows "set rs \<subseteq> set rsb \<union> set (rdistinct rs (set rsb))"
+  by (metis rdistinct_concat_general rdistinct_set_equality set_append sup_ge2)
+
+lemma subset_distinct_rewrite1:
+  shows "set1 \<subseteq> set rsb \<Longrightarrow> rsb @ rs \<leadsto>g* rsb @ (rdistinct rs set1)"
+  apply(induct rs arbitrary: rsb)
+   apply simp
+  apply(case_tac "a \<in> set1")
+   apply simp
+  
+  using gmany_steps_later grewrite_variant1 apply blast
+  apply simp
+  apply(drule_tac x = "rsb @ [a]" in meta_spec)
+  apply(subgoal_tac "set1 \<subseteq> set (rsb @ [a])")
+   apply (simp only:)
+  apply(subgoal_tac "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)")
+    apply (metis (no_types, opaque_lifting) append.assoc append_Cons append_Nil greal_trans)
+  apply (metis append.assoc empty_set grewrite_rdistinct_aux grewrites_append inf_sup_aci(5) insert_is_Un list.simps(15))
+  by auto
+
+
+lemma subset_distinct_rewrite:
+  shows "set rsb' \<subseteq> set rsb \<Longrightarrow> rsb @ rs \<leadsto>g* rsb @ (rdistinct rs (set rsb'))"
+  by (simp add: subset_distinct_rewrite1)
+  
+
+
+lemma distinct_3list:
+  shows "rsb @ (rdistinct rs (set rsb)) @ rsa \<leadsto>g* 
+         rsb @ (rdistinct rs (set rsb)) @ (rdistinct rsa (set rs))"
+  by (metis append.assoc list_dlist_union set_append subset_distinct_rewrite)
+  
+
+
+
+lemma grewrites_shape1:
+  shows "      RALTS rs \<notin> set rsb \<Longrightarrow>
+       rsb @
+       RALTS rs #
+       rdistinct rsa
+        (
+          (set rsb)) \<leadsto>g* rsb @
+                          rdistinct rs (set rsb) @
+                          rdistinct (rflts (rdistinct rsa ( (set rsb \<union> set rs)))) (set rs)"
+
+
+  apply (subgoal_tac "       rsb @
+       RALTS rs #
+       rdistinct rsa
+        (
+          (set rsb))  \<leadsto>g*        rsb @
+       rs @
+       rdistinct rsa
+        (
+          (set rsb)) ")
+   prefer 2
+  using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger
+  apply(subgoal_tac "rsb @ rs @ rdistinct rsa (  (set rsb)) \<leadsto>g* rsb @ 
+(rdistinct rs (set rsb) @ rdistinct rsa (  (set rsb)))")
+  prefer 2
+  apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
+  apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct rsa (  (set rsb))
+\<leadsto>g*  rsb @ rdistinct rs (set rsb) @ rdistinct rsa (  (set rsb) \<union> (set rs))")
+  prefer 2
+  apply (smt (verit, best) append.assoc append_assoc boolean_algebra_cancel.sup2 grewrite_rdistinct_aux inf_sup_aci(5) insert_is_Un rdistinct_concat_general rdistinct_set_equality set_append sup.commute sup.right_idem sup_commute)
+  apply(subgoal_tac "rdistinct rsa (  (set rsb)  \<union> set rs) \<leadsto>g*
+rflts (rdistinct rsa (  (set rsb) \<union> set rs))")
+   apply(subgoal_tac "rsb @ (rdistinct rs (set rsb)) @ rflts (rdistinct rsa (  (set rsb) \<union> set rs)) \<leadsto>g* 
+rsb @ (rdistinct rs (set rsb)) @ (rdistinct (rflts (rdistinct rsa (  (set rsb) \<union> set rs))) (set rs))")
+  apply (smt (verit, ccfv_SIG) Un_insert_left greal_trans grewrites_append)
+  using distinct_3list apply presburger
+  using flts_gstar apply blast
+  done
+
+lemma r_finite1:
+  shows "r = RALTS (r # rs) = False"
+  apply(induct r)
+  apply simp+
+   apply (metis list.set_intros(1))
+  by blast
+  
+
+
+lemma grewrite_singleton:
+  shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []"
+  apply (induct "[r]" "r # rs" rule: grewrite.induct)
+    apply simp
+  apply (metis r_finite1)
+  using grewrite.simps apply blast
+  by simp
+
+lemma impossible_grewrite1:
+  shows "\<not>( [RONE] \<leadsto>g [])"
+  using grewrite.cases by fastforce
+
+
+lemma impossible_grewrite2:
+  shows "\<not> ([RALTS rs] \<leadsto>g (RALTS rs) # a # rs)"
+  
+  using grewrite_singleton by blast
+thm grewrite.cases
+lemma impossible_grewrite3:
+  shows "\<not> (RALTS rs # rs1 \<leadsto>g (RALTS rs) # a # rs1)"
+  oops
+
+
+lemma grewrites_singleton:
+  shows "[r] \<leadsto>g* r # rs \<Longrightarrow> rs = []"
+  apply(induct "[r]" "r # rs" rule: grewrites.induct)
+   apply simp
+  
+  oops
+
+lemma grewrite_nonequal_elem:
+  shows "r # rs2 \<leadsto>g r # rs3 \<Longrightarrow> rs2 \<leadsto>g rs3"
+  oops
+
+lemma grewrites_nonequal_elem:
+  shows "r # rs2 \<leadsto>g* r # rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
+  apply(induct r)
+  
+  oops
+
+  
+
+
+lemma :
+  shows "rs1 @ rs2 \<leadsto>g* rs1 @ rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
+  apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct)
+   apply simp
+  apply(drule_tac x = "[x] @ rs2" in meta_spec)
+  apply(drule_tac x = "[x] @ rs3" in meta_spec)
+  apply(simp)
+
+  oops
+
+
+
+lemma grewrites_shape3_aux:
+  shows "rs @ (rdistinct rsa (insert (RALTS rs) rsc)) \<leadsto>g* rs @ rdistinct (rflts (rdistinct rsa rsc)) (set rs)"
+  apply(induct rsa arbitrary: rsc rs)
+   apply simp
+  apply(case_tac "a \<in> rsc")
+   apply simp
+  apply(case_tac "a = RALTS rs")
+   apply simp
+  apply(subgoal_tac " rdistinct (rs @ rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs) \<leadsto>g*
+ rdistinct (rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs)")
+  apply (metis insertI1 insert_absorb rdistinct_concat2)
+   apply (simp add: rdistinct_concat)
+
+  apply simp
+  apply(case_tac "a = RZERO")
+  apply (metis gmany_steps_later grewrite.intros(1) grewrite_append rflts.simps(2))
+  apply(case_tac "\<exists>rs1. a = RALTS rs1")
+   prefer 2
+   apply simp
+   apply(subgoal_tac "rflts (a # rdistinct rsa (insert a rsc)) = a # rflts (rdistinct rsa (insert a rsc))")
+    apply (simp  only:)
+    apply(case_tac "a \<notin> set rs")
+     apply simp
+  apply(drule_tac x = "insert a rsc" in meta_spec)
+  apply(drule_tac x = "rs " in meta_spec)
+  
+    apply(erule exE)
+    apply simp
+  apply(subgoal_tac "RALTS rs1 #
+           rdistinct rsa
+            (insert (RALTS rs)
+              (insert (RALTS rs1)
+                rsc)) \<leadsto>g* rs1 @
+           rdistinct rsa
+            (insert (RALTS rs)
+              (insert (RALTS rs1)
+                rsc)) ")
+     apply(subgoal_tac " rs1 @
+           rdistinct rsa
+            (insert (RALTS rs)
+              (insert (RALTS rs1)
+                rsc)) \<leadsto>g*
+                        rs1 @
+           rdistinct rsa
+            (insert (RALTS rs)
+              (insert (RALTS rs1)
+                rsc))")
+  
+  apply(case_tac "a \<in> set rs")
+  
+
+
+  sorry
+
+
+lemma grewrites_shape3:
+  shows "      RALTS rs \<notin> set rsb \<Longrightarrow>
+       rsb @
+       RALTS rs #
+       rdistinct rsa
+        (insert (RALTS rs)
+          (set rsb)) \<leadsto>g* rsb @
+                          rdistinct rs (set rsb) @
+                          rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)"
+  apply(subgoal_tac "rsb @ RALTS rs # rdistinct rsa (insert (RALTS rs) (set rsb)) \<leadsto>g*
+                     rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb))")
+  prefer 2
+  using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger
+  apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb )) \<leadsto>g*
+                     rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs))")
+  prefer 2
+  apply (metis Un_insert_left grewrite_rdistinct_aux grewrites_append)
+
+  apply(subgoal_tac "rsb @  rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs)) \<leadsto>g* 
+rsb @ rs @ rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)")
+   prefer 2
+  using grewrites_append grewrites_shape3_aux apply presburger
+  apply(subgoal_tac "rsb @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb)")
+  apply (smt (verit, ccfv_SIG) append_eq_appendI greal_trans grewrites.simps grewritess_concat)
+  using gstar_rdistinct_general by blast
+
+
+lemma grewrites_shape2:
+  shows "       RALTS rs \<notin> set rsb \<Longrightarrow>
+       rsb @
+       rdistinct (rs @ rsa)
+        (set rsb) \<leadsto>g* rsb @
+                       rdistinct rs (set rsb) @
+                       rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)"
+
+ (* by (smt (z3) append.assoc distinct_3list flts_gstar greal_trans grewrites_append rdistinct_concat_general same_append_eq set_append)
+*)
+  sorry
+
+
+
+
 
 lemma frewrite_rd_grewrites:
   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> 
-\<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) "
-  apply(induct rs1 rs2 rule: frewrite.induct)
-    apply(rule_tac x = "rs" in exI)
+\<exists>rs3. (rs @ (rdistinct rs1 (set rs)) \<leadsto>g* rs3) \<and> (rs @ (rdistinct rs2 (set rs)) \<leadsto>g* rs3) "
+  apply(induct rs1 rs2 arbitrary: rs rule: frewrite.induct)
+    apply(rule_tac x = "rsa @ (rdistinct rs ({RZERO} \<union> set rsa))" in exI)
     apply(rule conjI)
-     apply(rule gr_in_rstar)
-  apply(rule grewrite.intros)
-    apply(rule grewrites.intros)
-  using grewrite.intros(2) apply blast
-  by (meson grewrites_cons)
+  apply(case_tac "RZERO \<in> set rsa")
+  apply simp+
+  using gstar0 apply fastforce
+     apply (simp add: gr_in_rstar grewrite.intros(1) grewrites_append)
+    apply (simp add: gstar0)
+    prefer 2
+    apply(case_tac "r \<in> set rs")
+  apply simp
+    apply(drule_tac x = "rs @ [r]" in meta_spec)
+    apply(erule exE)
+    apply(rule_tac x = "rs3" in exI)
+   apply simp
+  apply(case_tac "RALTS rs \<in> set rsb")
+   apply simp
+   apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb)" in exI)
+   apply(rule conjI)
+  apply (simp add: flts_gstar grewritess_concat)
+  apply (meson flts_gstar greal_trans grewrites.intros(1) grewrites_middle_distinct grewritess_concat)
+  apply(simp)
+  apply(rule_tac x = 
+"rsb @ (rdistinct rs (set rsb)) @
+ (rdistinct (rflts (rdistinct  rsa ( (set rsb \<union> set rs)) ) ) (set rs))" in exI)
+  apply(rule conjI)
+   prefer 2
+  using grewrites_shape2 apply force
+  using grewrites_shape3 by auto
+
+
+
+lemma frewrite_simprd:
+  shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+  by (meson frewrite_simpeq)
 
 
 lemma frewrites_rd_grewrites:
   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
-\<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3)"
+rsimp (RALTS rs1) = rsimp (RALTS rs2)"
   apply(induct rs1 rs2 rule: frewrites.induct)
    apply simp
-  apply(rule exI)
-  apply(rule grewrites.intros)
-  by (metis frewrite_simpeq grewrites_equal_rsimp grewrites_equal_simp_2)
-
+  using frewrite_simprd by presburger
 
 
 
 
 lemma frewrite_simpeq2:
   shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
-  apply(induct rs1 rs2 rule: frewrite.induct)
-    apply simp  
-    apply (simp add: distinct_flts_no0)
-  apply simp
+  apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)")
+  using grewrites_equal_rsimp apply fastforce
+  using frewrite_rd_grewrites by presburger
+
 (*a more refined notion of \<leadsto>* is needed,
 this lemma fails when rs1 contains some RALTS rs where elements
 of rs appear in later parts of rs1, which will be picked up by rs2
@@ -757,9 +858,7 @@
  rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
   apply(induct rs1 rs2 rule: frewrites.induct)
    apply simp
-  
-  sorry
-
+  using frewrite_simpeq2 by presburger
 
 
 lemma frewrite_single_step:
@@ -814,13 +913,10 @@
   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 
          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
   apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)")
-   apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} 
-                    \<leadsto>g* rdistinct ( rflts (map (rder x) rs)) {RZERO}")
-  apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) 
-                   = rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))")
-  apply meson
-  apply (metis distinct_flts_no0 grewrites_equal_rsimp rsimp.simps(2))
-  sorry
+  using frewrites_simpeq apply presburger
+  using early_late_der_frewrites by auto
+
+  
 
 
 
@@ -832,11 +928,7 @@
 lemma simp_der_pierce_flts_prelim:
   shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) 
        = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))"
-  apply(subgoal_tac "map (rder x) (rflts rs) \<leadsto>g* rflts (map (rder x) rs)")
-  apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} \<leadsto>g* rdistinct (rflts (map (rder x) rs)) {RZERO}")
-  using grewrites_equal_simp_2 grewrites_simpalts simp_der_flts apply blast
-  apply (simp add: early_late_der_frewrites frewrites_with_distinct2_grewrites)
-  using early_late_der_frewrites frewrites_equivalent_simp grewrites_equal_simp_2 by blast
+  by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)
 
 
 lemma simp_der_pierce_flts:
@@ -1170,7 +1262,8 @@
 lemma alts_closed_form_variant: shows 
 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
-  sorry
+  by (metis alts_closed_form comp_apply rders_simp_nonempty_simped)
+