diff -r 51af5f882350 -r b2a8610cf110 thys2/ClosedForms.thy --- a/thys2/ClosedForms.thy Sun Apr 03 22:12:27 2022 +0100 +++ b/thys2/ClosedForms.thy Mon Apr 04 23:56:40 2022 +0100 @@ -534,13 +534,31 @@ by simp -lemma grewrites_middle_distinct: - shows "RALTS rs \ set rsb \ - rsb @ - rdistinct ( rs @ rsa) - (set rsb) \g* rsb @ rdistinct rsa (set rsb)" +lemma alts_g_can_flts: + shows "RALTS rs \ set rsb \ \rs1 rs2.( rflts rsb = rs1 @ rs @ rs2)" + by (metis flts_append rflts.simps(3) split_list_last) + +lemma flts_gstar: + shows "rs \g* rflts rs" + sorry + +lemma create_nonexistent_distinct_set: + shows "a \ set rs1 \ rs1 @ (rdistinct rs (insert a rset)) \g* rs1 @ (rdistinct rs (rset))" sorry +lemma grewrites_in_distinct0: + shows "a \ set rs1 \ rs1 @ (rdistinct (a # rs) rset) \g* rs1 @ (rdistinct rs rset)" + apply(case_tac "a \ rset") + apply simp + apply simp + oops + + + + + + + lemma frewrite_rd_grewrites_aux: @@ -552,9 +570,7 @@ sorry -lemma flts_gstar: - shows "rs \g* rflts rs" - sorry + lemma list_dlist_union: shows "set rs \ set rsb \ set (rdistinct rs (set rsb))" @@ -655,35 +671,12 @@ lemma impossible_grewrite2: shows "\ ([RALTS rs] \g (RALTS rs) # a # rs)" - using grewrite_singleton by blast -thm grewrite.cases -lemma impossible_grewrite3: - shows "\ (RALTS rs # rs1 \g (RALTS rs) # a # rs1)" - oops - - -lemma grewrites_singleton: - shows "[r] \g* r # rs \ rs = []" - apply(induct "[r]" "r # rs" rule: grewrites.induct) - apply simp - - oops - -lemma grewrite_nonequal_elem: - shows "r # rs2 \g r # rs3 \ rs2 \g rs3" - oops - -lemma grewrites_nonequal_elem: - shows "r # rs2 \g* r # rs3 \ rs2 \g* rs3" - apply(induct r) - - oops -lemma : +lemma wront_sublist_grewrites: shows "rs1 @ rs2 \g* rs1 @ rs3 \ rs2 \g* rs3" apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct) apply simp @@ -695,87 +688,34 @@ -lemma grewrites_shape3_aux: - shows "rs @ (rdistinct rsa (insert (RALTS rs) rsc)) \g* rs @ rdistinct (rflts (rdistinct rsa rsc)) (set rs)" - apply(induct rsa arbitrary: rsc rs) - apply simp - apply(case_tac "a \ rsc") - apply simp - apply(case_tac "a = RALTS rs") - apply simp - apply(subgoal_tac " rdistinct (rs @ rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs) \g* - rdistinct (rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs)") - apply (metis insertI1 insert_absorb rdistinct_concat2) - apply (simp add: rdistinct_concat) - apply simp - apply(case_tac "a = RZERO") - apply (metis gmany_steps_later grewrite.intros(1) grewrite_append rflts.simps(2)) - apply(case_tac "\rs1. a = RALTS rs1") - prefer 2 +lemma concat_rdistinct_equality1: + shows "rdistinct (rs @ rsa) rset = rdistinct rs rset @ rdistinct rsa (rset \ (set rs))" + apply(induct rs arbitrary: rsa rset) apply simp - apply(subgoal_tac "rflts (a # rdistinct rsa (insert a rsc)) = a # rflts (rdistinct rsa (insert a rsc))") - apply (simp only:) - apply(case_tac "a \ set rs") - apply simp - apply(drule_tac x = "insert a rsc" in meta_spec) - apply(drule_tac x = "rs " in meta_spec) - - apply(erule exE) - apply simp - apply(subgoal_tac "RALTS rs1 # - rdistinct rsa - (insert (RALTS rs) - (insert (RALTS rs1) - rsc)) \g* rs1 @ - rdistinct rsa - (insert (RALTS rs) - (insert (RALTS rs1) - rsc)) ") - apply(subgoal_tac " rs1 @ - rdistinct rsa - (insert (RALTS rs) - (insert (RALTS rs1) - rsc)) \g* - rs1 @ - rdistinct rsa - (insert (RALTS rs) - (insert (RALTS rs1) - rsc))") - - apply(case_tac "a \ set rs") - + apply(case_tac "a \ rset") + apply simp + apply (simp add: insert_absorb) + by auto +lemma ends_removal: + shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \g* rsb @ rdistinct rs (set rsb) @ rsc" sorry +lemma grewrites_rev_append: + shows "rs1 \g* rs2 \ rs1 @ [x] \g* rs2 @ [x]" + using grewritess_concat by auto -lemma grewrites_shape3: - shows " RALTS rs \ set rsb \ - rsb @ - RALTS rs # - rdistinct rsa - (insert (RALTS rs) - (set rsb)) \g* rsb @ - rdistinct rs (set rsb) @ - rdistinct (rflts (rdistinct rsa (set rsb \ set rs))) (set rs)" - apply(subgoal_tac "rsb @ RALTS rs # rdistinct rsa (insert (RALTS rs) (set rsb)) \g* - rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb))") - prefer 2 - using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger - apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb )) \g* - rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \ set rs))") - prefer 2 - apply (metis Un_insert_left grewrite_rdistinct_aux grewrites_append) +lemma grewrites_inclusion: + shows "set rs \ set rs1 \ rs1 @ rs \g* rs1" + apply(induct rs arbitrary: rs1) + apply simp + by (meson gmany_steps_later grewrite_variant1 list.set_intros(1) set_subset_Cons subset_code(1)) - apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \ set rs)) \g* -rsb @ rs @ rdistinct (rflts (rdistinct rsa (set rsb \ set rs))) (set rs)") - prefer 2 - using grewrites_append grewrites_shape3_aux apply presburger - apply(subgoal_tac "rsb @ rs \g* rsb @ rdistinct rs (set rsb)") - apply (smt (verit, ccfv_SIG) append_eq_appendI greal_trans grewrites.simps grewritess_concat) - using gstar_rdistinct_general by blast - +lemma distinct_keeps_last: + shows "\x \ rset; x \ set xs \ \ rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" + by (simp add: concat_rdistinct_equality1) lemma grewrites_shape2: shows " RALTS rs \ set rsb \ @@ -783,12 +723,76 @@ rdistinct (rs @ rsa) (set rsb) \g* rsb @ rdistinct rs (set rsb) @ - rdistinct (rflts (rdistinct rsa (set rsb \ set rs))) (set rs)" + rdistinct rsa (set rs \ set rsb \ {RALTS rs})" + apply(subgoal_tac " rdistinct (rs @ rsa) (set rsb) = rdistinct rs (set rsb) @ rdistinct rsa (set rs \ set rsb)") + apply (simp only:) + prefer 2 + apply (simp add: Un_commute concat_rdistinct_equality1) + apply(induct rsa arbitrary: rs rsb rule: rev_induct) + apply simp + apply(case_tac "x \ set rs") + apply (simp add: distinct_removes_middle3) + apply(case_tac "x = RALTS rs") + apply simp + apply(case_tac "x \ set rsb") + apply simp + apply (simp add: concat_rdistinct_equality1) + apply (simp add: concat_rdistinct_equality1) + apply simp + apply(drule_tac x = "rs " in meta_spec) + apply(drule_tac x = rsb in meta_spec) + apply simp + apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb) \g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (insert (RALTS rs) (set rs \ set rsb))") + prefer 2 + apply (simp add: concat_rdistinct_equality1) + apply(case_tac "x \ set xs") + apply simp + apply (simp add: distinct_removes_last2) + apply(case_tac "x \ set rsb") + apply (smt (verit, ccfv_threshold) Un_iff append.right_neutral concat_rdistinct_equality1 insert_is_Un rdistinct.simps(2)) + apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (set rs \ set rsb) = rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb) @ [x]") + apply(simp only:) + apply(case_tac "x = RALTS rs") + apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb) @ [x] \g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb) @ rs") + apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb) @ rs \g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb) ") + apply (smt (verit, ccfv_SIG) Un_insert_left append.right_neutral concat_rdistinct_equality1 greal_trans insert_iff rdistinct.simps(2)) + apply(subgoal_tac "set rs \ set ( rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \ set rsb))") + apply (metis append.assoc grewrites_inclusion) + apply (metis Un_upper1 append.assoc dual_order.trans list_dlist_union set_append) + apply (metis append_Nil2 gr_in_rstar grewrite.intros(2) grewrite_append) + apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (insert (RALTS rs) (set rs \ set rsb)) = rsb @ rdistinct rs (set rsb) @ rdistinct (xs) (insert (RALTS rs) (set rs \ set rsb)) @ [x]") + apply(simp only:) + apply (metis append.assoc grewrites_rev_append) + apply (simp add: insert_absorb) + apply (simp add: distinct_keeps_last)+ + done - (* by (smt (z3) append.assoc distinct_3list flts_gstar greal_trans grewrites_append rdistinct_concat_general same_append_eq set_append) -*) - sorry +lemma rdistinct_add_acc: + shows "rset2 \ set rsb \ rsb @ rdistinct rs rset \g* rsb @ rdistinct rs (rset \ rset2)" + apply(induct rs arbitrary: rsb rset rset2) + apply simp + apply (case_tac "a \ rset") + apply simp + apply(case_tac "a \ rset2") + apply simp + apply (meson create_nonexistent_distinct_set gr_in_rstar greal_trans grewrite_variant1 in_mono) + apply simp + apply(drule_tac x = "rsb @ [a]" in meta_spec) + by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1) + +lemma frewrite_fun1: + shows " RALTS rs \ set rsb \ + rsb @ rdistinct rsa (set rsb) \g* rflts rsb @ rdistinct rsa (set rsb \ set rs)" + apply(subgoal_tac "rsb @ rdistinct rsa (set rsb) \g* rflts rsb @ rdistinct rsa (set rsb)") + apply(subgoal_tac " set rs \ set (rflts rsb)") + prefer 2 + using spilled_alts_contained apply blast + apply(subgoal_tac "rflts rsb @ rdistinct rsa (set rsb) \g* rflts rsb @ rdistinct rsa (set rsb \ set rs)") + using greal_trans apply blast + using rdistinct_add_acc apply presburger + using flts_gstar grewritess_concat by auto + @@ -813,24 +817,21 @@ apply simp apply(case_tac "RALTS rs \ set rsb") apply simp - apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb)" in exI) + apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb \ set rs)" in exI) apply(rule conjI) - apply (simp add: flts_gstar grewritess_concat) - apply (meson flts_gstar greal_trans grewrites.intros(1) grewrites_middle_distinct grewritess_concat) + using frewrite_fun1 apply force + apply (metis frewrite_fun1 rdistinct_concat sup_ge2) apply(simp) apply(rule_tac x = -"rsb @ (rdistinct rs (set rsb)) @ - (rdistinct (rflts (rdistinct rsa ( (set rsb \ set rs)) ) ) (set rs))" in exI) + "rsb @ + rdistinct rs (set rsb) @ + rdistinct rsa (set rs \ set rsb \ {RALTS rs})" in exI) apply(rule conjI) prefer 2 using grewrites_shape2 apply force - using grewrites_shape3 by auto - + by (metis Un_insert_left frewrite_rd_grewrites_aux inf_sup_aci(5) insert_is_Un rdistinct.simps(2)) -lemma frewrite_simprd: - shows "rs1 \f rs2 \ rsimp (RALTS rs1) = rsimp (RALTS rs2)" - by (meson frewrite_simpeq) lemma frewrites_rd_grewrites: @@ -838,16 +839,16 @@ rsimp (RALTS rs1) = rsimp (RALTS rs2)" apply(induct rs1 rs2 rule: frewrites.induct) apply simp - using frewrite_simprd by presburger - - - + using frewrite_simpeq by presburger lemma frewrite_simpeq2: shows "rs1 \f rs2 \ rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" apply(subgoal_tac "\ rs3. (rdistinct rs1 {} \g* rs3) \ (rdistinct rs2 {} \g* rs3)") using grewrites_equal_rsimp apply fastforce - using frewrite_rd_grewrites by presburger + by (metis append_self_conv2 frewrite_rd_grewrites list.set(1)) + + + (*a more refined notion of \* is needed, this lemma fails when rs1 contains some RALTS rs where elements @@ -902,10 +903,7 @@ sorry *) -lemma "rsimp (rsimp_ALTs (RZERO # rdistinct (map (rder x) (rflts rs)) {RZERO})) = - rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) " - sorry