--- a/thys2/ClosedForms.thy	Mon Mar 28 20:00:04 2022 +0100
+++ b/thys2/ClosedForms.thy	Tue Mar 29 10:57:02 2022 +0100
@@ -505,8 +505,28 @@
 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"
+  [intro, simp]:"rs \<leadsto>f* rs"
+| [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>f* rs3"
+
+inductive grewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g _" [10, 10] 10)
+  where
+  "(RZERO # rs) \<leadsto>g rs"
+| "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"
+| "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"
+| "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 
+
+
+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)
+where 
+ [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"
+*)
 
 lemma fr_in_rstar : "r1 \<leadsto>f r2 \<Longrightarrow> r1 \<leadsto>f* r2"
   using frewrites.intros(1) frewrites.intros(2) by blast
@@ -560,8 +580,13 @@
   apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later)
   using frewrites_cons by auto
 
+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))
 
-
+lemma frewrites_alt:
+  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>
@@ -577,13 +602,14 @@
   using frewrite.intros(1) many_steps_later apply blast
      apply(case_tac "x = x3")
       apply simp
-  
   using frewrites_cons apply presburger
   using frewrite.intros(1) many_steps_later apply fastforce
   apply(case_tac "rnullable x41")
-  apply simp
-
-
+     apply simp+
+     apply (simp add: frewrites_alt)
+  apply (simp add: frewrites_cons)
+   apply (simp add: frewrites_append)
+  by (simp add: frewrites_cons)
 
 
 fun alt_set:: "rrexp \<Rightarrow> rrexp set"
@@ -596,49 +622,134 @@
 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)
+
+  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)))"
-  using frewrite.intros(2) by blast
+  oops
 
-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))"
+lemma with_wo0_distinct:
+  shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac a)
+  apply(case_tac "RZERO \<in> rset")
+        apply simp+
+  using fr_in_rstar frewrite.intros(1) apply presburger
+  apply (case_tac "RONE \<in> rset")
+       apply simp+
+  using frewrites_cons apply presburger
+     apply(case_tac "a \<in> rset")
+  apply simp
+  apply (simp add: frewrites_cons)
+     apply(case_tac "a \<in> rset")
+  apply simp
+  apply (simp add: frewrites_cons)
+       apply(case_tac "a \<in> rset")
+  apply simp
+  apply (simp add: frewrites_cons)
+       apply(case_tac "a \<in> rset")
+  apply simp
+  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>
+       \<Longrightarrow> rdistinct rs2
+            (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f* 
+           rdistinct rs3 
+            (insert RZERO (rset \<union> \<Union> (alt_set ` rset)))"
+  apply(induct rs2 rs3 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
 
 
+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) ))))"
+  apply(induct rs1 rs2 rule: frewrites.induct)
+   apply simp
+  
+
+  sorry
+
+(*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:
+  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow>
+ (rdistinct rs1 {RZERO}) \<leadsto>f* rdistinct rs2 {RZERO}"
+  oops
+
+lemma frewrite_single_step:
+  shows " rs2 \<leadsto>f rs3 \<Longrightarrow> rsimp (RALTS rs2) = rsimp (RALTS rs3)"
+  apply(induct rs2 rs3 rule: frewrite.induct)
+    apply simp
+  using simp_flatten apply blast
+  by (metis (no_types, opaque_lifting) list.simps(9) rsimp.simps(2) simp_flatten2)
+
+lemma frewrites_equivalent_simp:
+  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
+  apply(induct rs1 rs2 rule: frewrites.induct)
+   apply simp
+  using frewrite_single_step 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 simp_der_flts:
   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = 
          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))"
-
-  apply(induct rs)
-   apply simp
-  apply(case_tac a)
-       apply simp+
-      prefer 2
-  apply simp
-      apply(case_tac "RZERO \<in> rset")
-       apply simp+
-  using distinct_flts_no0 apply presburger
-     apply (case_tac "x = x3")
-  prefer 2
-  apply simp
-  using distinct_flts_no0 apply presburger
-  apply(case_tac "RONE \<in> rset")
-     apply simp+
-  
-  sorry
+  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}")
+  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
 
 
 lemma simp_der_pierce_flts: