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