--- a/thys2/ClosedForms.thy	Sat Apr 09 09:32:49 2022 +0100
+++ b/thys2/ClosedForms.thy	Sat Apr 09 19:17:42 2022 +0100
@@ -1183,7 +1183,10 @@
 
 lemma basic_regex_property1:
   shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
-  sorry
+  apply(induct r rule: rsimp.induct)
+  apply(auto)
+  apply (metis idiot idiot2 rrexp.distinct(5))
+  by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
 
 lemma basic_rsimp_SEQ_property1:
   shows "rsimp_SEQ RONE r = r"
@@ -1371,9 +1374,66 @@
   using grewrites_ralts hrewrite.intros(9) apply blast
   by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
-lemma hrewrites_list:
-  shows "\<forall>r \<in> set rs. r \<leadsto>* f r \<Longrightarrow> rs \<leadsto>g* map f rs"
-  sorry
+lemma hrewrites_alts:
+  shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS  (rs1 @ [r'] @ rs2))"
+  apply(induct r r' rule: hrewrites.induct)
+  apply simp
+  using hrewrite.intros(6) by blast
+
+inductive 
+  srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
+where
+  ss1: "[] scf\<leadsto>* []"
+| ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
+
+
+lemma hrewrites_alts_cons:
+  shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')"
+
+
+  oops
+
+
+lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))"
+
+  apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
+   apply(rule rs1)
+  apply(drule_tac x = "rsa@[r']" in meta_spec)
+  apply simp
+  apply(rule hreal_trans)
+   prefer 2
+   apply(assumption)
+  apply(drule hrewrites_alts)
+  by auto
+
+
+corollary srewritescf_alt1: 
+  assumes "rs1 scf\<leadsto>* rs2"
+  shows "RALTS rs1 \<leadsto>* RALTS rs2"
+  using assms
+  by (metis append_Nil srewritescf_alt)
+
+
+
+
+lemma trivialrsimp_srewrites: 
+  "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
+
+  apply(induction rs)
+   apply simp
+   apply(rule ss1)
+  by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps)
+
+lemma hrewrites_list: 
+  shows
+" (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)"
+  apply(induct x)
+   apply(simp)+
+  by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
+(*  apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
+
+  
+
 
 
 lemma simp_hrewrites:
@@ -1401,10 +1461,38 @@
   apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
   using hreal_trans apply blast
     apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
-sledgehammer
+
+   apply (simp add: grewrites_ralts hrewrites_list)
+  by simp
+
+lemma interleave_aux1:
+  shows " RALT (RSEQ RZERO r1) r \<leadsto>*  r"
+  apply(subgoal_tac "RSEQ RZERO r1 \<leadsto>* RZERO")
+   apply (metis   append_eq_Cons_conv  hr_in_rstar hrewrite.intros(10) hrewrite.intros(7) hrewrites.simps)
+  by (simp add: hr_in_rstar hrewrite.intros(1))
+
+lemma rnullable_hrewrite:
+  shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
   sorry
 
 
+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
+
+  
+
+
 lemma inside_simp_removal:
   shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
   apply(induct r)
@@ -1415,7 +1503,7 @@
   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)
-
+  
   
   sorry
 
@@ -1458,25 +1546,10 @@
 
 lemma add0_isomorphic:
   shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r"
-  sorry
+  by (metis append.left_neutral append_Cons flts_removes0 idem_after_simp1)
 
 
-lemma distinct_append_simp:
-  shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow>
-           rsimp (rsimp_ALTs (f a # rs1)) =
-           rsimp (rsimp_ALTs (f a # rs2))"
-  apply(case_tac rs1)
-   apply simp
-   apply(case_tac rs2)
-    apply simp
-   apply simp
-   prefer 2
-   apply(case_tac list)
-    apply(case_tac rs2)
-     apply simp
-  using add0_isomorphic apply blast 
-    apply simp
-  oops
+
 
 lemma alts_closed_form: shows 
 "rsimp (rders_simp (RALTS rs) s) = 
@@ -1560,18 +1633,27 @@
 
 
 fun sflat :: "rrexp  \<Rightarrow> rrexp list " where
-  "sflat (RALT r1 r2) = sflat r1 @ [r2]"
-| "sflat (RALTS rs) = rs"
+  "sflat (RALTS (r # rs)) = sflat r @ rs"
+| "sflat (RALTS []) = []"
 | "sflat r = [r]"
 
 lemma softrewrite_flat:
   shows "r \<leadsto>o sflat r"
-  
+  oops
+
+lemma sflat_der:
+  shows "sflat r1 = sflat r2 \<Longrightarrow> sflat (rder c r1) = sflat (rder c r2)"
+  apply(case_tac r1 )
+
+
+
 
 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 seq_sflat1: