diff -r 15d182ffbc76 -r aecf1ddf3541 thys3/ClosedForms.thy --- a/thys3/ClosedForms.thy Sun Jun 26 22:22:47 2022 +0100 +++ b/thys3/ClosedForms.thy Tue Jun 28 21:07:42 2022 +0100 @@ -1,20 +1,8 @@ theory ClosedForms - imports "BasicIdentities" + imports "HarderProps" begin -lemma flts_middle0: - shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" - apply(induct rsa) - apply simp - by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) - - - -lemma simp_flatten_aux0: - shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))" - by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts) - inductive hrewrite:: "rrexp \ rrexp \ bool" ("_ h\ _" [99, 99] 99) @@ -68,44 +56,8 @@ by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) -lemma simp_removes_duplicate1: - shows " a \ set rsa \ rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" -and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" - apply(induct rsa arbitrary: a1) - apply simp - apply simp - prefer 2 - apply(case_tac "a = aa") - apply simp - apply simp - apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) - apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) - by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) - -lemma simp_removes_duplicate2: - shows "a \ set rsa \ rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" - apply(induct rsb arbitrary: rsa) - apply simp - using distinct_removes_duplicate_flts apply auto[1] - by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) -lemma simp_removes_duplicate3: - shows "a \ set rsa \ rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" - using simp_removes_duplicate2 by auto -(* -lemma distinct_removes_middle4: - shows "a \ set rsa \ rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset" - using distinct_removes_middle(1) by fastforce -*) - -(* -lemma distinct_removes_middle_list: - shows "\a \ set x. a \ set rsa \ rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset" - apply(induct x) - apply simp - by (simp add: distinct_removes_middle3) -*) inductive frewrite:: "rrexp list \ rrexp list \ bool" ("_ \f _" [10, 10] 10) where @@ -260,11 +212,6 @@ using grewrites_append apply blast by (meson greal_trans grewrites.simps grewrites_concat) -fun alt_set:: "rrexp \ rrexp set" - where - "alt_set (RALTS rs) = set rs \ \ (alt_set ` (set rs))" -| "alt_set r = {r}" - lemma grewrite_cases_middle: shows "rs1 \g rs2 \ @@ -279,211 +226,6 @@ by blast -lemma good_singleton: - shows "good a \ nonalt a \ rflts [a] = [a]" - using good.simps(1) k0b by blast - - - - - - - - -lemma distinct_early_app1: - shows "rset1 \ rset \ rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" - apply(induct rs arbitrary: rset rset1) - apply simp - apply simp - apply(case_tac "a \ rset1") - apply simp - apply(case_tac "a \ rset") - apply simp+ - - apply blast - apply(case_tac "a \ rset1") - apply simp+ - apply(case_tac "a \ rset") - apply simp - apply (metis insert_subsetI) - apply simp - by (meson insert_mono) - - -lemma distinct_early_app: - shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset" - apply(induct rsb) - apply simp - using distinct_early_app1 apply blast - by (metis distinct_early_app1 distinct_once_enough empty_subsetI) - - -lemma distinct_eq_interesting1: - shows "a \ rset \ rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset" - apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset") - apply(simp only:) - using distinct_early_app apply blast - by (metis append_Cons distinct_early_app rdistinct.simps(2)) - - - -lemma good_flatten_aux_aux1: - shows "\ size rs \2; -\r \ set rs. good r \ r \ RZERO \ nonalt r; \r \ set rsb. good r \ r \ RZERO \ nonalt r \ - \ rdistinct (rs @ rsb) rset = - rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" - apply(induct rs arbitrary: rset) - apply simp - apply(case_tac "a \ rset") - apply simp - apply(case_tac "rdistinct rs {a}") - apply simp - apply(subst good_singleton) - apply force - apply simp - apply (meson all_that_same_elem) - apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ") - prefer 2 - using k0a rsimp_ALTs.simps(3) apply presburger - apply(simp only:) - apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ") - apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2)) - apply (meson distinct_eq_interesting1) - apply simp - apply(case_tac "rdistinct rs {a}") - prefer 2 - apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})") - apply(simp only:) - apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) = - rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset") - apply simp - apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2)) - using rsimp_ALTs.simps(3) apply presburger - by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left) - - - - - -lemma good_flatten_aux_aux: - shows "\\a aa lista list. rs = a # list \ list = aa # lista; -\r \ set rs. good r \ r \ RZERO \ nonalt r; \r \ set rsb. good r \ r \ RZERO \ nonalt r \ - \ rdistinct (rs @ rsb) rset = - rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" - apply(erule exE)+ - apply(subgoal_tac "size rs \ 2") - apply (metis good_flatten_aux_aux1) - by (simp add: Suc_leI length_Cons less_add_Suc1) - - - -lemma good_flatten_aux: - shows " \\r\set rs. good r \ r = RZERO; \r\set rsa . good r \ r = RZERO; - \r\set rsb. good r \ r = RZERO; - rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); - rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = - rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); - map rsimp rsa = rsa; - map rsimp rsb = rsb; - map rsimp rs = rs; - rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = - rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); - rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = - rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\ - \ rdistinct (rflts rs @ rflts rsb) rset = - rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset" - apply simp - apply(case_tac "rflts rs ") - apply simp - apply(case_tac "list") - apply simp - apply(case_tac "a \ rset") - apply simp - apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2)) - apply simp - apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) - apply(subgoal_tac "\r \ set (rflts rs). good r \ r \ RZERO \ nonalt r") - prefer 2 - apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1) - apply(subgoal_tac "\r \ set (rflts rsb). good r \ r \ RZERO \ nonalt r") - prefer 2 - apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1) - by (smt (verit, ccfv_threshold) good_flatten_aux_aux) - - - - -lemma good_flatten_middle: - shows "\\r \ set rs. good r \ r = RZERO; \r \ set rsa. good r \ r = RZERO; \r \ set rsb. good r \ r = RZERO\ \ -rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" - apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ -map rsimp rs @ map rsimp rsb)) {})") - prefer 2 - apply simp - apply(simp only:) - apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ -[rsimp (RALTS rs)] @ map rsimp rsb)) {})") - prefer 2 - apply simp - apply(simp only:) - apply(subgoal_tac "map rsimp rsa = rsa") - prefer 2 - apply (metis map_idI rsimp.simps(3) test) - apply(simp only:) - apply(subgoal_tac "map rsimp rsb = rsb") - prefer 2 - apply (metis map_idI rsimp.simps(3) test) - apply(simp only:) - apply(subst flts_append)+ - apply(subgoal_tac "map rsimp rs = rs") - apply(simp only:) - prefer 2 - apply (metis map_idI rsimp.simps(3) test) - apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = -rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") - apply(simp only:) - prefer 2 - using rdistinct_concat_general apply blast - apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = -rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") - apply(simp only:) - prefer 2 - using rdistinct_concat_general apply blast - apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = - rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") - apply presburger - using good_flatten_aux by blast - - - -lemma simp_flatten3: - shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" - apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = - rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") - prefer 2 - apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) - apply (simp only:) - apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = -rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))") - prefer 2 - apply (metis map_append simp_flatten_aux0) - apply(simp only:) - apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = - rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") - - apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) - apply(subgoal_tac "\r \ set (map rsimp rsa). good r \ r = RZERO") - apply(subgoal_tac "\r \ set (map rsimp rs). good r \ r = RZERO") - apply(subgoal_tac "\r \ set (map rsimp rsb). good r \ r = RZERO") - - using good_flatten_middle apply presburger - - apply (simp add: good1) - apply (simp add: good1) - apply (simp add: good1) - - done - @@ -1286,6 +1028,16 @@ by fastforce +fun vsuf :: "char list \ rrexp \ char list list" where +"vsuf [] _ = []" +|"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] + else (vsuf cs (rder c r1)) + ) " + + + + + lemma vsuf_prop1: shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) then [x] # (map (\s. s @ [x]) (vsuf xs r) ) @@ -1533,6 +1285,30 @@ (*AALTS [a\x . b.c, b\x .c, c \x]*) (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) +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 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 stupdate_induct1: shows " concat (map (hflat_aux \ (rder x \ (\s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"