# HG changeset patch # User paulson # Date 959960563 -7200 # Node ID ff259b415c4de192019c990be29d0d879b37046f # Parent d61c7671698435686427bb617687dd678091b58d Many new theorems about multisets and their ordering, including basic laws like {#} <= M. Renamed union_comm to union_commute. Introduced the collection operator {# x:M. P x #}. diff -r d61c76716984 -r ff259b415c4d src/HOL/Induct/Multiset.ML --- a/src/HOL/Induct/Multiset.ML Fri Jun 02 15:19:18 2000 +0200 +++ b/src/HOL/Induct/Multiset.ML Fri Jun 02 17:42:43 2000 +0200 @@ -46,6 +46,7 @@ qed "multiset_eq_conv_Rep_eq"; Addsimps [multiset_eq_conv_Rep_eq]; Addsimps [expand_fun_eq]; + (* Goal "[| f : multiset; g : multiset |] ==> \ @@ -74,7 +75,7 @@ Goalw [union_def] "(M::'a multiset) + N = N + M"; by (simp_tac (simpset() addsimps add_ac) 1); -qed "union_comm"; +qed "union_commute"; Goalw [union_def] "((M::'a multiset)+N)+K = M+(N+K)"; @@ -82,10 +83,10 @@ qed "union_assoc"; qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)" - (fn _ => [rtac (union_comm RS trans) 1, rtac (union_assoc RS trans) 1, - rtac (union_comm RS arg_cong) 1]); + (fn _ => [rtac (union_commute RS trans) 1, rtac (union_assoc RS trans) 1, + rtac (union_commute RS arg_cong) 1]); -bind_thms ("union_ac", [union_assoc, union_comm, union_lcomm]); +bind_thms ("union_ac", [union_assoc, union_commute, union_lcomm]); (* diff *) @@ -150,6 +151,10 @@ by Auto_tac; qed "set_of_eq_empty_iff"; +Goalw [set_of_def] "(x : set_of M) = (x :# M)"; +by Auto_tac; +qed "mem_set_of_iff"; + (* size *) Goalw [size_def] "size {#} = 0"; @@ -186,6 +191,17 @@ qed "size_union"; Addsimps [size_union]; +Goalw [size_def, empty_def, count_def] "(size M = 0) = (M = {#})"; +by Auto_tac; +by (asm_full_simp_tac (simpset() addsimps [set_of_def, count_def]) 1); +qed "size_eq_0_iff_empty"; +AddIffs [size_eq_0_iff_empty]; + +Goalw [size_def] "size M = Suc n ==> EX a. a :# M"; +by (dtac setsum_SucD 1); +by Auto_tac; +qed "size_eq_Suc_imp_elem"; + (* equalities *) @@ -290,6 +306,7 @@ Better: use wf_finite_psubset in WF_Rel *) + (** Towards the induction rule **) Goal "[| finite F; 0 < f a |] ==> \ @@ -362,6 +379,29 @@ by (etac(simplify (simpset()) prem2)1); qed "multiset_induct"; +Goal "M : multiset ==> (%x. if P x then M x else 0) : multiset"; +by (asm_full_simp_tac (simpset() addsimps [multiset_def]) 1); +by (rtac finite_subset 1); +by Auto_tac; +qed "MCollect_preserves_multiset"; + +Goalw [count_def,MCollect_def] + "count {# x:M. P x #} a = (if P a then count M a else 0)"; +by (asm_full_simp_tac (simpset() addsimps [MCollect_preserves_multiset]) 1); +qed "count_MCollect"; +Addsimps [count_MCollect]; + +Goalw [set_of_def] + "set_of {# x:M. P x #} = set_of M Int {x. P x}"; +by Auto_tac; +qed "set_of_MCollect"; +Addsimps [set_of_MCollect]; + +Goal "M = {# x:M. P x #} + {# x:M. ~ P x #}"; +by (stac multiset_eq_conv_count_eq 1); +by Auto_tac; +qed "multiset_partition"; + Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq]; Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset]; @@ -381,7 +421,7 @@ Goalw [mult1_def] "(N,M0 + {#a#}) : mult1(r) = \ \ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \ -\ (? K. (!b. K :# b --> (b,a) : r) & N = M0 + K))"; +\ (? K. (!b. b :# K --> (b,a) : r) & N = M0 + K))"; by (rtac iffI 1); by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1); by (Clarify_tac 1); @@ -455,7 +495,7 @@ (* Badly needed: a linear arithmetic tactic for multisets *) -Goal "J :# a ==> I+J - {#a#} = I + (J-{#a#})"; +Goal "a :# J ==> I+J - {#a#} = I + (J-{#a#})"; by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1); qed "diff_union_single_conv"; @@ -469,7 +509,7 @@ by (res_inst_tac [("x","M0")] exI 1); by (Simp_tac 1); by (Clarify_tac 1); -by (case_tac "K :# a" 1); +by (case_tac "a :# K" 1); by (res_inst_tac [("x","I")] exI 1); by (Simp_tac 1); by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1); @@ -478,7 +518,7 @@ by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1); by (full_simp_tac (simpset() addsimps [trans_def]) 1); by (Blast_tac 1); -by (subgoal_tac "I :# a" 1); +by (subgoal_tac "a :# I" 1); by (res_inst_tac [("x","I-{#a#}")] exI 1); by (res_inst_tac [("x","J+{#a#}")] exI 1); by (res_inst_tac [("x","K + Ka")] exI 1); @@ -492,11 +532,64 @@ addsplits [nat_diff_split]) 1); by (full_simp_tac (simpset() addsimps [trans_def]) 1); by (Blast_tac 1); -by (subgoal_tac "(M0 +{#a#}) :# a" 1); +by (subgoal_tac "a :# (M0 +{#a#})" 1); by (Asm_full_simp_tac 1); by (Simp_tac 1); qed "mult_implies_one_step"; +Goal "a :# M ==> M = M - {#a#} + {#a#}"; +by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1); +qed "elem_imp_eq_diff_union"; + +Goal "size M = Suc n ==> EX a N. M = N + {#a#}"; +by (etac (size_eq_Suc_imp_elem RS exE) 1); +by (dtac elem_imp_eq_diff_union 1); +by Auto_tac; +qed "size_eq_Suc_imp_eq_union"; + + +Goal "trans r ==> \ +\ ALL I J K. \ +\ (size J = n & J ~= {#} & \ +\ (! k : set_of K. ? j : set_of J. (k,j) : r)) --> (I+K, I+J) : mult r"; +by (induct_tac "n" 1); +by Auto_tac; +by (ftac size_eq_Suc_imp_eq_union 1); +by (Clarify_tac 1); +ren "J'" 1; +by (Asm_full_simp_tac 1); +by (etac notE 1); +by Auto_tac; +by (case_tac "J' = {#}" 1); + by (asm_full_simp_tac (simpset() addsimps [mult_def]) 1); + by (rtac r_into_trancl 1); + by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); + by (Blast_tac 1); +(*Now we know J' ~= {#}*) +by (cut_inst_tac [("M","K"),("P", "%x. (x,a):r")] multiset_partition 1); +by (eres_inst_tac [("P", "ALL k : set_of K. ?P k")] rev_mp 1); +by (etac ssubst 1); +by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); +by Auto_tac; +by (subgoal_tac "((I + {# x : K. (x, a) : r#}) + {# x : K. (x, a) ~: r#}, \ +\ (I + {# x : K. (x, a) : r#}) + J') : mult r" 1); + by (Force_tac 2); +by (full_simp_tac (simpset() addsimps [union_assoc RS sym, mult_def]) 1); +by (etac trancl_trans 1); +by (rtac r_into_trancl 1); +by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); +by (res_inst_tac [("x", "a")] exI 1); +by (res_inst_tac [("x", "I + J'")] exI 1); +by (asm_simp_tac (simpset() addsimps union_ac) 1); +qed_spec_mp "one_step_implies_mult_lemma"; + +Goal "[| trans r; J ~= {#}; \ +\ ALL k : set_of K. EX j : set_of J. (k,j) : r |] \ +\ ==> (I+K, I+J) : mult r"; +by (rtac one_step_implies_mult_lemma 1); +by Auto_tac; +qed "one_step_implies_mult"; + (** Proving that multisets are partially ordered **) @@ -532,7 +625,7 @@ (*asymmetry*) Goal "M < N ==> ~ N < (M :: ('a::order)multiset)"; by Auto_tac; -br (mult_less_not_refl RS notE) 1; +by (rtac (mult_less_not_refl RS notE) 1); by (etac mult_less_trans 1); by (assume_tac 1); qed "mult_less_not_sym"; @@ -543,6 +636,7 @@ Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)"; by Auto_tac; qed "mult_le_refl"; +AddIffs [mult_le_refl]; (*anti-symmetry*) Goalw [mult_le_def] "[| M <= N; N <= M |] ==> M = (N :: ('a::order)multiset)"; @@ -558,3 +652,63 @@ Goalw [mult_le_def] "M < N = (M <= N & M ~= (N :: ('a::order)multiset))"; by Auto_tac; qed "mult_less_le"; + + +(** Monotonicity of multiset union **) + +Goalw [mult1_def] + "[| (B,D) : mult1 r; trans r |] ==> (C + B, C + D) : mult1 r"; +by Auto_tac; +by (res_inst_tac [("x", "a")] exI 1); +by (res_inst_tac [("x", "C+M0")] exI 1); +by (asm_simp_tac (simpset() addsimps [union_assoc]) 1); +qed "mult1_union"; + +Goalw [mult_less_def, mult_def] + "!!C:: ('a::order) multiset. B C+B < C+D"; +by (etac trancl_induct 1); +by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, + r_into_trancl]) 1); +by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, + r_into_trancl, trancl_trans]) 1); +qed "union_less_mono2"; + +Goal "!!C:: ('a::order) multiset. B B+C < D+C"; +by (simp_tac (simpset() addsimps [union_commute]) 1); +by (etac union_less_mono2 1); +qed "union_less_mono1"; + +Goal "!!C:: ('a::order) multiset. [| A A+B < C+D"; +by (blast_tac (claset() addIs [union_less_mono1, union_less_mono2, + mult_less_trans]) 1); +qed "union_less_mono"; + +Goalw [mult_le_def] + "!!D:: ('a::order) multiset. [| A<=C; B<=D |] ==> A+B <= C+D"; +by (blast_tac (claset() addIs [union_less_mono, union_less_mono1, + union_less_mono2]) 1); +qed "union_le_mono"; + + + +Goalw [mult_le_def, mult_less_def] + "{#} <= (M :: ('a::order) multiset)"; +by (case_tac "M={#}" 1); +by (subgoal_tac "({#} + {#}, {#} + M) : mult(Collect (split op <))" 2); +by (rtac one_step_implies_mult 3); +bw trans_def; +by Auto_tac; +by (blast_tac (claset() addIs [order_less_trans]) 1); +qed "empty_leI"; +AddIffs [empty_leI]; + + +Goal "!!A:: ('a::order) multiset. A <= A+B"; +by (subgoal_tac "A+{#} <= A+B" 1); +by (rtac union_le_mono 2); +by Auto_tac; +qed "union_upper1"; + +Goal "!!A:: ('a::order) multiset. B <= A+B"; +by (stac union_commute 1 THEN rtac union_upper1 1); +qed "union_upper2"; diff -r d61c76716984 -r ff259b415c4d src/HOL/Induct/Multiset.thy --- a/src/HOL/Induct/Multiset.thy Fri Jun 02 15:19:18 2000 +0200 +++ b/src/HOL/Induct/Multiset.thy Fri Jun 02 17:42:43 2000 +0200 @@ -21,12 +21,16 @@ single :: 'a => 'a multiset ("{#_#}") count :: ['a multiset, 'a] => nat set_of :: 'a multiset => 'a set + MCollect :: ['a multiset, 'a => bool] => 'a multiset (*comprehension*) + syntax - elem :: ['a multiset, 'a] => bool ("(_/ :# _)" [50, 51] 50) + elem :: ['a, 'a multiset] => bool ("(_/ :# _)" [50, 51] 50) + "@MColl" :: [pttrn, 'a multiset, bool] => 'a multiset ("(1{# _ : _./ _#})") translations - "M :# a" == "0 < count M a" + "a :# M" == "0 < count M a" + "{#x:M. P#}" == "MCollect M (%x. P)" defs count_def "count == Rep_multiset" @@ -34,14 +38,16 @@ single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)" union_def "M+N == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)" diff_def "M-N == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)" - set_of_def "set_of M == {x. M :# x}" + MCollect_def "MCollect M P == + Abs_multiset(%x. if P x then Rep_multiset M x else 0)" + set_of_def "set_of M == {x. x :# M}" size_def "size (M) == setsum (count M) (set_of M)" Zero_def "0 == {#}" constdefs mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set" "mult1(r) == {(N,M) . ? a M0 K. M = M0 + {#a#} & N = M0 + K & - (!b. K :# b --> (b,a) : r)}" + (!b. b :# K --> (b,a) : r)}" mult :: "('a * 'a)set => ('a multiset * 'a multiset)set" "mult(r) == (mult1 r)^+" diff -r d61c76716984 -r ff259b415c4d src/HOL/Induct/MultisetOrder.thy --- a/src/HOL/Induct/MultisetOrder.thy Fri Jun 02 15:19:18 2000 +0200 +++ b/src/HOL/Induct/MultisetOrder.thy Fri Jun 02 17:42:43 2000 +0200 @@ -11,5 +11,5 @@ instance multiset :: (order) order (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le) -instance multiset :: (term) plus_ac0 (union_comm,union_assoc) {|Auto_tac|} +instance multiset :: (term) plus_ac0 (union_commute,union_assoc) {|Auto_tac|} end