diff -r 812e5d112f49 -r 671a83abccf3 thys3/ClosedForms.thy
--- a/thys3/ClosedForms.thy	Fri Jul 01 13:02:15 2022 +0100
+++ b/thys3/ClosedForms.thy	Mon Jul 04 12:27:13 2022 +0100
@@ -1079,7 +1079,8 @@
 
 
 lemma vsuf_compose2:
-  shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = map (rders r2) (vsuf (xs @ [x]) r1)"
+  shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = 
+          map (rders r2) (vsuf (xs @ [x]) r1)"
 proof(induct xs arbitrary: r1)
   case Nil
   then show ?case 
@@ -1244,6 +1245,19 @@
 
 
 
+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 cbs_ders_cbs:
   shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)"
@@ -1261,16 +1275,11 @@
   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 hflat_aux (map (rder c) (hflat_aux r)))"
-
 proof(induct r rule: created_by_star.induct)
   case (1 ra rb)
   then show ?case by simp
@@ -1287,19 +1296,6 @@
 (*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)
@@ -1321,8 +1317,11 @@
 
 
 lemma stupdates_join_general:
-  shows  "concat (map hflat_aux (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)"
+  shows  "concat 
+            (map hflat_aux (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
@@ -1386,30 +1385,6 @@
   apply (metis rsimp.simps(6) rsimp_seq_equal1)
   using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger
 
-  
-(*
-lemma hfau_rsimpeq2_oldproof:  shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
-  apply(induct r)
-       apply simp+
-    apply (metis rsimp_seq_equal1)
-  prefer 2
-   apply simp
-  apply(case_tac x)
-   apply simp
-  apply(case_tac "list")
-   apply simp
-  apply (metis idem_after_simp1)
-  apply(case_tac "lista")
-  prefer 2
-   apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2))
-  apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))")
-  apply simp
-  apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))")
-  using hflat_aux.simps(1) apply presburger
-  apply simp
-  using cbs_hfau_rsimpeq1 by fastforce
-*)
-
 lemma star_closed_form1:
   shows "rsimp (rders (RSTAR r0) (c#s)) = 
 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"