
diff -r 15d182ffbc76 -r aecf1ddf3541 thys3/ClosedForms.thy
--- a/thys3/ClosedForms.thy	Sun Jun 26 22:22:47 2022 +0100
+++ b/thys3/ClosedForms.thy	Tue Jun 28 21:07:42 2022 +0100
@@ -1,20 +1,8 @@
 theory ClosedForms 
-  imports "BasicIdentities"
+  imports "HarderProps"
 begin
 
 
-lemma flts_middle0:
-  shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
-  apply(induct rsa)
-  apply simp
-  by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
-
-
-
-lemma simp_flatten_aux0:
-  shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"
-  by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts)
-  
 
 inductive 
   hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
@@ -68,44 +56,8 @@
   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
 
-lemma simp_removes_duplicate1:
-  shows  " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) =  rsimp (RALTS (rsa))"
-and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
-  apply(induct rsa arbitrary: a1)
-     apply simp
-    apply simp
-  prefer 2
-  apply(case_tac "a = aa")
-     apply simp
-    apply simp
-  apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
-  apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
-  by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2))
-  
-lemma simp_removes_duplicate2:
-  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
-  apply(induct rsb arbitrary: rsa)
-   apply simp
-  using distinct_removes_duplicate_flts apply auto[1]
-  by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
 
-lemma simp_removes_duplicate3:
-  shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
-  using simp_removes_duplicate2 by auto
 
-(*
-lemma distinct_removes_middle4:
-  shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
-  using distinct_removes_middle(1) by fastforce
-*)
-
-(*
-lemma distinct_removes_middle_list:
-  shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
-  apply(induct x)
-   apply simp
-  by (simp add: distinct_removes_middle3)
-*)
 
 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
   where
@@ -260,11 +212,6 @@
   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 grewrite_cases_middle:
   shows "rs1 \<leadsto>g rs2 \<Longrightarrow> 
@@ -279,211 +226,6 @@
   by blast
 
 
-lemma good_singleton:
-  shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"
-  using good.simps(1) k0b by blast
-
-
-
-
-
-
-
-
-lemma distinct_early_app1:
-  shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
-  apply(induct rs arbitrary: rset rset1)
-   apply simp
-  apply simp
-  apply(case_tac "a \<in> rset1")
-   apply simp
-   apply(case_tac "a \<in> rset")
-    apply simp+
-  
-   apply blast
-  apply(case_tac "a \<in> rset1")
-   apply simp+
-  apply(case_tac "a \<in> rset")
-   apply simp
-   apply (metis insert_subsetI)
-  apply simp
-  by (meson insert_mono)
-
-
-lemma distinct_early_app:
-  shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"
-  apply(induct rsb)
-   apply simp
-  using distinct_early_app1 apply blast
-  by (metis distinct_early_app1 distinct_once_enough empty_subsetI)
-
-
-lemma distinct_eq_interesting1:
-  shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"
-  apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")
-   apply(simp only:)
-  using distinct_early_app apply blast 
-  by (metis append_Cons distinct_early_app rdistinct.simps(2))
-
-
-
-lemma good_flatten_aux_aux1:
-  shows "\<lbrakk> size rs \<ge>2; 
-\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
-       \<Longrightarrow> rdistinct (rs @ rsb) rset =
-           rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
-  apply(induct rs arbitrary: rset)
-   apply simp
-  apply(case_tac "a \<in> rset")
-   apply simp
-   apply(case_tac "rdistinct rs {a}")
-    apply simp
-    apply(subst good_singleton)
-     apply force
-  apply simp
-    apply (meson all_that_same_elem)
-   apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")
-  prefer 2
-  using k0a rsimp_ALTs.simps(3) apply presburger
-  apply(simp only:)
-  apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")
-    apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))
-   apply (meson distinct_eq_interesting1)
-  apply simp
-  apply(case_tac "rdistinct rs {a}")
-  prefer 2
-   apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")
-  apply(simp only:)
-  apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =
-           rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")
-   apply simp
-  apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))
-  using rsimp_ALTs.simps(3) apply presburger
-  by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)
-
-
-
-  
-
-lemma good_flatten_aux_aux:
-  shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; 
-\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
-       \<Longrightarrow> rdistinct (rs @ rsb) rset =
-           rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
-  apply(erule exE)+
-  apply(subgoal_tac "size rs \<ge> 2")
-   apply (metis good_flatten_aux_aux1)
-  by (simp add: Suc_leI length_Cons less_add_Suc1)
-
-
-
-lemma good_flatten_aux:
-  shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; 
-           \<forall>r\<in>set rsb. good r \<or> r = RZERO;
-     rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});
-     rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =
-     rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});
-     map rsimp rsa = rsa; 
-     map rsimp rsb = rsb; 
-     map rsimp rs = rs;
-     rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =
-     rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));
-     rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =
-     rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>
-    \<Longrightarrow>    rdistinct (rflts rs @ rflts rsb) rset =
-           rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"
-  apply simp
-  apply(case_tac "rflts rs ")
-   apply simp
-  apply(case_tac "list")
-   apply simp
-   apply(case_tac "a \<in> rset")
-    apply simp
-  apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2))
-   apply simp
-  apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left)
-  apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
-   prefer 2
-  apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)  
-  apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
-   prefer 2
-  apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1)  
-  by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
-
-  
-
-
-lemma good_flatten_middle:
-  shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>
-rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))"
-  apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
-map rsimp rs @ map rsimp rsb)) {})")
-  prefer 2
-  apply simp
-  apply(simp only:)
-    apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 
-[rsimp (RALTS rs)] @ map rsimp rsb)) {})")
-  prefer 2
-   apply simp
-  apply(simp only:)
-  apply(subgoal_tac "map rsimp rsa = rsa")
-  prefer 2
-  apply (metis map_idI rsimp.simps(3) test)
-  apply(simp only:)
-  apply(subgoal_tac "map rsimp rsb = rsb")
-   prefer 2
-  apply (metis map_idI rsimp.simps(3) test)
-  apply(simp only:)
-  apply(subst flts_append)+
-  apply(subgoal_tac "map rsimp rs = rs")
-   apply(simp only:)
-   prefer 2
-  apply (metis map_idI rsimp.simps(3) test)
-  apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = 
-rdistinct (rflts rsa) {} @ rdistinct  (rflts rs @ rflts rsb) (set (rflts rsa))")
-   apply(simp only:)
-  prefer 2
-  using rdistinct_concat_general apply blast
-  apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = 
-rdistinct (rflts rsa) {} @ rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
-   apply(simp only:)
-  prefer 2
-  using rdistinct_concat_general apply blast
-  apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = 
-                     rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")
-   apply presburger
-  using good_flatten_aux by blast
-
-
-
-lemma simp_flatten3:
-  shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
-  apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 
-                     rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
-  prefer 2
-   apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)
-  apply (simp only:)
-  apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = 
-rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")
-  prefer 2
-   apply (metis map_append simp_flatten_aux0)
-  apply(simp only:)
-  apply(subgoal_tac "rsimp  (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =
- rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")
-  
-   apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)
-  apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
-   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
-    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
-  
-  using good_flatten_middle apply presburger
-  
-  apply (simp add: good1)
-  apply (simp add: good1)
-  apply (simp add: good1)
-
-  done
-
 
 
   
@@ -1286,6 +1028,16 @@
   by fastforce
 
 
+fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where
+"vsuf [] _ = []"
+|"vsuf (c#cs) r1 = (if (rnullable r1) then  (vsuf cs (rder c r1)) @ [c # cs]
+                                      else  (vsuf cs (rder c r1))
+                   ) "
+
+
+
+
+
 lemma vsuf_prop1:
   shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) 
                                 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
@@ -1533,6 +1285,30 @@
 (*AALTS [a\x . b.c, b\x .c,  c \x]*)
 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
 
+fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where
+"star_update c r [] = []"
+|"star_update c r (s # Ss) = (if (rnullable (rders r s)) 
+                                then (s@[c]) # [c] # (star_update c r Ss) 
+                               else   (s@[c]) # (star_update c r Ss) )"
+
+
+fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
+  where
+"star_updates [] r Ss = Ss"
+| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
+
+
+lemma stupdates_append: shows 
+"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)"
+  apply(induct s arbitrary: Ss)
+   apply simp
+  apply simp
+  done
+
+
+
+
+
 lemma stupdate_induct1:
   shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"




