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