# HG changeset patch # User Chengsong # Date 1649872644 -3600 # Node ID 9f3d6f09b093759ab2035ad9fde25b3176bf8aae # Parent f5b96a532c852321d2fc516454ffa2e6223bffa6 again starClosedForms diff -r f5b96a532c85 -r 9f3d6f09b093 thys2/ClosedForms.thy --- a/thys2/ClosedForms.thy Wed Apr 13 09:18:29 2022 +0100 +++ b/thys2/ClosedForms.thy Wed Apr 13 18:57:24 2022 +0100 @@ -2065,26 +2065,152 @@ apply(subst stupdates_append[symmetric]) using stupdates_join_general by blast - - -lemma star_closed_form_seq2: - shows "RSEQ (rders (rder c r0) s) (RSTAR r0) # map (rders (RSTAR r0)) (vsuf s (rder c r0)) = - map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])" - apply(induct s rule: rev_induct) +lemma starders_hfau_also1: + shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])" + using star_hfau_induct by force + +lemma hflat_aux_grewrites: + shows "a # rs \g* hflat_aux a @ rs" + apply(induct a arbitrary: rs) + apply simp+ + apply(case_tac x) + apply simp + apply(case_tac list) + + apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq) + apply(case_tac lista) + apply simp + apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv) + apply simp + by simp + + + + +lemma cbs_hfau_rsimpeq1: + 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 + + +lemma hfau_rsimpeq2: + shows "created_by_star r \ rsimp r = rsimp ( (RALTS (hflat_aux r)))" + apply(induct r) + apply simp+ + + apply (metis rsimp_seq_equal1) + prefer 2 apply simp - apply(subst rders_append)+ - apply(case_tac "rnullable (rder c r0)") + apply(case_tac x) + apply simp + apply(case_tac "list") apply simp - sorry + apply (metis idem_after_simp1) + apply(case_tac "lista") + prefer 2 + apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) + apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") + apply simp + apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") + using hflat_aux.simps(1) apply presburger + apply simp + using cbs_hfau_rsimpeq1 by fastforce + + +lemma hfau_rsimpeq1: + shows "created_by_star r \ hflat_aux r = rs \ rsimp r = rsimp (RALTS rs)" + apply(induct r arbitrary: rs rule: created_by_star.induct ) + apply (metis created_by_seq.intros(1) hflat_aux.simps(5) sflat_aux.simps(6) sflat_rsimpeq) + apply simp + oops + + + + lemma star_closed_form1: - shows "rders (RSTAR r0) (c#s) = - ( RALTS ( (map (\s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" + shows "rsimp (rders (RSTAR r0) (c#s)) = +rsimp ( ( RALTS ( (map (\s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" + using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger + +lemma star_closed_form2: + shows "rsimp (rders_simp (RSTAR r0) (c#s)) = +rsimp ( ( RALTS ( (map (\s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" + by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem star_closed_form1) + +lemma star_closed_form3: + shows "rsimp (rders_simp (RSTAR r0) (c#s)) = (rders_simp (RSTAR r0) (c#s))" + by (metis list.distinct(1) rders_simp_same_simpders star_closed_form1 star_closed_form2) + +lemma star_closed_form4: + shows " (rders_simp (RSTAR r0) (c#s)) = +rsimp ( ( RALTS ( (map (\s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" + using star_closed_form2 star_closed_form3 by presburger + +lemma star_closed_form5: + shows " rsimp ( ( RALTS ( (map (\s1. RSEQ (rders r0 s1) (RSTAR r0) ) Ss )))) = + rsimp ( ( RALTS ( (map (\s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ))))" + by (metis (mono_tags, lifting) list.map_comp map_eq_conv o_apply rsimp.simps(2) rsimp_idem) + +lemma star_closed_form6_hrewrites: + shows " + (map (\s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ) + scf\* +(map (\s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )" + apply(induct Ss) + apply simp + apply (simp add: ss1) + by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2) + +lemma star_closed_form6: + shows " rsimp ( ( RALTS ( (map (\s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )))) = + rsimp ( ( RALTS ( (map (\s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ))))" + apply(subgoal_tac " map (\s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss scf\* + map (\s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ") + using hrewrites_simpeq srewritescf_alt1 apply fastforce + using star_closed_form6_hrewrites by blast + +lemma star_closed_form7: + shows " (rders_simp (RSTAR r0) (c#s)) = +rsimp ( ( RALTS ( (map (\s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" + using star_closed_form4 star_closed_form5 star_closed_form6 by presburger + +lemma derssimp_nonempty_list: + shows "\s \ set Ss. s \ [] \ + rsimp ( ( RALTS ( (map (\s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) Ss)))) = + rsimp ( ( RALTS ( (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) Ss)))) " - - sorry + by (metis (no_types, lifting) map_eq_conv rders_simp_same_simpders) + +lemma stupdate_nonempty: + shows "\s \ set Ss. s \ [] \ \s \ set (star_update c r Ss). s \ []" + apply(induct Ss) + apply simp + apply(case_tac "rnullable (rders r a)") + apply simp+ + done + + +lemma stupdates_nonempty: + shows "\s \ set Ss. s\ [] \ \s \ set (star_updates s r Ss). s \ []" + apply(induct s arbitrary: Ss) + apply simp + apply simp + using stupdate_nonempty by presburger + + + + +lemma star_closed_form8: + shows +"rsimp ( ( RALTS ( (map (\s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))) = + rsimp ( ( RALTS ( (map (\s1. RSEQ ( (rders_simp r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" + by (metis derssimp_nonempty_list neq_Nil_conv non_empty_list set_ConsD stupdates_nonempty) + + lemma star_closed_form: shows "rders_simp (RSTAR r0) (c#s) = @@ -2092,9 +2218,7 @@ apply(induct s) apply simp apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) - - - sorry + using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger lemma simp_helps_der_pierce: