posetScript.sml

1(* ========================================================================= *)
2(* Create "posetTheory" for reasoning about arbitrary partial orders.        *)
3(* Originally created by Joe Hurd to support the pGCL formalization.         *)
4(* ========================================================================= *)
5Theory poset[bare]
6Ancestors
7  pair
8Libs
9  HolKernel Parse boolLib pairLib BasicProvers metisLib simpLib
10
11
12(* ------------------------------------------------------------------------- *)
13(* Start a new theory called "poset"                                         *)
14(* ------------------------------------------------------------------------- *)
15
16(* ------------------------------------------------------------------------- *)
17(* Helpful proof tools                                                       *)
18(* ------------------------------------------------------------------------- *)
19
20val Know = Q_TAC KNOW_TAC;
21
22val bool_ss = boolSimps.bool_ss;
23val pair_cases_tac = MATCH_ACCEPT_TAC ABS_PAIR_THM;
24
25fun UNPRIME_CONV tmp =
26  let
27    val (vp,b) = dest_abs tmp
28    val (sp,ty) = dest_var vp
29    val v = mk_var (unprime sp, ty)
30    val tm = mk_abs (v, subst [vp |-> v] b)
31  in
32    ALPHA tmp tm
33  end;
34
35(* ------------------------------------------------------------------------- *)
36(* Functions from one predicate to another                                   *)
37(* NOTE: this is actually pred_setTheory.FUNSET                              *)
38(* ------------------------------------------------------------------------- *)
39
40val function_def = new_definition
41  ("function_def",
42   ``function a b (f : 'a -> 'b) = !x. a x ==> b (f x)``);
43
44Theorem function_in:
45    function s s t /\ s x ==> s (t x)
46Proof
47   RW_TAC (srw_ss()) [function_def]
48QED
49
50(* ------------------------------------------------------------------------- *)
51(* A HOL type of partial orders                                              *)
52(* ------------------------------------------------------------------------- *)
53
54Type poset[pp] = “:('a -> bool) # ('a -> 'a -> bool)”
55
56(* ------------------------------------------------------------------------- *)
57(* Definition of partially-ordered sets                                      *)
58(* ------------------------------------------------------------------------- *)
59
60val poset_def = new_definition
61  ("poset_def",
62   ``poset ((s,r) : 'a poset) <=>
63     (?x. s x) /\
64     (!x. s x ==> r x x) /\
65     (!x y. s x /\ s y /\ r x y /\ r y x ==> (x = y)) /\
66     (!x y z. s x /\ s y /\ s z /\ r x y /\ r y z ==> r x z)``);
67
68val carrier_def = new_definition
69  ("carrier_def[simp]",
70   ``carrier ((s,r) : 'a poset) = s``);
71
72val relation_def = new_definition
73  ("relation_def[simp]",
74   ``relation ((s,r) : 'a poset) = r``);
75
76val top_def = new_definition
77  ("top_def",
78   ``top ((s,r) : 'a poset) x <=> s x /\ !y. s y ==> r y x``);
79
80val bottom_def = new_definition
81  ("bottom_def",
82   ``bottom ((s,r) : 'a poset) x <=> s x /\ !y. s y ==> r x y``);
83
84val chain_def = new_definition
85  ("chain_def",
86   ``chain ((s,r) : 'a poset) c <=>
87     !x y. s x /\ s y /\ c x /\ c y ==> r x y \/ r y x``);
88
89val lub_def = new_definition
90  ("lub_def",
91   ``lub ((s,r) : 'a poset) p x <=>
92     s x /\ (!y. s y /\ p y ==> r y x) /\
93     !z. s z /\ (!y. s y /\ p y ==> r y z) ==> r x z``);
94
95val glb_def = new_definition
96  ("glb_def",
97   ``glb ((s,r) : 'a poset) p x <=>
98     s x /\ (!y. s y /\ p y ==> r x y) /\
99     !z. s z /\ (!y. s y /\ p y ==> r z y) ==> r z x``);
100
101val complete_def = new_definition
102  ("complete_def",
103   ``complete (p : 'a poset) = !c. (?x. lub p c x) /\ (?x. glb p c x)``);
104
105Theorem poset_nonempty:
106     !s r. poset (s,r) ==> ?x. s x
107Proof
108   RW_TAC bool_ss [poset_def]
109QED
110
111Theorem poset_refl:
112     !s r x. poset (s,r) /\ s x ==> r x x
113Proof
114   RW_TAC bool_ss [poset_def]
115QED
116
117Theorem poset_antisym:
118     !s r x y.
119       poset (s,r) /\ s x /\ s y /\ r x y /\ r y x ==> (x = y)
120Proof
121   RW_TAC bool_ss [poset_def]
122QED
123
124Theorem poset_trans:
125     !s r x y z.
126       poset (s,r) /\ s x /\ s y /\ s z /\ r x y /\ r y z ==> r x z
127Proof
128   RW_TAC bool_ss [poset_def] >> RES_TAC
129QED
130
131Theorem lub_pred:
132     !s r p x. lub (s,r) (\j. s j /\ p j) x = lub (s,r) p x
133Proof
134   RW_TAC bool_ss [lub_def]
135   >> PROVE_TAC []
136QED
137
138Theorem glb_pred:
139     !s r p x. glb (s,r) (\j. s j /\ p j) x = glb (s,r) p x
140Proof
141   RW_TAC bool_ss [glb_def]
142   >> PROVE_TAC []
143QED
144
145Theorem complete_up:
146     !p c. complete p ==> ?x. lub p c x
147Proof
148   PROVE_TAC [complete_def]
149QED
150
151Theorem complete_down:
152     !p c. complete p ==> ?x. glb p c x
153Proof
154   PROVE_TAC [complete_def]
155QED
156
157Theorem complete_top:
158     !p : 'a poset. poset p /\ complete p ==> ?x. top p x
159Proof
160   GEN_TAC
161   >> Know `?s r. p = (s,r)` >- pair_cases_tac
162   >> STRIP_TAC
163   >> RW_TAC bool_ss [complete_def]
164   >> Q.PAT_X_ASSUM `!p. X p` (MP_TAC o Q.SPEC `\x. T`)
165   >> RW_TAC bool_ss [lub_def]
166   >> Q.EXISTS_TAC `x`
167   >> RW_TAC bool_ss [top_def]
168QED
169
170Theorem complete_bottom:
171     !p : 'a poset. poset p /\ complete p ==> ?x. bottom p x
172Proof
173   GEN_TAC
174   >> Know `?s r. p = (s,r)` >- pair_cases_tac
175   >> STRIP_TAC
176   >> RW_TAC bool_ss [complete_def]
177   >> Q.PAT_X_ASSUM `!p. X p` (MP_TAC o Q.SPEC `\x. T`)
178   >> RW_TAC bool_ss [glb_def]
179   >> Q.EXISTS_TAC `x'`
180   >> RW_TAC bool_ss [bottom_def]
181QED
182
183(* ------------------------------------------------------------------------- *)
184(* Pointwise lifting of posets                                               *)
185(* ------------------------------------------------------------------------- *)
186
187val pointwise_lift_def = new_definition
188  ("pointwise_lift_def",
189   ``pointwise_lift (t : 'a -> bool) ((s,r) : 'b poset) =
190     (function t s, \f g. !x. t x ==> r (f x) (g x))``);
191
192Theorem complete_pointwise:
193     !p t. complete p ==> complete (pointwise_lift t p)
194Proof
195   GEN_TAC
196   >> Know `?s r. p = (s,r)` >- pair_cases_tac
197   >> STRIP_TAC
198   >> RW_TAC bool_ss [complete_def, pointwise_lift_def] >|
199   [Know
200    `!y.
201       t y ==>
202       ?l. lub (s,r) (\z. ?f. (!x. t x ==> s (f x)) /\ c f /\ (f y = z)) l`
203    >- RW_TAC bool_ss []
204    >> DISCH_THEN
205       (MP_TAC o CONV_RULE (QUANT_CONV RIGHT_IMP_EXISTS_CONV THENC SKOLEM_CONV))
206    >> RW_TAC bool_ss [lub_def, function_def]
207    >> Q.EXISTS_TAC `l`
208    >> CONJ_TAC >- METIS_TAC []
209    >> CONJ_TAC >- METIS_TAC []
210    >> CONV_TAC (DEPTH_CONV UNPRIME_CONV)
211    >> RW_TAC bool_ss []
212    >> Q.PAT_X_ASSUM `!y. t y ==> P y /\ Q y /\ R y` (MP_TAC o Q.SPEC `x`)
213    >> RW_TAC bool_ss []
214    >> POP_ASSUM MATCH_MP_TAC
215    >> CONJ_TAC >- METIS_TAC []
216    >> RW_TAC bool_ss []
217    >> Q.PAT_X_ASSUM `!y. P y ==> !x. Q x y` (MP_TAC o Q.SPEC `f`)
218    >> MATCH_MP_TAC (PROVE [] ``(y ==> z) /\ x ==> ((x ==> y) ==> z)``)
219    >> CONJ_TAC >- METIS_TAC []
220    >> METIS_TAC [],
221    Know
222    `!y.
223       t y ==>
224       ?l. glb (s,r) (\z. ?f. (!x. t x ==> s (f x)) /\ c f /\ (f y = z)) l`
225    >- RW_TAC bool_ss []
226    >> DISCH_THEN
227       (MP_TAC o CONV_RULE (QUANT_CONV RIGHT_IMP_EXISTS_CONV THENC SKOLEM_CONV))
228    >> RW_TAC bool_ss [glb_def, function_def]
229    >> Q.EXISTS_TAC `l`
230    >> CONJ_TAC >- METIS_TAC []
231    >> CONJ_TAC >- METIS_TAC []
232    >> CONV_TAC (DEPTH_CONV UNPRIME_CONV)
233    >> RW_TAC bool_ss []
234    >> Q.PAT_X_ASSUM `!y. t y ==> P y /\ Q y /\ R y` (MP_TAC o Q.SPEC `x`)
235    >> RW_TAC bool_ss []
236    >> POP_ASSUM MATCH_MP_TAC
237    >> CONJ_TAC >- METIS_TAC []
238    >> RW_TAC bool_ss []
239    >> Q.PAT_X_ASSUM `!y. P y ==> !x. Q x y` (MP_TAC o Q.SPEC `f'`)
240    >> MATCH_MP_TAC (PROVE [] ``(y ==> z) /\ x ==> ((x ==> y) ==> z)``)
241    >> CONJ_TAC >- METIS_TAC []
242    >> METIS_TAC []]
243QED
244
245(*
246val lub_pointwise_push = store_thm
247  ("lub_pointwise_push",
248   ``!p t c l x.
249       poset p /\ t x /\ lub (pointwise_lift t p) c l ==>
250       lub p
251       (\y. ?f. (carrier (pointwise_lift t p) f /\ c f) /\ (y = f x)) (l x)``,
252   GEN_TAC
253   >> Know `?s r. p = (s,r)` >- pair_cases_tac
254   >> STRIP_TAC
255   >> RW_TAC bool_ss [lub_def, pointwise_lift_def, carrier_def]
256   >> METIS_TAC []
257*)
258
259(* ------------------------------------------------------------------------- *)
260(* Functions acting on posets.                                               *)
261(* ------------------------------------------------------------------------- *)
262
263val monotonic_def = new_definition
264  ("monotonic_def",
265   ``monotonic ((s,r) : 'a poset) f =
266     !x y. s x /\ s y /\ r x y ==> r (f x) (f y)``);
267
268val up_continuous_def = new_definition
269  ("up_continuous_def",
270   ``up_continuous ((s,r) : 'a poset) f =
271     !c x.
272       chain (s,r) c /\ lub (s,r) c x ==>
273       lub (s,r) (\y. ?z. (s z /\ c z) /\ (y = f z)) (f x)``);
274
275val down_continuous_def = new_definition
276  ("down_continuous_def",
277   ``down_continuous ((s,r) : 'a poset) f =
278     !c x.
279       chain (s,r) c /\ glb (s,r) c x ==>
280       glb (s,r) (\y. ?z. (s z /\ c z) /\ (y = f z)) (f x)``);
281
282val continuous_def = new_definition
283  ("continuous_def",
284   “continuous (p : 'a poset) f <=> up_continuous p f /\ down_continuous p f”);
285
286
287Theorem monotonic_comp:
288     monotonic (s,r) f /\ monotonic (s,r) g /\ function s s g
289     ==> monotonic (s,r) (f o g)
290Proof
291   RW_TAC (srw_ss()) [monotonic_def, function_def]
292QED
293
294(* ------------------------------------------------------------------------- *)
295(* Least and greatest fixed points.                                          *)
296(* ------------------------------------------------------------------------- *)
297
298val lfp_def = new_definition
299  ("lfp_def",
300   ``lfp ((s,r) : 'a poset) f x <=>
301     s x /\ (f x = x) /\ !y. s y /\ r (f y) y ==> r x y``);
302
303val gfp_def = new_definition
304  ("gfp_def",
305   ``gfp ((s,r) : 'a poset) f x <=>
306     s x /\ (f x = x) /\ !y. s y /\ r y (f y) ==> r y x``);
307
308Theorem lfp_unique:
309     !p f x x'.
310        poset p /\ lfp p f x /\ lfp p f x' ==>
311        (x = x')
312Proof
313   GEN_TAC
314   >> Know `?s r. p = (s,r)` >- pair_cases_tac
315   >> STRIP_TAC
316   >> RW_TAC bool_ss [poset_def, lfp_def]
317QED
318
319Theorem gfp_unique:
320     !p f x x'.
321        poset p /\ gfp p f x /\ gfp p f x' ==>
322        (x = x')
323Proof
324   GEN_TAC
325   >> Know `?s r. p = (s,r)` >- pair_cases_tac
326   >> STRIP_TAC
327   >> RW_TAC bool_ss [poset_def, gfp_def]
328QED
329
330Theorem lfp_induct:
331    lfp (s,r) b lfix /\ s x /\ r (b x) x
332    ==> r lfix x
333Proof
334   RW_TAC bool_ss [lfp_def]
335QED
336
337Theorem gfp_coinduct:
338    gfp (s,r) b gfix /\ s x /\ r x (b x)
339   ==> r x gfix
340Proof
341   RW_TAC bool_ss [gfp_def]
342QED
343
344Theorem glb_unique:
345  poset (s,r) /\
346  glb (s,r) P x /\ glb (s,r) P y
347  ==> x = y
348Proof
349  RW_TAC bool_ss [glb_def] >>
350  drule_then irule poset_antisym >> RW_TAC bool_ss[]
351QED
352
353Theorem lub_unique:
354  poset (s,r) /\
355  lub (s,r) P x /\ lub (s,r) P y
356  ==> x = y
357Proof
358  RW_TAC bool_ss [lub_def] >>
359  drule_then irule poset_antisym >> RW_TAC bool_ss[]
360QED
361
362(* ------------------------------------------------------------------------- *)
363(* The Knaster-Tarski theorem                                                *)
364(* ------------------------------------------------------------------------- *)
365
366Theorem knaster_tarski_lfp:
367     !p f.
368       poset p /\ complete p /\ function (carrier p) (carrier p) f /\
369       monotonic p f ==> ?x. lfp p f x
370Proof
371   RW_TAC bool_ss []
372   >> Know `?x. top p x` >- PROVE_TAC [complete_top]
373   >> Know `?s r. p = (s,r)` >- pair_cases_tac
374   >> RW_TAC bool_ss []
375   >> FULL_SIMP_TAC bool_ss [function_def, carrier_def]
376   >> Q.UNDISCH_TAC `complete (s,r)`
377   >> SIMP_TAC bool_ss [complete_def]
378   >> DISCH_THEN (MP_TAC o CONJUNCT2 o Q.SPEC `\x : 'a. r ((f x) : 'a) x`)
379   >> DISCH_THEN (Q.X_CHOOSE_THEN `k` ASSUME_TAC)
380   >> Q.EXISTS_TAC `k`
381   >> Know `s k /\ s (f k)` >- PROVE_TAC [glb_def]
382   >> STRIP_TAC
383   >> ASM_SIMP_TAC bool_ss [lfp_def]
384   >> MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``)
385   >> REPEAT STRIP_TAC
386   >- (Q.PAT_X_ASSUM `glb X Y Z` MP_TAC >> ASM_SIMP_TAC bool_ss [glb_def])
387   >> MATCH_MP_TAC poset_antisym
388   >> Q.EXISTS_TAC `s`
389   >> Q.EXISTS_TAC `r`
390   >> ASM_SIMP_TAC bool_ss []
391   >> MATCH_MP_TAC (PROVE [] ``x /\ (x ==> y) ==> x /\ y``)
392   >> CONJ_TAC
393   >| [Q.PAT_X_ASSUM `glb X Y Z` MP_TAC
394       >> ASM_SIMP_TAC bool_ss [glb_def]
395       >> DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MATCH_MP_TAC)
396       >> RW_TAC bool_ss []
397       >> MATCH_MP_TAC poset_trans
398       >> Q.EXISTS_TAC `s`
399       >> METIS_TAC [monotonic_def],
400       STRIP_TAC
401       >> Q.PAT_X_ASSUM `glb X Y Z` MP_TAC
402       >> ASM_SIMP_TAC bool_ss [glb_def]
403       >> DISCH_THEN MATCH_MP_TAC
404       >> Know `s (f (f k))` >- PROVE_TAC []
405       >> RW_TAC bool_ss []
406       >> Q.PAT_X_ASSUM `monotonic X Y`
407          (MATCH_MP_TAC o REWRITE_RULE [monotonic_def])
408       >> PROVE_TAC []]
409QED
410
411Theorem knaster_tarski_gfp:
412     !p f.
413       poset p /\ complete p /\ function (carrier p) (carrier p) f /\
414       monotonic p f ==> ?x. gfp p f x
415Proof
416   RW_TAC bool_ss []
417   >> Know `?x. bottom p x` >- PROVE_TAC [complete_bottom]
418   >> Know `?s r. p = (s,r)` >- pair_cases_tac
419   >> RW_TAC bool_ss []
420   >> FULL_SIMP_TAC bool_ss [function_def, carrier_def]
421   >> Q.UNDISCH_TAC `complete (s,r)`
422   >> SIMP_TAC bool_ss [complete_def]
423   >> DISCH_THEN (MP_TAC o CONJUNCT1 o Q.SPEC `\x : 'a. r x ((f x) : 'a)`)
424   >> DISCH_THEN (Q.X_CHOOSE_THEN `k` ASSUME_TAC)
425   >> Q.EXISTS_TAC `k`
426   >> Know `s k /\ s (f k)` >- PROVE_TAC [lub_def]
427   >> STRIP_TAC
428   >> ASM_SIMP_TAC bool_ss [gfp_def]
429   >> MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``)
430   >> REPEAT STRIP_TAC
431   >- (Q.PAT_X_ASSUM `lub X Y Z` MP_TAC >> ASM_SIMP_TAC bool_ss [lub_def])
432   >> MATCH_MP_TAC poset_antisym
433   >> Q.EXISTS_TAC `s`
434   >> Q.EXISTS_TAC `r`
435   >> ASM_SIMP_TAC bool_ss []
436   >> MATCH_MP_TAC (PROVE [] ``y /\ (y ==> x) ==> x /\ y``)
437   >> CONJ_TAC
438   >| [Q.PAT_X_ASSUM `lub X Y Z` MP_TAC
439       >> ASM_SIMP_TAC bool_ss [lub_def]
440       >> DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MATCH_MP_TAC)
441       >> RW_TAC bool_ss []
442       >> MATCH_MP_TAC poset_trans
443       >> Q.EXISTS_TAC `s`
444       >> METIS_TAC [monotonic_def],
445       STRIP_TAC
446       >> Q.PAT_X_ASSUM `lub X Y Z` MP_TAC
447       >> ASM_SIMP_TAC bool_ss [lub_def]
448       >> DISCH_THEN MATCH_MP_TAC
449       >> Know `s (f (f k))` >- PROVE_TAC []
450       >> RW_TAC bool_ss []
451       >> Q.PAT_X_ASSUM `monotonic X Y`
452          (MATCH_MP_TAC o REWRITE_RULE [monotonic_def])
453       >> PROVE_TAC []]
454QED
455
456Theorem knaster_tarski:
457     !p f.
458       poset p /\ complete p /\ function (carrier p) (carrier p) f /\
459       monotonic p f ==> (?x. lfp p f x) /\ (?x. gfp p f x)
460Proof
461   PROVE_TAC [knaster_tarski_lfp, knaster_tarski_gfp]
462QED