--- a/thys2/ClosedForms.thy	Sat Mar 26 11:24:36 2022 +0000
+++ b/thys2/ClosedForms.thy	Mon Mar 28 00:59:42 2022 +0100
@@ -494,6 +494,117 @@
 
 
 
+
+inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
+  where
+  "(RZERO # rs) \<leadsto>f rs"
+| "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"
+| "rs1 \<leadsto>f rs2 \<Longrightarrow> (r # rs1) \<leadsto>f (r # rs2)"
+
+
+inductive 
+  frewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f* _" [10, 10] 10)
+where 
+  rs1[intro, simp]:"rs \<leadsto>f* rs"
+| rs2[intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>f* rs3"
+
+lemma fr_in_rstar : "r1 \<leadsto>f r2 \<Longrightarrow> r1 \<leadsto>f* r2"
+  using frewrites.intros(1) frewrites.intros(2) by blast
+ 
+lemma freal_trans[trans]: 
+  assumes a1: "r1 \<leadsto>f* r2"  and a2: "r2 \<leadsto>f* r3"
+  shows "r1 \<leadsto>f* r3"
+  using a2 a1
+  apply(induct r2 r3 arbitrary: r1 rule: frewrites.induct) 
+  apply(auto)
+  done
+
+
+lemma  many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3"
+  by (meson fr_in_rstar freal_trans)
+
+
+lemma frewrite_append:
+  shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb"
+  apply(induct rs)
+  apply simp+
+  oops
+
+
+lemma frewrites_cons:
+  shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb"
+
+  oops
+
+lemma frewrites_append:
+  shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"
+  apply(induct rsa rsb rule: frewrites.induct)
+   apply simp
+  oops
+
+
+
+lemma frewrites_concat:
+  shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)"
+  apply(induct rs1 rs2 rule: frewrite.induct)
+    apply(simp)
+  apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>f (rs @ rsa)")
+  prefer 2
+  using frewrite.intros(1) apply blast
+    apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)")
+  using many_steps_later apply blast
+
+
+
+
+
+
+
+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)
+   apply simp
+  apply(case_tac a)
+       apply simp+
+  using frewrite.intros(1) many_steps_later apply blast
+     apply(case_tac "x = x3")
+     apply simp
+  
+
+
+
+
+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 (insert RZERO (rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f*  
+                          rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))"
+  by (meson frewrite.intros(2) frewrites.simps)
+  
+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)))"
+  using frewrite.intros(2) by blast
+
+lemma rd_flts_incorrect:
+  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 rset \<leadsto>f* rdistinct rs2 rset"
+  sledgehammer
+  by (smt (verit, ccfv_threshold) frewrites.simps)
+
+lemma flts_does_rewrite:
+  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rflts rs1 = rflts rs2"
+  oops
+
 lemma rflts_fltsder_derflts:
   shows "rflts (map rsimp (rdistinct (map (rder x3) (rflts rs)) rset)) = 
          rflts (map rsimp (rdistinct (rflts (map (rder x3) rs)) rset))"
@@ -501,13 +612,15 @@
 
 
 lemma simp_der_flts:
-  shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= 
-         rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))"
+  shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 
+         rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
 
-  apply(induct rs arbitrary: rset)
+  apply(induct rs)
    apply simp
   apply(case_tac a)
-       apply simp
+       apply simp+
+      prefer 2
+  apply simp
       apply(case_tac "RZERO \<in> rset")
        apply simp+
   using distinct_flts_no0 apply presburger
@@ -522,8 +635,13 @@
 
 
 lemma simp_der_pierce_flts:
-  shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
-           rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))"
+  shows " rsimp (
+rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
+) =
+          rsimp (
+rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})
+)"
+  
   sorry