moved to HOL/Library;
authorwenzelm
Wed Oct 18 23:38:41 2000 +0200 (2000-10-18)
changeset 10258d549f2534e6d
parent 10257 21055ac27708
child 10259 93ec82d535f2
moved to HOL/Library;
src/HOL/Induct/Acc.ML
src/HOL/Induct/Acc.thy
src/HOL/Induct/Multiset.ML
src/HOL/Induct/Multiset.thy
src/HOL/Induct/Multiset0.ML
src/HOL/Induct/Multiset0.thy
src/HOL/Induct/MultisetOrder.thy
     1.1 --- a/src/HOL/Induct/Acc.ML	Wed Oct 18 23:35:56 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,8 +0,0 @@
     1.4 -
     1.5 -val accI = thm "acc.accI";
     1.6 -val acc_induct = thm "acc_induct";
     1.7 -val acc_downward = thm "acc_downward";
     1.8 -val acc_downwards = thm "acc_downwards";
     1.9 -val acc_wfI = thm "acc_wfI";
    1.10 -val acc_wfD = thm "acc_wfD";
    1.11 -val wf_acc_iff = thm "wf_acc_iff";
     2.1 --- a/src/HOL/Induct/Acc.thy	Wed Oct 18 23:35:56 2000 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,78 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Acc.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1994  University of Cambridge
     2.8 -
     2.9 -Inductive definition of acc(r)
    2.10 -
    2.11 -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    2.12 -Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    2.13 -*)
    2.14 -
    2.15 -header {* The accessible part of a relation *}
    2.16 -
    2.17 -theory Acc = Main:
    2.18 -
    2.19 -consts
    2.20 -  acc  :: "('a \<times> 'a) set => 'a set"  -- {* accessible part *}
    2.21 -
    2.22 -inductive "acc r"
    2.23 -  intros
    2.24 -    accI [rule_format]:
    2.25 -      "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
    2.26 -
    2.27 -syntax
    2.28 -  termi :: "('a \<times> 'a) set => 'a set"
    2.29 -translations
    2.30 -  "termi r" == "acc (r^-1)"
    2.31 -
    2.32 -
    2.33 -theorem acc_induct:
    2.34 -  "[| a \<in> acc r;
    2.35 -      !!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x
    2.36 -  |] ==> P a"
    2.37 -proof -
    2.38 -  assume major: "a \<in> acc r"
    2.39 -  assume hyp: "!!x. [| x \<in> acc r;  \<forall>y. (y, x) \<in> r --> P y |] ==> P x"
    2.40 -  show ?thesis
    2.41 -    apply (rule major [THEN acc.induct])
    2.42 -    apply (rule hyp)
    2.43 -     apply (rule accI)
    2.44 -     apply fast
    2.45 -    apply fast
    2.46 -    done
    2.47 -qed
    2.48 -
    2.49 -theorem acc_downward: "[| b \<in> acc r; (a, b) \<in> r |] ==> a \<in> acc r"
    2.50 -  apply (erule acc.elims)
    2.51 -  apply fast
    2.52 -  done
    2.53 -
    2.54 -lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r"
    2.55 -  apply (erule rtrancl_induct)
    2.56 -   apply blast
    2.57 -  apply (blast dest: acc_downward)
    2.58 -  done
    2.59 -
    2.60 -theorem acc_downwards: "[| a \<in> acc r; (b, a) \<in> r^* |] ==> b \<in> acc r"
    2.61 -  apply (blast dest: acc_downwards_aux)
    2.62 -  done
    2.63 -
    2.64 -theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    2.65 -  apply (rule wfUNIVI)
    2.66 -  apply (induct_tac P x rule: acc_induct)
    2.67 -   apply blast
    2.68 -  apply blast
    2.69 -  done
    2.70 -
    2.71 -theorem acc_wfD: "wf r ==> x \<in> acc r"
    2.72 -  apply (erule wf_induct)
    2.73 -  apply (rule accI)
    2.74 -  apply blast
    2.75 -  done
    2.76 -
    2.77 -theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    2.78 -  apply (blast intro: acc_wfI dest: acc_wfD)
    2.79 -  done
    2.80 -
    2.81 -end
     3.1 --- a/src/HOL/Induct/Multiset.ML	Wed Oct 18 23:35:56 2000 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,715 +0,0 @@
     3.4 -(*  Title:      HOL/Induct/Multiset.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -    Copyright   1998 TUM
     3.8 -*)
     3.9 -
    3.10 -Addsimps [Abs_multiset_inverse, Rep_multiset_inverse, Rep_multiset,
    3.11 -	  Zero_def];
    3.12 -
    3.13 -(** Preservation of representing set `multiset' **)
    3.14 -
    3.15 -Goalw [multiset_def] "(%a. 0) : multiset";
    3.16 -by (Simp_tac 1);
    3.17 -qed "const0_in_multiset";
    3.18 -Addsimps [const0_in_multiset];
    3.19 -
    3.20 -Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
    3.21 -by (Simp_tac 1);
    3.22 -qed "only1_in_multiset";
    3.23 -Addsimps [only1_in_multiset];
    3.24 -
    3.25 -Goalw [multiset_def]
    3.26 - "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
    3.27 -by (Asm_full_simp_tac 1);
    3.28 -by (dtac finite_UnI 1);
    3.29 -by (assume_tac 1);
    3.30 -by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
    3.31 -qed "union_preserves_multiset";
    3.32 -Addsimps [union_preserves_multiset];
    3.33 -
    3.34 -Goalw [multiset_def]
    3.35 - "[| M : multiset |] ==> (%a. M a - N a) : multiset";
    3.36 -by (Asm_full_simp_tac 1);
    3.37 -by (etac (rotate_prems 1 finite_subset) 1);
    3.38 -by Auto_tac;
    3.39 -qed "diff_preserves_multiset";
    3.40 -Addsimps [diff_preserves_multiset];
    3.41 -
    3.42 -(** Injectivity of Rep_multiset **)
    3.43 -
    3.44 -Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
    3.45 -by (rtac iffI 1);
    3.46 - by (Asm_simp_tac 1);
    3.47 -by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
    3.48 -by (Asm_full_simp_tac 1);
    3.49 -qed "multiset_eq_conv_Rep_eq";
    3.50 -Addsimps [multiset_eq_conv_Rep_eq];
    3.51 -Addsimps [expand_fun_eq];
    3.52 -
    3.53 -(*
    3.54 -Goal
    3.55 - "[| f : multiset; g : multiset |] ==> \
    3.56 -\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
    3.57 -by (rtac iffI 1);
    3.58 - by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
    3.59 - by (Asm_full_simp_tac 1);
    3.60 -by (subgoal_tac "f = g" 1);
    3.61 - by (Asm_simp_tac 1);
    3.62 -by (rtac ext 1);
    3.63 -by (Blast_tac 1);
    3.64 -qed "Abs_multiset_eq";
    3.65 -Addsimps [Abs_multiset_eq];
    3.66 -*)
    3.67 -
    3.68 -(** Equations **)
    3.69 -
    3.70 -(* union *)
    3.71 -
    3.72 -Goalw [union_def,empty_def]
    3.73 - "M + {#} = M & {#} + M = M";
    3.74 -by (Simp_tac 1);
    3.75 -qed "union_empty";
    3.76 -Addsimps [union_empty];
    3.77 -
    3.78 -Goalw [union_def]
    3.79 - "(M::'a multiset) + N = N + M";
    3.80 -by (simp_tac (simpset() addsimps add_ac) 1);
    3.81 -qed "union_commute";
    3.82 -
    3.83 -Goalw [union_def]
    3.84 - "((M::'a multiset)+N)+K = M+(N+K)";
    3.85 -by (simp_tac (simpset() addsimps add_ac) 1);
    3.86 -qed "union_assoc";
    3.87 -
    3.88 -Goal "M+(N+K) = N+((M+K)::'a multiset)";
    3.89 -by (rtac (union_commute RS trans) 1);
    3.90 -by (rtac (union_assoc RS trans) 1);
    3.91 -by (rtac (union_commute RS arg_cong) 1);
    3.92 -qed "union_lcomm";
    3.93 -
    3.94 -bind_thms ("union_ac", [union_assoc, union_commute, union_lcomm]);
    3.95 -
    3.96 -(* diff *)
    3.97 -
    3.98 -Goalw [empty_def,diff_def]
    3.99 - "M-{#} = M & {#}-M = {#}";
   3.100 -by (Simp_tac 1);
   3.101 -qed "diff_empty";
   3.102 -Addsimps [diff_empty];
   3.103 -
   3.104 -Goalw [union_def,diff_def]
   3.105 - "M+{#a#}-{#a#} = M";
   3.106 -by (Simp_tac 1);
   3.107 -qed "diff_union_inverse2";
   3.108 -Addsimps [diff_union_inverse2];
   3.109 -
   3.110 -(* count *)
   3.111 -
   3.112 -Goalw [count_def,empty_def]
   3.113 - "count {#} a = 0";
   3.114 -by (Simp_tac 1);
   3.115 -qed "count_empty";
   3.116 -Addsimps [count_empty];
   3.117 -
   3.118 -Goalw [count_def,single_def]
   3.119 - "count {#b#} a = (if b=a then 1 else 0)";
   3.120 -by (Simp_tac 1);
   3.121 -qed "count_single";
   3.122 -Addsimps [count_single];
   3.123 -
   3.124 -Goalw [count_def,union_def]
   3.125 - "count (M+N) a = count M a + count N a";
   3.126 -by (Simp_tac 1);
   3.127 -qed "count_union";
   3.128 -Addsimps [count_union];
   3.129 -
   3.130 -Goalw [count_def,diff_def]
   3.131 - "count (M-N) a = count M a - count N a";
   3.132 -by (Simp_tac 1);
   3.133 -qed "count_diff";
   3.134 -Addsimps [count_diff];
   3.135 -
   3.136 -(* set_of *)
   3.137 -
   3.138 -Goalw [set_of_def] "set_of {#} = {}";
   3.139 -by (Simp_tac 1);
   3.140 -qed "set_of_empty";
   3.141 -Addsimps [set_of_empty];
   3.142 -
   3.143 -Goalw [set_of_def]
   3.144 - "set_of {#b#} = {b}";
   3.145 -by (Simp_tac 1);
   3.146 -qed "set_of_single";
   3.147 -Addsimps [set_of_single];
   3.148 -
   3.149 -Goalw [set_of_def]
   3.150 - "set_of(M+N) = set_of M Un set_of N";
   3.151 -by Auto_tac;
   3.152 -qed "set_of_union";
   3.153 -Addsimps [set_of_union];
   3.154 -
   3.155 -Goalw [set_of_def, empty_def, count_def] "(set_of M = {}) = (M = {#})";
   3.156 -by Auto_tac;
   3.157 -qed "set_of_eq_empty_iff";
   3.158 -
   3.159 -Goalw [set_of_def] "(x : set_of M) = (x :# M)";
   3.160 -by Auto_tac; 
   3.161 -qed "mem_set_of_iff";
   3.162 -
   3.163 -(* size *)
   3.164 -
   3.165 -Goalw [size_def] "size {#} = 0";
   3.166 -by (Simp_tac 1);
   3.167 -qed "size_empty";
   3.168 -Addsimps [size_empty];
   3.169 -
   3.170 -Goalw [size_def] "size {#b#} = 1";
   3.171 -by (Simp_tac 1);
   3.172 -qed "size_single";
   3.173 -Addsimps [size_single];
   3.174 -
   3.175 -Goal "finite (set_of M)";
   3.176 -by (cut_inst_tac [("x", "M")] Rep_multiset 1);
   3.177 -by (asm_full_simp_tac
   3.178 -    (simpset() addsimps [multiset_def, set_of_def, count_def]) 1);
   3.179 -qed "finite_set_of";
   3.180 -AddIffs [finite_set_of];
   3.181 -
   3.182 -Goal "finite A ==> setsum (count N) (A Int set_of N) = setsum (count N) A";
   3.183 -by (etac finite_induct 1);
   3.184 -by (Simp_tac 1);
   3.185 -by (asm_full_simp_tac (simpset() addsimps [Int_insert_left, set_of_def]) 1);
   3.186 -qed "setsum_count_Int";
   3.187 -
   3.188 -Goalw [size_def] "size (M+N::'a multiset) = size M + size N";
   3.189 -by (subgoal_tac "count (M+N) = (%a. count M a + count N a)" 1);
   3.190 -by (rtac ext 2);
   3.191 -by (Simp_tac 2);
   3.192 -by (asm_simp_tac
   3.193 -    (simpset() addsimps [setsum_Un, setsum_addf, setsum_count_Int]) 1);
   3.194 -by (stac Int_commute 1);
   3.195 -by (asm_simp_tac (simpset() addsimps [setsum_count_Int]) 1);
   3.196 -qed "size_union";
   3.197 -Addsimps [size_union];
   3.198 -
   3.199 -Goalw [size_def, empty_def, count_def] "(size M = 0) = (M = {#})";
   3.200 -by Auto_tac; 
   3.201 -by (asm_full_simp_tac (simpset() addsimps [set_of_def, count_def]) 1); 
   3.202 -qed "size_eq_0_iff_empty";
   3.203 -AddIffs [size_eq_0_iff_empty];
   3.204 -
   3.205 -Goalw [size_def] "size M = Suc n ==> EX a. a :# M";
   3.206 -by (dtac setsum_SucD 1);
   3.207 -by Auto_tac; 
   3.208 -qed "size_eq_Suc_imp_elem";
   3.209 -
   3.210 -
   3.211 -(* equalities *)
   3.212 -
   3.213 -Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
   3.214 -by (Simp_tac 1);
   3.215 -qed "multiset_eq_conv_count_eq";
   3.216 -
   3.217 -Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
   3.218 -by (Simp_tac 1);
   3.219 -qed "single_not_empty";
   3.220 -Addsimps [single_not_empty];
   3.221 -
   3.222 -Goalw [single_def] "({#a#}={#b#}) = (a=b)";
   3.223 -by Auto_tac;
   3.224 -qed "single_eq_single";
   3.225 -Addsimps [single_eq_single];
   3.226 -
   3.227 -Goalw [union_def,empty_def]
   3.228 - "(M+N = {#}) = (M = {#} & N = {#})";
   3.229 -by (Simp_tac 1);
   3.230 -by (Blast_tac 1);
   3.231 -qed "union_eq_empty";
   3.232 -AddIffs [union_eq_empty];
   3.233 -
   3.234 -Goalw [union_def,empty_def]
   3.235 - "({#} = M+N) = (M = {#} & N = {#})";
   3.236 -by (Simp_tac 1);
   3.237 -by (Blast_tac 1);
   3.238 -qed "empty_eq_union";
   3.239 -AddIffs [empty_eq_union];
   3.240 -
   3.241 -Goalw [union_def]
   3.242 - "(M+K = N+K) = (M=(N::'a multiset))";
   3.243 -by (Simp_tac 1);
   3.244 -qed "union_right_cancel";
   3.245 -Addsimps [union_right_cancel];
   3.246 -
   3.247 -Goalw [union_def]
   3.248 - "(K+M = K+N) = (M=(N::'a multiset))";
   3.249 -by (Simp_tac 1);
   3.250 -qed "union_left_cancel";
   3.251 -Addsimps [union_left_cancel];
   3.252 -
   3.253 -Goalw [empty_def,single_def,union_def]
   3.254 - "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
   3.255 -by (simp_tac (simpset() addsimps [add_is_1]) 1);
   3.256 -by (Blast_tac 1);
   3.257 -qed "union_is_single";
   3.258 -
   3.259 -Goalw [empty_def,single_def,union_def]
   3.260 - "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
   3.261 -by (simp_tac (simpset() addsimps [one_is_add]) 1);
   3.262 -by (blast_tac (claset() addDs [sym]) 1);
   3.263 -qed "single_is_union";
   3.264 -
   3.265 -Goalw [single_def,union_def,diff_def]
   3.266 - "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
   3.267 -by (Simp_tac 1);
   3.268 -by (rtac conjI 1);
   3.269 - by (Force_tac 1);
   3.270 -by (Clarify_tac 1);
   3.271 -by (rtac conjI 1);
   3.272 - by (Blast_tac 1);
   3.273 -by (Clarify_tac 1);
   3.274 -by (rtac iffI 1);
   3.275 - by (rtac conjI 1);
   3.276 - by (Clarify_tac 1);
   3.277 -  by (rtac conjI 1);
   3.278 -   by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   3.279 -(* PROOF FAILED:
   3.280 -by (Blast_tac 1);
   3.281 -*)
   3.282 -  by (Fast_tac 1);
   3.283 - by (Asm_simp_tac 1);
   3.284 -by (Force_tac 1);
   3.285 -qed "add_eq_conv_diff";
   3.286 -
   3.287 -(* FIXME
   3.288 -val prems = Goal
   3.289 - "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   3.290 -by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
   3.291 -     measure_induct 1);
   3.292 -by (Clarify_tac 1);
   3.293 -by (resolve_tac prems 1);
   3.294 - by (assume_tac 1);
   3.295 -by (Clarify_tac 1);
   3.296 -by (subgoal_tac "finite G" 1);
   3.297 - by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   3.298 -by (etac allE 1);
   3.299 -by (etac impE 1);
   3.300 - by (Blast_tac 2);
   3.301 -by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   3.302 -no_qed();
   3.303 -val lemma = result();
   3.304 -
   3.305 -val prems = Goal
   3.306 - "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
   3.307 -by (rtac (lemma RS mp) 1);
   3.308 -by (REPEAT(ares_tac prems 1));
   3.309 -qed "finite_psubset_induct";
   3.310 -
   3.311 -Better: use wf_finite_psubset in WF_Rel
   3.312 -*)
   3.313 -
   3.314 -
   3.315 -(** Towards the induction rule **)
   3.316 -
   3.317 -Goal "[| finite F; 0 < f a |] ==> \
   3.318 -\     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
   3.319 -by (etac finite_induct 1);
   3.320 -by Auto_tac;
   3.321 - by (asm_simp_tac (simpset() addsimps add_ac) 1);
   3.322 -by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   3.323 -by Auto_tac;
   3.324 -qed "setsum_decr";
   3.325 -
   3.326 -val prems = Goalw [multiset_def]
   3.327 - "[| P(%a.0); \
   3.328 -\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
   3.329 -\  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
   3.330 -by (induct_tac "n" 1);
   3.331 - by (Asm_simp_tac 1);
   3.332 - by (Clarify_tac 1);
   3.333 - by (subgoal_tac "f = (%a.0)" 1);
   3.334 -  by (Asm_simp_tac 1);
   3.335 -  by (resolve_tac prems 1);
   3.336 - by (rtac ext 1);
   3.337 - by (Force_tac 1);
   3.338 -by (Clarify_tac 1);
   3.339 -by (ftac setsum_SucD 1);
   3.340 -by (Clarify_tac 1);
   3.341 -by (rename_tac "a" 1);
   3.342 -by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
   3.343 - by (etac (rotate_prems 1 finite_subset) 2);
   3.344 - by (Simp_tac 2);
   3.345 - by (Blast_tac 2);
   3.346 -by (subgoal_tac
   3.347 -   "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
   3.348 - by (rtac ext 2);
   3.349 - by (Asm_simp_tac 2);
   3.350 -by (EVERY1[etac ssubst, resolve_tac prems]);
   3.351 - by (Blast_tac 1);
   3.352 -by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
   3.353 - by (Blast_tac 1);
   3.354 -by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
   3.355 -by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
   3.356 - by (Blast_tac 2);
   3.357 -by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
   3.358 - by (Blast_tac 2);
   3.359 -by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
   3.360 -                           addcongs [conj_cong]) 1);
   3.361 -no_qed();
   3.362 -val lemma = result();
   3.363 -
   3.364 -val major::prems = Goal
   3.365 - "[| f : multiset; \
   3.366 -\    P(%a.0); \
   3.367 -\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
   3.368 -by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
   3.369 -by (REPEAT(ares_tac (refl::prems) 1));
   3.370 -qed "Rep_multiset_induct";
   3.371 -
   3.372 -val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
   3.373 - "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
   3.374 -by (rtac (Rep_multiset_inverse RS subst) 1);
   3.375 -by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
   3.376 - by (rtac prem1 1);
   3.377 -by (Clarify_tac 1);
   3.378 -by (subgoal_tac
   3.379 -    "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
   3.380 - by (Simp_tac 2);
   3.381 -by (etac ssubst 1);
   3.382 -by (etac (Abs_multiset_inverse RS subst) 1);
   3.383 -by (etac(simplify (simpset()) prem2)1);
   3.384 -qed "multiset_induct";
   3.385 -
   3.386 -Goal "M : multiset ==> (%x. if P x then M x else 0) : multiset";
   3.387 -by (asm_full_simp_tac (simpset() addsimps [multiset_def]) 1);
   3.388 -by (rtac finite_subset 1);
   3.389 -by Auto_tac; 
   3.390 -qed "MCollect_preserves_multiset";
   3.391 -
   3.392 -Goalw [count_def,MCollect_def]
   3.393 - "count {# x:M. P x #} a = (if P a then count M a else 0)";
   3.394 -by (asm_full_simp_tac (simpset() addsimps [MCollect_preserves_multiset]) 1); 
   3.395 -qed "count_MCollect";
   3.396 -Addsimps [count_MCollect];
   3.397 -
   3.398 -Goalw [set_of_def]
   3.399 - "set_of {# x:M. P x #} = set_of M Int {x. P x}";
   3.400 -by Auto_tac; 
   3.401 -qed "set_of_MCollect";
   3.402 -Addsimps [set_of_MCollect];
   3.403 -
   3.404 -Goal "M = {# x:M. P x #} + {# x:M. ~ P x #}";
   3.405 -by (stac multiset_eq_conv_count_eq 1);
   3.406 -by Auto_tac; 
   3.407 -qed "multiset_partition";
   3.408 -
   3.409 -Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
   3.410 -Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
   3.411 -
   3.412 -Goal
   3.413 - "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
   3.414 -by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
   3.415 -by Auto_tac;
   3.416 -qed "add_eq_conv_ex";
   3.417 -
   3.418 -(** order **)
   3.419 -
   3.420 -Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
   3.421 -by (Simp_tac 1);
   3.422 -qed "not_less_empty";
   3.423 -AddIffs [not_less_empty];
   3.424 -
   3.425 -Goalw [mult1_def]
   3.426 - "(N,M0 + {#a#}) : mult1(r) = \
   3.427 -\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
   3.428 -\  (? K. (!b. b :# K --> (b,a) : r) & N = M0 + K))";
   3.429 -by (rtac iffI 1);
   3.430 - by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
   3.431 - by (Clarify_tac 1);
   3.432 - by (etac disjE 1);
   3.433 -  by (Blast_tac 1);
   3.434 - by (Clarify_tac 1);
   3.435 - by (res_inst_tac [("x","Ka+K")] exI 1);
   3.436 - by (simp_tac (simpset() addsimps union_ac) 1);
   3.437 - by (Blast_tac 1);
   3.438 -by (etac disjE 1);
   3.439 - by (Clarify_tac 1);
   3.440 - by (res_inst_tac [("x","aa")] exI 1);
   3.441 - by (res_inst_tac [("x","M0+{#a#}")] exI 1);
   3.442 - by (res_inst_tac [("x","K")] exI 1);
   3.443 - by (simp_tac (simpset() addsimps union_ac) 1);
   3.444 -by (Blast_tac 1);
   3.445 -qed "less_add_conv";
   3.446 -
   3.447 -Open_locale "MSOrd";
   3.448 -
   3.449 -val W_def = thm "W_def";
   3.450 -
   3.451 -Goalw [W_def]
   3.452 - "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
   3.453 -\    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
   3.454 -\ ==> M0+{#a#} : W";
   3.455 -by (rtac accI 1);
   3.456 -by (rename_tac "N" 1);
   3.457 -by (full_simp_tac (simpset() addsimps [less_add_conv]) 1);
   3.458 -by (etac disjE 1);
   3.459 - by (Blast_tac 1);
   3.460 -by (Clarify_tac 1);
   3.461 -by (rotate_tac ~1 1);
   3.462 -by (etac rev_mp 1);
   3.463 -by (induct_thm_tac multiset_induct "K" 1);
   3.464 - by (Asm_simp_tac 1);
   3.465 -by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   3.466 -by (Blast_tac 1);
   3.467 -qed "lemma1";
   3.468 -
   3.469 -Goalw [W_def]
   3.470 - "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
   3.471 -by (etac acc_induct 1);
   3.472 -by (blast_tac (claset() addIs [export lemma1]) 1);
   3.473 -qed "lemma2";
   3.474 -
   3.475 -Goalw [W_def]
   3.476 - "wf(r) ==> !M:W. M+{#a#} : W";
   3.477 -by (eres_inst_tac [("a","a")] wf_induct 1);
   3.478 -by (blast_tac (claset() addIs [export lemma2]) 1);
   3.479 -qed "lemma3";
   3.480 -
   3.481 -Goalw [W_def] "wf(r) ==> M : W";
   3.482 -by (induct_thm_tac multiset_induct "M" 1);
   3.483 - by (rtac accI 1);
   3.484 - by (Asm_full_simp_tac 1);
   3.485 -by (blast_tac (claset() addDs [export lemma3]) 1);
   3.486 -qed "all_accessible";
   3.487 -
   3.488 -Close_locale "MSOrd";
   3.489 -
   3.490 -Goal "wf(r) ==> wf(mult1 r)";
   3.491 -by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
   3.492 -qed "wf_mult1";
   3.493 -
   3.494 -Goalw [mult_def] "wf(r) ==> wf(mult r)";
   3.495 -by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
   3.496 -qed "wf_mult";
   3.497 -
   3.498 -(** Equivalence of mult with the usual (closure-free) def **)
   3.499 -
   3.500 -(* Badly needed: a linear arithmetic tactic for multisets *)
   3.501 -
   3.502 -Goal "a :# J ==> I+J - {#a#} = I + (J-{#a#})";
   3.503 -by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
   3.504 -qed "diff_union_single_conv";
   3.505 -
   3.506 -(* One direction *)
   3.507 -Goalw [mult_def,mult1_def,set_of_def]
   3.508 - "trans r ==> \
   3.509 -\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
   3.510 -\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
   3.511 -by (etac converse_trancl_induct 1);
   3.512 - by (Clarify_tac 1);
   3.513 - by (res_inst_tac [("x","M0")] exI 1);
   3.514 - by (Simp_tac 1);
   3.515 -by (Clarify_tac 1);
   3.516 -by (case_tac "a :# K" 1);
   3.517 - by (res_inst_tac [("x","I")] exI 1);
   3.518 - by (Simp_tac 1);
   3.519 - by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
   3.520 - by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   3.521 - by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   3.522 - by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
   3.523 - by (full_simp_tac (simpset() addsimps [trans_def]) 1);
   3.524 - by (Blast_tac 1);
   3.525 -by (subgoal_tac "a :# I" 1);
   3.526 - by (res_inst_tac [("x","I-{#a#}")] exI 1);
   3.527 - by (res_inst_tac [("x","J+{#a#}")] exI 1);
   3.528 - by (res_inst_tac [("x","K + Ka")] exI 1);
   3.529 - by (rtac conjI 1);
   3.530 -  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   3.531 -                             addsplits [nat_diff_split]) 1);
   3.532 - by (rtac conjI 1);
   3.533 -  by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   3.534 -  by (Asm_full_simp_tac 1);
   3.535 -  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   3.536 -                             addsplits [nat_diff_split]) 1);
   3.537 - by (full_simp_tac (simpset() addsimps [trans_def]) 1);
   3.538 - by (Blast_tac 1);
   3.539 -by (subgoal_tac "a :# (M0 +{#a#})" 1);
   3.540 - by (Asm_full_simp_tac 1);
   3.541 -by (Simp_tac 1);
   3.542 -qed "mult_implies_one_step";
   3.543 -
   3.544 -Goal "a :# M ==> M = M - {#a#} + {#a#}";
   3.545 -by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
   3.546 -qed "elem_imp_eq_diff_union";
   3.547 -
   3.548 -Goal "size M = Suc n ==> EX a N. M = N + {#a#}";
   3.549 -by (etac (size_eq_Suc_imp_elem RS exE) 1);
   3.550 -by (dtac elem_imp_eq_diff_union 1); 
   3.551 -by Auto_tac; 
   3.552 -qed "size_eq_Suc_imp_eq_union";
   3.553 -
   3.554 -
   3.555 -Goal  "trans r ==> \
   3.556 -\ ALL I J K. \
   3.557 -\  (size J = n & J ~= {#} & \
   3.558 -\   (! k : set_of K. ? j : set_of J. (k,j) : r)) --> (I+K, I+J) : mult r";
   3.559 -by (induct_tac "n" 1);
   3.560 -by Auto_tac; 
   3.561 -by (ftac size_eq_Suc_imp_eq_union 1);
   3.562 -by (Clarify_tac 1); 
   3.563 -ren "J'" 1;
   3.564 -by (Asm_full_simp_tac 1); 
   3.565 -by (etac notE 1); 
   3.566 -by Auto_tac; 
   3.567 -by (case_tac "J' = {#}" 1);
   3.568 - by (asm_full_simp_tac (simpset() addsimps [mult_def]) 1); 
   3.569 - by (rtac r_into_trancl 1); 
   3.570 - by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1);
   3.571 - by (Blast_tac 1); 
   3.572 -(*Now we know J' ~= {#}*)
   3.573 -by (cut_inst_tac [("M","K"),("P", "%x. (x,a):r")] multiset_partition 1);
   3.574 -by (eres_inst_tac [("P", "ALL k : set_of K. ?P k")] rev_mp 1); 
   3.575 -by (etac ssubst 1); 
   3.576 -by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); 
   3.577 -by Auto_tac; 
   3.578 -by (subgoal_tac "((I + {# x : K. (x, a) : r#}) + {# x : K. (x, a) ~: r#}, \
   3.579 -\                 (I + {# x : K. (x, a) : r#}) + J') : mult r" 1);
   3.580 - by (Force_tac 2);
   3.581 -by (full_simp_tac (simpset() addsimps [union_assoc RS sym, mult_def]) 1); 
   3.582 -by (etac trancl_trans 1); 
   3.583 -by (rtac r_into_trancl 1); 
   3.584 -by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); 
   3.585 -by (res_inst_tac [("x", "a")] exI 1); 
   3.586 -by (res_inst_tac [("x", "I + J'")] exI 1); 
   3.587 -by (asm_simp_tac (simpset() addsimps union_ac) 1); 
   3.588 -qed_spec_mp "one_step_implies_mult_lemma";
   3.589 -
   3.590 -Goal  "[| trans r;  J ~= {#};  \
   3.591 -\         ALL k : set_of K. EX j : set_of J. (k,j) : r |] \
   3.592 -\      ==> (I+K, I+J) : mult r";
   3.593 -by (rtac one_step_implies_mult_lemma 1); 
   3.594 -by Auto_tac; 
   3.595 -qed "one_step_implies_mult";
   3.596 -
   3.597 -
   3.598 -(** Proving that multisets are partially ordered **)
   3.599 -
   3.600 -Goalw [trans_def] "trans {(x',x). x' < (x::'a::order)}";
   3.601 -by (blast_tac (claset() addIs [order_less_trans]) 1);
   3.602 -qed "trans_base_order";
   3.603 -
   3.604 -Goal "finite A ==> (ALL x: A. EX y : A. x < (y::'a::order)) --> A={}";
   3.605 -by (etac finite_induct 1);
   3.606 -by Auto_tac;
   3.607 -by (blast_tac (claset() addIs [order_less_trans]) 1);
   3.608 -qed_spec_mp "mult_irrefl_lemma";
   3.609 -
   3.610 -(*irreflexivity*)
   3.611 -Goalw [mult_less_def] "~ M < (M :: ('a::order)multiset)";
   3.612 -by Auto_tac;
   3.613 -by (dtac (trans_base_order RS mult_implies_one_step) 1);
   3.614 -by Auto_tac;
   3.615 -by (dtac (finite_set_of RS mult_irrefl_lemma) 1);
   3.616 -by (asm_full_simp_tac (simpset() addsimps [set_of_eq_empty_iff]) 1);
   3.617 -qed "mult_less_not_refl";
   3.618 -
   3.619 -(* N<N ==> R *)
   3.620 -bind_thm ("mult_less_irrefl", mult_less_not_refl RS notE);
   3.621 -AddSEs [mult_less_irrefl];
   3.622 -
   3.623 -(*transitivity*)
   3.624 -Goalw [mult_less_def, mult_def]
   3.625 -     "[| K < M; M < N |] ==> K < (N :: ('a::order)multiset)";
   3.626 -by (blast_tac (claset() addIs [trancl_trans]) 1);
   3.627 -qed "mult_less_trans";
   3.628 -
   3.629 -(*asymmetry*)
   3.630 -Goal "M < N ==> ~ N < (M :: ('a::order)multiset)";
   3.631 -by Auto_tac;
   3.632 -by (rtac (mult_less_not_refl RS notE) 1);
   3.633 -by (etac mult_less_trans 1);
   3.634 -by (assume_tac 1);
   3.635 -qed "mult_less_not_sym";
   3.636 -
   3.637 -(* [| M<N;  ~P ==> N<M |] ==> P *)
   3.638 -bind_thm ("mult_less_asym", mult_less_not_sym RS contrapos_np);
   3.639 -
   3.640 -Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)";
   3.641 -by Auto_tac;
   3.642 -qed "mult_le_refl";
   3.643 -AddIffs [mult_le_refl];
   3.644 -
   3.645 -(*anti-symmetry*)
   3.646 -Goalw [mult_le_def] "[| M <= N;  N <= M |] ==> M = (N :: ('a::order)multiset)";
   3.647 -by (blast_tac (claset() addDs [mult_less_not_sym]) 1);
   3.648 -qed "mult_le_antisym";
   3.649 -
   3.650 -(*transitivity*)
   3.651 -Goalw [mult_le_def]
   3.652 -     "[| K <= M; M <= N |] ==> K <= (N :: ('a::order)multiset)";
   3.653 -by (blast_tac (claset() addIs [mult_less_trans]) 1);
   3.654 -qed "mult_le_trans";
   3.655 -
   3.656 -Goalw [mult_le_def] "M < N = (M <= N & M ~= (N :: ('a::order)multiset))";
   3.657 -by Auto_tac;
   3.658 -qed "mult_less_le";
   3.659 -
   3.660 -
   3.661 -(** Monotonicity of multiset union **)
   3.662 -
   3.663 -Goalw [mult1_def]
   3.664 -     "[| (B,D) : mult1 r; trans r |] ==> (C + B, C + D) : mult1 r";
   3.665 -by Auto_tac; 
   3.666 -by (res_inst_tac [("x", "a")] exI 1); 
   3.667 -by (res_inst_tac [("x", "C+M0")] exI 1); 
   3.668 -by (asm_simp_tac (simpset() addsimps [union_assoc]) 1); 
   3.669 -qed "mult1_union";
   3.670 -
   3.671 -Goalw [mult_less_def, mult_def]
   3.672 -     "!!C:: ('a::order) multiset. B<D ==> C+B < C+D";
   3.673 -by (etac trancl_induct 1); 
   3.674 -by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, 
   3.675 -                               r_into_trancl]) 1); 
   3.676 -by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, 
   3.677 -                               r_into_trancl, trancl_trans]) 1); 
   3.678 -qed "union_less_mono2";
   3.679 -
   3.680 -Goal "!!C:: ('a::order) multiset. B<D ==> B+C < D+C";
   3.681 -by (simp_tac (simpset() addsimps [union_commute]) 1); 
   3.682 -by (etac union_less_mono2 1); 
   3.683 -qed "union_less_mono1";
   3.684 -
   3.685 -Goal "!!C:: ('a::order) multiset. [| A<C; B<D |] ==> A+B < C+D";
   3.686 -by (blast_tac (claset() addIs [union_less_mono1, union_less_mono2,
   3.687 -                               mult_less_trans]) 1); 
   3.688 -qed "union_less_mono";
   3.689 -
   3.690 -Goalw [mult_le_def]
   3.691 -     "!!D:: ('a::order) multiset. [| A<=C;  B<=D |] ==> A+B <= C+D";
   3.692 -by (blast_tac (claset() addIs [union_less_mono, union_less_mono1, 
   3.693 -                               union_less_mono2]) 1); 
   3.694 -qed "union_le_mono";
   3.695 -
   3.696 -
   3.697 -
   3.698 -Goalw [mult_le_def, mult_less_def]
   3.699 -     "{#} <= (M :: ('a::order) multiset)";
   3.700 -by (case_tac "M={#}" 1);
   3.701 -by (subgoal_tac "({#} + {#}, {#} + M) : mult(Collect (split op <))" 2);
   3.702 -by (rtac one_step_implies_mult 3);
   3.703 -bw trans_def;
   3.704 -by Auto_tac; 
   3.705 -by (blast_tac (claset() addIs [order_less_trans]) 1); 
   3.706 -qed "empty_leI";
   3.707 -AddIffs [empty_leI];
   3.708 -
   3.709 -
   3.710 -Goal "!!A:: ('a::order) multiset. A <= A+B";
   3.711 -by (subgoal_tac "A+{#} <= A+B" 1);
   3.712 -by (rtac union_le_mono 2); 
   3.713 -by Auto_tac; 
   3.714 -qed "union_upper1";
   3.715 -
   3.716 -Goal "!!A:: ('a::order) multiset. B <= A+B";
   3.717 -by (stac union_commute 1 THEN rtac union_upper1 1);
   3.718 -qed "union_upper2";
     4.1 --- a/src/HOL/Induct/Multiset.thy	Wed Oct 18 23:35:56 2000 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,65 +0,0 @@
     4.4 -(*  Title:      HOL/Induct/Multiset.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow
     4.7 -    Copyright   1998 TUM
     4.8 -
     4.9 -A definitional theory of multisets,
    4.10 -including a wellfoundedness proof for the multiset order.
    4.11 -*)
    4.12 -
    4.13 -Multiset = Multiset0 + Acc +
    4.14 -
    4.15 -typedef
    4.16 -  'a multiset = "{f :: 'a => nat . finite{x . 0 < f x}}" (multiset_witness)
    4.17 -
    4.18 -instance multiset :: (term){ord,zero,plus,minus}
    4.19 -
    4.20 -consts
    4.21 -  "{#}"  :: 'a multiset                        ("{#}")
    4.22 -  single :: 'a                => 'a multiset   ("{#_#}")
    4.23 -  count  :: ['a multiset, 'a] => nat
    4.24 -  set_of :: 'a multiset => 'a set
    4.25 -  MCollect :: ['a multiset, 'a => bool] => 'a multiset (*comprehension*)
    4.26 -
    4.27 -
    4.28 -syntax
    4.29 -  elem     :: ['a, 'a multiset] => bool              ("(_/ :# _)" [50, 51] 50)
    4.30 -  "@MColl" :: [pttrn, 'a multiset, bool] => 'a multiset ("(1{# _ : _./ _#})")
    4.31 -
    4.32 -translations
    4.33 -  "a :# M"     == "0 < count M a"
    4.34 -  "{#x:M. P#}" == "MCollect M (%x. P)"
    4.35 -
    4.36 -defs
    4.37 -  count_def  "count == Rep_multiset"
    4.38 -  empty_def  "{#}   == Abs_multiset(%a. 0)"
    4.39 -  single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)"
    4.40 -  union_def  "M+N   == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)"
    4.41 -  diff_def   "M-N    == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)"
    4.42 -  MCollect_def "MCollect M P ==
    4.43 -		Abs_multiset(%x. if P x then Rep_multiset M x else 0)"
    4.44 -  set_of_def "set_of M == {x. x :# M}"
    4.45 -  size_def   "size (M) == setsum (count M) (set_of M)"
    4.46 -  Zero_def   "0 == {#}"
    4.47 -
    4.48 -constdefs
    4.49 -  mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set"
    4.50 - "mult1(r) == {(N,M) . ? a M0 K. M = M0 + {#a#} & N = M0 + K &
    4.51 -                                 (!b. b :# K --> (b,a) : r)}"
    4.52 -
    4.53 -  mult :: "('a * 'a)set => ('a multiset * 'a multiset)set"
    4.54 - "mult(r) == (mult1 r)^+"
    4.55 -
    4.56 -locale MSOrd =
    4.57 -  fixes
    4.58 -    r :: "('a * 'a)set"
    4.59 -    W :: "'a multiset set"
    4.60 -
    4.61 -  defines
    4.62 -    W_def       "W == acc(mult1 r)"
    4.63 -
    4.64 -defs
    4.65 -  mult_less_def  "M' < M  ==  (M',M) : mult {(x',x). x'<x}"
    4.66 -  mult_le_def    "M' <= M  ==  M'=M | M' < (M :: 'a multiset)"
    4.67 -
    4.68 -end
     5.1 --- a/src/HOL/Induct/Multiset0.ML	Wed Oct 18 23:35:56 2000 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,11 +0,0 @@
     5.4 -(*  Title:      HOL/Induct/Multiset0.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Nipkow
     5.7 -    Copyright   1998 TUM
     5.8 -
     5.9 -This theory merely proves that the representation of multisets is nonempty.
    5.10 -*)
    5.11 -
    5.12 -Goal "(%x. (0::nat)) : {f. finite {x. 0 < f x}}";
    5.13 -by (Simp_tac 1);
    5.14 -qed "multiset_witness";
     6.1 --- a/src/HOL/Induct/Multiset0.thy	Wed Oct 18 23:35:56 2000 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,9 +0,0 @@
     6.4 -(*  Title:      HOL/Induct/Multiset0.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Tobias Nipkow
     6.7 -    Copyright   1998 TUM
     6.8 -
     6.9 -This theory merely proves that the representation of multisets is nonempty.
    6.10 -*)
    6.11 -
    6.12 -Multiset0 = Main
     7.1 --- a/src/HOL/Induct/MultisetOrder.thy	Wed Oct 18 23:35:56 2000 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,28 +0,0 @@
     7.4 -(*  Title:      HOL/Induct/MultisetOrder.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   2000  University of Cambridge
     7.8 -
     7.9 -Multisets are partially ordered.
    7.10 -*)
    7.11 -
    7.12 -theory MultisetOrder = Multiset:
    7.13 -
    7.14 -instance multiset :: (order) order
    7.15 -  apply intro_classes
    7.16 -     apply (rule mult_le_refl)
    7.17 -    apply (erule mult_le_trans)
    7.18 -    apply assumption
    7.19 -   apply (erule mult_le_antisym)
    7.20 -   apply assumption
    7.21 -  apply (rule mult_less_le)
    7.22 -  done
    7.23 -
    7.24 -instance multiset :: ("term") plus_ac0
    7.25 -  apply intro_classes
    7.26 -    apply (rule union_commute)
    7.27 -   apply (rule union_assoc)
    7.28 -  apply simp
    7.29 -  done
    7.30 -
    7.31 -end