--- a/thys2/ClosedForms.thy	Wed Apr 13 09:18:29 2022 +0100
+++ b/thys2/ClosedForms.thy	Wed Apr 13 18:57:24 2022 +0100
@@ -2065,26 +2065,152 @@
   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)
+lemma starders_hfau_also1:
+  shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])"
+  using star_hfau_induct by force
+
+lemma hflat_aux_grewrites:
+  shows "a # rs \<leadsto>g* hflat_aux a @ rs"
+  apply(induct a arbitrary: rs)
+       apply simp+
+   apply(case_tac x)
+    apply simp
+  apply(case_tac list)
+  
+  apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq)
+   apply(case_tac lista)
+  apply simp
+  apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv)
+  apply simp
+  by simp
+  
+
+
+
+lemma cbs_hfau_rsimpeq1:
+  shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))"
+  apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b")
+  using grewrites_equal_rsimp apply presburger
+  sorry
+
+
+lemma hfau_rsimpeq2:
+  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(subst rders_append)+
-  apply(case_tac "rnullable (rder c r0)")
+  apply(case_tac x)
+   apply simp
+  apply(case_tac "list")
    apply simp
   
-  sorry
+  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 hfau_rsimpeq1:
+  shows "created_by_star r \<Longrightarrow> hflat_aux r = rs \<Longrightarrow> rsimp r = rsimp (RALTS rs)"
+  apply(induct r arbitrary: rs rule: created_by_star.induct )
+  apply (metis created_by_seq.intros(1) hflat_aux.simps(5) sflat_aux.simps(6) sflat_rsimpeq)
+  apply simp
+  oops
+
+
+
+
 
 
 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]]) ) ))"
+  shows "rsimp (rders (RSTAR r0) (c#s)) = 
+rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+  using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger
+
+lemma star_closed_form2:
+  shows  "rsimp (rders_simp (RSTAR r0) (c#s)) = 
+rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+  by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem star_closed_form1)
+
+lemma star_closed_form3:
+  shows  "rsimp (rders_simp (RSTAR r0) (c#s)) =   (rders_simp (RSTAR r0) (c#s))"
+  by (metis list.distinct(1) rders_simp_same_simpders star_closed_form1 star_closed_form2)
+
+lemma star_closed_form4:
+  shows " (rders_simp (RSTAR r0) (c#s)) = 
+rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+  using star_closed_form2 star_closed_form3 by presburger
+
+lemma star_closed_form5:
+  shows " rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) Ss         )))) = 
+          rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ))))"
+  by (metis (mono_tags, lifting) list.map_comp map_eq_conv o_apply rsimp.simps(2) rsimp_idem)
+
+lemma star_closed_form6_hrewrites:
+  shows "  
+ (map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss )
+ scf\<leadsto>*
+(map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )"
+  apply(induct Ss)
+  apply simp
+  apply (simp add: ss1)
+  by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2)
+
+lemma star_closed_form6:
+  shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )))) = 
+          rsimp ( ( RALTS ( (map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ))))"
+  apply(subgoal_tac " map (\<lambda>s1.  (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss  scf\<leadsto>*
+                      map (\<lambda>s1.  rsimp (RSEQ  (rders r0 s1) (RSTAR r0)) ) Ss ")
+  using hrewrites_simpeq srewritescf_alt1 apply fastforce
+  using star_closed_form6_hrewrites by blast
+
+lemma star_closed_form7:
+  shows  " (rders_simp (RSTAR r0) (c#s)) = 
+rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+  using star_closed_form4 star_closed_form5 star_closed_form6 by presburger
+
+lemma derssimp_nonempty_list:
+  shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> 
+ rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) Ss)))) =
+ rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) Ss)))) "
   
-
-  sorry
+  by (metis (no_types, lifting) map_eq_conv rders_simp_same_simpders)
+
+lemma stupdate_nonempty:
+  shows "\<forall>s \<in> set  Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []"
+  apply(induct Ss)
+  apply simp
+  apply(case_tac "rnullable (rders r a)")
+   apply simp+
+  done
+
+
+lemma stupdates_nonempty:
+  shows "\<forall>s \<in> set Ss. s\<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_updates s r Ss). s \<noteq> []"
+  apply(induct s arbitrary: Ss)
+   apply simp
+  apply simp
+  using stupdate_nonempty by presburger
+
+
+
+
+lemma star_closed_form8:
+  shows  
+"rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))) = 
+ rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ ( (rders_simp r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))"
+  by (metis derssimp_nonempty_list neq_Nil_conv non_empty_list set_ConsD stupdates_nonempty)
+
+
 
 lemma star_closed_form:
   shows "rders_simp (RSTAR r0) (c#s) = 
@@ -2092,9 +2218,7 @@
   apply(induct s)
    apply simp
    apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem)
-  
-
-  sorry
+  using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
 
 
 lemma simp_helps_der_pierce: