diff -r feacb89b784c -r 4bf2367e6e53 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Thu Apr 07 21:38:01 2022 +0100
+++ b/thys2/ClosedForms.thy	Fri Apr 08 21:45:32 2022 +0100
@@ -1264,7 +1264,144 @@
   apply(subgoal_tac "rnullable (rsimp r1)")
    apply simp
   using rsimp_idem apply presburger
+  using der_simp_nullability by presburger
+  
 
+inductive 
+  hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+where
+  "RSEQ  RZERO r2 \<leadsto> RZERO"
+| "RSEQ  r1 RZERO \<leadsto> RZERO"
+| "RSEQ  RONE r \<leadsto>  r"
+| "r1 \<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 \<leadsto> RSEQ r2 r3"
+| "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
+| "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"
+(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
+| "RALTS  (rsa @ [AZERO] @ rsb) \<leadsto> RALTS  (rsa @ rsb)"
+| "RALTS  (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
+| "RALTS  [] \<leadsto> RZERO"
+| "RALTS  [r] \<leadsto> r"
+| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
+
+inductive 
+  hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+where 
+  rs1[intro, simp]:"r \<leadsto>* r"
+| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+
+
+lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
+  using hrewrites.intros(1) hrewrites.intros(2) by blast
+ 
+lemma hreal_trans[trans]: 
+  assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
+  shows "r1 \<leadsto>* r3"
+  using a2 a1
+  apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 
+  apply(auto)
+  done
+
+lemma  hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+  by (meson hr_in_rstar hreal_trans)
+
+lemma hrewrites_seq_context:
+  shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
+  apply(induct r1 r2 rule: hrewrites.induct)
+   apply simp
+  using hrewrite.intros(4) by blast
+
+lemma hrewrites_seq_context2:
+  shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
+  apply(induct r1 r2 rule: hrewrites.induct)
+   apply simp
+  using hrewrite.intros(5) by blast
+
+lemma hrewrites_seq_context0:
+  shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
+  apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
+  using hrewrite.intros(1) apply blast
+  by (simp add: hrewrites_seq_context)
+
+lemma hrewrites_seq_contexts:
+  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 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
+
+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 simp
+  using grewrite_ralts hreal_trans by blast
+
+
+lemma grewrites_ralts_rsimpalts:
+  shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' "
+  apply(induct rs rs' rule: grewrites.induct)
+   apply(case_tac rs)
+  using hrewrite.intros(9) apply force
+   apply(case_tac list)
+  apply simp
+  using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger
+   apply simp
+  apply(case_tac rs2)
+   apply simp
+   apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1))
+  apply(case_tac list)
+   apply(simp)
+  using distinct_grewrites_subgoal1 apply blast
+  apply simp
+  apply(case_tac rs3)
+   apply simp
+  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 simp_hrewrites:
+  shows "r1 \<leadsto>* rsimp r1"
+  apply(induct r1)
+       apply simp+
+    apply(case_tac "rsimp r11 = RONE")
+     apply simp
+     apply(subst basic_rsimp_SEQ_property1)
+  apply(subgoal_tac "RSEQ r11 r12 \<leadsto>* RSEQ RONE r12")
+  using hreal_trans hrewrite.intros(3) apply blast
+  using hrewrites_seq_context apply presburger
+    apply(case_tac "rsimp r11 = RZERO")
+     apply simp
+  using hrewrite.intros(1) hrewrites_seq_context apply blast
+    apply(case_tac "rsimp r12 = RZERO")
+     apply simp
+  apply(subst basic_rsimp_SEQ_property3)
+  apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2)
+    apply(subst basic_rsimp_SEQ_property2)
+       apply simp+
+  using hrewrites_seq_contexts apply presburger
+   apply simp
+   apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")
+  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
   sorry
 
 
@@ -1276,9 +1413,14 @@
      apply simp
   
   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
 
 
+
 lemma rders_simp_same_simpders:
   shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
   apply(induct s rule: rev_induct)
@@ -1394,17 +1536,121 @@
    apply simp
   sorry
 
+thm vsuf.simps
 
 
+
+lemma rsimp_seq_equal1:
+  shows "rsimp_SEQ (rsimp r1) (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp r1) (rsimp r2)]) {})"
+  by (metis idem_after_simp1 rsimp.simps(1))
+
+
+
+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
+
+fun sflat :: "rrexp  \<Rightarrow> rrexp list " where
+  "sflat (RALT r1 r2) = sflat r1 @ [r2]"
+| "sflat (RALTS rs) = rs"
+| "sflat r = [r]"
+
+lemma seq_sflat0:
+  shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) #
+                                       (map (rders r2) (vsuf s r1))) )"
+  
+  sorry
+
+lemma seq_sflat1:
+  shows "sflat  ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # 
+                (map (rders r2) (vsuf (s @ [c]) r1)) 
+              ) ) = sflat (rders (RSEQ r1 r2) (s @ [c]))"
+  sorry
+
+
+lemma seq_sflat:
+  shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # 
+                (map (rders r2) (vsuf (s @ [c]) r1)) 
+              ) )  = sflat ( rder x (RALTS ( (RSEQ (rders r1 s) r2) # 
+                (map (rders r2) (vsuf s r1)) 
+              ))  )"
+  sorry
+
+
+
+lemma sflat_rsimpeq:
+  shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  sorry
+
+
+
+lemma seq_closed_form_general:
+  shows "rsimp (rders (RSEQ r1 r2) s) = 
+rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
+  apply(subgoal_tac "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))")
+  using sflat_rsimpeq apply blast
+  by (simp add: seq_sflat0)
+  
+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))))))"
+  by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem)
+
+lemma add_simp_to_rest:
+  shows "rsimp (RALTS (r # rs)) = rsimp (RALTS (r # map rsimp rs))"
+  by (metis append_Nil2 grewrite.intros(2) grewrite_simpalts head_one_more_simp list.simps(9) rsimp_ALTs.simps(2) spawn_simp_rsimpalts)
+
+lemma rsimp_compose_der:
+  shows "map rsimp (map (rders r) ss) = map (\<lambda>s. rsimp (rders r s)) ss"
+  apply simp
+  done
+
+lemma rsimp_compose_der2:
+  shows "\<forall>s \<in> set ss. s \<noteq> [] \<Longrightarrow> map rsimp (map (rders r) ss) = map (\<lambda>s.  (rders_simp r s)) ss"  
+  by (simp add: rders_simp_same_simpders)
+
+lemma vsuf_nonempty:
+  shows "\<forall>s \<in> set ( vsuf s1 r). s \<noteq> []"
+  apply(induct s1 arbitrary: r)
+   apply simp
+  apply simp
+  done
+
+lemma rsimp_compose_der3:
+  shows " map rsimp (map (rders r) (vsuf s1 r')) = map (\<lambda>s. rsimp  (rders_simp r s)) (vsuf s1 r')"  
+  by (simp add: rders_simp_same_simpders rsimp_idem vsuf_nonempty)
+
+thm rders_simp_same_simpders
+
+
+
+lemma seq_closed_form_aux2:
+  shows "s \<noteq> [] \<Longrightarrow> rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = 
+         rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))))"
+  
+  by (metis add_simp_to_rest rsimp_compose_der2 vsuf_nonempty)
+  
+
 lemma seq_closed_form: shows 
 "rsimp (rders_simp (RSEQ r1 r2) s) = 
 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # 
                 (map (rders_simp r2) (vsuf s r1)) 
               )  
       )"
-  apply(induct s)
-  apply simp
-  sorry
+  apply(case_tac s )
+   apply simp  
+  apply (metis idem_after_simp1 rsimp.simps(1))
+  apply(subgoal_tac " s \<noteq> []")
+  using rders_simp_same_simpders rsimp_idem seq_closed_form_aux1 seq_closed_form_aux2 seq_closed_form_general apply presburger
+  
+  by fastforce
+  
+
+
 
 
 lemma seq_closed_form_variant: shows