
diff -r 10fd25fba2ba -r 56837303ce61 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Wed Mar 30 11:18:51 2022 +0100
+++ b/thys2/ClosedForms.thy	Fri Apr 01 23:17:40 2022 +0100
@@ -10,6 +10,10 @@
   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>
@@ -92,33 +96,15 @@
   by (metis distinct_removes_middle(1))
 
 lemma distinct_removes_list:
-  shows "\<lbrakk>a \<in> set as; \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
+  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 @ aa # rs) {} = rdistinct (as @ rs) {}")
+  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 simp_rdistinct_f: shows 
-"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = 
-                      rsimp (rsimp_ALTs (rdistinct (map f rs) frset))  "
-  apply(induct rs arbitrary: rset)
-   apply simp
-   apply(case_tac "a \<in> rset")
-  apply(case_tac " f a \<in> frset")
-   apply simp
-   apply blast
-  apply(subgoal_tac "f a \<notin> frset")
-   apply(simp)
-   apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
-  prefer 2
-  apply (meson image_insert)
-  
-  oops
-
 lemma spawn_simp_rsimpalts:
   shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
   apply(cases rs)
@@ -139,90 +125,6 @@
   apply(subst rsimp_idem)+
   by (metis comp_apply rsimp_idem)
 
-lemma spawn_simp_distinct:
-  shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs))
-\<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs)))
-\<and> rsimp  (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))"
-  apply(induct rs arbitrary: rsa rsa1 a1 rsc)
-   apply simp
-   apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))")
-  prefer 2
-  
-
-
-
-  oops
-
-lemma inv_one_derx:
-  shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"
-  apply(case_tac r2)
-       apply simp+
-  using rrexp.distinct(1) apply presburger
-    apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))
-   apply simp+
-  done
-
-lemma shape_of_derseq:
-  shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))"
-  using rder.simps(5) by presburger
-lemma shape_of_derseq2:
-  shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11"
-  by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq)
-
-lemma alts_preimage_case1:
-  shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]"
-  apply(case_tac r)
-       apply simp+
-  apply (metis rrexp.simps(12) rrexp.simps(20))
-  apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq)
-   apply auto[1]
-  by auto
-
-lemma alts_preimage_case2:
-  shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)"
-  apply(case_tac r)
-       apply simp+
-  apply (metis rrexp.distinct(15) rrexp.distinct(7))
-    apply simp
-  apply auto[1]
-  by auto
-
-lemma alts_preimage_case2_2:
-  shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)"
-  using alts_preimage_case2 by blast
-
-lemma alts_preimage_case3:
-  shows "rder x r = RALT r1 r2 \<Longrightarrow>  (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])"
-  using alts_preimage_case2 by blast
-
-lemma star_seq:
-  shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)"
-  using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger
-
-lemma language_equality_id1:
-  shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)"
-  apply (subst star_seq)
-  apply simp
-  done
-
-
-
-lemma distinct_der_set:
-  shows "(rder x) ` rset = dset \<Longrightarrow>
-rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"
-  apply(induct rs arbitrary: rset dset)
-   apply simp
-  apply(case_tac "a \<in> rset")
-   apply(subgoal_tac "rder x a \<in> dset")
-  prefer 2
-    apply blast
-   apply simp
-  apply(case_tac "rder x a \<notin> dset")
-   prefer 2
-   apply simp
- 
-  oops
-
 lemma map_concat_cons:
   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
   by simp
@@ -231,29 +133,6 @@
   shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
   by simp
 
-lemma simp_more_flts:
-  shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))"
-
-  oops
-
-lemma simp_more_distinct1:
-  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))"
-  apply(induct rs)
-   apply simp
-  apply simp
-  oops
-
-
-(*
-\<and>
-  rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = 
-  rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))
-*)
-lemma simp_removes_duplicate2:
-  shows "a "
-
-  oops
-
 lemma flts_removes0:
   shows "  rflts (rs @ [RZERO])  =
            rflts rs"
@@ -469,13 +348,6 @@
    apply simp
   using rsimpalts_conscons by presburger
 
-lemma no0_flts:
-  shows "RZERO \<notin> set (rflts rs)"
-  apply (induct rs)
-   apply simp
-  apply(case_tac a)
-       apply simp+
-  oops
 
 
 
@@ -641,11 +513,78 @@
   using grewrites_append apply blast   
   by (meson greal_trans grewrites.simps grewrites_concat)
 
+fun alt_set:: "rrexp \<Rightarrow> rrexp set"
+  where
+  "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
+| "alt_set r = {r}"
+
+lemma alt_set_has_all:
+  shows "RALTS rs \<in> alt_set rx \<Longrightarrow> set rs \<subseteq> alt_set rx"
+  apply(induct rx arbitrary: rs)
+       apply simp_all
+  apply(rename_tac rSS rss)
+  using in_mono by fastforce
+
+
+
+
+lemma grewrite_equal_rsimp:
+  shows "\<lbrakk>rs1 \<leadsto>g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \<union> \<Union>(alt_set ` rset))) =
+          rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \<union> \<Union>(alt_set ` rset)))\<rbrakk>
+       \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1))  (rset \<union> \<Union>(alt_set ` rset))) =
+           rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2))  (rset \<union> \<Union>(alt_set ` rset)))"
+  apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct)
+     apply simp
+  apply (metis append_Cons append_Nil flts_middle0)
+    apply(case_tac "rsimp r \<in> rset")
+     apply simp
+  oops
+
+
+
+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
+
+
 lemma grewrites_equal_rsimp:
   shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+  apply (induct rs1 rs2 rule: grewrites.induct)
   apply simp
+  using grewrite_equal_rsimp by presburger
+  
+
+
+
+lemma grewrites_equal_simp_2:
+  shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \<Longrightarrow> rs1 \<leadsto>g* rs2"
   sorry
 
+lemma grewrites_last:
+  shows "r # [RALTS rs] \<leadsto>g*  r # rs"
+  by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)
+
+lemma simp_flatten2:
+  shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
+  using grewrites_equal_rsimp grewrites_last by blast
 
 lemma frewrites_middle:
   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)"
@@ -674,18 +613,9 @@
   by (simp add: frewrites_cons)
 
 
-fun alt_set:: "rrexp \<Rightarrow> rrexp set"
-  where
-  "alt_set (RALTS rs) = set rs"
-| "alt_set r = {r}"
 
 
 
-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)))"
-  sorry
-
 lemma with_wo0_distinct:
   shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
   apply(induct rs arbitrary: rset)
@@ -711,50 +641,126 @@
   apply (simp add: frewrites_cons)
   done
 
+(*Interesting lemma: not obvious but easily proven by sledgehammer*)
 
+  
+
+
+(*lemma induction last rule not go through
+ example:
+r #
+           rdistinct rs1
+            (insert RZERO
+              (insert r
+                (rset \<union>
+                 \<Union> (alt_set `
+                     rset)))) \<leadsto>g* r #
+                                   rdistinct rs2
+                                    (insert RZERO (insert r (rset \<union> \<Union> (alt_set ` rset))))
+ rs2 = [+rs] rs3 = rs,
+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>f* 
+            (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>g* 
            rdistinct rs3 
             (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"
-  apply(induct rs2 rs3 rule: frewrite.induct)
+  apply(induct rs2 rs3  arbitrary: rset rule: frewrite.induct)
     apply(case_tac "RZERO \<in>  (rset \<union> \<Union> (alt_set ` rset))")
   apply simp
     apply simp
-   apply(case_tac "RALTS rs \<in> rset")
-    apply simp
-  apply(subgoal_tac "\<forall>r \<in> set rs. r \<in> \<Union> (alt_set ` rset)")
-  apply(subgoal_tac " rdistinct (rs @ rsa) (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) = 
-                       rdistinct rsa (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))")
-  using frewrites.intros(1) apply presburger
-     apply (simp add: rdistinct_concat2)
-    apply simp
-  using alt_set.simps(1) apply blast
-   apply(case_tac "RALTS rs \<in> rset \<union> \<Union>(alt_set ` rset)")
-  
+
 
-  sorry
+  oops
+
 
 
 lemma frewrites_with_distinct:
-  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
- rs1 @ (rdistinct rsa (insert RZERO (set rs1 \<union> \<Union>(alt_set ` (set rs1) )))) \<leadsto>f* 
- rs2 @ (rdistinct rsb (insert RZERO (set rs2 \<union> \<Union>(alt_set ` (set rs2) ))))"
+  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)
+
+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)
+    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)
 
-  sorry
+
+lemma frewrites_rd_grewrites:
+  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
+\<exists>rs3. (rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3)"
+  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)
 
+
+
+
+
+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
 (*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
 and deduplicated*)
-lemma wrong_frewrites_with_distinct2:
+lemma frewrites_simpeq:
   shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
- (rdistinct rs1 {RZERO}) \<leadsto>f* rdistinct rs2 {RZERO}"
-  oops
+ rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) "
+  apply(induct rs1 rs2 rule: frewrites.induct)
+   apply simp
+  
+  sorry
+
+
 
 lemma frewrite_single_step:
   shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
@@ -769,11 +775,38 @@
    apply simp
   using frewrite_single_step by presburger
 
+lemma grewrite_simpalts:
+  shows " rs2 \<leadsto>g rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+  apply(induct rs2 rs3 rule : grewrite.induct)
+  using identity_wwo0 apply presburger
+  apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten)
+  apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3))
+  apply simp
+  apply(subst rsimp_alts_equal)
+  apply(case_tac "rsa = [] \<and> rsb = [] \<and> rsc = []")
+   apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]")
+  apply (simp only:)
+  apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2))
+   apply simp
+  by (smt (verit, best) append.assoc append_Cons frewrite.intros(1) frewrite_single_step identity_wwo0 in_set_conv_decomp rsimp_ALTs.simps(3) simp_removes_duplicate3)
+
+
+lemma grewrites_simpalts:
+  shows " rs2 \<leadsto>g* rs3 \<Longrightarrow> rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)"
+  apply(induct rs2 rs3 rule: grewrites.induct)
+   apply simp
+  using grewrite_simpalts by presburger
+(*
 lemma frewrites_dB_wwo0_simp:
   shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO} 
          \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
 
   sorry
+*)
+lemma "rsimp (rsimp_ALTs (RZERO # rdistinct (map (rder x) (rflts rs)) {RZERO})) =
+       rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) "
+
+  sorry
 
 
 
@@ -782,13 +815,28 @@
          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>f* rdistinct ( rflts (map (rder x) 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
-  using frewrites_dB_wwo0_simp apply blast
-  using frewrites_with_distinct2 apply blast
-  using early_late_der_frewrites by blast
+  apply (metis distinct_flts_no0 grewrites_equal_rsimp rsimp.simps(2))
+  sorry
+
+
+
+
+ 
+
+
+
+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
 
 
 lemma simp_der_pierce_flts:
@@ -798,9 +846,7 @@
           rsimp (
 rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
 )"
-  
-  sorry
-
+  using simp_der_pierce_flts_prelim by presburger
 
 
 
@@ -1119,10 +1165,7 @@
      apply simp
   apply fastforce
    apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
-  sledgehammer
- (* by (metis inside_simp_removal rder_rsimp_ALTs_commute self_append_conv2 set_empty simp_more_distinct)
-
-  *)
+  using simp_der_pierce_flts by blast
 
 lemma alts_closed_form_variant: shows 
 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
@@ -1167,4 +1210,16 @@
    apply force
   by presburger
 
+lemma simp_helps_der_pierce:
+  shows " rsimp
+            (rder x
+              (rsimp_ALTs rs)) = 
+          rsimp 
+            (rsimp_ALTs 
+              (map (rder x )
+                rs
+              )
+            )"
+  sorry
+
 end
\ No newline at end of file




