structure MS = struct val thy = the_context () end ; val _ = use_legacy_bindings MS.thy ; val msuth = ([Rep_multiset, Rep_multiset] MRS union_preserves_multiset RS Abs_multiset_inverse) ; val msth = (Rep_multiset RS diff_preserves_multiset RS Abs_multiset_inverse) ; val ms_delete_le' = order_refl RS transfer MS.thy ms_delete_le ; AddIffs [ms_delete_le'] ; val _ = bind_thm ("in_ms_mono", [single_le, single_le RS iffD2 RS transfer MS.thy order_trans] MRS iffD1) ; val _ = bind_thm ("minsI1_eq", [minsI1, order_eq_refl] MRS in_ms_mono) ; val _ = bind_thm ("in_ms_delete", ms_delete_le' RSN (2, in_ms_mono)) ; val _ = bind_thm ("in_set_of_ms_delete", mk_mono' (ms_delete_le' RS set_of_mono)) ; val _ = bind_thm ("single_add_diff_exE", single_le RS iffD2 RS transfer MS.thy le_add_diff_exE) ; val mmth = [mins_def RS def_imp_eq, le_add_diff_iff RS iffD2] MRS transfer MS.thy trans RS sym ; val _ = bind_thm ("mins_minus", single_le RS iffD2 RS mmth) ; val () = qed_goal_spec_mp "mins_ex" MS.thy "A :# M --> (EX N. M = mins A N)" (fn _ => [ (rtac impI 1), (dtac mins_minus 1), etac exI 1 ]) ; val () = qed_goalw "mins_minus_eq" MS.thy [mins_def] "mins A M - {#A#} = M" (fn _ => [ (rtac pm0_class.pm0_plus_minus 1) ]) ; val _ = qed_goal "size_times" MS.thy "size (times n M :: 'a multiset) = size M * n" (indAu "n") ; val _ = qed_goal "count_times_single" MS.thy "count (times n {#A#}) a = (if A = a then n else 0)" (indAu "n") ; val _ = qed_goal "count_same_times_single" MS.thy "count (times n {#A#}) A = n" (indAu "n") ; Addsimps [count_same_times_single] ; val _ = qed_goalw "times_le_iff" MS.thy [ms_le_def] "(times n {#A#} <= M) = (count M A >= n)" (fn _ => [ Safe_tac, (etac allE 1), (etac xt6 1), (ALLGOALS (force_tac (cesimps [count_times_single]))) ]) ; val _ = qed_goal "times_eq_iff" MS.thy "(times n {#A#} = 0) = (n = 0)" (indAu "n") ; val _ = qed_goal "map_times" MS.thy "mset_map f (times n M :: 'a multiset) = times n (mset_map f M)" (fn _ => [ (induct_tac "n" 1), (ALLGOALS (clarsimp_tac (cesimps [mset_map_union]))) ]) ; val _ = qed_goal "delete_times" MS.thy "ms_delete S (times n M :: 'a multiset) = times n (ms_delete S M)" (fn _ => [ (induct_tac "n" 1), (ALLGOALS (clarsimp_tac (cesimps [ms_delete_sum]))) ]) ; val _ = qed_goal "filter_times" MS.thy "ms_filter P (times n M :: 'a multiset) = times n (ms_filter P M)" (fn _ => [ (induct_tac "n" 1), (ALLGOALS (clarsimp_tac (cesimps [ms_filter_sum]))) ]) ; val _ = qed_goal "ms_in_times" MS.thy "x :# times n A = (0 < n & x :# A)" (fn _ => [ (induct_tac "n" 1), ALLGOALS Force_tac ]) ; val _ = qed_goal_spec_mp "single_eq_times" MS.thy "({#A#} = times n {#B#}) = (n = 1 & A = B)" (fn _ => [ (induct_tac "n" 1), Simp_tac 1, (force_tac (claset (), esimps [single_is_union, times_eq_iff, Mempty_eq_0] delsimps [Zero_multiset_def]) 1) ]) ; val _ = qed_goalw "ms_meet_pg" MS.thy [meta_eq_def, pg_meet_def, ms_meet_def, diff_def] "ms_meet x y == pg_meet x y" (fn _ => [ cong_tac 1, (rtac ext 1), (simp_tac (esimps [meet_count_def, msth, count_def]) 1), (rtac nat_min_alt 1) ]) ; val _ = qed_goalw "ms_join_pg" MS.thy [meta_eq_def, pg_join_def, ms_join_def, diff_def, union_def] "ms_join x y == pg_join x y" (fn _ => [ cong_tac 1, (rtac ext 1), (simp_tac (esimps [join_count_def, msth, count_def]) 1), (rtac nat_max_alt 1) ]) ; val ms_meet_alt = [pg_meet_alt, symmetric ms_meet_pg] MRS transitive_thm ; val ms_join_alt = [pg_join_alt, symmetric ms_join_pg] MRS transitive_thm ; val count_meet = fold_rule [ms_meet_alt] (transfer MS.thy count_ms_meet) ; val count_join = fold_rule [ms_join_alt] (transfer MS.thy count_ms_join) ; val _ = qed_goalw "ms_inf" MS.thy [ms_meet_pg] "is_inf x y (ms_meet x y)" fn_at; val _ = qed_goalw "ms_sup" MS.thy [ms_join_pg] "is_sup x y (ms_join x y)" fn_at; AddIffs [ms_inf, ms_sup] ; val _ = bind_thms ("ms_meet_join_0", [[ms_meet_pg, ms_join_pg], map mk_eq (msc pg_meet_join_0)] MRL [transitive_thm]) ; val [pg_meet_ms, pg_join_ms] = [ms_meet_pg, ms_join_pg] RL [def_imp_eq RS sym] ; val _ = bind_thm ("ms_meet_commute", [pg_meet_commute, pg_meet_ms, pg_meet_ms] MRS box_equals) ; val _ = bind_thm ("ms_join_commute", [pg_join_commute, pg_join_ms, pg_join_ms] MRS box_equals) ; (* previously val ms_meet_alt = mk_eq (transfer MS.thy ms_inf RS meet_equality) ; val ms_join_alt = mk_eq (transfer MS.thy ms_sup RS join_equality) ; val ms_meet_pg = [symmetric ms_meet_alt, pg_meet_alt] MRS transitive_thm ; val ms_join_pg = [symmetric ms_join_alt, pg_join_alt] MRS transitive_thm ; *) val _ = qed_goal_spec_mp "mset_map_mono" MS.thy "A <= B --> mset_map f A <= mset_map f B" (fn _ => [ (rtac impI 1), (dtac le_add_diff_ex 1), Clarify_tac 1, (simp_tac (esimps [mset_map_union]) 1) ]) ; val _ = qed_goal_spec_mp "mset_map_diff_le" MS.thy "B <= A --> mset_map f (A - B) = mset_map f A - mset_map f B" (fn _ => [ (rtac impI 1), (ftac (le_add_diff_eq RS sym) 1), (dres_inst_tac [("f", "mset_map f")] arg_cong 1), (asm_simp_tac HOL_ss 1), (simp_tac (esimps [mset_map_union]) 1) ]) ; val _ = qed_goal_spec_mp "mset_map_diff_inj" MS.thy "inj f --> mset_map f (A - B) = mset_map f A - mset_map f B" (fn _ => [ (rtac impI 1), (rtac ms_eqI 1), (case_tac "x : range f" 1), (clarsimp_tac (cesimps [count_mset_map_inj]) 1), (clarsimp_tac (cesimps [count_mset_map_notin]) 1) ]) ; val _ = qed_goalw_spec_mp "mset_map_le_inj" MS.thy [mk_eq (diff_0_le RS sym)] "inj f --> mset_map f A <= mset_map f B --> A <= B" (fn _ => [ (clarsimp_tac (cesimps [mset_map_diff_inj RS sym]) 1), rewtac Zero_multiset_def, (etac (mset_map_empty_conv RS iffD1) 1) ]) ; (* consequence of multisets being disjoint *) val _ = qed_goalw "ms_disj_minus" MS.thy [ms_meet_pg] "(ms_meet c ic = 0) = (c - ic = c)" (fn _ => [ (rtac pg_disj_minus 1) ]) ; val _ = bind_thm ("ms_disj_le_add", ms_disj_minus RS iffD1 RS disj_le_add) ; val _ = qed_goal "ms_meet_singleton" MS.thy "ms_meet {#x#} M = (if x :# M then {#x#} else 0)" (fn _ => [ (rtac (count_inject RS iffD1) 1), (simp_tac (esimps [count_ms_meet]) 1), Safe_tac, (ALLGOALS (rtac ext)), (ALLGOALS (clarsimp_tac (cesimps [meet_count_def]))), ALLGOALS arith_tac ]) ; val _ = qed_goal "ms_meet_singleton_0" MS.thy "(ms_meet {#x#} M = 0) = (count M x = 0)" (fn _ => [ (simp_tac (esimps [ms_meet_singleton]) 1) ]) ; val _ = qed_goal "ms_meet_singletons" MS.thy "ms_meet {#x#} {#xa#} = (if x = xa then {#x#} else 0)" (fn _ => [ (simp_tac (esimps [ms_meet_singleton]) 1) ]) ; val ms_meet_singleton' = [ms_meet_commute, ms_meet_singleton] MRS trans ; val () = qed_goalw "subset_minsI" MS.thy [mins_def] "B <= mins a B" fn_at ; Delsimps [Zero_multiset_def] ; (* better to use results for 0 *) val () = qed_goal_spec_mp "less_size_less" MS.thy "M < N --> size M < size (N :: 'a multiset)" (fn _ => [ (rtac impI 1), (ftac order_less_imp_le 1), (dtac le_add_diff_eq 1), (dres_inst_tac [("f", "size")] arg_cong 1), (dtac sym 1), (asm_full_simp_tac (esimps [neq0_conv RS sym]) 1), (rtac notI 1), (etac less_diff_ZE 1), (simp_tac (esimps [Zero_multiset_def]) 1)]) ; val () = qed_goal_spec_mp "le_size_le" MS.thy "M <= N --> size M <= size (N :: 'a multiset)" (fn _ => [ (rtac impI 1), (dtac order_le_imp_less_or_eq 1), Safe_tac, (dtac less_size_less 1), Asm_simp_tac 1]) ; val () = qed_goal_spec_mp "ms_size_diff" MS.thy "A <= B --> size (B - A) = size B - size (A :: 'a multiset)" (fn _ => [ (rtac impI 1), (dtac le_add_diff_eq 1), (dtac sym 1), (dres_inst_tac [("f", "size")] arg_cong 1), (asm_simp_tac HOL_ss 1), Simp_tac 1]) ; Addsimps [ms_size_diff, le_size_le, less_size_less] ; val () = qed_goalw "ms_atomic_def" MS.thy [atomic_def] "atomic (M :: 'a multiset) = (size M <= 1)" (fn _ => [ (res_inst_tac [("M", "M")] multiset_induct 1), (auto_tac (cds [less_size_less], esimps [symmetric Zero_multiset_def])), (ALLGOALS (EVERY' [ etac allE, (etac mp), (rtac (ms_less_le RS iffD2)), (rtac (le_plus1 RS conjI)), (rtac notI), (dres_inst_tac [("f", "%x. x - M")] arg_cong), Full_simp_tac ])) ]) ; val ms_atom_disj_or_le = fold_rule [ms_meet_pg] (ms_atomic_def RS iffD2 RS atomicD) ; val ms_atom_disj_or_le' = rewrite_rule [One_nat_def] ms_atom_disj_or_le ; val make_pos_rule_c = disj_commute RS iffD1 RS make_pos_rule' ; val ms_atom_disj_or_le_c = ms_atom_disj_or_le RS make_pos_rule_c ; (* val mins_def' = comm_all mins_def ; *) val _ = bind_thm ("mins_assoc_alt", fcomm_all add_commute mins_assoc) ; val _ = bind_thm ("single_is_union'", [eq_commute, single_is_union] MRS trans) ; val _ = qed_goalw "atomic_single" MS.thy [mk_eq ms_atomic_def] "atomic {#A#}" fn_at ; AddIffs [atomic_single] ; val _ = bind_thm ("single_atomicD", rewrite_rule [mk_eq single_le] (atomic_single RS atomicD)) ; val _ = qed_goal_spec_mp "mset_map_split" MS.thy "ALL Y Z. mset_map f X' = Y + Z --> (EX Y' Z'. X' = Y' + Z' & \ \ mset_map f Y' = Y & mset_map f Z' = Z)" (fn _ => [ (res_inst_tac [("M", "X'")] multiset_induct 1), (Simp_tac 1), (clarsimp_tac (cesimps [mset_map_union]) 1), (ftac ([sym, le_plus2] MRS xt3) 1), (dtac sum_diff 1), (etac (atomic_single RS atomic_le_sumD RS disjE) 1), (fatac (le_pm_assoc RS trans) 1 2), (fatac (le_pm_assocc RS trans) 1 1), (ALLGOALS (EVERY' [(etac allE2), (etac impE), (etac sym)])), Safe_tac, (REPEAT_FIRST (rtac exI)), Safe_tac, (TRYALL (rtac refl)), (safe_asm_full_simp_tac (esimps [] addsimprocs pmgsps) 3), (safe_asm_full_simp_tac (esimps [] addsimprocs pmgsps) 1), (TRYALL (rtac refl)), (ALLGOALS (asm_simp_tac (esimps [mset_map_union]))) ]) ; val _ = qed_goal_spec_mp "le_mset_map" MS.thy "Y <= mset_map f X' --> (EX Y'. Y' <= X' & Y = mset_map f Y')" (fn _ => [ Clarify_tac 1, (dtac le_add_diff_ex 1), Clarify_tac 1, (ftac (sym RS mset_map_split) 1), Clarify_tac 1, rtac exI 1, rtac conjI 1, rtac refl 2, Simp_tac 1 ]) ; val _ = qed_goal_spec_mp "in_mset_map" MS.thy "y :# mset_map f X --> (EX x. x :# X & y = f x)" (fn _ => [ (fast_tac (cds [ (single_le RS iffD2 RS le_mset_map), (sym RS mset_map_is_single), (single_le RS iffD1)]) 1) ]) ; val in_mset_mapE = tacthm Safe_tac (in_mset_map RS exE) ; Delsimps union_ac ; (* WHY IS THIS HERE? DO WE WANT IT GENERALLY? see note in Multiset_no_le.ML *) val _ = qed_goal_spec_mp "subset_single_diff" MS.thy "M <= {#B#} --> set_of M - {B} = {}" (fn _ => [ rtac impI 1, (dtac ([Diff_eq_empty_iff, set_of_mono] MRS iffD2) 1), (asm_full_simp_tac (esimps [] delsimps [Diff_eq_empty_iff]) 1) ]) ; val _ = qed_goal_spec_mp "ms_map_ex_list" MS.thy "ALL abcm. mset_map f abcm = ms_of_list xs --> \ \ (EX abcl. map f abcl = xs & ms_of_list abcl = abcm)" (fn _ => [ (induct_tac "xs" 1), (ALLGOALS (clarsimp_tac (cesimps [mset_map_empty_conv, mins_def]))), (dtac mset_map_split 1), Clarify_tac 1, (etac allE 1), mp_tac 1, Clarify_tac 1, (dtac mset_map_is_single 1), Clarify_tac 1, (REPEAT_FIRST (resolve_tac [exI, conjI, refl])), (simp_tac (esimps [mins_def]) 1) ]) ; val tsl2 = transfer MS.thy single_le RS iffD2 ; val thY = reop rev (tsl2 RS le_pm_assoc RS trans) ; val thX = reop rev (tsl2 RS le_pm_assocc RS trans) ; val _ = qed_goal_spec_mp "mins_sum_lem" MS.thy "set_of U <= S --> X + Y = mins a U --> \ \ (EX V W. set_of V <= S & set_of W <= S & \ \ (X = V & Y = mins a W | X = mins a W & Y = V))" (fn _ => [ Clarify_tac 1, (ftac (sym RS minsI1_eq) 1), rewtac mins_def, (dtac (sym RS sum_diffc) 1), (dtac (ms_atomic RS iffD1) 1), etac disjE 1, (datac thY 1 2), (datac thX 1 1), (ALLGOALS Clarsimp_tac), (REPEAT_SOME (resolve_tac [exI, conjI])), (rtac disjI1 6), (rtac disjI2 3), (TRYALL (rtac conjI THEN_ALL_NEW (etac (rewrite_rule [mins_def] mins_minus) ORELSE' rtac refl))), (TRYALL atac) ]) ; val _ = bind_thm ("mins_sum_lem_alt", simplify init_ss (subset_UNIV RS mins_sum_lem)) ; val _ = qed_goal_spec_mp "mins_eq_sum" MS.thy "mins a U = X + Y --> \ \ (EX W. (U = X + W & Y = mins a W | X = mins a W & U = W + Y))" (fn _ => [ Clarify_tac 1, (ftac (sym RS mins_sum_lem_alt) 1), Safe_tac, (TRYALL (EVERY' [ rtac exI, resolve_tac [disjI1, disjI2], resolve_tac [refl RS conjI, refl RSN (2, conjI)], (clarsimp_tac (cesimps [mins_assoc, mins_assoc_alt, mins_eq_eq])) ])) ]); val mins_eq_sumE = tacthm Safe_tac (mins_eq_sum RS exE) ; val sumtacs = [ (etac allE2), mp_tac, Clarify_tac, (((REPEAT o resolve_tac [exI, conjI, refl]) THEN_ALL_NEW simp_tac (esimps [mins_eqE, eq_minsE]) THEN_ALL_NEW Fast_tac)) ] ; val _ = qed_goal_spec_mp "ms_of_sum" MS.thy "ALL C D. ms_of_list xs = C + D --> (EX xbs. map fst xbs = xs & \ \ ms_of_list (map fst (filter snd xbs)) = C & \ \ ms_of_list (map fst (filter (Not o snd) xbs)) = D)" (fn _ => [ (induct_tac "xs" 1), ALLGOALS Clarsimp_tac, (etac mins_eq_sumE 1), (EVERY' sumtacs 1), (EVERY' sumtacs 1) ]) ; val add_lem = prove_goal MS.thy "t + {#x#} + m = {#x#} + (t + m)" (fn _ => [ (simp_tac (esimps [] addsimprocs pmgsps) 1) ]) ; val add_lem_tss = prove_goal MS.thy "times (Suc (Suc n)) {#a#} + M = {#a#} + (times (Suc n) {#a#} + M)" (fn _ => [ (simp_tac (esimps [] addsimprocs pmgsps) 1) ]) ; (* extension of add_eq_conv_ex' *) val _ = qed_goal_spec_mp "times_single_add1" MS.thy "ALL M N. (times (Suc n) {#a#} + M = {#b#} + N) --> \ \ (times n {#a#} + M = N & a = b | \ \ (EX K. M = {#b#} + K & N = times (Suc n) {#a#} + K))" (fn _ => [ (induct_tac "n" 1), (strip_tac 1), Full_simp_tac 1, (etac (add_eq_conv_ex' RS iffD1) 1), (strip_tac 1), (dtac (add_lem_tss RS sym RS trans) 1), (dtac (add_eq_conv_ex' RS iffD1) 1), (etac disjE 1), (etac disjI1 1), (clarify_tac csp 1), (etac allE2 1), (eatac impE 1 1), (etac disjE 1), Fast_tac 1, (rtac disjI2 1), (etac ex_forward 1), (etac conj_forward 1), (atac 1), (asm_simp_tac (esimps [] addsimprocs pmgsps) 1) ]) ; val times_single_add1' = full_simplify (esimps []) times_single_add1 ; val _ = qed_goal_spec_mp "mset_maps_eq" MS.thy "(ALL x. x:# M --> f x = g x) --> mset_map f M = mset_map g M" (fn _ => [ (res_inst_tac [("M", "M")] multiset_induct 1), (ALLGOALS (clarsimp_tac (cesimps [mset_map_union]))) ]) ; val _ = qed_goalw "mset_remove1" MS.thy [ms_of_list_def] "ms_of_list (remove1 A As) = ms_of_list As - {#A#}" (fn _ => [ (induct_tac "As" 1), ALLGOALS Clarsimp_tac, Safe_tac, (ALLGOALS (clarsimp_tac (cesimps [mins_eq]))), (rtac ms_eqI 1), Simp_tac 1, Safe_tac ]) ; val _ = qed_goal "ms_delete_plus_times" MS.thy "EX n. M = ms_delete {A} M + times n {#A#}" (fn _ => [ (res_inst_tac [("M", "M")] multiset_induct 1), (force_tac (cis [times.Z], esimps [symmetric Zero_multiset_def]) 1), (case_tac "x = A" 1), (ALLGOALS (clarsimp_tac (cesimps [ms_delete_sum, ms_delete_single]))), (res_inst_tac [("x", "Suc n")] exI 1), (res_inst_tac [("x", "n")] exI 2), (ALLGOALS (simp_tac (esimps add_ac addsimprocs pmgsps))), (ALLGOALS (etac box_equals THEN_ALL_NEW Simp_tac)) ]) ; val _ = qed_goalw "c2lem" MS.thy [ms_le_def] "({#A#} + {#A#} <= x) = (count x A >= Suc (Suc 0))" (fn _ => [ Safe_tac, (case_tac "a = A" 2), (eres_inst_tac [("x", "A")] allE 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "s4_ctr_lem" MS.thy "{#Bb#} <= X --> mset_map Box X + X - {#Box Bb#} - {#Bb#} = \ \ mset_map Box (X - {#Bb#}) + (X - {#Bb#})" (fn _ => [ (rtac impI 1), (asm_simp_tac (esimps [le_pm_assoc]) 1), (cong_tac 1), (stac (le_pm_assocc RS sym) 1), (asm_simp_tac (esimps [mset_map_diff_le]) 2), (dtac mset_map_mono 1), (etac xt6 1), Simp_tac 1 ]) ;