--- a/thys2/ClosedForms.thy	Wed Apr 13 18:57:24 2022 +0100
+++ b/thys2/ClosedForms.thy	Wed Apr 13 22:20:08 2022 +0100
@@ -1329,28 +1329,52 @@
   shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
   by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
 
+lemma hrewrite_simpeq:
+  shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  apply(induct rule: hrewrite.induct)
+            apply simp+
+  apply (simp add: basic_rsimp_SEQ_property3)
+  apply (simp add: basic_rsimp_SEQ_property1)
+  using rsimp.simps(1) apply presburger
+        apply simp+
+  using flts_middle0 apply force
+  using simp_flatten3 apply presburger
+  apply simp+
+  apply (simp add: idem_after_simp1)
+  using grewrite.intros(4) grewrite_equal_rsimp by presburger
+
 lemma hrewrites_simpeq:
   shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
-  sorry
-
-lemma distinct_grewrites_subgoal1:
-  shows "  \<And>rs1 rs2 rs3 a list.
-       \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3; rs2 = [a]; list = []\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
- (* apply (smt (z3) append.left_neutral append.right_neutral append_Cons grewrite.simps grewrite_singleton hrewrite.intros(10) hrewrite.intros(9) hrewrites.simps list.inject r_finite1 rsimp_ALTs.elims rsimp_ALTs.simps(2) rsimp_alts_equal)*)
-  sorry
+  apply(induct rule: hrewrites.induct)
+   apply simp
+  apply(subgoal_tac "rsimp r2 = rsimp r3")
+   apply auto[1]
+  using hrewrite_simpeq by presburger
+  
 
 lemma grewrite_ralts:
   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
   by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
-  
-
-
 
 lemma grewrites_ralts:
   shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
-  apply(induct rs rs' rule: grewrites.induct)
+  apply(induct rule: grewrites.induct)
   apply simp
   using grewrite_ralts hreal_trans by blast
+  
+
+lemma distinct_grewrites_subgoal1:
+  shows "  
+       \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
+  apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
+  apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+  apply(subgoal_tac "rs1 \<leadsto>g* rs3")
+  using grewrites_ralts apply blast
+  using grewrites.intros(2) by presburger
+
+
+
+
 
 
 lemma grewrites_ralts_rsimpalts:
@@ -1477,24 +1501,51 @@
 
 lemma rnullable_hrewrite:
   shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
-  sorry
+  apply(induct rule: hrewrite.induct)
+            apply simp+
+     apply blast
+    apply simp+
+  done
 
 
 lemma interleave1:
   shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
   apply(induct r r' rule: hrewrite.induct)
-            
-  
             apply (simp add: hr_in_rstar hrewrite.intros(1))
   apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)
           apply simp
           apply(subst interleave_aux1)
           apply simp
          apply(case_tac "rnullable r1")
-
-  sorry
-
+          apply simp
+  
+          apply (simp add: hrewrites_seq_context rnullable_hrewrite srewritescf_alt1 ss1 ss2)
+  
+         apply (simp add: hrewrites_seq_context rnullable_hrewrite)
+        apply(case_tac "rnullable r1")
+  apply simp
+  
+  using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger
+  apply simp
+  using hr_in_rstar hrewrites_seq_context2 apply blast
+       apply simp
   
+  using hrewrites_alts apply auto[1]
+  apply simp
+  using grewrite.intros(1) grewrite_append grewrite_ralts apply auto[1]
+  apply simp
+  apply (simp add: grewrite.intros(2) grewrite_append grewrite_ralts)
+  apply (simp add: hr_in_rstar hrewrite.intros(9))
+   apply (simp add: hr_in_rstar hrewrite.intros(10))
+  apply simp
+  using hrewrite.intros(11) by auto
+
+lemma interleave_star1:
+  shows "r \<leadsto>* r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
+  apply(induct rule : hrewrites.induct)
+   apply simp
+  by (meson hreal_trans interleave1)
+
 
 
 lemma inside_simp_removal:
@@ -1507,9 +1558,11 @@
   using inside_simp_seq_nullable apply blast
     apply simp
   apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)
-  
+   apply(subgoal_tac "rder x (RALTS xa) \<leadsto>* rder x (rsimp (RALTS xa))")
+  using hrewrites_simpeq apply presburger
+  using interleave_star1 simp_hrewrites apply presburger
+  by simp
   
-  sorry
 
 
 
@@ -2091,7 +2144,7 @@
   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
+  by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites)
 
 
 lemma hfau_rsimpeq2:
@@ -2221,16 +2274,5 @@
   using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
 
 
-lemma simp_helps_der_pierce:
-  shows " rsimp
-            (rder x
-              (rsimp_ALTs rs)) = 
-          rsimp 
-            (rsimp_ALTs 
-              (map (rder x )
-                rs
-              )
-            )"
-  sorry
 
 end
\ No newline at end of file