1 (* ========================================================================= *)
2 (* Part 1: Background theories. *)
3 (* ========================================================================= *)
5 let EMPTY_IS_FINITE = prove
6 (`!s. (s = EMPTY) ==> FINITE s`,
7 SIMP_TAC[FINITE_RULES]);;
9 let SING_IS_FINITE = prove
10 (`!s a. (s = {a}) ==> FINITE s`,
11 SIMP_TAC[FINITE_INSERT; FINITE_RULES]);;
13 let UNION_NONZERO = prove
14 (`{a | ~(f a + g a = 0)} = {a | ~(f a = 0)} UNION {a | ~(g a = 0)}`,
15 REWRITE_TAC[ADD_EQ_0; EXTENSION; IN_UNION; IN_ELIM_THM; DE_MORGAN_THM]);;
17 (* ------------------------------------------------------------------------- *)
18 (* Definition of type of finite multisets with a few basic operations. *)
19 (* ------------------------------------------------------------------------- *)
21 parse_as_infix("mmember",(11,"right"));;
22 parse_as_infix("munion",(16,"right"));;
23 parse_as_infix("mdiff",(18,"left"));;
25 let multiset_tybij_th = prove
26 (`?f. FINITE {a:A | ~(f a = 0)}`,
27 EXISTS_TAC `\a:A. 0` THEN
28 SIMP_TAC[EMPTY_IS_FINITE; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY]);;
30 let multiset_tybij = new_type_definition
31 "multiset" ("multiset","multiplicity") multiset_tybij_th;;
33 let mempty = new_definition
34 `mempty = multiset (\b. 0)`;;
36 let mmember = new_definition
37 `a mmember M <=> ~(multiplicity M a = 0)`;;
39 let msing = new_definition
40 `msing a = multiset (\b. if b = a then 1 else 0)`;;
42 let munion = new_definition
43 `M munion N = multiset(\b. multiplicity M b + multiplicity N b)`;;
45 let mdiff = new_definition
46 `M mdiff N = multiset(\b. multiplicity M b - multiplicity N b)`;;
48 (* ------------------------------------------------------------------------- *)
49 (* Extensionality for multisets. *)
50 (* ------------------------------------------------------------------------- *)
52 let MEXTENSION = prove
53 (`(M = N) = !a. multiplicity M a = multiplicity N a`,
54 REWRITE_TAC[GSYM FUN_EQ_THM] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
55 MESON_TAC[multiset_tybij]);;
57 (* ------------------------------------------------------------------------- *)
58 (* Basic properties of multisets. *)
59 (* ------------------------------------------------------------------------- *)
61 let MULTIPLICITY_MULTISET = prove
62 (`FINITE {a | ~(f a = 0)} /\ (f a = y) ==> (multiplicity(multiset f) a = y)`,
63 SIMP_TAC[multiset_tybij]);;
66 (`multiplicity mempty a = 0`,
67 REWRITE_TAC[mempty] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
68 SIMP_TAC[EMPTY_IS_FINITE; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY]);;
71 (`multiplicity (msing (a:A)) b = if b = a then 1 else 0`,
72 REWRITE_TAC[msing] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
73 REWRITE_TAC[] THEN MATCH_MP_TAC SING_IS_FINITE THEN EXISTS_TAC `a:A` THEN
74 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
75 GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[ARITH_EQ]);;
78 (`multiplicity (M munion N) a = multiplicity M a + multiplicity N a`,
79 REWRITE_TAC[munion] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
80 REWRITE_TAC[UNION_NONZERO; FINITE_UNION] THEN SIMP_TAC[multiset_tybij] THEN
81 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[multiset_tybij]);;
84 (`multiplicity (M mdiff N) (a:A) = multiplicity M a - multiplicity N a`,
85 REWRITE_TAC[mdiff] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
86 REWRITE_TAC[] THEN MATCH_MP_TAC FINITE_SUBSET THEN
87 EXISTS_TAC `{a:A | ~(multiplicity M a = 0)}` THEN
88 SIMP_TAC[SUBSET; IN_ELIM_THM; multiset_tybij] THEN
89 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[multiset_tybij] THEN
92 (* ------------------------------------------------------------------------- *)
93 (* Some trivial properties of multisets that we use later. *)
94 (* ------------------------------------------------------------------------- *)
96 let MUNION_MEMPTY = prove
97 (`~(M munion (msing(a:A)) = mempty)`,
98 REWRITE_TAC[MEXTENSION; MEMPTY; MSING; MUNION] THEN
99 DISCH_THEN(MP_TAC o SPEC `a:A`) THEN
100 REWRITE_TAC[ADD_EQ_0; ARITH_EQ]);;
102 let MMEMBER_MUNION = prove
103 (`x mmember (M munion N) <=> x mmember M \/ x mmember N`,
104 REWRITE_TAC[mmember; MUNION; ADD_EQ_0; DE_MORGAN_THM]);;
106 let MMEMBER_MSING = prove
107 (`x mmember (msing a) <=> (x = a)`,
108 REWRITE_TAC[mmember; MSING] THEN COND_CASES_TAC THEN REWRITE_TAC[ARITH_EQ]);;
110 let MUNION_EMPTY = prove
111 (`M munion mempty = M`,
112 REWRITE_TAC[MEXTENSION; MUNION; MEMPTY; ADD_CLAUSES]);;
114 let MUNION_ASSOC = prove
115 (`M1 munion (M2 munion M3) = (M1 munion M2) munion M3`,
116 REWRITE_TAC[MEXTENSION; MUNION; ADD_ASSOC]);;
118 let MUNION_AC = prove
119 (`(M1 munion M2 = M2 munion M1) /\
120 ((M1 munion M2) munion M3 = M1 munion M2 munion M3) /\
121 (M1 munion M2 munion M3 = M2 munion M1 munion M3)`,
122 REWRITE_TAC[MEXTENSION; MUNION; ADD_AC]);;
124 let MUNION_11 = prove
125 (`(M1 munion N = M2 munion N) <=> (M1 = M2)`,
126 REWRITE_TAC[MEXTENSION; MUNION; EQ_ADD_RCANCEL]);;
128 let MUNION_INUNION = prove
129 (`a mmember (M munion (msing b)) /\ ~(b = a) ==> a mmember M`,
130 REWRITE_TAC[mmember; MUNION; MSING; ADD_EQ_0] THEN
131 COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ]);;
133 let MMEMBER_MDIFF = prove
134 (`(a:A) mmember M ==> (M = (M mdiff (msing a)) munion (msing a))`,
135 REWRITE_TAC[mmember; MEXTENSION; MUNION; MDIFF; MSING] THEN
136 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
137 UNDISCH_TAC `~(multiplicity M (a:A) = 0)` THEN ARITH_TAC);;
139 (* ------------------------------------------------------------------------- *)
140 (* Induction principle for multisets. *)
141 (* ------------------------------------------------------------------------- *)
143 let MULTISET_INDUCT_LEMMA1 = prove
144 (`(!M. ({a | ~(multiplicity M a = 0)} SUBSET s) ==> P M) /\
145 (!a:A M. P M ==> P (M munion (msing a)))
146 ==> !n M. (multiplicity M a = n) /\
147 {a:A | ~(multiplicity M a = 0)} SUBSET (a INSERT s)
149 STRIP_TAC THEN INDUCT_TAC THEN REPEAT STRIP_TAC THENL
150 [FIRST_X_ASSUM MATCH_MP_TAC THEN
151 UNDISCH_TAC `{a:A | ~(multiplicity M a = 0)} SUBSET (a INSERT s)` THEN
152 REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INSERT] THEN ASM_MESON_TAC[];
153 SUBGOAL_THEN `M = (M mdiff (msing(a:A))) munion (msing a)` SUBST1_TAC THENL
154 [MATCH_MP_TAC MMEMBER_MDIFF THEN ASM_REWRITE_TAC[mmember; NOT_SUC];
156 MAP_EVERY (MATCH_MP_TAC o ASSUME)
157 [`!a:A M. P M ==> P (M munion msing a)`;
158 `!M. (multiplicity M a = n) /\
159 {a:A | ~(multiplicity M a = 0)} SUBSET (a INSERT s)
161 ASM_REWRITE_TAC[MDIFF; MSING; ARITH_RULE `SUC n - 1 = n`] THEN
162 MATCH_MP_TAC SUBSET_TRANS THEN
163 EXISTS_TAC `{a:A | ~(multiplicity M a = 0)}` THEN
164 ASM_SIMP_TAC[SUBSET; IN_ELIM_THM; CONTRAPOS_THM; SUB_0]]);;
166 let MULTISET_INDUCT_LEMMA2 = prove
168 (!a:A M. P M ==> P (M munion (msing a)))
169 ==> !s. FINITE s ==> !M. {a:A | ~(multiplicity M a = 0)} SUBSET s ==> P M`,
170 STRIP_TAC THEN MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
171 [REWRITE_TAC[SUBSET; IN_ELIM_THM; NOT_IN_EMPTY] THEN
172 REPEAT STRIP_TAC THEN
173 SUBGOAL_THEN `M:(A)multiset = mempty` (fun th -> ASM_REWRITE_TAC[th]) THEN
174 ASM_REWRITE_TAC[MEXTENSION; MEMPTY]; X_GEN_TAC `a:A`] THEN
175 REPEAT STRIP_TAC THEN MP_TAC MULTISET_INDUCT_LEMMA1 THEN
176 ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
177 ASM_REWRITE_TAC[GSYM EXISTS_REFL]);;
179 let MULTISET_INDUCT = prove
181 (!a:A M. P M ==> P (M munion (msing a)))
183 DISCH_THEN(MP_TAC o MATCH_MP MULTISET_INDUCT_LEMMA2) THEN
184 REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
185 REWRITE_TAC[IMP_IMP] THEN
186 GEN_TAC THEN DISCH_THEN MATCH_MP_TAC THEN
187 EXISTS_TAC `{a:A | ~(multiplicity M a = 0)}` THEN
188 REWRITE_TAC[SUBSET_REFL; multiset_tybij] THEN
189 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[multiset_tybij]);;
191 (* ========================================================================= *)
192 (* Part 2: Transcription of Tobias's paper. *)
193 (* ========================================================================= *)
195 parse_as_infix("<<",(12,"right"));;
197 (* ------------------------------------------------------------------------- *)
198 (* Wellfounded part of a relation. *)
199 (* ------------------------------------------------------------------------- *)
201 let WFP_RULES,WFP_INDUCT,WFP_CASES = new_inductive_definition
202 `!x. (!y. y << x ==> WFP(<<) y) ==> WFP(<<) x`;;
204 (* ------------------------------------------------------------------------- *)
205 (* Wellfounded part induction. *)
206 (* ------------------------------------------------------------------------- *)
208 let WFP_PART_INDUCT = prove
209 (`!P. (!x. x IN WFP(<<) /\ (!y. y << x ==> P(y)) ==> P(x))
210 ==> !x:A. x IN WFP(<<) ==> P(x)`,
211 GEN_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN
212 ONCE_REWRITE_TAC[TAUT `a ==> b <=> a ==> a /\ b`] THEN
213 MATCH_MP_TAC WFP_INDUCT THEN ASM_MESON_TAC[WFP_RULES]);;
215 (* ------------------------------------------------------------------------- *)
216 (* A relation is wellfounded iff WFP is the whole universe. *)
217 (* ------------------------------------------------------------------------- *)
220 (`WF(<<) <=> (WFP(<<) = UNIV:A->bool)`,
222 [REWRITE_TAC[WF_IND; EXTENSION; IN; UNIV] THEN MESON_TAC[WFP_RULES];
223 DISCH_TAC THEN MP_TAC WFP_PART_INDUCT THEN
224 ASM_REWRITE_TAC[IN; UNIV; WF_IND]]);;
226 (* ------------------------------------------------------------------------- *)
227 (* The multiset order. *)
228 (* ------------------------------------------------------------------------- *)
230 let morder = new_definition
231 `morder(<<) N M <=> ?M0 a K. (M = M0 munion (msing a)) /\
233 (!b. b mmember K ==> b << a)`;;
235 (* ------------------------------------------------------------------------- *)
236 (* We separate off this part from the proof of LEMMA_2_1. *)
237 (* ------------------------------------------------------------------------- *)
239 let LEMMA_2_0 = prove
240 (`morder(<<) N (M0 munion (msing a))
241 ==> (?M. morder(<<) M M0 /\ (N = M munion (msing a))) \/
242 (?K. (N = M0 munion K) /\ (!b:A. b mmember K ==> b << a))`,
243 GEN_REWRITE_TAC LAND_CONV [morder] THEN
244 DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN
245 [`M1:(A)multiset`; `b:A`; `K:(A)multiset`]) STRIP_ASSUME_TAC) THEN
246 ASM_CASES_TAC `b:A = a` THENL
247 [DISJ2_TAC THEN UNDISCH_THEN `b:A = a` SUBST_ALL_TAC THEN
248 EXISTS_TAC `K:(A)multiset` THEN ASM_MESON_TAC[MUNION_11]; DISJ1_TAC] THEN
249 SUBGOAL_THEN `?M2. M1 = M2 munion (msing(a:A))` STRIP_ASSUME_TAC THENL
250 [EXISTS_TAC `M1 mdiff (msing(a:A))` THEN
251 MAP_EVERY MATCH_MP_TAC [MMEMBER_MDIFF; MUNION_INUNION] THEN
252 UNDISCH_TAC `M0 munion (msing a) = M1 munion (msing(b:A))` THEN
253 ASM_REWRITE_TAC[MEXTENSION; MUNION; MSING; mmember] THEN
254 DISCH_THEN(MP_TAC o SPEC `a:A`) THEN ASM_REWRITE_TAC[] THEN
255 ARITH_TAC; ALL_TAC] THEN
256 EXISTS_TAC `M2 munion K:(A)multiset` THEN ASM_REWRITE_TAC[MUNION_AC] THEN
257 REWRITE_TAC[morder] THEN
258 MAP_EVERY EXISTS_TAC [`M2:(A)multiset`; `b:A`; `K:(A)multiset`] THEN
259 UNDISCH_TAC `M0 munion msing (a:A) = M1 munion msing b` THEN
260 ASM_REWRITE_TAC[MUNION_AC] THEN MESON_TAC[MUNION_AC; MUNION_11]);;
262 (* ------------------------------------------------------------------------- *)
263 (* The sequence of lemmas from Tobias's paper. *)
264 (* ------------------------------------------------------------------------- *)
266 let LEMMA_2_1 = prove
267 (`(!M b:A. b << a /\ M IN WFP(morder(<<))
268 ==> (M munion (msing b)) IN WFP(morder(<<))) /\
269 M0 IN WFP(morder(<<)) /\
270 (!M. morder(<<) M M0 ==> (M munion (msing a)) IN WFP(morder(<<)))
271 ==> (M0 munion (msing a)) IN WFP(morder(<<))`,
272 STRIP_TAC THEN REWRITE_TAC[IN] THEN MATCH_MP_TAC WFP_RULES THEN
273 X_GEN_TAC `N:(A)multiset` THEN
274 DISCH_THEN(DISJ_CASES_THEN MP_TAC o MATCH_MP LEMMA_2_0) THENL
275 [ASM_MESON_TAC[IN]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
276 SPEC_TAC(`N:(A)multiset`,`N:(A)multiset`) THEN
277 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
278 MATCH_MP_TAC MULTISET_INDUCT THEN REPEAT STRIP_TAC THEN
279 RULE_ASSUM_TAC(REWRITE_RULE[MUNION_ASSOC; MMEMBER_MUNION; MMEMBER_MSING]) THEN
280 ASM_MESON_TAC[IN; MUNION_EMPTY]);;
282 let LEMMA_2_2 = prove
283 (`(!M b. b << a /\ M IN WFP(morder(<<))
284 ==> (M munion (msing b)) IN WFP(morder(<<)))
285 ==> !M. M IN WFP(morder(<<)) ==> (M munion (msing a)) IN WFP(morder(<<))`,
286 STRIP_TAC THEN MATCH_MP_TAC WFP_PART_INDUCT THEN
287 REPEAT STRIP_TAC THEN MATCH_MP_TAC LEMMA_2_1 THEN ASM_REWRITE_TAC[]);;
289 let LEMMA_2_3 = prove
291 ==> !a M. M IN WFP(morder(<<)) ==> (M munion (msing a)) IN WFP(morder(<<))`,
292 REWRITE_TAC[WF_IND] THEN DISCH_THEN MATCH_MP_TAC THEN MESON_TAC[LEMMA_2_2]);;
294 let LEMMA_2_4 = prove
295 (`WF(<<) ==> !M. M IN WFP(morder(<<))`,
296 DISCH_TAC THEN MATCH_MP_TAC MULTISET_INDUCT THEN CONJ_TAC THENL
297 [REWRITE_TAC[IN] THEN MATCH_MP_TAC WFP_RULES THEN
298 REWRITE_TAC[morder; MUNION_MEMPTY];
299 ASM_SIMP_TAC[LEMMA_2_3]]);;
301 (* ------------------------------------------------------------------------- *)
302 (* Hence the final result. *)
303 (* ------------------------------------------------------------------------- *)
305 let MORDER_WF = prove
306 (`WF(<<) ==> WF(morder(<<))`,
307 SIMP_TAC[WFP_WF; EXTENSION; IN_UNIV; LEMMA_2_4]);;