# HG changeset patch # User Chengsong # Date 1650061891 -3600 # Node ID 64183736777a5f25371076c27ff4009a122aef2d # Parent 2b5b3f83e2b60e3767d6becfa2a91c5ac3fa9fdd almost there diff -r 2b5b3f83e2b6 -r 64183736777a thys2/ClosedForms.thy --- a/thys2/ClosedForms.thy Fri Apr 15 19:35:29 2022 +0100 +++ b/thys2/ClosedForms.thy Fri Apr 15 23:31:31 2022 +0100 @@ -8,13 +8,21 @@ apply simp by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) -lemma simp_flatten3: - shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" - apply(induct rsa) + + +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) + + + + + + + + + - using simp_flatten apply force - - sorry inductive hrewrite:: "rrexp \ rrexp \ bool" ("_ \ _" [99, 99] 99) @@ -415,6 +423,216 @@ by blast +lemma good_singleton: + shows "good a \ nonalt a \ rflts [a] = [a]" + using good.simps(1) k0b by blast + + + + + + + +lemma all_that_same_elem: + shows "\ a \ rset; rdistinct rs {a} = []\ + \ rdistinct (rs @ rsb) rset = rdistinct rsb rset" + apply(induct rs) + apply simp + apply(subgoal_tac "aa = a") + apply simp + by (metis empty_iff insert_iff list.discI rdistinct.simps(2)) + +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\set rsa. good r; \r\set rsb. good r; + 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_Cons append_Nil flts_append list.set(1) list.simps(15) nonalt.simps(1) nonalt0_flts_keeps nonalt_flts_rd qqq1 rdistinct.simps(2) rdistinct_set_equality singleton_iff) + 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 flts3 nn1b nn1c qqq1 test) + apply(subgoal_tac "\r \ set (rflts rsb). good r \ r \ RZERO \ nonalt r") + prefer 2 + apply (metis flts3 nn1b nn1c qqq1 test) + by (smt (verit, ccfv_threshold) good_flatten_aux_aux) + + + + +lemma good_flatten_middle: + shows "\\r \ set rs. good r; \r \ set rsa. good r; \r \ set rsb. good r\ \ +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 (simp add: map_idI test) + apply(simp only:) + apply(subgoal_tac "map rsimp rsb = rsb") + prefer 2 + apply (meson map_idI test) + apply(simp only:) + apply(subst k00)+ + apply(subgoal_tac "map rsimp rs = rs") + apply(simp only:) + prefer 2 + apply (meson map_idI 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") + apply(subgoal_tac "\r \ set (map rsimp rs). good r") + apply(subgoal_tac "\r \ set (map rsimp rsb). good r") + + using good_flatten_middle apply presburger + + + sorry + + + + + lemma grewrite_equal_rsimp: shows "rs1 \g rs2 \ rsimp (RALTS rs1) = rsimp (RALTS rs2)" apply(frule grewrite_cases_middle)