1(* Title: ZF/Induct/Multiset.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 4A definitional theory of multisets, 5including a wellfoundedness proof for the multiset order. 6 7The theory features ordinal multisets and the usual ordering. 8*) 9 10theory Multiset 11imports FoldSet Acc 12begin 13 14abbreviation (input) 15 \<comment> \<open>Short cut for multiset space\<close> 16 Mult :: "i=>i" where 17 "Mult(A) == A -||> nat-{0}" 18 19definition 20 (* This is the original "restrict" from ZF.thy. 21 Restricts the function f to the domain A 22 FIXME: adapt Multiset to the new "restrict". *) 23 funrestrict :: "[i,i] => i" where 24 "funrestrict(f,A) == \<lambda>x \<in> A. f`x" 25 26definition 27 (* M is a multiset *) 28 multiset :: "i => o" where 29 "multiset(M) == \<exists>A. M \<in> A -> nat-{0} & Finite(A)" 30 31definition 32 mset_of :: "i=>i" where 33 "mset_of(M) == domain(M)" 34 35definition 36 munion :: "[i, i] => i" (infixl \<open>+#\<close> 65) where 37 "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N). 38 if x \<in> mset_of(M) \<inter> mset_of(N) then (M`x) #+ (N`x) 39 else (if x \<in> mset_of(M) then M`x else N`x)" 40 41definition 42 (*convert a function to a multiset by eliminating 0*) 43 normalize :: "i => i" where 44 "normalize(f) == 45 if (\<exists>A. f \<in> A -> nat & Finite(A)) then 46 funrestrict(f, {x \<in> mset_of(f). 0 < f`x}) 47 else 0" 48 49definition 50 mdiff :: "[i, i] => i" (infixl \<open>-#\<close> 65) where 51 "M -# N == normalize(\<lambda>x \<in> mset_of(M). 52 if x \<in> mset_of(N) then M`x #- N`x else M`x)" 53 54definition 55 (* set of elements of a multiset *) 56 msingle :: "i => i" (\<open>{#_#}\<close>) where 57 "{#a#} == {<a, 1>}" 58 59definition 60 MCollect :: "[i, i=>o] => i" (*comprehension*) where 61 "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})" 62 63definition 64 (* Counts the number of occurrences of an element in a multiset *) 65 mcount :: "[i, i] => i" where 66 "mcount(M, a) == if a \<in> mset_of(M) then M`a else 0" 67 68definition 69 msize :: "i => i" where 70 "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))" 71 72abbreviation 73 melem :: "[i,i] => o" (\<open>(_/ :# _)\<close> [50, 51] 50) where 74 "a :# M == a \<in> mset_of(M)" 75 76syntax 77 "_MColl" :: "[pttrn, i, o] => i" (\<open>(1{# _ \<in> _./ _#})\<close>) 78translations 79 "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)" 80 81 (* multiset orderings *) 82 83definition 84 (* multirel1 has to be a set (not a predicate) so that we can form 85 its transitive closure and reason about wf(.) and acc(.) *) 86 multirel1 :: "[i,i]=>i" where 87 "multirel1(A, r) == 88 {<M, N> \<in> Mult(A)*Mult(A). 89 \<exists>a \<in> A. \<exists>M0 \<in> Mult(A). \<exists>K \<in> Mult(A). 90 N=M0 +# {#a#} & M=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r)}" 91 92definition 93 multirel :: "[i, i] => i" where 94 "multirel(A, r) == multirel1(A, r)^+" 95 96 (* ordinal multiset orderings *) 97 98definition 99 omultiset :: "i => o" where 100 "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))" 101 102definition 103 mless :: "[i, i] => o" (infixl \<open><#\<close> 50) where 104 "M <# N == \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))" 105 106definition 107 mle :: "[i, i] => o" (infixl \<open><#=\<close> 50) where 108 "M <#= N == (omultiset(M) & M = N) | M <# N" 109 110 111subsection\<open>Properties of the original "restrict" from ZF.thy\<close> 112 113lemma funrestrict_subset: "[| f \<in> Pi(C,B); A\<subseteq>C |] ==> funrestrict(f,A) \<subseteq> f" 114by (auto simp add: funrestrict_def lam_def intro: apply_Pair) 115 116lemma funrestrict_type: 117 "[| !!x. x \<in> A ==> f`x \<in> B(x) |] ==> funrestrict(f,A) \<in> Pi(A,B)" 118by (simp add: funrestrict_def lam_type) 119 120lemma funrestrict_type2: "[| f \<in> Pi(C,B); A\<subseteq>C |] ==> funrestrict(f,A) \<in> Pi(A,B)" 121by (blast intro: apply_type funrestrict_type) 122 123lemma funrestrict [simp]: "a \<in> A ==> funrestrict(f,A) ` a = f`a" 124by (simp add: funrestrict_def) 125 126lemma funrestrict_empty [simp]: "funrestrict(f,0) = 0" 127by (simp add: funrestrict_def) 128 129lemma domain_funrestrict [simp]: "domain(funrestrict(f,C)) = C" 130by (auto simp add: funrestrict_def lam_def) 131 132lemma fun_cons_funrestrict_eq: 133 "f \<in> cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))" 134apply (rule equalityI) 135prefer 2 apply (blast intro: apply_Pair funrestrict_subset [THEN subsetD]) 136apply (auto dest!: Pi_memberD simp add: funrestrict_def lam_def) 137done 138 139declare domain_of_fun [simp] 140declare domainE [rule del] 141 142 143text\<open>A useful simplification rule\<close> 144lemma multiset_fun_iff: 145 "(f \<in> A -> nat-{0}) \<longleftrightarrow> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)" 146apply safe 147apply (rule_tac [4] B1 = "range (f) " in Pi_mono [THEN subsetD]) 148apply (auto intro!: Ord_0_lt 149 dest: apply_type Diff_subset [THEN Pi_mono, THEN subsetD] 150 simp add: range_of_fun apply_iff) 151done 152 153(** The multiset space **) 154lemma multiset_into_Mult: "[| multiset(M); mset_of(M)\<subseteq>A |] ==> M \<in> Mult(A)" 155apply (simp add: multiset_def) 156apply (auto simp add: multiset_fun_iff mset_of_def) 157apply (rule_tac B1 = "nat-{0}" in FiniteFun_mono [THEN subsetD], simp_all) 158apply (rule Finite_into_Fin [THEN [2] Fin_mono [THEN subsetD], THEN fun_FiniteFunI]) 159apply (simp_all (no_asm_simp) add: multiset_fun_iff) 160done 161 162lemma Mult_into_multiset: "M \<in> Mult(A) ==> multiset(M) & mset_of(M)\<subseteq>A" 163apply (simp add: multiset_def mset_of_def) 164apply (frule FiniteFun_is_fun) 165apply (drule FiniteFun_domain_Fin) 166apply (frule FinD, clarify) 167apply (rule_tac x = "domain (M) " in exI) 168apply (blast intro: Fin_into_Finite) 169done 170 171lemma Mult_iff_multiset: "M \<in> Mult(A) \<longleftrightarrow> multiset(M) & mset_of(M)\<subseteq>A" 172by (blast dest: Mult_into_multiset intro: multiset_into_Mult) 173 174lemma multiset_iff_Mult_mset_of: "multiset(M) \<longleftrightarrow> M \<in> Mult(mset_of(M))" 175by (auto simp add: Mult_iff_multiset) 176 177 178text\<open>The \<^term>\<open>multiset\<close> operator\<close> 179 180(* the empty multiset is 0 *) 181 182lemma multiset_0 [simp]: "multiset(0)" 183by (auto intro: FiniteFun.intros simp add: multiset_iff_Mult_mset_of) 184 185 186text\<open>The \<^term>\<open>mset_of\<close> operator\<close> 187 188lemma multiset_set_of_Finite [simp]: "multiset(M) ==> Finite(mset_of(M))" 189by (simp add: multiset_def mset_of_def, auto) 190 191lemma mset_of_0 [iff]: "mset_of(0) = 0" 192by (simp add: mset_of_def) 193 194lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 \<longleftrightarrow> M=0" 195by (auto simp add: multiset_def mset_of_def) 196 197lemma mset_of_single [iff]: "mset_of({#a#}) = {a}" 198by (simp add: msingle_def mset_of_def) 199 200lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) \<union> mset_of(N)" 201by (simp add: mset_of_def munion_def) 202 203lemma mset_of_diff [simp]: "mset_of(M)\<subseteq>A ==> mset_of(M -# N) \<subseteq> A" 204by (auto simp add: mdiff_def multiset_def normalize_def mset_of_def) 205 206(* msingle *) 207 208lemma msingle_not_0 [iff]: "{#a#} \<noteq> 0 & 0 \<noteq> {#a#}" 209by (simp add: msingle_def) 210 211lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) \<longleftrightarrow> (a = b)" 212by (simp add: msingle_def) 213 214lemma msingle_multiset [iff,TC]: "multiset({#a#})" 215apply (simp add: multiset_def msingle_def) 216apply (rule_tac x = "{a}" in exI) 217apply (auto intro: Finite_cons Finite_0 fun_extend3) 218done 219 220(** normalize **) 221 222lemmas Collect_Finite = Collect_subset [THEN subset_Finite] 223 224lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)" 225apply (simp add: normalize_def funrestrict_def mset_of_def) 226apply (case_tac "\<exists>A. f \<in> A -> nat & Finite (A) ") 227apply clarify 228apply (drule_tac x = "{x \<in> domain (f) . 0 < f ` x}" in spec) 229apply auto 230apply (auto intro!: lam_type simp add: Collect_Finite) 231done 232 233lemma normalize_multiset [simp]: "multiset(M) ==> normalize(M) = M" 234by (auto simp add: multiset_def normalize_def mset_of_def funrestrict_def multiset_fun_iff) 235 236lemma multiset_normalize [simp]: "multiset(normalize(f))" 237apply (simp add: normalize_def) 238apply (simp add: normalize_def mset_of_def multiset_def, auto) 239apply (rule_tac x = "{x \<in> A . 0<f`x}" in exI) 240apply (auto intro: Collect_subset [THEN subset_Finite] funrestrict_type) 241done 242 243(** Typechecking rules for union and difference of multisets **) 244 245(* union *) 246 247lemma munion_multiset [simp]: "[| multiset(M); multiset(N) |] ==> multiset(M +# N)" 248apply (unfold multiset_def munion_def mset_of_def, auto) 249apply (rule_tac x = "A \<union> Aa" in exI) 250apply (auto intro!: lam_type intro: Finite_Un simp add: multiset_fun_iff zero_less_add) 251done 252 253(* difference *) 254 255lemma mdiff_multiset [simp]: "multiset(M -# N)" 256by (simp add: mdiff_def) 257 258(** Algebraic properties of multisets **) 259 260(* Union *) 261 262lemma munion_0 [simp]: "multiset(M) ==> M +# 0 = M & 0 +# M = M" 263apply (simp add: multiset_def) 264apply (auto simp add: munion_def mset_of_def) 265done 266 267lemma munion_commute: "M +# N = N +# M" 268by (auto intro!: lam_cong simp add: munion_def) 269 270lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)" 271apply (unfold munion_def mset_of_def) 272apply (rule lam_cong, auto) 273done 274 275lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)" 276apply (unfold munion_def mset_of_def) 277apply (rule lam_cong, auto) 278done 279 280lemmas munion_ac = munion_commute munion_assoc munion_lcommute 281 282(* Difference *) 283 284lemma mdiff_self_eq_0 [simp]: "M -# M = 0" 285by (simp add: mdiff_def normalize_def mset_of_def) 286 287lemma mdiff_0 [simp]: "0 -# M = 0" 288by (simp add: mdiff_def normalize_def) 289 290lemma mdiff_0_right [simp]: "multiset(M) ==> M -# 0 = M" 291by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def) 292 293lemma mdiff_union_inverse2 [simp]: "multiset(M) ==> M +# {#a#} -# {#a#} = M" 294apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def) 295apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1]) 296prefer 2 apply (force intro!: lam_type) 297apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A") 298apply (rule fun_extension, auto) 299apply (drule_tac x = "A \<union> {a}" in spec) 300apply (simp add: Finite_Un) 301apply (force intro!: lam_type) 302done 303 304(** Count of elements **) 305 306lemma mcount_type [simp,TC]: "multiset(M) ==> mcount(M, a) \<in> nat" 307by (auto simp add: multiset_def mcount_def mset_of_def multiset_fun_iff) 308 309lemma mcount_0 [simp]: "mcount(0, a) = 0" 310by (simp add: mcount_def) 311 312lemma mcount_single [simp]: "mcount({#b#}, a) = (if a=b then 1 else 0)" 313by (simp add: mcount_def mset_of_def msingle_def) 314 315lemma mcount_union [simp]: "[| multiset(M); multiset(N) |] 316 ==> mcount(M +# N, a) = mcount(M, a) #+ mcount (N, a)" 317apply (auto simp add: multiset_def multiset_fun_iff mcount_def munion_def mset_of_def) 318done 319 320lemma mcount_diff [simp]: 321 "multiset(M) ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)" 322apply (simp add: multiset_def) 323apply (auto dest!: not_lt_imp_le 324 simp add: mdiff_def multiset_fun_iff mcount_def normalize_def mset_of_def) 325apply (force intro!: lam_type) 326apply (force intro!: lam_type) 327done 328 329lemma mcount_elem: "[| multiset(M); a \<in> mset_of(M) |] ==> 0 < mcount(M, a)" 330apply (simp add: multiset_def, clarify) 331apply (simp add: mcount_def mset_of_def) 332apply (simp add: multiset_fun_iff) 333done 334 335(** msize **) 336 337lemma msize_0 [simp]: "msize(0) = #0" 338by (simp add: msize_def) 339 340lemma msize_single [simp]: "msize({#a#}) = #1" 341by (simp add: msize_def) 342 343lemma msize_type [simp,TC]: "msize(M) \<in> int" 344by (simp add: msize_def) 345 346lemma msize_zpositive: "multiset(M)==> #0 $\<le> msize(M)" 347by (auto simp add: msize_def intro: g_zpos_imp_setsum_zpos) 348 349lemma msize_int_of_nat: "multiset(M) ==> \<exists>n \<in> nat. msize(M)= $# n" 350apply (rule not_zneg_int_of) 351apply (simp_all (no_asm_simp) add: msize_type [THEN znegative_iff_zless_0] not_zless_iff_zle msize_zpositive) 352done 353 354lemma not_empty_multiset_imp_exist: 355 "[| M\<noteq>0; multiset(M) |] ==> \<exists>a \<in> mset_of(M). 0 < mcount(M, a)" 356apply (simp add: multiset_def) 357apply (erule not_emptyE) 358apply (auto simp add: mset_of_def mcount_def multiset_fun_iff) 359apply (blast dest!: fun_is_rel) 360done 361 362lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0" 363apply (simp add: msize_def, auto) 364apply (rule_tac P = "setsum (u,v) \<noteq> #0" for u v in swap) 365apply blast 366apply (drule not_empty_multiset_imp_exist, assumption, clarify) 367apply (subgoal_tac "Finite (mset_of (M) - {a}) ") 368 prefer 2 apply (simp add: Finite_Diff) 369apply (subgoal_tac "setsum (%x. $# mcount (M, x), cons (a, mset_of (M) -{a}))=#0") 370 prefer 2 apply (simp add: cons_Diff, simp) 371apply (subgoal_tac "#0 $\<le> setsum (%x. $# mcount (M, x), mset_of (M) - {a}) ") 372apply (rule_tac [2] g_zpos_imp_setsum_zpos) 373apply (auto simp add: Finite_Diff not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym]) 374apply (rule not_zneg_int_of [THEN bexE]) 375apply (auto simp del: int_of_0 simp add: int_of_add [symmetric] int_of_0 [symmetric]) 376done 377 378lemma setsum_mcount_Int: 379 "Finite(A) ==> setsum(%a. $# mcount(N, a), A \<inter> mset_of(N)) 380 = setsum(%a. $# mcount(N, a), A)" 381apply (induct rule: Finite_induct) 382 apply auto 383apply (subgoal_tac "Finite (B \<inter> mset_of (N))") 384prefer 2 apply (blast intro: subset_Finite) 385apply (auto simp add: mcount_def Int_cons_left) 386done 387 388lemma msize_union [simp]: 389 "[| multiset(M); multiset(N) |] ==> msize(M +# N) = msize(M) $+ msize(N)" 390apply (simp add: msize_def setsum_Un setsum_addf int_of_add setsum_mcount_Int) 391apply (subst Int_commute) 392apply (simp add: setsum_mcount_Int) 393done 394 395lemma msize_eq_succ_imp_elem: "[|msize(M)= $# succ(n); n \<in> nat|] ==> \<exists>a. a \<in> mset_of(M)" 396apply (unfold msize_def) 397apply (blast dest: setsum_succD) 398done 399 400(** Equality of multisets **) 401 402lemma equality_lemma: 403 "[| multiset(M); multiset(N); \<forall>a. mcount(M, a)=mcount(N, a) |] 404 ==> mset_of(M)=mset_of(N)" 405apply (simp add: multiset_def) 406apply (rule sym, rule equalityI) 407apply (auto simp add: multiset_fun_iff mcount_def mset_of_def) 408apply (drule_tac [!] x=x in spec) 409apply (case_tac [2] "x \<in> Aa", case_tac "x \<in> A", auto) 410done 411 412lemma multiset_equality: 413 "[| multiset(M); multiset(N) |]==> M=N\<longleftrightarrow>(\<forall>a. mcount(M, a)=mcount(N, a))" 414apply auto 415apply (subgoal_tac "mset_of (M) = mset_of (N) ") 416prefer 2 apply (blast intro: equality_lemma) 417apply (simp add: multiset_def mset_of_def) 418apply (auto simp add: multiset_fun_iff) 419apply (rule fun_extension) 420apply (blast, blast) 421apply (drule_tac x = x in spec) 422apply (auto simp add: mcount_def mset_of_def) 423done 424 425(** More algebraic properties of multisets **) 426 427lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) \<longleftrightarrow> (M=0 & N=0)" 428by (auto simp add: multiset_equality) 429 430lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) \<longleftrightarrow> (M=0 & N=0)" 431apply (rule iffI, drule sym) 432apply (simp_all add: multiset_equality) 433done 434 435lemma munion_right_cancel [simp]: 436 "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)\<longleftrightarrow>(M=N)" 437by (auto simp add: multiset_equality) 438 439lemma munion_left_cancel [simp]: 440 "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) \<longleftrightarrow> (M = N)" 441by (auto simp add: multiset_equality) 442 443lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) \<longleftrightarrow> (m=1 & n=0) | (m=0 & n=1)" 444by (induct_tac n) auto 445 446lemma munion_is_single: 447 "[|multiset(M); multiset(N)|] 448 ==> (M +# N = {#a#}) \<longleftrightarrow> (M={#a#} & N=0) | (M = 0 & N = {#a#})" 449apply (simp (no_asm_simp) add: multiset_equality) 450apply safe 451apply simp_all 452apply (case_tac "aa=a") 453apply (drule_tac [2] x = aa in spec) 454apply (drule_tac x = a in spec) 455apply (simp add: nat_add_eq_1_cases, simp) 456apply (case_tac "aaa=aa", simp) 457apply (drule_tac x = aa in spec) 458apply (simp add: nat_add_eq_1_cases) 459apply (case_tac "aaa=a") 460apply (drule_tac [4] x = aa in spec) 461apply (drule_tac [3] x = a in spec) 462apply (drule_tac [2] x = aaa in spec) 463apply (drule_tac x = aa in spec) 464apply (simp_all add: nat_add_eq_1_cases) 465done 466 467lemma msingle_is_union: "[| multiset(M); multiset(N) |] 468 ==> ({#a#} = M +# N) \<longleftrightarrow> ({#a#} = M & N=0 | M = 0 & {#a#} = N)" 469apply (subgoal_tac " ({#a#} = M +# N) \<longleftrightarrow> (M +# N = {#a#}) ") 470apply (simp (no_asm_simp) add: munion_is_single) 471apply blast 472apply (blast dest: sym) 473done 474 475(** Towards induction over multisets **) 476 477lemma setsum_decr: 478"Finite(A) 479 ==> (\<forall>M. multiset(M) \<longrightarrow> 480 (\<forall>a \<in> mset_of(M). setsum(%z. $# mcount(M(a:=M`a #- 1), z), A) = 481 (if a \<in> A then setsum(%z. $# mcount(M, z), A) $- #1 482 else setsum(%z. $# mcount(M, z), A))))" 483apply (unfold multiset_def) 484apply (erule Finite_induct) 485apply (auto simp add: multiset_fun_iff) 486apply (unfold mset_of_def mcount_def) 487apply (case_tac "x \<in> A", auto) 488apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1") 489apply (erule ssubst) 490apply (rule int_of_diff, auto) 491done 492 493lemma setsum_decr2: 494 "Finite(A) 495 ==> \<forall>M. multiset(M) \<longrightarrow> (\<forall>a \<in> mset_of(M). 496 setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) = 497 (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a 498 else setsum(%x. $# mcount(M, x), A)))" 499apply (simp add: multiset_def) 500apply (erule Finite_induct) 501apply (auto simp add: multiset_fun_iff mcount_def mset_of_def) 502done 503 504lemma setsum_decr3: "[| Finite(A); multiset(M); a \<in> mset_of(M) |] 505 ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) = 506 (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a 507 else setsum(%x. $# mcount(M, x), A))" 508apply (subgoal_tac "setsum (%x. $# mcount (funrestrict (M, mset_of (M) -{a}),x),A-{a}) = setsum (%x. $# mcount (funrestrict (M, mset_of (M) -{a}),x),A) ") 509apply (rule_tac [2] setsum_Diff [symmetric]) 510apply (rule sym, rule ssubst, blast) 511apply (rule sym, drule setsum_decr2, auto) 512apply (simp add: mcount_def mset_of_def) 513done 514 515lemma nat_le_1_cases: "n \<in> nat ==> n \<le> 1 \<longleftrightarrow> (n=0 | n=1)" 516by (auto elim: natE) 517 518lemma succ_pred_eq_self: "[| 0<n; n \<in> nat |] ==> succ(n #- 1) = n" 519apply (subgoal_tac "1 \<le> n") 520apply (drule add_diff_inverse2, auto) 521done 522 523text\<open>Specialized for use in the proof below.\<close> 524lemma multiset_funrestict: 525 "\<lbrakk>\<forall>a\<in>A. M ` a \<in> nat \<and> 0 < M ` a; Finite(A)\<rbrakk> 526 \<Longrightarrow> multiset(funrestrict(M, A - {a}))" 527apply (simp add: multiset_def multiset_fun_iff) 528apply (rule_tac x="A-{a}" in exI) 529apply (auto intro: Finite_Diff funrestrict_type) 530done 531 532lemma multiset_induct_aux: 533 assumes prem1: "!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))" 534 and prem2: "!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))" 535 shows 536 "[| n \<in> nat; P(0) |] 537 ==> (\<forall>M. multiset(M)\<longrightarrow> 538 (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) \<longrightarrow> P(M))" 539apply (erule nat_induct, clarify) 540apply (frule msize_eq_0_iff) 541apply (auto simp add: mset_of_def multiset_def multiset_fun_iff msize_def) 542apply (subgoal_tac "setsum (%x. $# mcount (M, x), A) =$# succ (x) ") 543apply (drule setsum_succD, auto) 544apply (case_tac "1 <M`a") 545apply (drule_tac [2] not_lt_imp_le) 546apply (simp_all add: nat_le_1_cases) 547apply (subgoal_tac "M= (M (a:=M`a #- 1)) (a:= (M (a:=M`a #- 1))`a #+ 1) ") 548apply (rule_tac [2] A = A and B = "%x. nat" and D = "%x. nat" in fun_extension) 549apply (rule_tac [3] update_type)+ 550apply (simp_all (no_asm_simp)) 551 apply (rule_tac [2] impI) 552 apply (rule_tac [2] succ_pred_eq_self [symmetric]) 553apply (simp_all (no_asm_simp)) 554apply (rule subst, rule sym, blast, rule prem2) 555apply (simp (no_asm) add: multiset_def multiset_fun_iff) 556apply (rule_tac x = A in exI) 557apply (force intro: update_type) 558apply (simp (no_asm_simp) add: mset_of_def mcount_def) 559apply (drule_tac x = "M (a := M ` a #- 1) " in spec) 560apply (drule mp, drule_tac [2] mp, simp_all) 561apply (rule_tac x = A in exI) 562apply (auto intro: update_type) 563apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}) ") 564prefer 2 apply (blast intro: Collect_subset [THEN subset_Finite] Finite_cons) 565apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}" in setsum_decr) 566apply (drule_tac x = M in spec) 567apply (subgoal_tac "multiset (M) ") 568 prefer 2 569 apply (simp add: multiset_def multiset_fun_iff) 570 apply (rule_tac x = A in exI, force) 571apply (simp_all add: mset_of_def) 572apply (drule_tac psi = "\<forall>x \<in> A. u(x)" for u in asm_rl) 573apply (drule_tac x = a in bspec) 574apply (simp (no_asm_simp)) 575apply (subgoal_tac "cons (a, A) = A") 576prefer 2 apply blast 577apply simp 578apply (subgoal_tac "M=cons (<a, M`a>, funrestrict (M, A-{a}))") 579 prefer 2 580 apply (rule fun_cons_funrestrict_eq) 581 apply (subgoal_tac "cons (a, A-{a}) = A") 582 apply force 583 apply force 584apply (rule_tac a = "cons (<a, 1>, funrestrict (M, A - {a}))" in ssubst) 585apply simp 586apply (frule multiset_funrestict, assumption) 587apply (rule prem1, assumption) 588apply (simp add: mset_of_def) 589apply (drule_tac x = "funrestrict (M, A-{a}) " in spec) 590apply (drule mp) 591apply (rule_tac x = "A-{a}" in exI) 592apply (auto intro: Finite_Diff funrestrict_type simp add: funrestrict) 593apply (frule_tac A = A and M = M and a = a in setsum_decr3) 594apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff) 595apply blast 596apply (simp (no_asm_simp) add: mset_of_def) 597apply (drule_tac b = "if u then v else w" for u v w in sym, simp_all) 598apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}") 599apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def) 600done 601 602lemma multiset_induct2: 603 "[| multiset(M); P(0); 604 (!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))); 605 (!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))) |] 606 ==> P(M)" 607apply (subgoal_tac "\<exists>n \<in> nat. setsum (\<lambda>x. $# mcount (M, x), {x \<in> mset_of (M) . 0 < M ` x}) = $# n") 608apply (rule_tac [2] not_zneg_int_of) 609apply (simp_all (no_asm_simp) add: znegative_iff_zless_0 not_zless_iff_zle) 610apply (rule_tac [2] g_zpos_imp_setsum_zpos) 611prefer 2 apply (blast intro: multiset_set_of_Finite Collect_subset [THEN subset_Finite]) 612 prefer 2 apply (simp add: multiset_def multiset_fun_iff, clarify) 613apply (rule multiset_induct_aux [rule_format], auto) 614done 615 616lemma munion_single_case1: 617 "[| multiset(M); a \<notin>mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)" 618apply (simp add: multiset_def msingle_def) 619apply (auto simp add: munion_def) 620apply (unfold mset_of_def, simp) 621apply (rule fun_extension, rule lam_type, simp_all) 622apply (auto simp add: multiset_fun_iff fun_extend_apply) 623apply (drule_tac c = a and b = 1 in fun_extend3) 624apply (auto simp add: cons_eq Un_commute [of _ "{a}"]) 625done 626 627lemma munion_single_case2: 628 "[| multiset(M); a \<in> mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)" 629apply (simp add: multiset_def) 630apply (auto simp add: munion_def multiset_fun_iff msingle_def) 631apply (unfold mset_of_def, simp) 632apply (subgoal_tac "A \<union> {a} = A") 633apply (rule fun_extension) 634apply (auto dest: domain_type intro: lam_type update_type) 635done 636 637(* Induction principle for multisets *) 638 639lemma multiset_induct: 640 assumes M: "multiset(M)" 641 and P0: "P(0)" 642 and step: "!!M a. [| multiset(M); P(M) |] ==> P(M +# {#a#})" 643 shows "P(M)" 644apply (rule multiset_induct2 [OF M]) 645apply (simp_all add: P0) 646apply (frule_tac [2] a = b in munion_single_case2 [symmetric]) 647apply (frule_tac a = a in munion_single_case1 [symmetric]) 648apply (auto intro: step) 649done 650 651(** MCollect **) 652 653lemma MCollect_multiset [simp]: 654 "multiset(M) ==> multiset({# x \<in> M. P(x)#})" 655apply (simp add: MCollect_def multiset_def mset_of_def, clarify) 656apply (rule_tac x = "{x \<in> A. P (x) }" in exI) 657apply (auto dest: CollectD1 [THEN [2] apply_type] 658 intro: Collect_subset [THEN subset_Finite] funrestrict_type) 659done 660 661lemma mset_of_MCollect [simp]: 662 "multiset(M) ==> mset_of({# x \<in> M. P(x) #}) \<subseteq> mset_of(M)" 663by (auto simp add: mset_of_def MCollect_def multiset_def funrestrict_def) 664 665lemma MCollect_mem_iff [iff]: 666 "x \<in> mset_of({#x \<in> M. P(x)#}) \<longleftrightarrow> x \<in> mset_of(M) & P(x)" 667by (simp add: MCollect_def mset_of_def) 668 669lemma mcount_MCollect [simp]: 670 "mcount({# x \<in> M. P(x) #}, a) = (if P(a) then mcount(M,a) else 0)" 671by (simp add: mcount_def MCollect_def mset_of_def) 672 673lemma multiset_partition: "multiset(M) ==> M = {# x \<in> M. P(x) #} +# {# x \<in> M. ~ P(x) #}" 674by (simp add: multiset_equality) 675 676lemma natify_elem_is_self [simp]: 677 "[| multiset(M); a \<in> mset_of(M) |] ==> natify(M`a) = M`a" 678by (auto simp add: multiset_def mset_of_def multiset_fun_iff) 679 680(* and more algebraic laws on multisets *) 681 682lemma munion_eq_conv_diff: "[| multiset(M); multiset(N) |] 683 ==> (M +# {#a#} = N +# {#b#}) \<longleftrightarrow> (M = N & a = b | 684 M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})" 685apply (simp del: mcount_single add: multiset_equality) 686apply (rule iffI, erule_tac [2] disjE, erule_tac [3] conjE) 687apply (case_tac "a=b", auto) 688apply (drule_tac x = a in spec) 689apply (drule_tac [2] x = b in spec) 690apply (drule_tac [3] x = aa in spec) 691apply (drule_tac [4] x = a in spec, auto) 692apply (subgoal_tac [!] "mcount (N,a) :nat") 693apply (erule_tac [3] natE, erule natE, auto) 694done 695 696lemma melem_diff_single: 697"multiset(M) ==> 698 k \<in> mset_of(M -# {#a#}) \<longleftrightarrow> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))" 699apply (simp add: multiset_def) 700apply (simp add: normalize_def mset_of_def msingle_def mdiff_def mcount_def) 701apply (auto dest: domain_type intro: zero_less_diff [THEN iffD1] 702 simp add: multiset_fun_iff apply_iff) 703apply (force intro!: lam_type) 704apply (force intro!: lam_type) 705apply (force intro!: lam_type) 706done 707 708lemma munion_eq_conv_exist: 709"[| M \<in> Mult(A); N \<in> Mult(A) |] 710 ==> (M +# {#a#} = N +# {#b#}) \<longleftrightarrow> 711 (M=N & a=b | (\<exists>K \<in> Mult(A). M= K +# {#b#} & N=K +# {#a#}))" 712by (auto simp add: Mult_iff_multiset melem_diff_single munion_eq_conv_diff) 713 714 715subsection\<open>Multiset Orderings\<close> 716 717(* multiset on a domain A are finite functions from A to nat-{0} *) 718 719 720(* multirel1 type *) 721 722lemma multirel1_type: "multirel1(A, r) \<subseteq> Mult(A)*Mult(A)" 723by (auto simp add: multirel1_def) 724 725lemma multirel1_0 [simp]: "multirel1(0, r) =0" 726by (auto simp add: multirel1_def) 727 728lemma multirel1_iff: 729" <N, M> \<in> multirel1(A, r) \<longleftrightarrow> 730 (\<exists>a. a \<in> A & 731 (\<exists>M0. M0 \<in> Mult(A) & (\<exists>K. K \<in> Mult(A) & 732 M=M0 +# {#a#} & N=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r))))" 733by (auto simp add: multirel1_def Mult_iff_multiset Bex_def) 734 735 736text\<open>Monotonicity of \<^term>\<open>multirel1\<close>\<close> 737 738lemma multirel1_mono1: "A\<subseteq>B ==> multirel1(A, r)\<subseteq>multirel1(B, r)" 739apply (auto simp add: multirel1_def) 740apply (auto simp add: Un_subset_iff Mult_iff_multiset) 741apply (rule_tac x = a in bexI) 742apply (rule_tac x = M0 in bexI, simp) 743apply (rule_tac x = K in bexI) 744apply (auto simp add: Mult_iff_multiset) 745done 746 747lemma multirel1_mono2: "r\<subseteq>s ==> multirel1(A,r)\<subseteq>multirel1(A, s)" 748apply (simp add: multirel1_def, auto) 749apply (rule_tac x = a in bexI) 750apply (rule_tac x = M0 in bexI) 751apply (simp_all add: Mult_iff_multiset) 752apply (rule_tac x = K in bexI) 753apply (simp_all add: Mult_iff_multiset, auto) 754done 755 756lemma multirel1_mono: 757 "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel1(A, r) \<subseteq> multirel1(B, s)" 758apply (rule subset_trans) 759apply (rule multirel1_mono1) 760apply (rule_tac [2] multirel1_mono2, auto) 761done 762 763subsection\<open>Toward the proof of well-foundedness of multirel1\<close> 764 765lemma not_less_0 [iff]: "<M,0> \<notin> multirel1(A, r)" 766by (auto simp add: multirel1_def Mult_iff_multiset) 767 768lemma less_munion: "[| <N, M0 +# {#a#}> \<in> multirel1(A, r); M0 \<in> Mult(A) |] ==> 769 (\<exists>M. <M, M0> \<in> multirel1(A, r) & N = M +# {#a#}) | 770 (\<exists>K. K \<in> Mult(A) & (\<forall>b \<in> mset_of(K). <b, a> \<in> r) & N = M0 +# K)" 771apply (frule multirel1_type [THEN subsetD]) 772apply (simp add: multirel1_iff) 773apply (auto simp add: munion_eq_conv_exist) 774apply (rule_tac x="Ka +# K" in exI, auto, simp add: Mult_iff_multiset) 775apply (simp (no_asm_simp) add: munion_left_cancel munion_assoc) 776apply (auto simp add: munion_commute) 777done 778 779lemma multirel1_base: "[| M \<in> Mult(A); a \<in> A |] ==> <M, M +# {#a#}> \<in> multirel1(A, r)" 780apply (auto simp add: multirel1_iff) 781apply (simp add: Mult_iff_multiset) 782apply (rule_tac x = a in exI, clarify) 783apply (rule_tac x = M in exI, simp) 784apply (rule_tac x = 0 in exI, auto) 785done 786 787lemma acc_0: "acc(0)=0" 788by (auto intro!: equalityI dest: acc.dom_subset [THEN subsetD]) 789 790lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r \<longrightarrow> 791 (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r))); 792 M0 \<in> acc(multirel1(A, r)); a \<in> A; 793 \<forall>M. <M,M0> \<in> multirel1(A, r) \<longrightarrow> M +# {#a#} \<in> acc(multirel1(A, r)) |] 794 ==> M0 +# {#a#} \<in> acc(multirel1(A, r))" 795apply (subgoal_tac "M0 \<in> Mult(A) ") 796 prefer 2 797 apply (erule acc.cases) 798 apply (erule fieldE) 799 apply (auto dest: multirel1_type [THEN subsetD]) 800apply (rule accI) 801apply (rename_tac "N") 802apply (drule less_munion, blast) 803apply (auto simp add: Mult_iff_multiset) 804apply (erule_tac P = "\<forall>x \<in> mset_of (K) . <x, a> \<in> r" in rev_mp) 805apply (erule_tac P = "mset_of (K) \<subseteq>A" in rev_mp) 806apply (erule_tac M = K in multiset_induct) 807(* three subgoals *) 808(* subgoal 1 \<in> the induction base case *) 809apply (simp (no_asm_simp)) 810(* subgoal 2 \<in> the induction general case *) 811apply (simp add: Ball_def Un_subset_iff, clarify) 812apply (drule_tac x = aa in spec, simp) 813apply (subgoal_tac "aa \<in> A") 814prefer 2 apply blast 815apply (drule_tac x = "M0 +# M" and P = 816 "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> Q(x)" for Q in spec) 817apply (simp add: munion_assoc [symmetric]) 818(* subgoal 3 \<in> additional conditions *) 819apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset) 820done 821 822lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r 823 \<longrightarrow> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r))); 824 M \<in> acc(multirel1(A, r)); a \<in> A|] ==> M +# {#a#} \<in> acc(multirel1(A, r))" 825apply (erule acc_induct) 826apply (blast intro: lemma1) 827done 828 829lemma lemma3: "[| wf[A](r); a \<in> A |] 830 ==> \<forall>M \<in> acc(multirel1(A, r)). M +# {#a#} \<in> acc(multirel1(A, r))" 831apply (erule_tac a = a in wf_on_induct, blast) 832apply (blast intro: lemma2) 833done 834 835lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A \<longrightarrow> 836 wf[A](r) \<longrightarrow> M \<in> field(multirel1(A, r)) \<longrightarrow> M \<in> acc(multirel1(A, r))" 837apply (erule multiset_induct) 838(* proving the base case *) 839apply clarify 840apply (rule accI, force) 841apply (simp add: multirel1_def) 842(* Proving the general case *) 843apply clarify 844apply simp 845apply (subgoal_tac "mset_of (M) \<subseteq>A") 846prefer 2 apply blast 847apply clarify 848apply (drule_tac a = a in lemma3, blast) 849apply (subgoal_tac "M \<in> field (multirel1 (A,r))") 850apply blast 851apply (rule multirel1_base [THEN fieldI1]) 852apply (auto simp add: Mult_iff_multiset) 853done 854 855lemma all_accessible: "[| wf[A](r); M \<in> Mult(A); A \<noteq> 0|] ==> M \<in> acc(multirel1(A, r))" 856apply (erule not_emptyE) 857apply (rule lemma4 [THEN mp, THEN mp, THEN mp]) 858apply (rule_tac [4] multirel1_base [THEN fieldI1]) 859apply (auto simp add: Mult_iff_multiset) 860done 861 862lemma wf_on_multirel1: "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))" 863apply (case_tac "A=0") 864apply (simp (no_asm_simp)) 865apply (rule wf_imp_wf_on) 866apply (rule wf_on_field_imp_wf) 867apply (simp (no_asm_simp) add: wf_on_0) 868apply (rule_tac A = "acc (multirel1 (A,r))" in wf_on_subset_A) 869apply (rule wf_on_acc) 870apply (blast intro: all_accessible) 871done 872 873lemma wf_multirel1: "wf(r) ==>wf(multirel1(field(r), r))" 874apply (simp (no_asm_use) add: wf_iff_wf_on_field) 875apply (drule wf_on_multirel1) 876apply (rule_tac A = "field (r) -||> nat - {0}" in wf_on_subset_A) 877apply (simp (no_asm_simp)) 878apply (rule field_rel_subset) 879apply (rule multirel1_type) 880done 881 882(** multirel **) 883 884lemma multirel_type: "multirel(A, r) \<subseteq> Mult(A)*Mult(A)" 885apply (simp add: multirel_def) 886apply (rule trancl_type [THEN subset_trans]) 887apply (auto dest: multirel1_type [THEN subsetD]) 888done 889 890(* Monotonicity of multirel *) 891lemma multirel_mono: 892 "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel(A, r)\<subseteq>multirel(B,s)" 893apply (simp add: multirel_def) 894apply (rule trancl_mono) 895apply (rule multirel1_mono, auto) 896done 897 898(* Equivalence of multirel with the usual (closure-free) definition *) 899 900lemma add_diff_eq: "k \<in> nat ==> 0 < k \<longrightarrow> n #+ k #- 1 = n #+ (k #- 1)" 901by (erule nat_induct, auto) 902 903lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |] 904 ==> I +# J -# {#a#} = I +# (J-# {#a#})" 905apply (simp (no_asm_simp) add: multiset_equality) 906apply (case_tac "a \<notin> mset_of (I) ") 907apply (auto simp add: mcount_def mset_of_def multiset_def multiset_fun_iff) 908apply (auto dest: domain_type simp add: add_diff_eq) 909done 910 911lemma diff_add_commute: "[| n \<le> m; m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n" 912by (auto simp add: le_iff less_iff_succ_add) 913 914(* One direction *) 915 916lemma multirel_implies_one_step: 917"<M,N> \<in> multirel(A, r) ==> 918 trans[A](r) \<longrightarrow> 919 (\<exists>I J K. 920 I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) & 921 N = I +# J & M = I +# K & J \<noteq> 0 & 922 (\<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r))" 923apply (simp add: multirel_def Ball_def Bex_def) 924apply (erule converse_trancl_induct) 925apply (simp_all add: multirel1_iff Mult_iff_multiset) 926(* Two subgoals remain *) 927(* Subgoal 1 *) 928apply clarify 929apply (rule_tac x = M0 in exI, force) 930(* Subgoal 2 *) 931apply clarify 932apply hypsubst_thin 933apply (case_tac "a \<in> mset_of (Ka) ") 934apply (rule_tac x = I in exI, simp (no_asm_simp)) 935apply (rule_tac x = J in exI, simp (no_asm_simp)) 936apply (rule_tac x = " (Ka -# {#a#}) +# K" in exI, simp (no_asm_simp)) 937apply (simp_all add: Un_subset_iff) 938apply (simp (no_asm_simp) add: munion_assoc [symmetric]) 939apply (drule_tac t = "%M. M-#{#a#}" in subst_context) 940apply (simp add: mdiff_union_single_conv melem_diff_single, clarify) 941apply (erule disjE, simp) 942apply (erule disjE, simp) 943apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> Q(x)" for Q in spec) 944apply clarify 945apply (rule_tac x = xa in exI) 946apply (simp (no_asm_simp)) 947apply (blast dest: trans_onD) 948(* new we know that a\<notin>mset_of(Ka) *) 949apply (subgoal_tac "a :# I") 950apply (rule_tac x = "I-#{#a#}" in exI, simp (no_asm_simp)) 951apply (rule_tac x = "J+#{#a#}" in exI) 952apply (simp (no_asm_simp) add: Un_subset_iff) 953apply (rule_tac x = "Ka +# K" in exI) 954apply (simp (no_asm_simp) add: Un_subset_iff) 955apply (rule conjI) 956apply (simp (no_asm_simp) add: multiset_equality mcount_elem [THEN succ_pred_eq_self]) 957apply (rule conjI) 958apply (drule_tac t = "%M. M-#{#a#}" in subst_context) 959apply (simp add: mdiff_union_inverse2) 960apply (simp_all (no_asm_simp) add: multiset_equality) 961apply (rule diff_add_commute [symmetric]) 962apply (auto intro: mcount_elem) 963apply (subgoal_tac "a \<in> mset_of (I +# Ka) ") 964apply (drule_tac [2] sym, auto) 965done 966 967lemma melem_imp_eq_diff_union [simp]: "[| a \<in> mset_of(M); multiset(M) |] ==> M -# {#a#} +# {#a#} = M" 968by (simp add: multiset_equality mcount_elem [THEN succ_pred_eq_self]) 969 970lemma msize_eq_succ_imp_eq_union: 971 "[| msize(M)=$# succ(n); M \<in> Mult(A); n \<in> nat |] 972 ==> \<exists>a N. M = N +# {#a#} & N \<in> Mult(A) & a \<in> A" 973apply (drule msize_eq_succ_imp_elem, auto) 974apply (rule_tac x = a in exI) 975apply (rule_tac x = "M -# {#a#}" in exI) 976apply (frule Mult_into_multiset) 977apply (simp (no_asm_simp)) 978apply (auto simp add: Mult_iff_multiset) 979done 980 981(* The second direction *) 982 983lemma one_step_implies_multirel_lemma [rule_format (no_asm)]: 984"n \<in> nat ==> 985 (\<forall>I J K. 986 I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) & 987 (msize(J) = $# n & J \<noteq>0 & (\<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k, j> \<in> r)) 988 \<longrightarrow> <I +# K, I +# J> \<in> multirel(A, r))" 989apply (simp add: Mult_iff_multiset) 990apply (erule nat_induct, clarify) 991apply (drule_tac M = J in msize_eq_0_iff, auto) 992(* one subgoal remains *) 993apply (subgoal_tac "msize (J) =$# succ (x) ") 994 prefer 2 apply simp 995apply (frule_tac A = A in msize_eq_succ_imp_eq_union) 996apply (simp_all add: Mult_iff_multiset, clarify) 997apply (rename_tac "J'", simp) 998apply (case_tac "J' = 0") 999apply (simp add: multirel_def) 1000apply (rule r_into_trancl, clarify) 1001apply (simp add: multirel1_iff Mult_iff_multiset, force) 1002(*Now we know J' \<noteq> 0*) 1003apply (drule sym, rotate_tac -1, simp) 1004apply (erule_tac V = "$# x = msize (J') " in thin_rl) 1005apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition) 1006apply (erule_tac P = "\<forall>k \<in> mset_of (K) . P(k)" for P in rev_mp) 1007apply (erule ssubst) 1008apply (simp add: Ball_def, auto) 1009apply (subgoal_tac "< (I +# {# x \<in> K. <x, a> \<in> r#}) +# {# x \<in> K. <x, a> \<notin> r#}, (I +# {# x \<in> K. <x, a> \<in> r#}) +# J'> \<in> multirel(A, r) ") 1010 prefer 2 1011 apply (drule_tac x = "I +# {# x \<in> K. <x, a> \<in> r#}" in spec) 1012 apply (rotate_tac -1) 1013 apply (drule_tac x = "J'" in spec) 1014 apply (rotate_tac -1) 1015 apply (drule_tac x = "{# x \<in> K. <x, a> \<notin> r#}" in spec, simp) apply blast 1016apply (simp add: munion_assoc [symmetric] multirel_def) 1017apply (rule_tac b = "I +# {# x \<in> K. <x, a> \<in> r#} +# J'" in trancl_trans, blast) 1018apply (rule r_into_trancl) 1019apply (simp add: multirel1_iff Mult_iff_multiset) 1020apply (rule_tac x = a in exI) 1021apply (simp (no_asm_simp)) 1022apply (rule_tac x = "I +# J'" in exI) 1023apply (auto simp add: munion_ac Un_subset_iff) 1024done 1025 1026lemma one_step_implies_multirel: 1027 "[| J \<noteq> 0; \<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r; 1028 I \<in> Mult(A); J \<in> Mult(A); K \<in> Mult(A) |] 1029 ==> <I+#K, I+#J> \<in> multirel(A, r)" 1030apply (subgoal_tac "multiset (J) ") 1031 prefer 2 apply (simp add: Mult_iff_multiset) 1032apply (frule_tac M = J in msize_int_of_nat) 1033apply (auto intro: one_step_implies_multirel_lemma) 1034done 1035 1036(** Proving that multisets are partially ordered **) 1037 1038(*irreflexivity*) 1039 1040lemma multirel_irrefl_lemma: 1041 "Finite(A) ==> part_ord(A, r) \<longrightarrow> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) \<longrightarrow>A=0" 1042apply (erule Finite_induct) 1043apply (auto dest: subset_consI [THEN [2] part_ord_subset]) 1044apply (auto simp add: part_ord_def irrefl_def) 1045apply (drule_tac x = xa in bspec) 1046apply (drule_tac [2] a = xa and b = x in trans_onD, auto) 1047done 1048 1049lemma irrefl_on_multirel: 1050 "part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))" 1051apply (simp add: irrefl_def) 1052apply (subgoal_tac "trans[A](r) ") 1053 prefer 2 apply (simp add: part_ord_def, clarify) 1054apply (drule multirel_implies_one_step, clarify) 1055apply (simp add: Mult_iff_multiset, clarify) 1056apply (subgoal_tac "Finite (mset_of (K))") 1057apply (frule_tac r = r in multirel_irrefl_lemma) 1058apply (frule_tac B = "mset_of (K) " in part_ord_subset) 1059apply simp_all 1060apply (auto simp add: multiset_def mset_of_def) 1061done 1062 1063lemma trans_on_multirel: "trans[Mult(A)](multirel(A, r))" 1064apply (simp add: multirel_def trans_on_def) 1065apply (blast intro: trancl_trans) 1066done 1067 1068lemma multirel_trans: 1069 "[| <M, N> \<in> multirel(A, r); <N, K> \<in> multirel(A, r) |] ==> <M, K> \<in> multirel(A,r)" 1070apply (simp add: multirel_def) 1071apply (blast intro: trancl_trans) 1072done 1073 1074lemma trans_multirel: "trans(multirel(A,r))" 1075apply (simp add: multirel_def) 1076apply (rule trans_trancl) 1077done 1078 1079lemma part_ord_multirel: "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))" 1080apply (simp (no_asm) add: part_ord_def) 1081apply (blast intro: irrefl_on_multirel trans_on_multirel) 1082done 1083 1084(** Monotonicity of multiset union **) 1085 1086lemma munion_multirel1_mono: 1087"[|<M,N> \<in> multirel1(A, r); K \<in> Mult(A) |] ==> <K +# M, K +# N> \<in> multirel1(A, r)" 1088apply (frule multirel1_type [THEN subsetD]) 1089apply (auto simp add: multirel1_iff Mult_iff_multiset) 1090apply (rule_tac x = a in exI) 1091apply (simp (no_asm_simp)) 1092apply (rule_tac x = "K+#M0" in exI) 1093apply (simp (no_asm_simp) add: Un_subset_iff) 1094apply (rule_tac x = Ka in exI) 1095apply (simp (no_asm_simp) add: munion_assoc) 1096done 1097 1098lemma munion_multirel_mono2: 1099 "[| <M, N> \<in> multirel(A, r); K \<in> Mult(A) |]==><K +# M, K +# N> \<in> multirel(A, r)" 1100apply (frule multirel_type [THEN subsetD]) 1101apply (simp (no_asm_use) add: multirel_def) 1102apply clarify 1103apply (drule_tac psi = "<M,N> \<in> multirel1 (A, r) ^+" in asm_rl) 1104apply (erule rev_mp) 1105apply (erule rev_mp) 1106apply (erule rev_mp) 1107apply (erule trancl_induct, clarify) 1108apply (blast intro: munion_multirel1_mono r_into_trancl, clarify) 1109apply (subgoal_tac "y \<in> Mult(A) ") 1110 prefer 2 1111 apply (blast dest: multirel_type [unfolded multirel_def, THEN subsetD]) 1112apply (subgoal_tac "<K +# y, K +# z> \<in> multirel1 (A, r) ") 1113prefer 2 apply (blast intro: munion_multirel1_mono) 1114apply (blast intro: r_into_trancl trancl_trans) 1115done 1116 1117lemma munion_multirel_mono1: 1118 "[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)" 1119apply (frule multirel_type [THEN subsetD]) 1120apply (rule_tac P = "%x. <x,u> \<in> multirel(A, r)" for u in munion_commute [THEN subst]) 1121apply (subst munion_commute [of N]) 1122apply (rule munion_multirel_mono2) 1123apply (auto simp add: Mult_iff_multiset) 1124done 1125 1126lemma munion_multirel_mono: 1127 "[|<M,K> \<in> multirel(A, r); <N,L> \<in> multirel(A, r)|] 1128 ==> <M +# N, K +# L> \<in> multirel(A, r)" 1129apply (subgoal_tac "M \<in> Mult(A) & N \<in> Mult(A) & K \<in> Mult(A) & L \<in> Mult(A) ") 1130prefer 2 apply (blast dest: multirel_type [THEN subsetD]) 1131apply (blast intro: munion_multirel_mono1 multirel_trans munion_multirel_mono2) 1132done 1133 1134 1135subsection\<open>Ordinal Multisets\<close> 1136 1137(* A \<subseteq> B ==> field(Memrel(A)) \<subseteq> field(Memrel(B)) *) 1138lemmas field_Memrel_mono = Memrel_mono [THEN field_mono] 1139 1140(* 1141[| Aa \<subseteq> Ba; A \<subseteq> B |] ==> 1142multirel(field(Memrel(Aa)), Memrel(A))\<subseteq> multirel(field(Memrel(Ba)), Memrel(B)) 1143*) 1144 1145lemmas multirel_Memrel_mono = multirel_mono [OF field_Memrel_mono Memrel_mono] 1146 1147lemma omultiset_is_multiset [simp]: "omultiset(M) ==> multiset(M)" 1148apply (simp add: omultiset_def) 1149apply (auto simp add: Mult_iff_multiset) 1150done 1151 1152lemma munion_omultiset [simp]: "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)" 1153apply (simp add: omultiset_def, clarify) 1154apply (rule_tac x = "i \<union> ia" in exI) 1155apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff) 1156apply (blast intro: field_Memrel_mono) 1157done 1158 1159lemma mdiff_omultiset [simp]: "omultiset(M) ==> omultiset(M -# N)" 1160apply (simp add: omultiset_def, clarify) 1161apply (simp add: Mult_iff_multiset) 1162apply (rule_tac x = i in exI) 1163apply (simp (no_asm_simp)) 1164done 1165 1166(** Proving that Memrel is a partial order **) 1167 1168lemma irrefl_Memrel: "Ord(i) ==> irrefl(field(Memrel(i)), Memrel(i))" 1169apply (rule irreflI, clarify) 1170apply (subgoal_tac "Ord (x) ") 1171prefer 2 apply (blast intro: Ord_in_Ord) 1172apply (drule_tac i = x in ltI [THEN lt_irrefl], auto) 1173done 1174 1175lemma trans_iff_trans_on: "trans(r) \<longleftrightarrow> trans[field(r)](r)" 1176by (simp add: trans_on_def trans_def, auto) 1177 1178lemma part_ord_Memrel: "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))" 1179apply (simp add: part_ord_def) 1180apply (simp (no_asm) add: trans_iff_trans_on [THEN iff_sym]) 1181apply (blast intro: trans_Memrel irrefl_Memrel) 1182done 1183 1184(* 1185 Ord(i) ==> 1186 part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i))) 1187*) 1188 1189lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel] 1190 1191(*irreflexivity*) 1192 1193lemma mless_not_refl: "~(M <# M)" 1194apply (simp add: mless_def, clarify) 1195apply (frule multirel_type [THEN subsetD]) 1196apply (drule part_ord_mless) 1197apply (simp add: part_ord_def irrefl_def) 1198done 1199 1200(* N<N ==> R *) 1201lemmas mless_irrefl = mless_not_refl [THEN notE, elim!] 1202 1203(*transitivity*) 1204lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N" 1205apply (simp add: mless_def, clarify) 1206apply (rule_tac x = "i \<union> ia" in exI) 1207apply (blast dest: multirel_Memrel_mono [OF Un_upper1 Un_upper1, THEN subsetD] 1208 multirel_Memrel_mono [OF Un_upper2 Un_upper2, THEN subsetD] 1209 intro: multirel_trans Ord_Un) 1210done 1211 1212(*asymmetry*) 1213lemma mless_not_sym: "M <# N ==> ~ N <# M" 1214apply clarify 1215apply (rule mless_not_refl [THEN notE]) 1216apply (erule mless_trans, assumption) 1217done 1218 1219lemma mless_asym: "[| M <# N; ~P ==> N <# M |] ==> P" 1220by (blast dest: mless_not_sym) 1221 1222lemma mle_refl [simp]: "omultiset(M) ==> M <#= M" 1223by (simp add: mle_def) 1224 1225(*anti-symmetry*) 1226lemma mle_antisym: 1227 "[| M <#= N; N <#= M |] ==> M = N" 1228apply (simp add: mle_def) 1229apply (blast dest: mless_not_sym) 1230done 1231 1232(*transitivity*) 1233lemma mle_trans: "[| K <#= M; M <#= N |] ==> K <#= N" 1234apply (simp add: mle_def) 1235apply (blast intro: mless_trans) 1236done 1237 1238lemma mless_le_iff: "M <# N \<longleftrightarrow> (M <#= N & M \<noteq> N)" 1239by (simp add: mle_def, auto) 1240 1241(** Monotonicity of mless **) 1242 1243lemma munion_less_mono2: "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N" 1244apply (simp add: mless_def omultiset_def, clarify) 1245apply (rule_tac x = "i \<union> ia" in exI) 1246apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff) 1247apply (rule munion_multirel_mono2) 1248 apply (blast intro: multirel_Memrel_mono [THEN subsetD]) 1249apply (simp add: Mult_iff_multiset) 1250apply (blast intro: field_Memrel_mono [THEN subsetD]) 1251done 1252 1253lemma munion_less_mono1: "[| M <# N; omultiset(K) |] ==> M +# K <# N +# K" 1254by (force dest: munion_less_mono2 simp add: munion_commute) 1255 1256lemma mless_imp_omultiset: "M <# N ==> omultiset(M) & omultiset(N)" 1257by (auto simp add: mless_def omultiset_def dest: multirel_type [THEN subsetD]) 1258 1259lemma munion_less_mono: "[| M <# K; N <# L |] ==> M +# N <# K +# L" 1260apply (frule_tac M = M in mless_imp_omultiset) 1261apply (frule_tac M = N in mless_imp_omultiset) 1262apply (blast intro: munion_less_mono1 munion_less_mono2 mless_trans) 1263done 1264 1265(* <#= *) 1266 1267lemma mle_imp_omultiset: "M <#= N ==> omultiset(M) & omultiset(N)" 1268by (auto simp add: mle_def mless_imp_omultiset) 1269 1270lemma mle_mono: "[| M <#= K; N <#= L |] ==> M +# N <#= K +# L" 1271apply (frule_tac M = M in mle_imp_omultiset) 1272apply (frule_tac M = N in mle_imp_omultiset) 1273apply (auto simp add: mle_def intro: munion_less_mono1 munion_less_mono2 munion_less_mono) 1274done 1275 1276lemma omultiset_0 [iff]: "omultiset(0)" 1277by (auto simp add: omultiset_def Mult_iff_multiset) 1278 1279lemma empty_leI [simp]: "omultiset(M) ==> 0 <#= M" 1280apply (simp add: mle_def mless_def) 1281apply (subgoal_tac "\<exists>i. Ord (i) & M \<in> Mult(field(Memrel(i))) ") 1282 prefer 2 apply (simp add: omultiset_def) 1283apply (case_tac "M=0", simp_all, clarify) 1284apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel(field (Memrel(i)), Memrel(i))") 1285apply (rule_tac [2] one_step_implies_multirel) 1286apply (auto simp add: Mult_iff_multiset) 1287done 1288 1289lemma munion_upper1: "[| omultiset(M); omultiset(N) |] ==> M <#= M +# N" 1290apply (subgoal_tac "M +# 0 <#= M +# N") 1291apply (rule_tac [2] mle_mono, auto) 1292done 1293 1294end 1295