# HG changeset patch # User Chengsong # Date 1649884808 -3600 # Node ID 370dae790b3032fbc0913ca2e5abd7070f76e581 # Parent 9f3d6f09b093759ab2035ad9fde25b3176bf8aae more sorrys fileld diff -r 9f3d6f09b093 -r 370dae790b30 thys2/BasicIdentities.thy --- a/thys2/BasicIdentities.thy Wed Apr 13 18:57:24 2022 +0100 +++ b/thys2/BasicIdentities.thy Wed Apr 13 22:20:08 2022 +0100 @@ -53,12 +53,24 @@ (if x \ acc then rdistinct xs acc else x # (rdistinct xs ({x} \ acc)))" +lemma rdistinct1: + assumes "a \ acc" + shows "a \ set (rdistinct rs acc)" + using assms + apply(induct rs arbitrary: acc a) + apply(auto) + done + + lemma rdistinct_does_the_job: shows "distinct (rdistinct rs s)" apply(induct rs arbitrary: s) - apply simp + apply simp apply simp - sorry + apply(auto) + by (simp add: rdistinct1) + + lemma rdistinct_concat: @@ -110,24 +122,18 @@ done -lemma rdistinct_concat_general: - shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" - sorry + + + +lemma rdistinct_set_equality1: + shows "set (rdistinct rs acc) = set rs - acc" + apply(induct rs acc rule: rdistinct.induct) + apply(auto) + done lemma rdistinct_set_equality: shows "set (rdistinct rs {}) = set rs" - sorry - -lemma distinct_once_enough: - shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" - apply(subgoal_tac "distinct (rdistinct rs {})") - apply(subgoal_tac -" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") - apply(simp only:) - using rdistinct_concat_general apply blast - apply (simp add: distinct_rdistinct_append rdistinct_set_equality) - by (simp add: rdistinct_does_the_job) - + by (simp add: rdistinct_set_equality1) fun rflts :: "rrexp list \ rrexp list" @@ -429,14 +435,97 @@ +fun + RL :: "rrexp \ string set" +where + "RL (RZERO) = {}" +| "RL (RONE) = {[]}" +| "RL (RCHAR c) = {[c]}" +| "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)" +| "RL (RALTS rs) = (\ (set (map RL rs)))" +| "RL (RSTAR r) = (RL r)\" + + +lemma RL_rnullable: + shows "rnullable r = ([] \ RL r)" + apply(induct r) + apply(auto simp add: Sequ_def) + done + +lemma RL_rder: + shows "RL (rder c r) = Der c (RL r)" + apply(induct r) + apply(auto simp add: Sequ_def Der_def) + apply (metis append_Cons) + using RL_rnullable apply blast + apply (metis append_eq_Cons_conv) + apply (metis append_Cons) + apply (metis RL_rnullable append_eq_Cons_conv) + apply (metis Star.step append_Cons) + using Star_decomp by auto + + + + +lemma RL_rsimp_RSEQ: + shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)" + apply(induct r1 r2 rule: rsimp_SEQ.induct) + apply(simp_all) + done + +lemma RL_rsimp_RALTS: + shows "RL (rsimp_ALTs rs) = (\ (set (map RL rs)))" + apply(induct rs rule: rsimp_ALTs.induct) + apply(simp_all) + done + +lemma RL_rsimp_rdistinct: + shows "(\ (set (map RL (rdistinct rs {})))) = (\ (set (map RL rs)))" + apply(auto) + apply (metis rdistinct_set_equality) + by (metis rdistinct_set_equality) + +lemma RL_rsimp_rflts: + shows "(\ (set (map RL (rflts rs)))) = (\ (set (map RL rs)))" + apply(induct rs rule: rflts.induct) + apply(simp_all) + done + +lemma RL_rsimp: + shows "RL r = RL (rsimp r)" + apply(induct r rule: rsimp.induct) + apply(auto simp add: Sequ_def RL_rsimp_RSEQ) + using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1] + by (smt (verit, del_insts) RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts UN_E image_iff list.set_map) + +lemma RL_rders: + shows "RL (rders_simp r s) = RL (rders r s)" + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + apply(simp add: rders_append rders_simp_append) + apply(subst RL_rsimp[symmetric]) + using RL_rder by force + + +lemma der_simp_nullability: + shows "rnullable r = rnullable (rsimp r)" + using RL_rnullable RL_rsimp by auto + lemma ders_simp_nullability: shows "rnullable (rders r s) = rnullable (rders_simp r s)" - sorry + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + apply(simp add: rders_append rders_simp_append) + apply(simp only: RL_rnullable) + apply(simp only: RL_rder) + apply(subst RL_rsimp[symmetric]) + apply(simp only: RL_rder) + by (simp add: RL_rders) -lemma der_simp_nullability: - shows "rnullable r = rnullable (rsimp r)" - sorry + + + lemma first_elem_seqder: @@ -459,21 +548,6 @@ -lemma seq_ders_closed_form1: - shows "\Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # -(map ( rders_simp r2 ) Ss)))" - apply(case_tac "rnullable r1") - apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = -rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))") - prefer 2 - apply (simp add: rsimp_idem) - apply(rule_tac x = "[[c]]" in exI) - apply simp - apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = -rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))") - apply blast - apply(simp add: rsimp_idem) - sorry @@ -632,10 +706,26 @@ apply simp by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30)) +lemma rsimp_good10: + shows "good1 (rsimp r)" + apply(induct r) + apply simp + + apply (simp add: good1.intros(2)) + apply simp + + apply (simp add: good1.intros(3)) + + apply (simp add: good1.intros(4)) + sledgehammer + + sorry + lemma rsimp_good1: shows "rsimp r = r1 \ good1 r1" + using rsimp_good10 by blast - sorry + lemma rsimp_no_dup: shows "rsimp r = RALTS rs \ distinct rs" @@ -740,6 +830,22 @@ +lemma rdistinct_concat_general: + shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" + + sorry + +lemma distinct_once_enough: + shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" + apply(subgoal_tac "distinct (rdistinct rs {})") + apply(subgoal_tac +" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") + apply(simp only:) + using rdistinct_concat_general apply blast + apply (simp add: distinct_rdistinct_append rdistinct_set_equality) + by (simp add: rdistinct_does_the_job) + + lemma simp_flatten: shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" apply simp diff -r 9f3d6f09b093 -r 370dae790b30 thys2/ClosedForms.thy --- 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 "\r1 \* r2; r3 \* r4\ \ RSEQ r1 r3 \* RSEQ r2 r4" by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) +lemma hrewrite_simpeq: + shows "r1 \ r2 \ 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 \* r2 \ rsimp r1 = rsimp r2" - sorry - -lemma distinct_grewrites_subgoal1: - shows " \rs1 rs2 rs3 a list. - \rs1 \g* [a]; RALTS rs1 \* a; [a] \g rs3; rs2 = [a]; list = []\ \ RALTS rs1 \* 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 \g rs' \ RALTS rs \* 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 \g* rs' \ RALTS rs \* 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 " + \rs1 \g* [a]; RALTS rs1 \* a; [a] \g rs3\ \ RALTS rs1 \* rsimp_ALTs rs3" + apply(subgoal_tac "RALTS rs1 \* 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 \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 \ r2 \ rnullable r1 = rnullable r2" - sorry + apply(induct rule: hrewrite.induct) + apply simp+ + apply blast + apply simp+ + done lemma interleave1: shows "r \ r' \ rder c r \* 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 \* r' \ rder c r \* 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) \* 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] \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