1(* file HS/FIN/tcScript.sml, created 1/23/13, revised 9/30, author F.L.Morris *) 2 3(* A theory to support implementation of Warshall's algorithm for transitive *) 4(* closure. Relations are represented as set-valued finite maps, but no *) 5(* particular representation is presumed for the sets or maps themselves. *) 6(* Accompanying tcTacs will offer a conversion to work with either set [...] *) 7(* sets and fmap [...] fmaps, only needing an equality-decider conversion *) 8(* for elements/arguments, or (prefeably) with FMAPAL fmaps & ENUMERAL sets, *) 9(* needing a conversion reducing a three-valued "toto" ordering, for which *) 10(* see totoTheory, totoTacs, and also enumeralTheory/Tacs, fmapalTheory/Tacs.*) 11 12(* app load ["pred_setLib", "pred_setTheory", "relationTheory", "pairTheory", 13"optionTheory", "TotalDefn", "bossLib", "finite_mapTheory", 14"wotTheory"]; *) (* wotTheory only for definiton of type 'a reln *) 15 16open HolKernel boolLib Parse bossLib; 17val _ = set_trace "Unicode" 0; 18open pred_setLib pred_setTheory relationTheory pairTheory optionTheory; 19open Defn TotalDefn combinTheory PairRules; 20open PairRules pairLib listTheory finite_mapTheory totoTheory; 21 22val _ = new_theory "tc"; 23 24(* My habitual abbreviations: *) 25 26val AR = ASM_REWRITE_TAC []; 27fun ulist x = [x]; 28fun rrs th = REWRITE_RULE [SPECIFICATION] th; 29 30val _ = Defn.def_suffix := ""; (* replacing default "_def" *) 31 32(* *************************************************************** *) 33 34val _ = set_fixity "^|" (Infixl 650); 35val _ = set_fixity "|^" (Infixl 650); 36val _ = set_fixity "^|^" (Infixl 650); 37 38(* Restriction of a relation to a subset of its domain, range, or both: 39^|, |^, ^|^ respectively. "RESTRICT" has been taken for mysterious purposes 40by the original relationTheory, and "DRESTRICT" by finite_mapTheory. *) 41 42val DRESTR = xDefine "DRESTR" 43`((R:'a reln) ^| (s:'a set)) a b = a IN s /\ R a b`; 44 45val DRESTR_IN = store_thm ("DRESTR_IN", 46``!R:'a reln s a. (R ^| s) a = if a IN s then R a else {}``, 47REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN REWRITE_TAC [DRESTR] THEN 48GEN_TAC THEN Cases_on `a IN s` THEN AR THEN 49REWRITE_TAC [rrs NOT_IN_EMPTY]); 50 51val RRESTR = xDefine "RRESTR" 52`((R:'a reln) |^ (s:'a set)) a b = b IN s /\ R a b`; 53 54(* restriction Both fore and aft *) 55 56val BRESTR = xDefine "BRESTR" `(R:'a reln) ^|^ s = R ^| s |^ s`; 57 58val DRESTR_EMPTY = store_thm ("DRESTR_EMPTY", 59``!R:'a reln. R ^| {} = REMPTY``, 60GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 61REWRITE_TAC [DRESTR_IN, NOT_IN_EMPTY, EMPTY_REL_DEF] THEN 62REWRITE_TAC [rrs NOT_IN_EMPTY]); 63 64val DRESTR_RDOM = store_thm ("DRESTR_RDOM", 65``!R:'a reln. R ^| (RDOM R) = R``, 66GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 67REWRITE_TAC [DRESTR_IN, IN_RDOM] THEN 68COND_CASES_TAC THENL 69[REFL_TAC 70,UNDISCH_THEN ``~?y. (R:'a reln) x y`` 71 (REWRITE_TAC o ulist o CONV_RULE NOT_EXISTS_CONV) THEN 72 REWRITE_TAC [rrs NOT_IN_EMPTY]]); 73 74val REMPTY_RRESTR = store_thm ("REMPTY_RRESTR", 75``!s. REMPTY:'a reln |^ s = REMPTY``, 76GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 77REWRITE_TAC [RRESTR, EMPTY_REL_DEF]); 78 79val O_REMPTY_O = store_thm ("O_REMPTY_O", 80``(!R:'a reln. R O REMPTY = REMPTY) /\ 81 (!R:'a reln. REMPTY O R = REMPTY)``, 82CONJ_TAC THEN GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 83REWRITE_TAC [EMPTY_REL_DEF, O_DEF]); 84 85(* Define subTC, the invariant for an arrayless form of the 86 Floyd-Warshall algorithm, in as low-level and symmetrical a way as 87 possible, with an eye to using (R)TC induction principles. *) 88 89val subTC = Define`subTC (R:'a reln) s x y = 90 R x y \/ ?a b. (R ^|^ s)^* a b /\ a IN s /\ b IN s /\ R x a /\ R b y`; 91 92(* Definition as first conceived becomes a theorem: *) 93(* Outer ^| s is meant just to trim off (x,x) pairs for x NOTIN s, and we 94 need a lemma about that: *) 95 96val RTC_trim_lem = BETA_RULE (prove ( 97``!R:'a reln s y y'. (\x. x IN s) y' /\ (R ^|^ s)^* y' y ==> (\x. x IN s) y``, 98REPEAT GEN_TAC THEN MATCH_MP_TAC RTC_lifts_invariants THEN BETA_TAC THEN 99REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN REPEAT STRIP_TAC THEN AR)); 100 101(* RTC_trim_lem = |- !R s y y'. y' IN s /\ (R ^|^ s)^* y' y ==> y IN s *) 102 103val subTC_thm = store_thm ("subTC_thm", 104``!R:'a reln s. subTC R s = R RUNION (R O ((R ^|^ s)^* ^| s) O R)``, 105REPEAT GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 106REWRITE_TAC [subTC, O_DEF, RUNION, DRESTR] THEN 107EQ_TAC THEN STRIP_TAC THEN AR THEN DISJ2_TAC THENL 108[EXISTS_TAC ``b:'a`` THEN AR THEN 109 EXISTS_TAC ``a:'a`` THEN AR 110,EXISTS_TAC ``y':'a`` THEN EXISTS_TAC ``y:'a`` THEN AR THEN 111 IMP_RES_TAC RTC_trim_lem]); 112 113val subTC_EMPTY = store_thm ("subTC_EMPTY", 114``!R:'a reln. subTC R {} = R``, 115GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 116REWRITE_TAC [subTC_thm, BRESTR, DRESTR_EMPTY, O_REMPTY_O, REMPTY_RRESTR, 117 EMPTY_REL_DEF, RUNION]); 118 119(* Dec 14 new departure: figure out what is bigger or equal (in fact equal) 120 to (R ^|^ (a INSERT s))^* because that's the only way I know to use a 121 transitive closure hypothesis. *) 122 123(* seemingly needs to be proved in two stages, one with RTC_STRONG_INDUCT, 124 one with RTC_STRONG_INDUCT_RIGHT1 *) 125 126val NOT_IN_RTC_EQ = prove ( 127``!R:'a reln s p q. (p NOTIN s \/ q NOTIN s) /\ (R ^|^ s)^* p q ==> (p = q)``, 128REPEAT GEN_TAC THEN CONV_TAC ANTE_CONJ_CONV THEN STRIP_TAC THENL 129[ONCE_REWRITE_TAC [RTC_CASES1], ONCE_REWRITE_TAC [RTC_CASES2]] THEN 130 CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN AR THEN 131 CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC THEN 132 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR]); 133 134val RTC_INSERT_MONO = prove ( 135``!R:'a reln s a w z. (R ^|^ s)^* w z ==> (R ^|^ (a INSERT s))^* w z``, 136REPEAT GEN_TAC THEN MATCH_MP_TAC RTC_MONOTONE THEN 137REPEAT GEN_TAC THEN REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] THEN 138STRIP_TAC THEN AR); 139 140val RTC_INSERT_RIGHT_IMP = prove ( 141``!R:'a reln s a w z. (R ^|^ (a INSERT s))^* w z ==> 142(R ^|^ s)^* w z \/ ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)``, 143REPEAT GEN_TAC THEN 144Cases_on `a IN s` 145THEN1 (IMP_RES_THEN SUBST1_TAC ABSORPTION_RWT THEN 146 DISCH_THEN (REWRITE_TAC o ulist)) THEN 147SUBGOAL_THEN ``(R:'a reln ^|^ s)^* w z \/ 148 ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z) = 149 (\w z. (R ^|^ s)^* w z \/ 150 ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)) w z`` 151SUBST1_TAC THEN1 (BETA_TAC THEN REFL_TAC) THEN 152MATCH_MP_TAC RTC_STRONG_INDUCT THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 153ASM_REWRITE_TAC [RTC_REFL] THENL 154 [Cases_on `x = a` THENL 155 [DISJ2_TAC THEN Cases_on `y IN s` THENL 156 [DISJ2_TAC THEN EXISTS_TAC ``y:'a`` THEN AR THEN 157 Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) x y` THEN 158 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN STRIP_TAC THEN AR 159 ,DISJ1_TAC THEN Q.SUBGOAL_THEN `z = y` ASSUME_TAC THENL 160 [IMP_RES_TAC NOT_IN_RTC_EQ THEN Cases_on `a = y` THEN AR 161 ,Cases_on `a = y` THEN1 AR THEN 162 Q.SUBGOAL_THEN `x = y` (ASM_REWRITE_TAC o ulist o SYM) THEN 163 Q.SUBGOAL_THEN `y NOTIN a INSERT s` ASSUME_TAC 164 THEN1 (ASM_REWRITE_TAC [IN_INSERT] THEN 165 Q.UNDISCH_THEN `a <> y` (ACCEPT_TAC o GSYM)) THEN 166 MATCH_MP_TAC (Q.SPECL [`R`, `a INSERT s`] NOT_IN_RTC_EQ) THEN 167 CONJ_TAC THENL [AR, IMP_RES_TAC RTC_SINGLE] 168 ]] 169 ,Cases_on `y = a` THENL 170 [DISJ2_TAC THEN 171 DISJ1_TAC THEN Q.SUBGOAL_THEN `y = z` (ASM_REWRITE_TAC o ulist o SYM) THEN 172 MATCH_MP_TAC NOT_IN_RTC_EQ THEN 173 Q.EXISTS_TAC `R` THEN Q.EXISTS_TAC `s` THEN AR 174 ,DISJ1_TAC THEN 175 ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN 176 AR THEN Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) x y` THEN 177 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] 178 ]] 179 ,DISJ2_TAC THEN DISJ2_TAC THEN Q.EXISTS_TAC `y'` THEN AR 180 ]); 181 182val RTC_INSERT_LEFT_IMP = prove ( 183``!R:'a reln s a w z. (R ^|^ (a INSERT s))^* w z ==> 184 (R ^|^ s)^* w z \/ ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a)``, 185REPEAT GEN_TAC THEN 186Cases_on `a IN s` 187THEN1 (IMP_RES_THEN SUBST1_TAC ABSORPTION_RWT THEN 188 DISCH_THEN (REWRITE_TAC o ulist)) THEN 189SUBGOAL_THEN ``(R:'a reln ^|^ s)^* w z \/ 190 ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a) = 191 (\w z. (R ^|^ s)^* w z \/ 192 ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a)) w z`` 193SUBST1_TAC THEN1 (BETA_TAC THEN REFL_TAC) THEN 194MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1 THEN BETA_TAC THEN REPEAT STRIP_TAC THEN 195ASM_REWRITE_TAC [RTC_REFL] THENL 196 [Cases_on `z = a` THENL 197 [DISJ2_TAC THEN Cases_on `y IN s` THENL 198 [DISJ2_TAC THEN EXISTS_TAC ``y:'a`` THEN AR THEN 199 Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) y z` THEN 200 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN STRIP_TAC THEN AR 201 ,DISJ1_TAC THEN Q.SUBGOAL_THEN `x = y` ASSUME_TAC THENL 202 [IMP_RES_TAC NOT_IN_RTC_EQ THEN Cases_on `a = y` THEN AR 203 ,Cases_on `a = y` THEN1 AR THEN 204 Q.SUBGOAL_THEN `y = z` (ASM_REWRITE_TAC o ulist) THEN 205 Q.SUBGOAL_THEN `y NOTIN a INSERT s` ASSUME_TAC 206 THEN1 (ASM_REWRITE_TAC [IN_INSERT] THEN 207 Q.UNDISCH_THEN `a <> y` (ACCEPT_TAC o GSYM)) THEN 208 MATCH_MP_TAC (Q.SPECL [`R`, `a INSERT s`] NOT_IN_RTC_EQ) THEN 209 CONJ_TAC THENL [AR, IMP_RES_TAC RTC_SINGLE] 210 ]] 211 ,Cases_on `y = a` THENL 212 [DISJ2_TAC THEN 213 DISJ1_TAC THEN Q.SUBGOAL_THEN `x = y` (ASM_REWRITE_TAC o ulist) THEN 214 MATCH_MP_TAC NOT_IN_RTC_EQ THEN 215 Q.EXISTS_TAC `R` THEN Q.EXISTS_TAC `s` THEN AR 216 ,DISJ1_TAC THEN 217 ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN 218 AR THEN Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) y z` THEN 219 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] 220 ]] 221 ,DISJ2_TAC THEN DISJ2_TAC THEN Q.EXISTS_TAC `x'` THEN AR 222 ]); 223 224val RTC_INSERT = store_thm ("RTC_INSERT", 225``!R:'a reln s a w z. (R ^|^ (a INSERT s))^* w z <=> 226(R ^|^ s)^* w z \/ ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a) /\ 227 ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)``, 228REPEAT GEN_TAC THEN EQ_TAC THENL 229[DISCH_TAC THEN CONV_TAC (REWR_CONV LEFT_OR_OVER_AND) THEN CONJ_TAC THENL 230 [MATCH_MP_TAC RTC_INSERT_LEFT_IMP THEN AR 231 ,MATCH_MP_TAC RTC_INSERT_RIGHT_IMP THEN AR 232 ] 233,STRIP_TAC THENL 234 [IMP_RES_TAC RTC_INSERT_MONO THEN AR 235 ,Q.UNDISCH_THEN `a = z` (CONV_TAC o RAND_CONV o REWR_CONV o SYM) THEN 236 Q.UNDISCH_THEN `a = w` 237 (CONV_TAC o RATOR_CONV o RAND_CONV o REWR_CONV o SYM) THEN 238 REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT, RTC_REFL] 239 ,ONCE_REWRITE_TAC [RTC_CASES1] THEN 240 DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN CONJ_TAC THENL 241 [Q.UNDISCH_THEN `a = w` (SUBST1_TAC o SYM) THEN 242 ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT] 243 ,IMP_RES_TAC RTC_INSERT_MONO THEN AR 244 ] 245 ,Q.UNDISCH_THEN `a = z` (CONV_TAC o RAND_CONV o REWR_CONV o SYM) THEN 246 ONCE_REWRITE_TAC [RTC_CASES2] THEN 247 DISJ2_TAC THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL 248 [IMP_RES_TAC RTC_INSERT_MONO THEN AR 249 ,ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT] 250 ] 251 ,MATCH_MP_TAC (REWRITE_RULE [transitive_def] (Q.SPEC `R` RTC_TRANSITIVE)) THEN 252 Q.EXISTS_TAC `a` THEN CONJ_TAC THENL 253 [ONCE_REWRITE_TAC [RTC_CASES2] THEN 254 DISJ2_TAC THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL 255 [IMP_RES_TAC RTC_INSERT_MONO THEN AR 256 ,ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT] 257 ] 258 ,ONCE_REWRITE_TAC [RTC_CASES1] THEN 259 DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN CONJ_TAC THENL 260 [ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT] 261 ,IMP_RES_TAC RTC_INSERT_MONO THEN AR 262]]]]); 263 264val NOT_EQ_RTC_IN = prove ( 265``!R:'a reln s p q. p <> q \/ q <> p ==> (R ^|^ s)^* p q ==> p IN s /\ q IN s``, 266REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN 267REWRITE_TAC [DE_MORGAN_THM, NOT_IMP] THEN REPEAT STRIP_TAC THENL 268[ALL_TAC, CONV_TAC (REWR_CONV EQ_SYM_EQ), 269 ALL_TAC, CONV_TAC (REWR_CONV EQ_SYM_EQ)] THEN 270MATCH_MP_TAC (Q.SPECL [`R`, `s`] NOT_IN_RTC_EQ) THEN AR); 271 272val RTC_IN_LR = prove ( 273``(!R:'a reln s p q. p IN s /\ (R ^|^ s)^* p q ==> q IN s)``, 274REPEAT STRIP_TAC THEN 275Cases_on `q IN s` THEN1 AR THEN 276IMP_RES_TAC NOT_IN_RTC_EQ THEN 277Q.UNDISCH_THEN `p = q` (SUBST1_TAC o SYM) THEN AR); 278 279val RTC_IN_RL = prove ( 280``(!R:'a reln s p q. q IN s /\ (R ^|^ s)^* p q ==> p IN s)``, 281REPEAT STRIP_TAC THEN 282Cases_on `p IN s` THEN1 AR THEN 283IMP_RES_TAC NOT_IN_RTC_EQ THEN 284Q.UNDISCH_THEN `p = q` SUBST1_TAC THEN AR); 285 286val RTC_subTC1 = prove ( 287``!R:'a reln s a w x. R w x /\ (R ^|^ (a INSERT s))^* x a ==> 288 subTC R s w a``, 289REPEAT GEN_TAC THEN REWRITE_TAC [subTC, RTC_INSERT] THEN STRIP_TAC THENL 290[Cases_on `a = x` THEN1 AR THEN 291 DISJ2_TAC THEN IMP_RES_TAC RTC_CASES2 292 THEN1 (Q.UNDISCH_TAC `a <> x` THEN AR) THEN 293 IMP_RES_TAC NOT_EQ_RTC_IN THEN 294 IMP_RES_TAC RTC_IN_LR THEN 295 Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `u` THEN 296 Q.UNDISCH_TAC `(R ^|^ s) u a` THEN 297 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR] 298,AR 299,DISJ2_TAC THEN Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `x'` THEN 300 IMP_RES_TAC RTC_IN_RL THEN AR 301]); 302 303val RTC_subTC2 = prove ( 304``!R:'a reln s a y z. (R ^|^ (a INSERT s))^* a y /\ R y z ==> 305 subTC R s a z``, 306REPEAT GEN_TAC THEN REWRITE_TAC [subTC, RTC_INSERT] THEN STRIP_TAC THENL 307[Cases_on `a = y` THEN1 AR THEN 308 DISJ2_TAC THEN IMP_RES_TAC RTC_CASES1 THEN 309 IMP_RES_TAC NOT_EQ_RTC_IN THEN 310 IMP_RES_TAC RTC_IN_RL THEN 311 Q.EXISTS_TAC `u` THEN Q.EXISTS_TAC `y` THEN 312 Q.UNDISCH_TAC `(R ^|^ s) a u` THEN 313 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR] 314,AR 315,DISJ2_TAC THEN Q.EXISTS_TAC `y'` THEN Q.EXISTS_TAC `y` THEN 316 IMP_RES_TAC RTC_IN_LR THEN AR 317]); 318 319(* The big lemma: what enlarging s by one does to subTC R x *) 320 321val subTC_INSERT = store_thm ("subTC_INSERT", 322``!R:'a reln s q x y. subTC R (q INSERT s) x y <=> 323 subTC R s x y \/ subTC R s x q /\ subTC R s q y``, 324REPEAT GEN_TAC THEN EQ_TAC THENL 325[CONV_TAC (LAND_CONV (REWRITE_CONV [subTC])) THEN 326 REWRITE_TAC [DISJ_IMP_THM] THEN CONJ_TAC THENL 327 [DISCH_TAC THEN ASM_REWRITE_TAC [subTC] 328 ,REPEAT (CONV_TAC LEFT_IMP_EXISTS_CONV THEN GEN_TAC) THEN 329 Cases_on `q IN s` 330 THEN1 (IMP_RES_THEN SUBST1_TAC ABSORPTION_RWT THEN 331 STRIP_TAC THEN DISJ1_TAC THEN REWRITE_TAC [subTC] THEN 332 DISJ2_TAC THEN Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b` THEN AR) THEN 333 STRIP_TAC THEN 334 Cases_on `a = q` THENL 335 [DISJ2_TAC THEN CONJ_TAC THENL 336 [Q.UNDISCH_THEN `a = q` (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [subTC] 337 ,MATCH_MP_TAC RTC_subTC2 THEN Q.EXISTS_TAC `b` THEN AR THEN 338 Q.UNDISCH_THEN `a = q` 339 (CONV_TAC o RATOR_CONV o RAND_CONV o REWR_CONV o SYM) THEN AR 340 ] 341 ,Q.SUBGOAL_THEN `a IN s` ASSUME_TAC THEN1 IMP_RES_TAC IN_INSERT THEN 342 Cases_on `b = q` THENL 343 [DISJ2_TAC THEN CONJ_TAC THENL 344 [MATCH_MP_TAC RTC_subTC1 THEN Q.EXISTS_TAC `a` THEN AR THEN 345 Q.UNDISCH_THEN `b = q` 346 (CONV_TAC o RAND_CONV o REWR_CONV o SYM) THEN AR 347 ,Q.UNDISCH_THEN `b = q` (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [subTC] 348 ] 349 ,Q.SUBGOAL_THEN `b IN s` ASSUME_TAC THEN1 IMP_RES_TAC IN_INSERT THEN 350 Cases_on `(R ^|^ s)^* a b` 351 THEN1 (DISJ1_TAC THEN ASM_REWRITE_TAC [subTC] THEN DISJ2_TAC THEN 352 Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b` THEN AR) THEN 353 Q.UNDISCH_TAC `(R ^|^ (q INSERT s))^* a b` THEN 354 REWRITE_TAC [RTC_INSERT] THEN 355 STRIP_TAC THENL 356 [Q.UNDISCH_TAC `a <> q` THEN Q.UNDISCH_THEN `q = a` (REWRITE_TAC o ulist) 357 ,Q.UNDISCH_TAC `a <> q` THEN AR 358 ,Q.UNDISCH_TAC `b <> q` THEN AR 359 ,DISJ2_TAC THEN CONJ_TAC THEN ASM_REWRITE_TAC [subTC] THEN DISJ2_TAC THENL 360 [Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `x'` THEN AR 361 ,Q.EXISTS_TAC `y'` THEN Q.EXISTS_TAC `b` THEN AR 362 ]]]]] 363,REWRITE_TAC [DISJ_IMP_THM] THEN REWRITE_TAC [subTC] THEN CONJ_TAC THENL 364 [STRIP_TAC THEN1 AR THEN DISJ2_TAC THEN 365 Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b` THEN 366 IMP_RES_TAC RTC_INSERT_MONO THEN ASM_REWRITE_TAC [IN_INSERT] 367 ,STRIP_TAC THEN DISJ2_TAC THENL 368 [Q.EXISTS_TAC `q` THEN Q.EXISTS_TAC `q` THEN 369 ASM_REWRITE_TAC [IN_INSERT, RTC_REFL] 370 ,Q.EXISTS_TAC `q` THEN Q.EXISTS_TAC `b` THEN ASM_REWRITE_TAC [IN_INSERT] THEN 371 ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN 372 Q.EXISTS_TAC `a` THEN IMP_RES_TAC RTC_INSERT_MONO THEN 373 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] 374 ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `q` THEN ASM_REWRITE_TAC [IN_INSERT] THEN 375 ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN 376 Q.EXISTS_TAC `b` THEN IMP_RES_TAC RTC_INSERT_MONO THEN 377 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] 378 ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b'` THEN ASM_REWRITE_TAC [IN_INSERT] THEN 379 MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) THEN 380 Q.EXISTS_TAC `q` THEN CONJ_TAC THENL 381 [ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN 382 Q.EXISTS_TAC `b` THEN IMP_RES_TAC RTC_INSERT_MONO THEN 383 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] 384 ,ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN 385 Q.EXISTS_TAC `a'` THEN IMP_RES_TAC RTC_INSERT_MONO THEN 386 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] 387]]]]); 388 389val subTC_RDOM = store_thm ("subTC_RDOM", 390``!R:'a reln. subTC R (RDOM R) = R^+``, 391GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN EQ_TAC THENL 392[REWRITE_TAC [subTC, DISJ_IMP_THM] THEN 393 CONJ_TAC THEN1 MATCH_ACCEPT_TAC TC_SUBSET THEN 394 STRIP_TAC THEN 395 MATCH_MP_TAC EXTEND_RTC_TC THEN Q.EXISTS_TAC `a` THEN AR THEN 396 ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `b` THEN 397 AR THEN Q.UNDISCH_TAC `(R ^|^ RDOM R)^* a b` THEN 398 MATCH_MP_TAC RTC_MONOTONE THEN 399 REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN REPEAT STRIP_TAC THEN AR 400,MATCH_MP_TAC TC_INDUCT THEN REWRITE_TAC [subTC] THEN 401 REPEAT STRIP_TAC 402 THEN1 AR THEN DISJ2_TAC THENL 403 [Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `y` THEN 404 ASM_REWRITE_TAC [RTC_REFL, IN_RDOM] THEN Q.EXISTS_TAC `z` THEN AR 405 ,Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `b` THEN 406 ASM_REWRITE_TAC [IN_RDOM] THEN CONJ_TAC THENL 407 [ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN Q.EXISTS_TAC `a` THEN 408 ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM] 409 ,ALL_TAC 410 ] THEN Q.EXISTS_TAC `a` THEN AR 411 ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `y` THEN 412 ASM_REWRITE_TAC [IN_RDOM] THEN CONJ_TAC THENL 413 [ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `b` THEN 414 ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM] 415 ,ALL_TAC 416 ] THEN Q.EXISTS_TAC `z` THEN AR 417 ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b'` THEN 418 ASM_REWRITE_TAC [IN_RDOM] THEN 419 MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) THEN 420 Q.EXISTS_TAC `y` THEN CONJ_TAC THENL 421 [ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `b` THEN 422 ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM] THEN 423 Q.EXISTS_TAC `a'` THEN AR 424 ,ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN Q.EXISTS_TAC `a'` THEN 425 ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM] THEN 426 Q.EXISTS_TAC `a'` THEN AR 427]]]); 428 429(* following corollary suggests how we want to compute. *) 430 431val subTC_INSERT_COR = store_thm ("subTC_INSERT_COR", 432``!R:'a reln s x a. subTC R (x INSERT s) a = 433 if x IN subTC R s a then subTC R s a UNION subTC R s x else subTC R s a``, 434REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 435REWRITE_TAC [SPECIFICATION, subTC_INSERT, COND_RATOR, rrs IN_UNION] THEN 436tautLib.TAUT_TAC); 437 438val RDOM_EMPTY = prove ( 439``!R:'a reln. (RDOM R = {}) ==> (R = REMPTY) /\ (!s. subTC R s = REMPTY)``, 440GEN_TAC THEN CONV_TAC (LAND_CONV FUN_EQ_CONV) THEN 441REWRITE_TAC [RDOM_DEF, rrs NOT_IN_EMPTY] THEN 442CONV_TAC (ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN STRIP_TAC THEN 443CONJ_TAC THEN REPEAT GEN_TAC THEN 444REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 445ASM_REWRITE_TAC [subTC, EMPTY_REL_DEF]); 446 447(* *************************************************************** *) 448(* Define the mapping by which set-valued finite maps represent *) 449(* binary relations of finite RDOM, and a one-sided inverse. *) 450(* *************************************************************** *) 451 452val FMAP_TO_RELN = Define 453`FMAP_TO_RELN (f:'a |-> 'a set) x = if x IN FDOM f then f ' x else {}`; 454 455val RELN_TO_FMAP = Define`RELN_TO_FMAP (R:'a reln) = FUN_FMAP R (RDOM R)`; 456 457val RDOM_SUBSET_FDOM = store_thm ("RDOM_SUBSET_FDOM", 458``!f:'a |-> 'a set. RDOM (FMAP_TO_RELN f) SUBSET FDOM f``, 459GEN_TAC THEN 460REWRITE_TAC [SUBSET_DEF, IN_RDOM, FMAP_TO_RELN] THEN 461Cases_on `x IN FDOM f` THEN ASM_REWRITE_TAC [rrs NOT_IN_EMPTY]); 462 463val FINITE_RDOM = store_thm ("FINITE_RDOM", 464``!f:'a |-> 'a set. FINITE (RDOM (FMAP_TO_RELN f))``, 465GEN_TAC THEN MP_TAC (SPEC_ALL RDOM_SUBSET_FDOM) THEN 466MATCH_MP_TAC SUBSET_FINITE THEN MATCH_ACCEPT_TAC FDOM_FINITE); 467 468val FDOM_RDOM = store_thm ("FDOM_RDOM", 469``!R:'a reln. FINITE (RDOM R) ==> (FDOM (RELN_TO_FMAP R) = RDOM R)``, 470REPEAT STRIP_TAC THEN 471IMP_RES_TAC (INST_TYPE [beta |-> ``:'a set``] FUN_FMAP_DEF) THEN 472ASM_REWRITE_TAC [RELN_TO_FMAP]); 473 474val RELN_TO_FMAP_TO_RELN_ID = store_thm ("RELN_TO_FMAP_TO_RELN_ID", 475``!R:'a reln. FINITE (RDOM R) ==> (FMAP_TO_RELN (RELN_TO_FMAP R) = R)``, 476REPEAT STRIP_TAC THEN IMP_RES_TAC FDOM_RDOM THEN 477CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 478REWRITE_TAC [FMAP_TO_RELN] THEN 479COND_CASES_TAC THENL 480[REWRITE_TAC [RELN_TO_FMAP] THEN 481 IMP_RES_TAC (INST_TYPE [beta |-> ``:'a set``] FUN_FMAP_DEF) THEN 482 Q.UNDISCH_TAC `x IN FDOM (RELN_TO_FMAP R)` THEN AR THEN DISCH_TAC THEN 483 RES_TAC THEN AR 484,CONV_TAC (REWR_CONV EQ_SYM_EQ) THEN 485 Q.UNDISCH_TAC `x NOTIN FDOM (RELN_TO_FMAP R)` THEN 486 ASM_REWRITE_TAC [IN_RDOM, GSYM SUBSET_EMPTY, SUBSET_DEF, NOT_IN_EMPTY, 487 IN_RDOM] THEN 488 REWRITE_TAC [SPECIFICATION] THEN 489 CONV_TAC (LAND_CONV NOT_EXISTS_CONV) THEN REWRITE_TAC []]); 490 491(* *** Now we may start to think about a conversion (actually two combined 492 under one name, one relying on pred_set.UNION_CONV and linear lists, the 493 other, which shoud be a somewhat nippier performer, making use of 494 an ENERMERAL-valued FMAPAL, but both following Warshall's algorithm 495 as closely as their data structures will permit) for TC. 496 Decided here not to call it "Floyd-Warshall algorithm", as Floyd's 497 addition was specifically for computing shortest paths from real 498 matrices represented edge-weighted graphs, rather than just transitive 499 closure of a relation, which Warshall had covered. Most likely, using 500 fmaps to real instead of finite sets, we could imitate 501 Floyd if there were any demand for it. *** *) 502 503val RDOM_subTC = store_thm ("RDOM_subTC", 504``!R:'a reln s. RDOM (subTC R s) = RDOM R``, 505REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 506REWRITE_TAC [RDOM_DEF, subTC] THEN EQ_TAC THEN STRIP_TAC THENL 507[Q.EXISTS_TAC `y` THEN AR 508,Q.EXISTS_TAC `a` THEN AR 509,Q.EXISTS_TAC `y` THEN AR]); 510 511val NOT_IN_RDOM = store_thm ("NOT_IN_RDOM", 512``!Q:'a reln x. (Q x = {}) <=> x NOTIN RDOM Q``, 513REPEAT GEN_TAC THEN REWRITE_TAC [RDOM_DEF, SPECIFICATION] THEN 514CONV_TAC (LAND_CONV FUN_EQ_CONV) THEN REWRITE_TAC [rrs NOT_IN_EMPTY] THEN 515CONV_TAC (LAND_CONV FORALL_NOT_CONV) THEN AR); 516 517(* Break out the function to be used by TC_ITER *) 518 519val TC_MOD = Define 520`TC_MOD (x:'a) (rx:'a set) (ra:'a set) = if x IN ra then ra UNION rx else ra`; 521 522val TC_MOD_EMPTY_ID = store_thm ("TC_MOD_EMPTY_ID", 523``!x:'a ra:'a set. TC_MOD x {} = I``, 524REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] [TC_MOD]); 525 526val I_o_f = store_thm ("I_o_f", ``!f:'a |-> 'b. I o_f f = f``, 527SRW_TAC [] [fmap_EXT]); 528 529val subTC_MAX_RDOM = store_thm ("subTC_MAX_RDOM", 530``!R:'a reln s x. x NOTIN RDOM R ==> (subTC R (x INSERT s) = subTC R s)``, 531REPEAT STRIP_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN 532REWRITE_TAC [subTC_INSERT] THEN 533`x NOTIN RDOM (subTC R s)` by METIS_TAC [RDOM_subTC] THEN 534METIS_TAC [RDOM_DEF, SPECIFICATION]); 535 536val subTC_SUPERSET_RDOM = store_thm ("subTC_SUPERSET_RDOM", 537``!R:'a reln s. FINITE s ==> (subTC R (RDOM R UNION s) = subTC R (RDOM R))``, 538GEN_TAC THEN CONV_TAC (TOP_DEPTH_CONV FUN_EQ_CONV) THEN 539HO_MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL 540[REWRITE_TAC [UNION_EMPTY] 541,REPEAT STRIP_TAC THEN 542 `RDOM R UNION (e INSERT s) = (e INSERT RDOM R) UNION s` 543 by (SRW_TAC [] [EXTENSION, IN_UNION, IN_INSERT, DISJ_ASSOC] THEN 544 CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV DISJ_COMM))) THEN REFL_TAC) THEN 545 AR THEN Cases_on `e IN RDOM R` THENL 546 [IMP_RES_THEN (ASM_REWRITE_TAC o ulist) ABSORPTION_RWT 547 ,IMP_RES_TAC subTC_MAX_RDOM THEN ASM_REWRITE_TAC [INSERT_UNION] 548]]); 549 550val subTC_FDOM = store_thm ("subTC_FDOM", ``!g R:'a reln. 551(subTC R (RDOM R) = FMAP_TO_RELN g) ==> (subTC R (FDOM g) = subTC R (RDOM R))``, 552REPEAT STRIP_TAC THEN 553Q.SUBGOAL_THEN `RDOM R SUBSET FDOM g` 554(SUBST1_TAC o GSYM o REWRITE_RULE [SUBSET_UNION_ABSORPTION]) THENL 555[Q.SUBGOAL_THEN `RDOM (subTC R (RDOM R)) = RDOM R` (SUBST1_TAC o SYM) 556 THEN1 MATCH_ACCEPT_TAC RDOM_subTC THEN 557 ASM_REWRITE_TAC [RDOM_SUBSET_FDOM] 558,MATCH_MP_TAC subTC_SUPERSET_RDOM THEN MATCH_ACCEPT_TAC FDOM_FINITE 559]); 560 561val SUBSET_FDOM_LEM = store_thm ("SUBSET_FDOM_LEM", 562``!R:'a reln s f. (subTC R s = FMAP_TO_RELN f) ==> RDOM R SUBSET FDOM f``, 563REPEAT STRIP_TAC THEN 564Q.SUBGOAL_THEN `RDOM R = RDOM (subTC R s)` SUBST1_TAC 565THEN1 MATCH_ACCEPT_TAC (GSYM RDOM_subTC) THEN AR THEN 566MATCH_ACCEPT_TAC RDOM_SUBSET_FDOM); 567 568(* Following is what seems needed: and now it needs a name. *) 569 570val subTC_FDOM_RDOM = store_thm ("subTC_FDOM_RDOM", 571``!R:'a reln f. (subTC R (FDOM f) = FMAP_TO_RELN f) ==> 572 (subTC R (RDOM R) = FMAP_TO_RELN f)``, 573REPEAT STRIP_TAC THEN 574Q.SUBGOAL_THEN `subTC R (FDOM f) = subTC R (RDOM R)` 575(ASM_REWRITE_TAC o ulist o SYM) THEN 576Q.SUBGOAL_THEN `FDOM f = RDOM R UNION FDOM f` 577(fn eq => SUBST1_TAC eq THEN MATCH_MP_TAC subTC_SUPERSET_RDOM THEN 578 MATCH_ACCEPT_TAC FDOM_FINITE) THEN 579Q.SUBGOAL_THEN `RDOM R SUBSET FDOM f` MP_TAC 580THEN1 (MATCH_MP_TAC SUBSET_FDOM_LEM THEN Q.EXISTS_TAC `FDOM f` THEN AR) THEN 581RW_TAC bool_ss [SUBSET_DEF, IN_UNION, EXTENSION] THEN METIS_TAC [] 582); 583 584(* We will use fmapalTheory.o_f_bt_map to compute the o_f in the following 585 lemma, but proving the lemma is another story. *) 586 587val TC_MOD_LEM = store_thm ("TC_MOD_LEM", 588``!R:'a reln s x f. x IN FDOM f /\ (subTC R s = FMAP_TO_RELN f) ==> 589 (subTC R (x INSERT s) = FMAP_TO_RELN (TC_MOD x (f ' x) o_f f))``, 590REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 591ASM_REWRITE_TAC [FMAP_TO_RELN, GSYM o_f_FDOM, subTC_INSERT_COR] THEN 592Cases_on `x' IN FDOM f` THEN 593ASM_REWRITE_TAC [EXTENSION] THENL 594[IMP_RES_THEN (REWRITE_TAC o ulist) 595 (REWRITE_RULE [GSYM o_f_FDOM] (Q.SPEC `TC_MOD x (f ' x)` 596 (INST_TYPE [beta |-> ``:'a set``, gamma |-> ``:'a set``] o_f_DEF))) THEN 597 GEN_TAC THEN CONV_TAC (RAND_CONV (REWR_CONV SPECIFICATION)) THEN 598 RW_TAC bool_ss [TC_MOD, SPECIFICATION, UNION_EMPTY] 599,SRW_TAC [] [] 600]); 601 602(* Define the recursion over RDOM R *) 603 604val TC_ITER = Define 605`(TC_ITER [] (r:'a|->'a set) = r) /\ 606 (TC_ITER (x :: d) r = TC_ITER d (TC_MOD x (r ' x) o_f r))`; 607 608val TC_ITER_THM = store_thm ("TC_ITER_THM", 609``!R:'a reln d f s. (s UNION set d = FDOM f) /\ 610 (subTC R s = FMAP_TO_RELN f) ==> 611 (TC R = FMAP_TO_RELN (TC_ITER d f))``, 612GEN_TAC THEN Induct THENL 613[REPEAT GEN_TAC THEN REWRITE_TAC [LIST_TO_SET_THM, UNION_EMPTY] THEN 614 CONV_TAC ANTE_CONJ_CONV THEN DISCH_THEN SUBST1_TAC THEN 615 DISCH_THEN (MP_TAC o MATCH_MP subTC_FDOM_RDOM) THEN 616 REWRITE_TAC [TC_ITER, subTC_RDOM] 617,REPEAT STRIP_TAC THEN 618 Q.SUBGOAL_THEN `h IN FDOM f` ASSUME_TAC THENL 619 [Q.UNDISCH_THEN `s UNION set (h::d) = FDOM f` (SUBST1_TAC o SYM) THEN 620 REWRITE_TAC [IN_UNION, MEM] 621 ,Q.SUBGOAL_THEN `(h INSERT s) UNION set d = FDOM f` ASSUME_TAC THENL 622 [Q.UNDISCH_THEN `s UNION set (h::d) = FDOM f` (SUBST1_TAC o SYM) THEN 623 REWRITE_TAC [LIST_TO_SET_THM, INSERT_UNION_EQ] THEN 624 CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV UNION_COMM)) THEN 625 REWRITE_TAC [INSERT_UNION_EQ] 626 ,IMP_RES_TAC TC_MOD_LEM THEN 627 `(h INSERT s) UNION set d = FDOM (TC_MOD h (f ' h) o_f f)` by 628 ASM_REWRITE_TAC [FDOM_o_f] THEN 629 RES_TAC THEN ASM_REWRITE_TAC [TC_ITER] 630]]]); 631 632val _ = export_theory (); 633