# HG changeset patch
# User Chengsong
# Date 1649450732 -3600
# Node ID 4bf2367e6e530b491a6469c72c81be0364b19c62
# Parent feacb89b784ca71e76a4ca9b4ed62c6532ee50f8
closedformseq
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