# HG changeset patch # User paulson # Date 958991407 -7200 # Node ID e1e4b73130635660a3bd6de0fd729d366fe99b91 # Parent 0bc13d5e60b81e5d0cc94ec8e94bd9db96234866 Proving that multisets are partially ordered New infix syntax for element-hood New theorem size_union diff -r 0bc13d5e60b8 -r e1e4b7313063 src/HOL/Induct/Multiset.ML --- a/src/HOL/Induct/Multiset.ML Mon May 22 12:29:02 2000 +0200 +++ b/src/HOL/Induct/Multiset.ML Mon May 22 12:30:07 2000 +0200 @@ -145,6 +145,10 @@ qed "set_of_union"; Addsimps [set_of_union]; +Goalw [set_of_def, empty_def, count_def] "(set_of M = {}) = (M = {#})"; +by Auto_tac; +qed "set_of_eq_empty_iff"; + (* size *) Goalw [size_def] "size {#} = 0"; @@ -152,16 +156,35 @@ qed "size_empty"; Addsimps [size_empty]; -Goalw [size_def] - "size {#b#} = 1"; +Goalw [size_def] "size {#b#} = 1"; by (Simp_tac 1); qed "size_single"; Addsimps [size_single]; -(* Some other day... -Goalw [size_def] - "size (M+N::'a multiset) = size M + size N"; -*) +Goal "finite (set_of M)"; +by (cut_inst_tac [("x", "M")] Rep_multiset 1); +by (asm_full_simp_tac + (simpset() addsimps [multiset_def, set_of_def, count_def]) 1); +qed "finite_set_of"; +AddIffs [finite_set_of]; + +Goal "finite A ==> setsum (count N) (A Int set_of N) = setsum (count N) A"; +by (etac finite_induct 1); +by (Simp_tac 1); +by (asm_full_simp_tac (simpset() addsimps [Int_insert_left, set_of_def]) 1); +qed "setsum_count_Int"; + +Goalw [size_def] "size (M+N::'a multiset) = size M + size N"; +by (subgoal_tac "count (M+N) = (%a. count M a + count N a)" 1); +by (rtac ext 2); +by (Simp_tac 2); +by (asm_simp_tac + (simpset() addsimps [setsum_Un, setsum_addf, setsum_count_Int]) 1); +by (stac Int_commute 1); +by (asm_simp_tac (simpset() addsimps [setsum_count_Int]) 1); +qed "size_union"; +Addsimps [size_union]; + (* equalities *) @@ -374,7 +397,7 @@ Goalw [mult1_def] "(N,M0 + {#a#}) : mult1(r) = \ \ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \ -\ (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))"; +\ (? K. (!b. K :# b --> (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); @@ -448,7 +471,7 @@ (* Badly needed: a linear arithmetic tactic for multisets *) -Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})"; +Goal "J :# a ==> I+J - {#a#} = I + (J-{#a#})"; by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1); qed "diff_union_single_conv"; @@ -462,7 +485,7 @@ by (res_inst_tac [("x","M0")] exI 1); by (Simp_tac 1); by (Clarify_tac 1); -by (case_tac "elem K a" 1); +by (case_tac "K :# a" 1); by (res_inst_tac [("x","I")] exI 1); by (Simp_tac 1); by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1); @@ -471,7 +494,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 "elem I a" 1); +by (subgoal_tac "I :# a" 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); @@ -485,7 +508,69 @@ addsplits [nat_diff_split]) 1); by (full_simp_tac (simpset() addsimps [trans_def]) 1); by (Blast_tac 1); -by (subgoal_tac "elem (M0 +{#a#}) a" 1); +by (subgoal_tac "(M0 +{#a#}) :# a" 1); by (Asm_full_simp_tac 1); by (Simp_tac 1); qed "mult_implies_one_step"; + + +(** Proving that multisets are partially ordered **) + +Goalw [trans_def] "trans {(x',x). x' < (x::'a::order)}"; +by (blast_tac (claset() addIs [order_less_trans]) 1); +qed "trans_base_order"; + +Goal "finite A ==> (ALL x: A. EX y : A. x < (y::'a::order)) --> A={}"; +by (etac finite_induct 1); +by Auto_tac; +by (blast_tac (claset() addIs [order_less_trans]) 1); +qed_spec_mp "mult_irrefl_lemma"; + +(*irreflexivity*) +Goalw [mult_less_def] "~ M < (M :: ('a::order)multiset)"; +by Auto_tac; +by (dtac (trans_base_order RS mult_implies_one_step) 1); +by Auto_tac; +by (dtac (finite_set_of RS mult_irrefl_lemma) 1); +by (asm_full_simp_tac (simpset() addsimps [set_of_eq_empty_iff]) 1); +qed "mult_less_not_refl"; + +(* N R *) +bind_thm ("mult_less_irrefl", mult_less_not_refl RS notE); +AddSEs [mult_less_irrefl]; + +(*transitivity*) +Goalw [mult_less_def, mult_def] + "[| K < M; M < N |] ==> K < (N :: ('a::order)multiset)"; +by (blast_tac (claset() addIs [trancl_trans]) 1); +qed "mult_less_trans"; + +(*asymmetry*) +Goal "M < N ==> ~ N < (M :: ('a::order)multiset)"; +by Auto_tac; +br (mult_less_not_refl RS notE) 1; +by (etac mult_less_trans 1); +by (assume_tac 1); +qed "mult_less_not_sym"; + +(* [| M N P *) +bind_thm ("mult_less_asym", mult_less_not_sym RS swap); + +Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)"; +by Auto_tac; +qed "mult_le_refl"; + +(*anti-symmetry*) +Goalw [mult_le_def] "[| M <= N; N <= M |] ==> M = (N :: ('a::order)multiset)"; +by (blast_tac (claset() addDs [mult_less_not_sym]) 1); +qed "mult_le_antisym"; + +(*transitivity*) +Goalw [mult_le_def] + "[| K <= M; M <= N |] ==> K <= (N :: ('a::order)multiset)"; +by (blast_tac (claset() addIs [mult_less_trans]) 1); +qed "mult_le_trans"; + +Goalw [mult_le_def] "M < N = (M <= N & M ~= (N :: ('a::order)multiset))"; +by Auto_tac; +qed "mult_less_le";