# 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<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 ==> N<M |] ==> 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";