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