# HG changeset patch # User Chengsong # Date 1649837909 -3600 # Node ID f5b96a532c852321d2fc516454ffa2e6223bffa6 # Parent 72edbac05c59755571c5dc58a7eed6ae24421b73 starclosed diff -r 72edbac05c59 -r f5b96a532c85 thys2/BasicIdentities.thy --- a/thys2/BasicIdentities.thy Tue Apr 12 15:51:35 2022 +0100 +++ b/thys2/BasicIdentities.thy Wed Apr 13 09:18:29 2022 +0100 @@ -768,15 +768,23 @@ fun star_update :: "char \ rrexp \ char list list \ char list list" where "star_update c r [] = []" -|"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) +|"star_update c r (s # Ss) = (if (rnullable (rders r s)) then (s@[c]) # [c] # (star_update c r Ss) else (s@[c]) # (star_update c r Ss) )" + fun star_updates :: "char list \ rrexp \ char list list \ char list list" where "star_updates [] r Ss = Ss" | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" +lemma stupdates_append: shows +"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" + apply(induct s arbitrary: Ss) + apply simp + apply simp + done + lemma distinct_flts_no0: shows " rflts (map rsimp (rdistinct rs (insert RZERO rset))) = diff -r 72edbac05c59 -r f5b96a532c85 thys2/ClosedForms.thy --- a/thys2/ClosedForms.thy Tue Apr 12 15:51:35 2022 +0100 +++ b/thys2/ClosedForms.thy Wed Apr 13 09:18:29 2022 +0100 @@ -1602,16 +1602,6 @@ "s \ [] \ rders_simp (RALTS rs) s = rsimp (RALTS (map (\r. rders_simp r s) rs))" by (metis alts_closed_form comp_apply rders_simp_nonempty_simped) - - - - -lemma star_closed_form: - shows "rders_simp (RSTAR r0) (c#s) = -rsimp ( RALTS ( (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" - apply(induct s) - apply simp - sorry thm vsuf.simps @@ -1623,17 +1613,6 @@ -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 - -inductive softrewrite :: "rrexp \ rrexp list \ bool" ("_ \o _" [100, 100] 100) where - "RALTS rs \o rs" -| "r1 \o rs1 \ (RALT r1 r2) \o (rs1 @ [r2])" fun sflat_aux :: "rrexp \ rrexp list " where @@ -1808,14 +1787,7 @@ -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 vsuf_prop1: shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) @@ -1887,18 +1859,11 @@ lemma sflat_rsimpeq: - shows "sflat_aux r1 = sflat_aux r2 \ rsimp r1 = rsimp r2" - apply(cases r1 ) - apply(cases r2) - apply simp+ - apply(case_tac x5) - apply simp - apply(case_tac list) - apply simp - - - - sorry + shows "created_by_seq r1 \ sflat_aux r1 = rs \ rsimp r1 = rsimp (RALTS rs)" + apply(induct r1 arbitrary: rs rule: created_by_seq.induct) + apply simp + using rsimp_seq_equal1 apply force + by (metis head_one_more_simp rsimp.simps(2) sflat_aux.simps(1) simp_flatten) @@ -1906,13 +1871,16 @@ shows "rsimp (rders (RSEQ r1 r2) s) = rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))" apply(case_tac "s \ []") - apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = sflat_aux (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))") + apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) s)") + apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))") using sflat_rsimpeq apply blast - using seq_sfau0 apply blast + apply (simp add: seq_sfau0) + using recursively_derseq1 apply blast apply simp by (metis idem_after_simp1 rsimp.simps(1)) + 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))))))" @@ -1986,6 +1954,149 @@ apply force by presburger + +lemma star_closed_form_seq1: + shows "sflat_aux (rders (RSTAR r0) (c # s)) = + RSEQ (rders (rder c r0) s) (RSTAR r0) # + map (rders (RSTAR r0)) (vsuf s (rder c r0))" + apply simp + using seq_sfau0 by blast + +fun hflat_aux :: "rrexp \ rrexp list" where + "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2" +| "hflat_aux r = [r]" + + +fun hflat :: "rrexp \ rrexp" where + "hflat (RALT r1 r2) = RALTS ((hflat_aux r1) @ (hflat_aux r2))" +| "hflat r = r" + +inductive created_by_star :: "rrexp \ bool" where + "created_by_star (RSEQ ra (RSTAR rb))" +| "\created_by_star r1; created_by_star r2\ \ created_by_star (RALT r1 r2)" + +fun hElem :: "rrexp \ rrexp list" where + "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)" +| "hElem r = [r]" + + + + +lemma cbs_ders_cbs: + shows "created_by_star r \ created_by_star (rder c r)" + apply(induct r rule: created_by_star.induct) + apply simp + using created_by_star.intros(1) created_by_star.intros(2) apply auto[1] + by (metis (mono_tags, lifting) created_by_star.simps list.simps(8) list.simps(9) rder.simps(4)) + +lemma star_ders_cbs: + shows "created_by_star (rders (RSEQ r1 (RSTAR r2)) s)" + apply(induct s rule: rev_induct) + apply simp + apply (simp add: created_by_star.intros(1)) + apply(subst rders_append) + apply simp + using cbs_ders_cbs by auto + +lemma created_by_star_cases: + shows "created_by_star r \ \ra rb. (r = RALT ra rb \ created_by_star ra \ created_by_star rb) \ r = RSEQ ra rb " + by (meson created_by_star.cases) + + + +lemma hfau_pushin: + shows "created_by_star r \ hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))" + apply(induct r rule: created_by_star.induct) + apply simp + apply(subgoal_tac "created_by_star (rder c r1)") + prefer 2 + apply(subgoal_tac "created_by_star (rder c r2)") + using cbs_ders_cbs apply blast + using cbs_ders_cbs apply auto[1] + apply simp + done + +lemma stupdate_induct1: + shows " concat (map (hElem \ (rder x \ (\s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = + map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" + apply(induct Ss) + apply simp+ + by (simp add: rders_append) + + + +lemma stupdates_join_general: + shows "concat (map hElem (map (rder x) (map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) = + map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" + apply(induct xs arbitrary: Ss) + apply (simp) + prefer 2 + apply auto[1] + using stupdate_induct1 by blast + + + + +lemma stupdates_join: + shows "concat (map hElem (map (rder x) (map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) = + map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 [[c]])" + using stupdates_join_general by auto + + + +lemma star_hfau_induct: + shows "hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) s) = + map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])" + apply(induct s rule: rev_induct) + apply simp + apply(subst rders_append)+ + apply simp + apply(subst stupdates_append) + apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)") + prefer 2 + apply (simp add: star_ders_cbs) + apply(subst hfau_pushin) + apply simp + apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) = + concat (map hElem (map (rder x) ( map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ") + apply(simp only:) + prefer 2 + apply presburger + 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) + apply simp + apply(subst rders_append)+ + apply(case_tac "rnullable (rder c r0)") + apply simp + + sorry + + +lemma star_closed_form1: + shows "rders (RSTAR r0) (c#s) = + ( RALTS ( (map (\s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" + + + sorry + +lemma star_closed_form: + shows "rders_simp (RSTAR r0) (c#s) = +rsimp ( RALTS ( (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" + apply(induct s) + apply simp + apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) + + + sorry + + lemma simp_helps_der_pierce: shows " rsimp (rder x