diff -r b2a8610cf110 -r 574749f5190b thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/ClosedForms.thy	Thu Apr 07 21:31:29 2022 +0100
@@ -498,7 +498,17 @@
 
 lemma grewrite_rdistinct_aux:
   shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"
-  sorry
+  apply(induct rsa arbitrary: rs rset)
+   apply simp
+  apply(case_tac " a \<in> rset")
+   apply simp
+  apply(case_tac "a \<in> set rs")
+  apply simp
+   apply (metis Un_insert_left Un_insert_right gmany_steps_later grewrite_variant1 insert_absorb)
+  apply simp
+  apply(drule_tac x = "rs @ [a]" in meta_spec)
+  by (metis Un_insert_left Un_insert_right append.assoc append.right_neutral append_Cons append_Nil insert_absorb2 list.simps(15) set_append)
+  
 
 lemma grewrite_rdistinct_worth1:
   shows "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)"
@@ -540,11 +550,37 @@
 
 lemma flts_gstar:
   shows "rs \<leadsto>g* rflts rs"
-  sorry
+  apply(induct rs)
+   apply simp
+  apply(case_tac "a = RZERO")
+   apply simp
+  using gmany_steps_later grewrite.intros(1) apply blast
+  apply(case_tac "\<exists>rsa. a = RALTS rsa")
+   apply(erule exE)
+  apply simp
+   apply (meson grewrite.intros(2) grewrites.simps grewrites_cons)
+  by (simp add: grewrites_cons rflts_def_idiot)
+
 
-lemma create_nonexistent_distinct_set:
+lemma wrong1:
   shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct rs (insert a rset)) \<leadsto>g* rs1 @ (rdistinct rs (rset))"
-  sorry
+  
+  oops
+
+lemma more_distinct1:
+  shows "       \<lbrakk>\<And>rsb rset rset2.
+           rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2);
+        rset2 \<subseteq> set rsb; a \<notin> rset; a \<in> rset2\<rbrakk>
+       \<Longrightarrow> rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+  apply(subgoal_tac "rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (insert a rset)")
+   apply(subgoal_tac "rsb @ rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)")
+    apply (meson greal_trans)
+   apply (metis Un_iff Un_insert_left insert_absorb)
+  by (simp add: gr_in_rstar grewrite_variant1 in_mono)
+  
+
+
+
 
 lemma grewrites_in_distinct0:
   shows "a \<in>  set rs1 \<Longrightarrow> rs1 @ (rdistinct (a # rs) rset) \<leadsto>g* rs1 @ (rdistinct rs rset)"
@@ -562,13 +598,38 @@
 
 
 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)"
+  shows     "       RALTS rs \<notin> set rsb \<Longrightarrow>
+       rsb @
+       RALTS rs #
+       rdistinct rsa
+        (insert (RALTS rs)
+          (set rsb)) \<leadsto>g* rflts rsb @
+                          rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
 
+   apply simp
+  apply(subgoal_tac "rsb @
+    RALTS rs #
+    rdistinct rsa
+     (insert (RALTS rs)
+       (set rsb)) \<leadsto>g* rsb @
+    rs @
+    rdistinct rsa
+     (insert (RALTS rs)
+       (set rsb)) ")
+  apply(subgoal_tac " rsb @
+    rs @
+    rdistinct rsa
+     (insert (RALTS rs)
+       (set rsb)) \<leadsto>g*
+                      rsb @
+    rdistinct rs (set rsb) @
+    rdistinct rsa
+     (insert (RALTS rs)
+       (set rsb)) ")
+    apply (smt (verit, ccfv_SIG) Un_insert_left flts_gstar greal_trans grewrite_rdistinct_aux grewritess_concat inf_sup_aci(5) rdistinct_concat_general rdistinct_set_equality set_append)
+   apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
+  by (simp add: gr_in_rstar grewrite.intros(2) grewrites_append)
   
-  sorry
 
 
 
@@ -698,10 +759,24 @@
   apply (simp add: insert_absorb)
   by auto
 
+lemma middle_grewrites: 
+"rs1 \<leadsto>g* rs2 \<Longrightarrow> rsa @ rs1 @ rsb \<leadsto>g* rsa @ rs2 @ rsb "
+  by (simp add: grewritess_concat)
+
+lemma rdistinct_removes_all:
+  shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct rs rset = []"
+  
+  by (metis append.right_neutral rdistinct.simps(1) rdistinct_concat)
 
 lemma ends_removal:
   shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc"
-  sorry
+  apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* 
+                     rsb @ rdistinct rs (set rsb) @ rs @ rsc")
+   apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rs @ rsc \<leadsto>g* 
+rsb @ rdistinct rs (set rsb) @ rdistinct rs (set (rsb @ rdistinct rs (set rsb))) @ rsc")
+  apply (metis (full_types) append_Nil2 append_eq_appendI greal_trans list_dlist_union rdistinct_removes_all set_append)
+   apply (metis append.assoc append_Nil gstar_rdistinct_general middle_grewrites)
+  using gr_in_rstar grewrite.intros(2) grewrites_append by presburger
 
 lemma grewrites_rev_append:
   shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]"
@@ -717,7 +792,7 @@
   shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
   by (simp add: concat_rdistinct_equality1)
 
-lemma grewrites_shape2:
+lemma grewrites_shape2_aux:
   shows "       RALTS rs \<notin> set rsb \<Longrightarrow>
        rsb @
        rdistinct (rs @ rsa)
@@ -767,6 +842,16 @@
    apply (simp add: distinct_keeps_last)+
   done
 
+lemma grewrites_shape2:
+  shows "       RALTS rs \<notin> set rsb \<Longrightarrow>
+       rsb @
+       rdistinct (rs @ rsa)
+        (set rsb) \<leadsto>g* rflts rsb @
+                       rdistinct rs (set rsb) @
+                       rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+  apply (meson flts_gstar greal_trans grewrites.simps grewrites_shape2_aux grewritess_concat)
+  done
+
 lemma rdistinct_add_acc:
   shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
   apply(induct rs arbitrary: rsb rset rset2)
@@ -774,8 +859,8 @@
   apply (case_tac "a \<in> rset")
    apply simp
   apply(case_tac "a \<in> rset2")
-  apply simp
-   apply (meson create_nonexistent_distinct_set gr_in_rstar greal_trans grewrite_variant1 in_mono)
+   apply simp
+  apply (simp add: more_distinct1)
   apply simp
   apply(drule_tac x = "rsb @ [a]" in meta_spec)
   by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1)
@@ -823,14 +908,13 @@
   apply (metis frewrite_fun1 rdistinct_concat sup_ge2)
   apply(simp)
   apply(rule_tac x = 
- "rsb @
+ "rflts rsb @
                        rdistinct rs (set rsb) @
                        rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI)
   apply(rule conjI)
    prefer 2
   using grewrites_shape2 apply force
-  by (metis Un_insert_left frewrite_rd_grewrites_aux inf_sup_aci(5) insert_is_Un rdistinct.simps(2))
-
+  using frewrite_rd_grewrites_aux by blast
 
 
 
@@ -896,13 +980,7 @@
   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
-*)
 
 
 
@@ -942,12 +1020,9 @@
 
 lemma simp_more_distinct:
   shows "rsimp  (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
-  
-
+  oops
 
 
-  sorry
-
 lemma non_empty_list:
   shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
   by (metis empty_iff empty_set)
@@ -1091,89 +1166,136 @@
   shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))"
   by (simp add: set_inclusion_with_flts1)
   
-lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
+lemma can_spill_lst:"\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
           \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = 
 rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"
+  
+  using flts_append rflts_spills_last rsimp_inner_idem4 by presburger
+  
+
+
+
+
+lemma common_rewrites_equal:
+  shows "(rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) \<Longrightarrow> rsimp (rsimp_ALTs rs1 ) = rsimp (rsimp_ALTs rs2)"
+  using grewrites_simpalts by force
+
+
+lemma basic_regex_property1:
+  shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
+  sorry
+
+lemma basic_rsimp_SEQ_property1:
+  shows "rsimp_SEQ RONE r = r"
+  by (simp add: idiot)
+
+lemma basic_rsimp_SEQ_property3:
+  shows "rsimp_SEQ r RZERO = RZERO"  
+  using rsimp_SEQ.elims by blast
+
+thm rsimp_SEQ.elims
+
+
+lemma basic_rsimp_SEQ_property2:
+  shows "\<lbrakk>r1 \<noteq> RZERO ; r1 \<noteq> RONE; r2 \<noteq> RZERO\<rbrakk> \<Longrightarrow>rsimp_SEQ r1 r2 = RSEQ r1 r2"
+  apply(case_tac r1)
+       apply simp+
+     apply (simp add: idiot2)
+  using idiot2 apply blast
+  using idiot2 apply auto[1]
+  using idiot2 by blast
+
+
+(*
+lemma rderssimp_same_rewrites_rder_induct1:
+  shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ;
+ ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow> 
+\<exists>rs3. ([rder x (rsimp (RSEQ r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RSEQ r1 r2)] \<leadsto>g* rs3) "
+  sorry
+
+lemma rderssimp_same_rewrites_rder_induct2:
+  shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) \<rbrakk> \<Longrightarrow> 
+\<exists>rs3. ([rder x (rsimp (RSTAR r1))] \<leadsto>g* rs3) \<and> ([rder x (RSTAR r1)] \<leadsto>g* rs3) "
+  sorry
+
+lemma rderssimp_same_rewrites_rder_induct3:
+  shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ;
+ ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow> 
+\<exists>rs3. ([rder x (rsimp (RALT r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RALT r1 r2)] \<leadsto>g* rs3) "
+  sorry
+
+lemma rderssimp_same_rewrites_rder_induct4:
+  shows "\<lbrakk>\<forall>r \<in> set rs. \<exists> rsa. ([rder x (rsimp r)] \<leadsto>g* rsa ) \<and> ([rder x r] \<leadsto>g* rsa) \<rbrakk> \<Longrightarrow> 
+\<exists>rsb. ([rder x (rsimp (RALTS rs))]  \<leadsto>g* rsb) \<and> ([rder x (RALTS rs)] \<leadsto>g* rsb) "
+  sorry
+
+lemma rderssimp_same_rewrites_rder_base1:
+  shows "([rder x (rsimp RONE)] \<leadsto>g* [] ) \<and> ([rder x RONE] \<leadsto>g* [])"
+  by (simp add: gr_in_rstar grewrite.intros(1))
+
+lemma rderssimp_same_rewrites_rder_base2:
+  shows " ([rder x (rsimp RZERO)] \<leadsto>g* [] ) \<and> ([rder x RZERO] \<leadsto>g* [])"
+  using rderssimp_same_rewrites_rder_base1 by auto
+
+lemma rderssimp_same_rewrites_rder_base3:
+  shows " ([rder x (rsimp (RCHAR c))] \<leadsto>g* [] ) \<and> ([rder x (RCHAR c)] \<leadsto>g* [])"
+  sorry
+*)
+
+lemma inside_simp_seq_nullable:
+  shows 
+"\<And>r1 r2.
+       \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
+        rnullable r1\<rbrakk>
+       \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
+           rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
+  apply(case_tac "rsimp r1 = RONE")
+   apply(simp)
+  apply(subst basic_rsimp_SEQ_property1)
+   apply (simp add: idem_after_simp1)
+  apply(case_tac "rsimp r1 = RZERO")
+  
+  using basic_regex_property1 apply blast
+  apply(case_tac "rsimp r2 = RZERO")
+  
+  apply (simp add: basic_rsimp_SEQ_property3)
+  apply(subst basic_rsimp_SEQ_property2)
+     apply simp+
+  apply(subgoal_tac "rnullable (rsimp r1)")
+   apply simp
+  using rsimp_idem apply presburger
 
   sorry
 
 
-lemma last_elem_dup1:
-  shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
-  apply simp
-  apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
-  prefer 2
-   apply simp
-  apply(case_tac "rsimp a")
-       apply simp
+lemma inside_simp_removal:
+  shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
+  apply(induct r)
+       apply simp+
+    apply(case_tac "rnullable r1")
+     apply simp
   
-  using flts_identity3 apply presburger
-      apply(subst flts_identity2)
-  using rrexp.distinct(1) rrexp.distinct(15) apply presburger
-      apply(subst distinct_removes_last3[symmetric])
-  using set_inclusion_with_flts apply blast
-  apply simp
-  apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10)
-  apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11)
-  sorry
-
-lemma last_elem_dup:
-  shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))"
-  apply(induct as rule: rev_induct)
-   apply simp
-  apply simp
-  apply(subgoal_tac "xs \<noteq> []")
-  prefer 2
-  
-
-  
-
-  sorry
-
-lemma appeared_before_remove_later:
-  shows "a \<in>  set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))"
-and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))"
-  apply(induct rs arbitrary: as)
-   apply simp
-  
-
-  sorry
-
-lemma distinct_remove_later:
-  shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk>
-       \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) =
-           rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))"
-  
+  using inside_simp_seq_nullable apply blast
   sorry
 
 
-lemma distinct_der_general:
-  shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) =
- rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )"
-  apply(induct rs arbitrary: rsa)
-   apply simp
-  apply(case_tac "a \<in> set rsa")
-   apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)")
-  apply simp
+lemma rders_simp_same_simpders:
+  shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
+  apply(induct s rule: rev_induct)
    apply simp
-  apply(case_tac "rder x a \<notin> set (map (rder x) rsa)")
-   apply(simp)
-  apply(subst map_concat_cons)+
-  apply(drule_tac x = "rsa @ [a]" in meta_spec)
+  apply(case_tac "xs = []")
    apply simp
-  apply(drule neg_removal_element_of)
-  apply simp
-  apply(subst distinct_remove_later)
-   apply simp
-  apply(drule_tac x = "rsa" in meta_spec)
-  by blast
+  apply(simp add: rders_append rders_simp_append)
+  using inside_simp_removal by blast
 
-  
+
 
 
 lemma distinct_der:
-  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
-  by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty)
+  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = 
+         rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+  by (metis grewrites_simpalts gstar_rdistinct inside_simp_removal rder_rsimp_ALTs_commute)
+