--- a/thys2/BasicIdentities.thy	Tue Apr 12 15:51:35 2022 +0100
+++ b/thys2/BasicIdentities.thy	Wed Apr 13 09:18:29 2022 +0100
@@ -768,15 +768,23 @@
 
 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_simp r s)) 
+|"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 distinct_flts_no0:
   shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =

--- a/thys2/ClosedForms.thy	Tue Apr 12 15:51:35 2022 +0100
+++ b/thys2/ClosedForms.thy	Wed Apr 13 09:18:29 2022 +0100
@@ -1602,16 +1602,6 @@
 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = 
 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
   by (metis alts_closed_form comp_apply rders_simp_nonempty_simped)
-  
-
-
-
-lemma star_closed_form:
-  shows "rders_simp (RSTAR r0) (c#s) = 
-rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
-  apply(induct s)
-   apply simp
-  sorry
 
 thm vsuf.simps
 
@@ -1623,17 +1613,6 @@
 
 
 
-lemma vsuf_der_stepwise:
-  shows "rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1))) = 
-rsimp (rder x (rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # map (rders_simp r2) (vsuf xs r1)))))"
-  apply simp
-  apply(subst rders_simp_append)
-
-  oops
-
-inductive softrewrite :: "rrexp \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>o _" [100, 100] 100) where
-  "RALTS rs  \<leadsto>o rs"
-| "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])"
 
 
 fun sflat_aux :: "rrexp  \<Rightarrow> rrexp list " where
@@ -1808,14 +1787,7 @@
 
 
 
-lemma seq_sflat0:
-  shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) #
-                                       (map (rders r2) (vsuf s r1))) )"
-  apply(induct s rule: rev_induct)
-   apply simp
-  apply(subst rders_append)+
 
-  sorry
 
 lemma vsuf_prop1:
   shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) 
@@ -1887,18 +1859,11 @@
 
 
 lemma sflat_rsimpeq:
-  shows "sflat_aux r1 = sflat_aux r2 \<Longrightarrow> rsimp r1 = rsimp r2"
-  apply(cases r1 )
-       apply(cases r2)
-            apply simp+
-        apply(case_tac x5)
-  apply simp
-        apply(case_tac list)
-         apply simp
-
-
-
-  sorry
+  shows "created_by_seq r1 \<Longrightarrow> sflat_aux r1 =  rs \<Longrightarrow> rsimp r1 = rsimp (RALTS rs)"
+  apply(induct r1 arbitrary: rs rule:  created_by_seq.induct)
+   apply simp
+  using rsimp_seq_equal1 apply force
+  by (metis head_one_more_simp rsimp.simps(2) sflat_aux.simps(1) simp_flatten)
 
 
 
@@ -1906,13 +1871,16 @@
   shows "rsimp (rders (RSEQ r1 r2) s) = 
 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
   apply(case_tac "s \<noteq> []")
-  apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = sflat_aux (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))")
+  apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) s)")
+  apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))")
   using sflat_rsimpeq apply blast
-  using seq_sfau0 apply blast
+    apply (simp add: seq_sfau0)
+  using recursively_derseq1 apply blast
   apply simp
   by (metis idem_after_simp1 rsimp.simps(1))
   
 
+
 lemma seq_closed_form_aux1:
   shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) =
 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
@@ -1986,6 +1954,149 @@
    apply force
   by presburger
 
+
+lemma star_closed_form_seq1:
+  shows "sflat_aux (rders (RSTAR r0) (c # s)) = 
+   RSEQ (rders (rder c r0) s) (RSTAR r0) #
+                                       map (rders (RSTAR r0)) (vsuf s (rder c r0))"
+  apply simp
+  using seq_sfau0 by blast
+
+fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where
+  "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2"
+| "hflat_aux r = [r]"
+
+
+fun hflat :: "rrexp \<Rightarrow> rrexp" where
+  "hflat (RALT r1 r2) = RALTS ((hflat_aux r1) @ (hflat_aux r2))"
+| "hflat r = r"
+
+inductive created_by_star :: "rrexp \<Rightarrow> bool" where
+  "created_by_star (RSEQ ra (RSTAR rb))"
+| "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)"
+
+fun hElem :: "rrexp  \<Rightarrow> rrexp list" where
+  "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)"
+| "hElem r = [r]"
+
+
+
+
+lemma cbs_ders_cbs:
+  shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)"
+  apply(induct r rule: created_by_star.induct)
+   apply simp
+  using created_by_star.intros(1) created_by_star.intros(2) apply auto[1]
+  by (metis (mono_tags, lifting) created_by_star.simps list.simps(8) list.simps(9) rder.simps(4))
+
+lemma star_ders_cbs:
+  shows "created_by_star (rders (RSEQ r1 (RSTAR r2)) s)"
+  apply(induct s rule: rev_induct)
+   apply simp
+   apply (simp add: created_by_star.intros(1))
+  apply(subst rders_append)
+  apply simp
+  using cbs_ders_cbs by auto
+
+lemma created_by_star_cases:
+  shows "created_by_star r \<Longrightarrow> \<exists>ra rb. (r = RALT ra rb \<and> created_by_star ra \<and> created_by_star rb) \<or> r = RSEQ ra rb "
+  by (meson created_by_star.cases)
+
+
+
+lemma hfau_pushin: 
+  shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))"
+  apply(induct r rule: created_by_star.induct)
+   apply simp
+  apply(subgoal_tac "created_by_star (rder c r1)")
+  prefer 2
+  apply(subgoal_tac "created_by_star (rder c r2)")
+  using cbs_ders_cbs apply blast
+  using cbs_ders_cbs apply auto[1]
+  apply simp
+  done
+
+lemma stupdate_induct1:
+  shows " concat (map (hElem \<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)"
+  apply(induct Ss)
+   apply simp+
+  by (simp add: rders_append)
+  
+
+
+lemma stupdates_join_general:
+  shows  "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) =
+           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)"
+  apply(induct xs arbitrary: Ss)
+   apply (simp)
+  prefer 2
+   apply auto[1]
+  using stupdate_induct1 by blast
+
+
+
+ 
+lemma stupdates_join:
+  shows "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) =
+           map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 [[c]])"
+  using stupdates_join_general by auto
+  
+
+
+lemma star_hfau_induct:
+  shows "hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) s) =   
+      map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst rders_append)+
+  apply simp
+  apply(subst stupdates_append)
+  apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)")
+  prefer 2
+  apply (simp add: star_ders_cbs)
+  apply(subst hfau_pushin)
+   apply simp
+  apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) =
+                     concat (map hElem (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ")
+   apply(simp only:)
+  prefer 2
+   apply presburger
+  apply(subst stupdates_append[symmetric])
+  using stupdates_join_general by blast
+
+
+
+lemma star_closed_form_seq2:
+  shows "RSEQ (rders (rder c r0) s) (RSTAR r0) # map (rders (RSTAR r0)) (vsuf s (rder c r0)) =
+         map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst rders_append)+
+  apply(case_tac "rnullable (rder c r0)")
+   apply simp
+  
+  sorry
+
+
+lemma star_closed_form1:
+  shows "rders (RSTAR r0) (c#s) = 
+ ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
+  
+
+  sorry
+
+lemma star_closed_form:
+  shows "rders_simp (RSTAR r0) (c#s) = 
+rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
+  apply(induct s)
+   apply simp
+   apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
+  
+
+  sorry
+
+
 lemma simp_helps_der_pierce:
   shows " rsimp
             (rder x