1open HolKernel boolLib bossLib Parse pred_setTheory relationTheory 2finite_mapTheory termTheory ramanaLib whileTheory 3prim_recTheory arithmeticTheory bagTheory listTheory; 4 5val _ = new_theory "subst"; 6 7val FUNPOW_extends_mono = Q.store_thm( 8"FUNPOW_extends_mono", 9`���P f. (���x. P x ��� P (f x)) ��� P x ��� P (FUNPOW f n x)`, 10STRIP_TAC THEN Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]); 11 12val _ = type_abbrev ("subst", ``:(num |-> 'a term)``); 13 14val rangevars_def = Define` 15 rangevars s = BIGUNION (IMAGE vars (FRANGE s))`; 16 17val FINITE_rangevars = RWstore_thm( 18"FINITE_rangevars", 19`FINITE (rangevars s)`, 20SRW_TAC [][rangevars_def] THEN SRW_TAC [][]); 21 22val IN_FRANGE_rangevars = Q.store_thm( 23"IN_FRANGE_rangevars", 24`t ��� FRANGE s ��� vars t SUBSET rangevars s`, 25SRW_TAC [][rangevars_def,SUBSET_DEF] THEN METIS_TAC []); 26 27val rangevars_FUPDATE = Q.store_thm( 28"rangevars_FUPDATE", 29`v ��� FDOM s ��� (rangevars (s |+ (v,t)) = rangevars s UNION vars t)`, 30SRW_TAC [][rangevars_def,DOMSUB_NOT_IN_DOM,UNION_COMM]); 31 32val substvars_def = Define` 33 substvars s = FDOM s UNION rangevars s`; 34 35val FINITE_substvars = RWstore_thm( 36"FINITE_substvars", 37`FINITE (substvars s)`, 38SRW_TAC [][substvars_def]); 39 40val vR_def = Define` 41 vR s y x = case FLOOKUP s x of SOME t => y IN vars t | _ => F`; 42 43val wfs_def = Define`wfs s = WF (vR s)`; 44 45val wfs_FEMPTY = RWstore_thm( 46"wfs_FEMPTY", 47`wfs FEMPTY`, 48SRW_TAC [][wfs_def] THEN 49Q_TAC SUFF_TAC `vR FEMPTY = EMPTY_REL` THEN1 METIS_TAC [WF_EMPTY_REL] THEN 50SRW_TAC [][FUN_EQ_THM,vR_def]); 51 52val wfs_SUBMAP = Q.store_thm( 53"wfs_SUBMAP", 54`wfs sx /\ s SUBMAP sx ==> wfs s`, 55SRW_TAC [][wfs_def,SUBMAP_DEF] THEN 56Q_TAC SUFF_TAC `!y x.vR s y x ==> vR sx y x` 57 THEN1 METIS_TAC [WF_SUBSET] THEN 58SRW_TAC [][vR_def,FLOOKUP_DEF] THEN 59METIS_TAC []); 60 61val wfs_no_cycles = Q.store_thm( 62 "wfs_no_cycles", 63 `wfs s <=> !v. ~(vR s)^+ v v`, 64 EQ_TAC THEN1 METIS_TAC [WF_TC,wfs_def,WF_NOT_REFL] THEN 65 SRW_TAC [] [wfs_def,WF_IFF_WELLFOUNDED,wellfounded_def] THEN 66 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 67 `!n. (f n) IN FDOM s /\ f (SUC n) IN vars (s ' (f n))` by 68 (STRIP_TAC THEN Q.PAT_X_ASSUM `!n.vR s (f (SUC n)) (f n)` (Q.SPEC_THEN `n` MP_TAC) 69 THEN FULL_SIMP_TAC (srw_ss()) [vR_def] THEN Cases_on `FLOOKUP s (f n)` THEN 70 Q.PAT_X_ASSUM `FLOOKUP s (f n) = Z` MP_TAC THEN SRW_TAC [] [FLOOKUP_DEF]) 71 THEN 72 `!n m. (vR s)^+ (f (SUC (n + m))) (f n)` by 73 (REPEAT STRIP_TAC THEN Induct_on `m` THEN1 74 (SRW_TAC [] [] THEN METIS_TAC [TC_SUBSET]) THEN 75 Q.PAT_X_ASSUM `!n. f n IN FDOM s /\ Z` (Q.SPEC_THEN `SUC (n + m)` MP_TAC) 76 THEN SRW_TAC [] [] THEN 77 `(vR s) (f (SUC (SUC (n + m)))) (f (SUC (n + m)))` by METIS_TAC 78 [vR_def,FLOOKUP_DEF] THEN METIS_TAC [TC_RULES,ADD_SUC]) 79 THEN 80 `?n m. f (SUC (n + m)) = f n` by 81 (`~INJ f (count (SUC (CARD (FDOM s)))) (FDOM s)` 82 by (SRW_TAC [] [PHP,CARD_COUNT,COUNT_SUC,CARD_DEF]) THEN 83 FULL_SIMP_TAC (srw_ss()) [INJ_DEF] THEN1 METIS_TAC [] THEN 84 ASSUME_TAC (Q.SPECL [`x`,`y`] LESS_LESS_CASES) THEN 85 FULL_SIMP_TAC (srw_ss()) [] THEN1 METIS_TAC [] THENL [ 86 Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `y - x - 1`, 87 Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `x - y - 1` 88 ] THEN SRW_TAC [ARITH_ss] [ADD1]) 89 THEN METIS_TAC []); 90 91val subst_APPLY_def = Define` 92 (subst_APPLY s (Var v) = case FLOOKUP s v of NONE => Var v | SOME t => t) /\ 93 (subst_APPLY s (Pair t1 t2) = Pair (subst_APPLY s t1) (subst_APPLY s t2)) /\ 94 (subst_APPLY s (Const c) = Const c)`; 95val _ = set_fixity "���" (Infixr 700); 96val _ = overload_on ("���", ``subst_APPLY``) 97val _ = export_rewrites["subst_APPLY_def"]; 98 99val subst_APPLY_FAPPLY = Q.store_thm( 100"subst_APPLY_FAPPLY", 101`v IN FDOM s ==> (s ' v = s ��� (Var v))`, 102SRW_TAC [][subst_APPLY_def,FLOOKUP_DEF]); 103 104val noids_def = Define` 105 noids s = ���v. FLOOKUP s v ��� SOME (Var v)`; 106 107val subst_APPLY_id = Q.store_thm( 108"subst_APPLY_id", 109`(s ��� t = t) <=> !v.v IN (vars t) ��� v IN FDOM s ��� (s ' v = Var v)`, 110EQ_TAC THEN 111Induct_on `t` THEN SRW_TAC [][FLOOKUP_DEF] THEN 112FULL_SIMP_TAC (srw_ss()) []); 113 114val idempotent_def = Define` 115 idempotent s = !t.s ��� (s ��� t) = s ��� t`; 116 117val wfs_noids = Q.store_thm( 118"wfs_noids", 119`wfs s ��� noids s`, 120SRW_TAC [][wfs_no_cycles,noids_def] THEN 121SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 122FIRST_X_ASSUM (Q.SPEC_THEN `v` MP_TAC) THEN 123SRW_TAC [][] THEN MATCH_MP_TAC TC_SUBSET THEN 124SRW_TAC [][vR_def]); 125 126val idempotent_rangevars = Q.store_thm( 127"idempotent_rangevars", 128`idempotent s ��� noids s <=> DISJOINT (FDOM s) (rangevars s)`, 129EQ_TAC THEN1 ( 130 SRW_TAC [][DISJOINT_BIGUNION,idempotent_def,noids_def,FLOOKUP_DEF,rangevars_def] THEN 131 `���v. v IN FDOM s ��� (s ' v = x)` 132 by (POP_ASSUM MP_TAC THEN SRW_TAC [][FRANGE_DEF]) THEN 133 FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN 134 SRW_TAC [][FLOOKUP_DEF] THEN 135 IMP_RES_TAC subst_APPLY_id THEN 136 SRW_TAC [][IN_DISJOINT] THEN 137 METIS_TAC [] ) THEN 138SRW_TAC [][noids_def,IN_DISJOINT,FLOOKUP_DEF,idempotent_def,subst_APPLY_id,rangevars_def] THEN1 ( 139 Induct_on `t` THEN SRW_TAC [][FLOOKUP_DEF] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 140 `s ' n IN FRANGE s` by (SRW_TAC [][FRANGE_DEF] THEN METIS_TAC []) THEN 141 METIS_TAC [] ) THEN 142Cases_on `v IN FDOM s` THEN SRW_TAC [][] THEN 143`s ' v IN FRANGE s` by (SRW_TAC [][FRANGE_DEF] THEN METIS_TAC []) THEN 144`v NOTIN (vars (s ' v))` by METIS_TAC [] THEN 145Cases_on `s ' v` THEN FULL_SIMP_TAC (srw_ss()) []); 146 147val wfs_FAPPLY_var = Q.store_thm( 148"wfs_FAPPLY_var", 149`wfs s ==> !v.v IN FDOM s ==> s ' v <> (Var v)`, 150SRW_TAC [][wfs_no_cycles] THEN 151`~vR s v v` by METIS_TAC [TC_SUBSET] THEN 152POP_ASSUM MP_TAC THEN 153Cases_on `s ' v` THEN 154SRW_TAC [][vR_def,FLOOKUP_DEF]); 155 156val TC_vR_vars_FRANGE = Q.store_thm( 157"TC_vR_vars_FRANGE", 158`���u v. (vR s)^+ u v ��� v IN FDOM s ��� u IN BIGUNION (IMAGE vars (FRANGE s))`, 159HO_MATCH_MP_TAC TC_STRONG_INDUCT_RIGHT1 THEN 160SRW_TAC [][vR_def] THEN1 ( 161 Cases_on `FLOOKUP s v` THEN FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN 162 Q.EXISTS_TAC `vars x` THEN SRW_TAC [][] THEN SRW_TAC [][FRANGE_DEF] THEN 163 Q.EXISTS_TAC `s ' v` THEN SRW_TAC [][] THEN 164 Q.EXISTS_TAC `v` THEN SRW_TAC [][] ) THEN 165FIRST_X_ASSUM MATCH_MP_TAC THEN 166IMP_RES_TAC TC_CASES2_E THEN 167FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 168FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN 169Cases_on `v IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) []); 170 171val wfs_idempotent = Q.store_thm( 172"wfs_idempotent", 173`idempotent s ��� noids s ��� wfs s`, 174STRIP_TAC THEN IMP_RES_TAC idempotent_rangevars THEN 175FULL_SIMP_TAC (srw_ss()) [rangevars_def] THEN 176SRW_TAC [][wfs_no_cycles] THEN 177SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 178IMP_RES_TAC TC_vR_vars_FRANGE THEN 179IMP_RES_TAC TC_CASES2_E THEN 180FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN 181Cases_on `v IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 182RES_TAC THEN SRW_TAC [][] THEN 183METIS_TAC [IN_DISJOINT]); 184 185val _ = set_fixity "s_o_s"(Infixl 740); 186 187val s_o_s_def = Define` 188 s1 s_o_s s2 = FUN_FMAP (($��� s1) o ($��� s2 o Var)) (FDOM s1 ��� FDOM s2)`; 189 190val selfapp_def = Define` 191 (selfapp s = ($��� s) o_f s)`; 192 193val selfapp_eq_iter_APPLY = Q.store_thm( 194"selfapp_eq_iter_APPLY", 195`���t. (selfapp s) ��� t = s ��� (s ��� t)`, 196Induct THEN SRW_TAC [][selfapp_def,FLOOKUP_DEF]); 197 198val FDOM_selfapp = RWstore_thm( 199"FDOM_selfapp", 200`FDOM (selfapp s) = FDOM s`, 201SRW_TAC [][selfapp_def]); 202 203val selfapp_eq_s_o_s = Q.store_thm( 204"selfapp_eq_s_o_s", 205`selfapp s = s s_o_s s`, 206SRW_TAC [][GSYM fmap_EQ,selfapp_def,s_o_s_def,FUN_FMAP_DEF,FUN_EQ_THM] THEN 207Cases_on `x ��� FDOM s` THEN SRW_TAC [][FUN_FMAP_DEF,NOT_FDOM_FAPPLY_FEMPTY,FLOOKUP_DEF]); 208 209val IN_vars_APPLY = Q.store_thm( 210"IN_vars_APPLY", 211`���t v. v IN vars (s ��� t) ��� v NOTIN FDOM s ��� v IN vars t ��� ���x. vR s v x ��� x IN vars t`, 212Induct THEN SRW_TAC [][vR_def] THEN 213SRW_TAC [][FLOOKUP_DEF] THEN EQ_TAC THEN 214FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 215SRW_TAC [][] THEN METIS_TAC []); 216 217val vR1_def = Define` 218 vR1 s y x = vR s y x ��� y NOTIN FDOM s`; 219 220val vR_selfapp = Q.store_thm( 221"vR_selfapp", 222`vR (selfapp s) = vR1 s RUNION NRC (vR s) 2`, 223SRW_TAC [][RUNION,FUN_EQ_THM,vR1_def,selfapp_def,vR_def, 224 FLOOKUP_DEF,EQ_IMP_THM] THEN 225FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 226Cases_on `x' IN FDOM s` THEN 227FULL_SIMP_TAC (srw_ss()) [IN_vars_APPLY,vR_def,FLOOKUP_DEF] THEN 228METIS_TAC []); 229 230val vR1_selfapp = Q.store_thm( 231"vR1_selfapp", 232`vR1 (selfapp s) = vR1 s RUNION (vR s O vR1 s)`, 233SRW_TAC [][FUN_EQ_THM,EQ_IMP_THM,vR1_def] THEN 234FULL_SIMP_TAC (srw_ss()) [vR_selfapp,RUNION,O_DEF] THEN 235FULL_SIMP_TAC bool_ss [TWO,ONE,NRC,vR1_def] THEN METIS_TAC []); 236 237val FDOM_FUNPOW_selfapp = RWstore_thm( 238"FDOM_FUNPOW_selfapp", 239`FDOM (FUNPOW selfapp n s) = FDOM s`, 240(FUNPOW_extends_mono |> Q.ISPEC `��s'. FDOM s' = FDOM s` |> 241 SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC ) THEN 242SRW_TAC [][]); 243 244val NRC_2_IMP_TC_vR_selfapp = Q.store_thm( 245"NRC_2_IMP_TC_vR_selfapp", 246`���n v u. NRC (vR s) (2* SUC n) v u ��� (vR (selfapp s))^+ v u`, 247Induct THEN SRW_TAC [][] THEN1 ( 248 MATCH_MP_TAC TC_SUBSET THEN 249 SRW_TAC [][vR_selfapp,RUNION] ) THEN 250Cases_on `2 * SUC (SUC n)` THEN 251FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,MULT_SUC,ADD1] THEN 252Cases_on `n'` THEN 253FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,ADD1] THEN 254`2*n + 2 = n''` by DECIDE_TAC THEN 255FULL_SIMP_TAC (srw_ss()) [] THEN 256RES_TAC THEN 257`vR (selfapp s) z' u` by ( 258 SRW_TAC [][vR_selfapp,RUNION] THEN 259 SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 260 METIS_TAC [] ) THEN 261METIS_TAC [TC_RULES]); 262 263val NRC_2_1_IMP_TC_vR_selfapp = Q.store_thm( 264"NRC_2_1_IMP_TC_vR_selfapp", 265`���n v u. NRC (vR s) (2 * n) v u ��� vR1 s w v ��� (vR (selfapp s))^+ w u`, 266Induct THEN SRW_TAC [][] THEN1 ( 267 MATCH_MP_TAC TC_SUBSET THEN 268 SRW_TAC [][vR_selfapp,RUNION] ) THEN 269Cases_on `2 * SUC n` THEN 270FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,ADD1] THEN 271Cases_on `n'` THEN 272FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,ADD1] THEN 273`2*n = n''` by DECIDE_TAC THEN 274FULL_SIMP_TAC (srw_ss()) [] THEN 275RES_TAC THEN 276`vR (selfapp s) z' u` by ( 277 SRW_TAC [][vR_selfapp,RUNION] THEN 278 SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 279 METIS_TAC [] ) THEN 280IMP_RES_TAC TC_RULES); 281 282val TC_vR_selfapp = Q.store_thm( 283"TC_vR_selfapp", 284`(vR (selfapp s))^+ v u ��� (���n. NRC (vR s) (2 * (SUC n)) v u) ��� (���n u'. NRC (vR s) (2 * n) u' u ��� vR1 s v u')`, 285EQ_TAC THEN1 ( 286 MAP_EVERY Q.ID_SPEC_TAC [`u`,`v`] THEN 287 HO_MATCH_MP_TAC TC_INDUCT THEN 288 SRW_TAC [][vR_selfapp,RUNION] THENL [ 289 DISJ2_TAC THEN 290 MAP_EVERY Q.EXISTS_TAC [`0`,`u`] THEN 291 SRW_TAC [][], 292 DISJ1_TAC THEN Q.EXISTS_TAC `0` THEN 293 SRW_TAC [][], 294 IMP_RES_TAC NRC_ADD_I THEN 295 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM LEFT_ADD_DISTRIB,GSYM ADD_SUC] THEN 296 METIS_TAC [], 297 Cases_on `2 * SUC n` THEN 298 FULL_SIMP_TAC (srw_ss()) [NRC_SUC_RECURSE_LEFT,vR1_def,vR_def,FLOOKUP_DEF], 299 IMP_RES_TAC NRC_ADD_I THEN 300 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM LEFT_ADD_DISTRIB,GSYM ADD_SUC] THEN 301 METIS_TAC [], 302 Cases_on `2 * n` THEN 303 FULL_SIMP_TAC (srw_ss()) [NRC_SUC_RECURSE_LEFT,vR1_def,vR_def,FLOOKUP_DEF] THEN 304 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] 305 ] ) THEN 306SRW_TAC [][] THEN1 307IMP_RES_TAC NRC_2_IMP_TC_vR_selfapp THEN 308IMP_RES_TAC NRC_2_1_IMP_TC_vR_selfapp); 309 310val wfs_selfapp = Q.store_thm( 311"wfs_selfapp", 312`wfs s ��� wfs (selfapp s)`, 313SRW_TAC [][wfs_no_cycles,EQ_IMP_THM,TC_vR_selfapp] THEN 314SPOSE_NOT_THEN STRIP_ASSUME_TAC THENL [ 315 Cases_on `2 * SUC n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 316 IMP_RES_TAC TC_eq_NRC THEN METIS_TAC [], 317 Cases_on `2 * n` THEN FULL_SIMP_TAC (srw_ss()) [NRC_SUC_RECURSE_LEFT] THEN 318 SRW_TAC [][] THEN 319 FULL_SIMP_TAC (srw_ss()) [vR1_def,vR_def,FLOOKUP_DEF] THEN 320 FULL_SIMP_TAC (srw_ss()) [], 321 IMP_RES_TAC TC_eq_NRC THEN 322 IMP_RES_TAC NRC_ADD_I THEN 323 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] THEN 324 METIS_TAC [] 325]); 326 327val vR_LRC_ALL_DISTINCT = Q.store_thm( 328"vR_LRC_ALL_DISTINCT", 329`wfs s ��� ���ls v u. LRC (vR s) ls v u ��� ALL_DISTINCT ls`, 330STRIP_TAC THEN Induct THEN SRW_TAC [][LRC_def] THEN1 ( 331 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 332 IMP_RES_TAC LRC_MEM_right THEN 333 Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) [LRC_def,wfs_no_cycles] THEN 334 SRW_TAC [][] THEN1 ( 335 IMP_RES_TAC TC_SUBSET THEN RES_TAC) THEN 336 RES_TAC THEN 337 IMP_RES_TAC NRC_LRC THEN 338 `NRC (vR s) (LENGTH p) h z` by METIS_TAC [] THEN 339 Cases_on `p` THEN FULL_SIMP_TAC (srw_ss()) [LRC_def] THEN 340 SRW_TAC [][] THEN1 ( 341 NTAC 2 (IMP_RES_TAC TC_RULES) THEN 342 RES_TAC ) THEN 343 IMP_RES_TAC TC_eq_NRC THEN 344 SRW_TAC [][] THEN 345 NTAC 2 (IMP_RES_TAC TC_RULES) THEN 346 RES_TAC) THEN RES_TAC); 347 348val vR_LRC_FDOM = Q.store_thm( 349"vR_LRC_FDOM", 350`LRC (vR s) (h::t) v u ��� MEM e t ��� e IN FDOM s`, 351SRW_TAC [][] THEN IMP_RES_TAC LRC_MEM_right THEN 352Cases_on `e IN FDOM s` THEN 353FULL_SIMP_TAC (srw_ss()) [LRC_def,vR_def,FLOOKUP_DEF]); 354 355val vR_LRC_bound = Q.store_thm( 356"vR_LRC_bound", 357`wfs s ��� LRC (vR s) ls v u ��� LENGTH ls ��� CARD (FDOM s) + 1`, 358Cases_on `ls` THEN SRW_TAC [ARITH_ss][ADD1] THEN 359IMP_RES_TAC vR_LRC_ALL_DISTINCT THEN 360IMP_RES_TAC vR_LRC_FDOM THEN 361FULL_SIMP_TAC (srw_ss()) [] THEN 362IMP_RES_TAC ALL_DISTINCT_CARD_LIST_TO_SET THEN 363`set t SUBSET FDOM s` by SRW_TAC [][SUBSET_DEF] THEN 364METIS_TAC [CARD_SUBSET,FDOM_FINITE]); 365 366val idempotent_selfapp = Q.store_thm( 367"idempotent_selfapp", 368`idempotent s ��� (selfapp s = s)`, 369SRW_TAC [][idempotent_def,EQ_IMP_THM,GSYM fmap_EQ,FUN_EQ_THM] THEN1 ( 370 Cases_on `x IN FDOM s` THEN1 ( 371 FIRST_X_ASSUM (Q.SPEC_THEN `Var x` MP_TAC) THEN 372 SRW_TAC [][FLOOKUP_DEF,selfapp_def] ) THEN 373 ASSUME_TAC FDOM_selfapp THEN 374 SRW_TAC [][NOT_FDOM_FAPPLY_FEMPTY] ) THEN 375Induct_on `t` THEN SRW_TAC [][] THEN 376Cases_on `n IN FDOM s` THEN SRW_TAC [][FLOOKUP_DEF] THEN 377FIRST_X_ASSUM (Q.SPEC_THEN `n` MP_TAC) THEN 378SRW_TAC [][selfapp_def,o_f_DEF]); 379 380val fixpoint_IMP_wfs = Q.store_thm( 381"fixpoint_IMP_wfs", 382`idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s) ��� wfs s`, 383SRW_TAC [][] THEN IMP_RES_TAC wfs_idempotent THEN 384POP_ASSUM MP_TAC THEN 385REPEAT (POP_ASSUM (K ALL_TAC)) THEN 386Induct_on `n` THEN SRW_TAC [][] THEN 387FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC] THEN 388IMP_RES_TAC wfs_selfapp THEN 389RES_TAC); 390 391val idempotent_substeq = Q.store_thm( 392"idempotent_substeq", 393`($��� s1 = $��� s2) ��� (idempotent s1 ��� idempotent s2)`, 394SRW_TAC [][idempotent_def,EQ_IMP_THM]); 395 396val vR_FUNPOW_selfapp_bound = Q.store_thm( 397"vR_FUNPOW_selfapp_bound", 398`���n v u. vR (FUNPOW selfapp n s) v u ��� ���m. 1 ��� m ��� NRC (vR s) m v u ��� (v IN FDOM s ��� n ��� m)`, 399Induct THEN SRW_TAC [][] THEN1 ( 400 Q.EXISTS_TAC `1` THEN SRW_TAC [][] ) THEN 401FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC,vR_selfapp,RUNION,vR1_def] THEN1 ( 402 RES_TAC THEN Q.EXISTS_TAC `m` THEN SRW_TAC [][] ) THEN 403FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 404RES_TAC THEN IMP_RES_TAC NRC_ADD_I THEN 405Q.EXISTS_TAC `m' + m` THEN SRW_TAC [][] THEN1 406 DECIDE_TAC THEN 407FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN 408Cases_on `z IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 409DECIDE_TAC); 410 411val idempotent_or_vR = Q.store_thm( 412"idempotent_or_vR", 413`idempotent s ��� ���u v. vR s v u ��� v IN FDOM s`, 414Cases_on `idempotent s` THEN SRW_TAC [][] THEN 415FULL_SIMP_TAC (srw_ss()) [idempotent_def] THEN 416Induct_on `t` THEN SRW_TAC [][] THENL [ 417 Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 418 Q.EXISTS_TAC `n` THEN SRW_TAC [][vR_def] THEN 419 (subst_APPLY_id |> Q.INST [`t`|->`x`] |> EQ_IMP_RULE |> snd |> 420 CONTRAPOS |> IMP_RES_TAC) THEN 421 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 422 METIS_TAC [], 423 METIS_TAC [] 424]); 425 426val wfs_IMP_fixpoint = Q.store_thm( 427"wfs_IMP_fixpoint", 428`wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`, 429STRIP_TAC THEN 430`���n. wfs (FUNPOW selfapp n s)` 431by (MATCH_MP_TAC FUNPOW_extends_mono THEN 432 SRW_TAC [][Once wfs_selfapp]) THEN 433`���n. noids (FUNPOW selfapp n s)` 434by METIS_TAC [wfs_noids] THEN 435SRW_TAC [][] THEN 436SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 437`���n. ���u v. vR (FUNPOW selfapp n s) v u ��� v IN FDOM (FUNPOW selfapp n s)` 438by METIS_TAC [idempotent_or_vR] THEN 439FULL_SIMP_TAC (srw_ss()) [] THEN 440`���n. ���m v u. 1 ��� m ��� NRC (vR s) m v u ��� n ��� m` 441by METIS_TAC [vR_FUNPOW_selfapp_bound] THEN 442`���n. ���ls v u. LRC (vR s) ls v u ��� n ��� LENGTH ls` 443by METIS_TAC [NRC_LRC] THEN 444POP_ASSUM (Q.SPEC_THEN `CARD (FDOM s) + 2` STRIP_ASSUME_TAC) THEN 445IMP_RES_TAC vR_LRC_bound THEN 446DECIDE_TAC); 447 448val wfs_iff_fixpoint = Q.store_thm( 449"wfs_iff_fixpoint", 450`wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`, 451METIS_TAC [wfs_IMP_fixpoint,fixpoint_IMP_wfs]); 452 453(* 454val BIG_BAG_UNION_def = Define` 455 BIG_BAG_UNION sob = ��x. SIGMA (��b. b x) sob`; 456 457val BIG_BAG_UNION_EMPTY = RWstore_thm( 458"BIG_BAG_UNION_EMPTY", 459`BIG_BAG_UNION {} = {||}`, 460SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,EMPTY_BAG,FUN_EQ_THM]); 461 462val BIG_BAG_UNION_INSERT = Q.store_thm( 463"BIG_BAG_UNION_INSERT", 464`FINITE sob ��� (BIG_BAG_UNION (b INSERT sob) = b + BIG_BAG_UNION (sob DELETE b))`, 465SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,BAG_UNION,FUN_EQ_THM]); 466 467val FINITE_BIG_BAG_UNION = Q.store_thm( 468"FINITE_BIG_BAG_UNION", 469`���sob. FINITE sob ��� (���b. b IN sob ��� FINITE_BAG b) ��� FINITE_BAG (BIG_BAG_UNION sob)`, 470SIMP_TAC bool_ss [GSYM AND_IMP_INTRO] THEN 471HO_MATCH_MP_TAC FINITE_INDUCT THEN 472SRW_TAC [][BIG_BAG_UNION_INSERT] THEN 473FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT]); 474 475val EMPTY_BIG_BAG_UNION = Q.store_thm( 476"EMPTY_BIG_BAG_UNION", 477`FINITE sob ��� ((BIG_BAG_UNION sob = {||}) ��� (���b. b IN sob ��� (b = {||})))`, 478Q.ID_SPEC_TAC `sob` THEN HO_MATCH_MP_TAC FINITE_INDUCT THEN 479SRW_TAC [][BIG_BAG_UNION_INSERT,DELETE_NON_ELEMENT] THEN 480SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][]); 481 482val BAG_IN_BIG_BAG_UNION = Q.store_thm( 483"BAG_IN_BIG_BAG_UNION", 484`���sob. FINITE sob ��� (e <: BIG_BAG_UNION sob ��� ���b. b IN sob ��� e <: b)`, 485HO_MATCH_MP_TAC FINITE_INDUCT THEN 486SRW_TAC [][BIG_BAG_UNION_INSERT,DELETE_NON_ELEMENT,EQ_IMP_THM] THEN 487METIS_TAC []); 488 489val IMAGE_FAPPLY_FDOM = Q.store_thm( 490"IMAGE_FAPPLY_FDOM", 491`IMAGE ($' s) (FDOM s) = FRANGE s`, 492SRW_TAC [][EXTENSION,FRANGE_DEF,EQ_IMP_THM] THEN METIS_TAC []); 493 494val rangevarb_def = Define` 495 rangevarb s = BIG_BAG_UNION (IMAGE varb (FRANGE s))`; 496 497val FINITE_rangevarb = RWstore_thm( 498"FINITE_rangevarb", 499`FINITE_BAG (rangevarb s)`, 500SRW_TAC [][rangevarb_def] THEN 501HO_MATCH_MP_TAC FINITE_BIG_BAG_UNION THEN 502SRW_TAC [][] THEN SRW_TAC [][]); 503 504val domrangevarb_def = Define` 505 domrangevarb s = BAG_FILTER (��v. v IN FDOM s) (rangevarb s)`; 506 507val BAG_FILTER_EQ_EMPTY = Q.store_thm( 508"BAG_FILTER_EQ_EMPTY", 509`(BAG_FILTER P b = {||}) ��� ���e. e <: b ��� ��P e`, 510SRW_TAC [][BAG_EXTENSION,BAG_INN_BAG_FILTER,BAG_IN,EQ_IMP_THM] THEN1 ( 511 FIRST_X_ASSUM (Q.SPECL_THEN [`1`,`e`] MP_TAC) 512 THEN SRW_TAC [][] ) THEN 513FIRST_X_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN 514SRW_TAC [][] THEN 515Cases_on `n < 1` THEN1 DECIDE_TAC THEN 516(BAG_INN_LESS |> Q.SPECL [`b`,`e`,`n`,`1`] |> CONTRAPOS |> IMP_RES_TAC) THEN 517FULL_SIMP_TAC (srw_ss()) [] THEN 518`n = 1` by DECIDE_TAC THEN 519SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []); 520 521val domrangevarb_idempotent = Q.store_thm( 522"domrangevarb_idempotent", 523`idempotent s ��� noids s ��� (domrangevarb s = {||})`, 524SRW_TAC [] 525[idempotent_rangevars,domrangevarb_def,rangevarb_def, 526 BAG_FILTER_EQ_EMPTY,BAG_IN_BIG_BAG_UNION,EQ_IMP_THM] THEN1 ( 527 IMP_RES_TAC IN_varb_vars THEN 528 RES_TAC THEN POP_ASSUM (Q.SPEC_THEN `vars x` MP_TAC) THEN 529 SRW_TAC [][DISJOINT_DEF,EXTENSION] THEN METIS_TAC [] ) THEN 530SRW_TAC [][DISJOINT_DEF,EXTENSION] THEN 531Cases_on `x' IN vars x` THEN SRW_TAC [][] THEN 532IMP_RES_TAC IN_varb_vars THEN 533RES_TAC THEN FULL_SIMP_TAC (srw_ss()) []); 534*) 535 536(* 537 538val selfapp_preserves_idempotent = Q.store_thm( 539"selfapp_preserves_idempotent", 540`idempotent s ��� noids s ��� idempotent (selfapp s) ��� noids (selfapp s)`, 541SRW_TAC [][idempotent_def,noids_def,selfapp_eq_iter_APPLY] THEN 542Cases_on `FLOOKUP (selfapp s) v` THEN 543FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF,selfapp_def] THEN 544FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN 545SRW_TAC [][FLOOKUP_DEF] THEN 546FIRST_X_ASSUM (Q.SPEC_THEN `v` MP_TAC) THEN 547SRW_TAC [][]); 548 549this will be a consequence of wfs_IMP_fixpoint above ? ... 550val repeated_selfapp_eq_apply_ts = Q.store_thm( 551"repeated_selfapp_eq_apply_ts", MAYBE n HAS TO DEPEND ON THE TERM !! 552`���n. apply_ts s = subst_APPLY (FUNPOW selfapp n s)`, 553Q_TAC SUFF_TAC `���t.���n. apply_ts s t = (FUNPOW selfapp n s) ��� t` 554THEN1 ( 555 SRW_TAC [][FUN_EQ_THM,SKOLEM_THM] 556 SKOLEM_THM 557 558FDOM s INTER BIGUNION (IMAGE vars (FRANGE s)) 559 560val wfs_IMP_fixpoint = Q.store_thm( 561"wfs_IMP_fixpoint", 562`wfs s ��� ���t.���n. (FUNPOW selfapp n s) ��� t = apply_ts s t` 563 564val FUNPOW_APPLY_apply_ts = Q.store_thm( 565"FUNPOW_APPLY_apply_ts", 566`(FUNPOW ($��� s) n t = apply_ts s t) ��� m >= n ��� wfs s ��� 567 (FUNPOW ($��� s) m t = apply_ts s t)`, 568Induct_on `m` THEN SRW_TAC [][] THEN1 ( 569 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] ) THEN 570Cases_on `SUC m = n` THEN1 SRW_TAC [][] THEN 571`m >= n` by FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] THEN 572SRW_TAC [][FUNPOW_SUC] THEN 573SRW_TAC [][apply_ts_eq_walkstar,subst_APPLY_walkstar]); 574 575val FUNPOW_APPLY_pair = Q.store_thm( 576"FUNPOW_APPLY_pair", 577`FUNPOW ($��� s) n (Pair t1 t2) = Pair (FUNPOW ($��� s) n t1) (FUNPOW ($��� s) n t2)`, 578Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC] ); 579 580val wfs_IMP_fixpoint = Q.store_thm( 581"wfs_IMP_fixpoint", 582`wfs s ��� ���n. idempotent (FUNPOW ($��� s) n)` 583`wfs s ��� ���t.���n. FUNPOW ($��� s) n t = apply_ts s t`, 584STRIP_TAC THEN HO_MATCH_MP_TAC apply_ts_ind THEN 585SRW_TAC [][] THEN1 ( 586 Cases_on `FLOOKUP s t` THEN SRW_TAC [][] THENL [ 587 Q.EXISTS_TAC `0` THEN SRW_TAC [][], 588 Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][FUNPOW] 589 ] ) THEN1 ( 590 SRW_TAC [][FUNPOW_APPLY_pair] THEN 591 Q.EXISTS_TAC `MAX n n'` THEN 592 SRW_TAC [][] THEN 593 MATCH_MP_TAC (GEN_ALL FUNPOW_APPLY_apply_ts) THENL [ 594 Q.EXISTS_TAC `n`, Q.EXISTS_TAC `n'` ] THEN 595 SRW_TAC [ARITH_ss][MAX_DEF] ) THEN 596Q.EXISTS_TAC `0` THEN SRW_TAC [][]); 597 598val fixpoint_IMP_wfs = Q.store_thm( 599"fixpoint_IMP_wfs", 600`(���t.���n. FUNPOW ($��� s) n t = FUNPOW ($��� s) (SUC n) t) ��� noids s ��� wfs s`, 601SRW_TAC [][] THEN 602MATCH_MP_TAC wfs_idempotent THEN 603SRW_TAC [][] THEN 604SRW_TAC [][idempotent_def] 605 606SRW_TAC [][wfs_no_cycles,noids_def] THEN 607SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 608TC_vR_vars_walkstar 609FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN 610SRW_TAC [][FUNPOW] THEN 611IMP_RES_TAC TC_CASES1 THEN 612FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 613Cases_on `FLOOKUP s v` THEN FULL_SIMP_TAC (srw_ss()) [] 614 615val FUNPOW_APPLY_term_depth = Q.store_thm( 616"FUNPOW_APPLY_term_depth", 617`���n t. term_depth (FUNPOW ($��� s) n t) ��� term_depth (FUNPOW ($��� s) (SUC n) t)`, 618Induct THEN SRW_TAC [][] THEN1 ( 619 Induct_on `t` THEN SRW_TAC [ARITH_ss][] ) THEN 620FULL_SIMP_TAC (srw_ss()) [FUNPOW]); 621 622val FUNPOW_APPLY_NOT_FDOM = Q.store_thm( 623"FUNPOW_APPLY_NOT_FDOM", 624`v NOTIN FDOM s ��� (FUNPOW ($��� s) n (Var v) = Var v)`, 625STRIP_TAC THEN Induct_on `n` THEN SRW_TAC [][FUNPOW,FLOOKUP_DEF]); 626 627val NOT_FDOM_vars_APPLY = Q.store_thm( 628"NOT_FDOM_vars_APPLY", 629`v NOTIN FDOM s ��� v IN vars t ��� v IN vars (s ��� t)`, 630Induct_on `t` THEN SRW_TAC [][FLOOKUP_DEF] THEN 631FULL_SIMP_TAC (srw_ss()) []); 632 633val term_depth_APPLY = Q.store_thm( 634"term_depth_APPLY", 635`term_depth t ��� term_depth (s ��� t)`, 636Induct_on `t` THEN SRW_TAC [ARITH_ss][]); 637 638val APPLY_subterm = Q.store_thm( 639"APPLY_subterm", 640`v IN vars t ��� t ��� Var v ��� measure term_depth (s ��� (Var v)) (s ��� t)`, 641Induct_on `t` THEN SRW_TAC [ARITH_ss][measure_thm] THEN 642Cases_on `FLOOKUP s v` THEN SRW_TAC [ARITH_ss][] THEN 643FULL_SIMP_TAC (srw_ss()) [measure_thm] THEN 644Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] 645THEN SRW_TAC [ARITH_ss][] THEN 646Cases_on `t'` THEN FULL_SIMP_TAC (srw_ss()) [] 647THEN SRW_TAC [ARITH_ss][]); 648 649val wfs_iff_fixpoint_exists = Q.store_thm( 650"wfs_iff_fixpoint_exists", 651`wfs s ��� noids s ��� ���t.���tt. OWHILE (��t. (s ��� t) ��� t) (subst_APPLY s) t = SOME tt`, 652SRW_TAC [][EQ_IMP_THM] THEN1 METIS_TAC [wfs_noids] THENL [ 653 Q.EXISTS_TAC `walk* s t` THEN SRW_TAC [][OWHILE_def] 654 655val substeq_def = Define` 656 substeq s1 s2 = noids s1 ��� noids s2 ��� (���t. s1 ��� t = s2 ��� t)`; 657 658val substeq_refl = Q.store_thm( 659"substeq_refl", 660`noids s ��� substeq s s`, 661SRW_TAC [][substeq_def]); 662 663val substeq_sym = Q.store_thm( 664"substeq_sym", 665`substeq s1 s2 ��� substeq s2 s1`, 666SRW_TAC [][substeq_def]); 667 668val substeq_trans = Q.store_thm( 669"substeq_trans", 670`substeq s1 s2 ��� substeq s2 s3 ��� substeq s1 s3`, 671SRW_TAC [][substeq_def]); 672 673val vR_substeq_mono = Q.store_thm( 674"vR_substeq_mono", 675`vR s1 u v ��� substeq s1 s2 ��� vR s2 u v`, 676SRW_TAC [][vR_def,substeq_def] THEN 677Cases_on `FLOOKUP s1 v` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 678FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN 679SRW_TAC [][] THEN 680Cases_on `FLOOKUP s2 v` THEN FULL_SIMP_TAC (srw_ss()) [noids_def] THEN 681METIS_TAC []); 682 683val wfs_substeq_mono = Q.store_thm( 684"wfs_substeq_mono", 685`wfs s1 ��� substeq s1 s2 ��� wfs s2`, 686SRW_TAC [][wfs_def] THEN 687Q_TAC SUFF_TAC `vR s1 = vR s2` THEN1 METIS_TAC [] THEN 688SRW_TAC [][FUN_EQ_THM,EQ_IMP_THM] THEN 689METIS_TAC [vR_substeq_mono,substeq_sym]); 690 691val wfs_noids = Q.store_thm( 692"wfs_noids", 693`wfs s ��� noids s`, 694SRW_TAC [][wfs_no_cycles,noids_def] THEN 695SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 696`vR s v v` by SRW_TAC [][vR_def] THEN 697METIS_TAC [TC_SUBSET]); 698 699val collapsable_eq_wfs = Q.store_thm( 700"collapsable_eq_wfs", FALSE 701`(���si. idempotent si ��� substeq si s) ��� wfs s`, 702SRW_TAC [][EQ_IMP_THM] THEN1 ( 703 IMP_RES_TAC wfs_idempotent THEN 704 METIS_TAC [wfs_substeq_mono,substeq_def] ) THEN 705Q.EXISTS_TAC `collapse s` THEN 706IMP_RES_TAC collapse_idempotent THEN 707 708val FUNPOW_exists = Q.store_thm( (* similar to WHILE_INDUCTION *) 709"FUNPOW_exists", 710`���R. WF R ��� (���n. ��(P (FUNPOW f n x)) ��� R (FUNPOW f (SUC n) x) (FUNPOW f n x)) ��� ���n. P (FUNPOW f n x)`, 711SRW_TAC [][] THEN POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `x` THEN 712HO_MATCH_MP_TAC (WF_INDUCTION_THM |> Q.SPEC `R` |> UNDISCH) THEN 713SRW_TAC [][] THEN 714Cases_on `P (FUNPOW f 0 x)` THEN1 METIS_TAC [] THEN 715RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN RES_TAC THEN 716Q_TAC SUFF_TAC `���n. P (FUNPOW f n (f x))` THEN1 ( 717 STRIP_TAC THEN Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][FUNPOW] ) THEN 718POP_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 719FIRST_X_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) THEN 720SRW_TAC [][FUNPOW]); 721 722val NRC_MUL_I = Q.store_thm( 723"NRC_MUL_I", 724`���m n x y. NRC (NRC R m) n x y ��� NRC R (m * n) x y`, 725Induct THEN Induct THEN SRW_TAC [][NRC] THEN1 ( 726 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] ) THEN 727RES_TAC THEN 728IMP_RES_TAC NRC_1 THEN 729IMP_RES_TAC NRC_ADD_I THEN 730Q_TAC SUFF_TAC `SUC m * SUC n = 1 + m + SUC m * n` 731THEN1 METIS_TAC [] THEN 732SRW_TAC [ARITH_ss][MULT,ADD1]); 733*) 734 735(* 736val collapsable_IMP_wfs = Q.store_thm( 737"collapsable_IMP_wfs", 738`���s.(���si. idempotent si ��� (���t. si ��� t = s ��� t)) ��� wfs s`, 739SRW_TAC [][wfs_no_cycles] 740 741val wfs_collapse = Q.store_thm( 742"wfs_collapse", 743`wfs s ==> wfs (collapse s)`, 744SIMP_TAC (srw_ss()) [wfs_no_cycles] THEN 745STRIP_TAC THEN 746Q_TAC SUFF_TAC `!v u.(vR (collapse s))^+ v u ==> v <> u` 747THEN1 METIS_TAC [] THEN 748HO_MATCH_MP_TAC TC_STRONG_INDUCT THEN 749SRW_TAC [][] THENL [ 750 Cases_on `u IN FDOM (collapse s)` THEN 751 FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN 752 `wfs s` by METIS_TAC [wfs_no_cycles] THEN 753 `u IN FDOM s` by FULL_SIMP_TAC (srw_ss()) [collapse_def,FUN_FMAP_DEF] THEN 754 FULL_SIMP_TAC (srw_ss()) [collapse_FAPPLY_eq_walkstar] 755 756val subst_compose_exists = Q.prove( 757`!s2 s1.?comp.!x.(subst_APPLY comp x = (subst_APPLY s2 (subst_APPLY s1 x)))`, 758GEN_TAC THEN INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [ 759 Q.EXISTS_TAC `s2` THEN Induct THEN SRW_TAC [][], 760 SRW_TAC [][] THEN 761 Q.EXISTS_TAC `comp |+ (x,s2 ��� y)` THEN 762 SRW_TAC [][] THEN 763 Induct_on `x'` THEN SRW_TAC [][] THEN 764 SRW_TAC [][FLOOKUP_UPDATE] THEN 765 Q.PAT_X_ASSUM `!x.Z` (Q.SPEC_THEN `Var s` MP_TAC) THEN 766 SRW_TAC [][] 767]); 768 769val subst_compose_def = new_specification 770 ("subst_compose_def", ["subst_compose"], 771 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) subst_compose_exists); 772set_fixity "oo" (Infixl 2000); 773overload_on ("oo", ``subst_compose``); 774 775val sunify_def = Define` 776 (sunify (Var x) (Var y) = SOME if x = y then FEMPTY else (FEMPTY |+ (x, Var y))) /\ 777 (sunify (Var x) t2 = if x IN vars t2 then NONE else SOME (FEMPTY |+ (x,t2))) /\ 778 (sunify t1 (Var y) = if y IN vars t1 then NONE else SOME (FEMPTY |+ (y,t1))) /\ 779 (sunify (Pair t1a t1d) (Pair t2a t2d) = 780 case sunify t1a t2a of NONE => NONE | 781 SOME sa => case sunify t1d t2d of NONE => NONE | 782 SOME sd => SOME (sa oo sd)) /\ 783 (sunify (Const c1) (Const c2) = if c1 = c2 then SOME FEMPTY else NONE) /\ 784 (sunify _ _ = NONE)`; 785 786val collapse_unify_eq_sunify = Q.store_thm( 787"collapse_unify_eq_sunify", 788`!s t1 t2 sx.wfs s /\ (unify s t1 t2 = SOME sx) ==> 789 ?ss.(sunify t1 t2 = SOME ss) /\ 790 !t.((collapse sx) ��� t = (ss oo s) ��� t)`, 791HO_MATCH_MP_TAC unify_ind THEN SRW_TAC [][] THEN 792`wfs sx` by METIS_TAC [unify_uP,uP_def] THEN 793Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN 794Q.PAT_X_ASSUM `unify X Y Z = D` MP_TAC THEN 795SRW_TAC [][Once unify_def] THENL 796 797`���t1 t2. (s ��� t1 = s ��� t2) ��� (t1 = t2)`, 798Induct THEN SRW_TAC [][] THENL [ false - x -> 3 and y -> 3 799 Induct_on `t2` THEN FULL_SIMP_TAC (srw_ss()) [] 800Induct_on `t1` THEN SRW_TAC [][] THENL [ 801 Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 802 Cases_on `t2` THEN FULL_SIMP_TAC (srw_ss()) [] 803 804val FUNPOW_extends_mono_cond = Q.store_thm( 805"FUNPOW_extends_mono_cond", 806`(���x y. P x y ��� Q x y ��� P (f x) (f y)) ��� ���x y. (P x y ��� Q x y ��� P (FUNPOW f n x) (FUNPOW f n y))`, 807STRIP_TAC THEN Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC] 808); 809 810`���t1 t2. (��t1 t2. ���v. (t1 = Var v) ��� v IN vars t2 ��� measure term_depth t1 t2) t1 t2 ��� 811(��t1 t2. ���v. (t1 = Var v) ��� v IN vars t2 ��� measure term_depth t1 t2) 812(FUNPOW ($��� s) n t1) (FUNPOW ($��� s) n t2)`, 813 814val tmp = 815FUNPOW_extends_mono |> 816Q.INST_TYPE[`:'a`|->`:term`] |> 817Q.INST[`P`|->`(��t1 t2. v IN vars t2 ��� measure term_depth t1 t2)`, 818 `f`|->`$��� s`] 819|> SIMP_RULE (srw_ss()) [] |> 820UNDISCH; 821 822val [rtp] = hyp tmp; 823val th = prove(rtp, 824Induct THEN SRW_TAC [][] THEN 825Cases_on `FLOOKUP s n` THEN SRW_TAC [][] THENL [ 826 FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN 827 METIS_TAC [NOT_FDOM_vars_APPLY], 828 FULL_SIMP_TAC (srw_ss()) [measure_thm] THEN 829 (term_depth_APPLY |> Q.GEN `t` |> Q.SPEC `y` |> MP_TAC) THEN 830 SRW_TAC [ARITH_ss][], 831 832 833`���n. v IN vars t ��� t ��� Var v ��� (measure term_depth) (FUNPOW ($��� s) n (Var v)) (FUNPOW ($��� s) n t)`, 834Induct THEN SRW_TAC [][] THEN1 ( 835 Induct_on `t` THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) [measure_thm] ) THEN 836SRW_TAC [][FUNPOW] THEN 837Cases_on `FLOOKUP s v` THEN SRW_TAC [][] THEN1 ( 838 FULL_SIMP_TAC (srw_ss()) [measure_thm] THEN 839 SRW_TAC [][GSYM FUNPOW] THEN 840 SRW_TAC [][FUNPOW_SUC] THEN 841 Q.MATCH_ABBREV_TAC `a < b` THEN 842 Q_TAC SUFF_TAC `term_depth (FUNPOW ($��� s) n t) ��� b` THEN1 ( 843 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [Abbr`a`,Abbr`b`] ) THEN 844 METIS_TAC [term_depth_APPLY] ) THEN 845Q_TAC SUFF_TAC `x = (s ��� (Var v))` 846THEN1 METIS_TAC [APPLY_subterm] 847SRW_TAC [][FUNPOW] 848 849 850 851HO_MATCH_MP_TAC FUNPOW_extends_mono THEN 852Induct THEN SRW_TAC [][] 853 854���t1 t2.(��t1 t2. ���v. (t1 = Var v) ��� v IN vars t2 ��� term_depth) t1 t2 ��� (measure term_depth) (FUNPOW ($��� s) n t1) (FUNPOW ($��� s) n t2)` 855HO_MATCH_MP_TAC FUNPOW_extends_mono THEN 856Induct THEN SRW_TAC [][] 857 858`(FUNPOW ($��� s) n (Var v) = FUNPOW ($��� s) n t) ��� (t ��� Var v) ��� v NOTIN vars t`, 859STRIP_TAC THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 860Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 861`term_depth (Var v) < term_depth t` 862by (Induct_on `t` THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) []) THEN 863 864 865 866Induct_on `n` THEN SRW_TAC [][] THEN 867FIRST_X_ASSUM MATCH_MP_TAC THEN 868SRW_TAC [][] THEN 869HR 870FULL_SIMP_TAC (srw_ss()) [FUNPOW] THEN 871Cases_on `FLOOKUP s v` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 872 873 874val FUNPOW_APPLY_preserves_type = Q.store_thm( 875"FUNPOW_APPLY_preserves_type", 876`���FUNPOW ($��� s) n (Var v) 877 878val rangevarb_recurses = save_thm( 879"rangevarb_recurses", 880COMMUTING_ITSET_RECURSES |> Q.ISPEC `rangevarb_acc` |> 881SIMP_RULE (srw_ss()) [rangevarb_acc_def,ASSOC_BAG_UNION] |> 882SIMP_RULE (srw_ss()) [COMM_BAG_UNION]); 883 884val RELPOW_def = Define` 885 (RELPOW R 0 = REMPTY) ��� 886 (RELPOW R (SUC n) = R O (RELPOW R n))`; 887 888val RELPOW1 = RWstore_thm( 889"RELPOW1", 890`RELPOW R 1 = R`, 891SRW_TAC [][FUN_EQ_THM] THEN Cases_on `1` THEN 892FULL_SIMP_TAC (srw_ss()) [RELPOW_def]); 893 894val selfapp_rangevarb = Q.store_thm( 895"selfapp_rangevarb", 896`rangevarb s = rangevarb (selfapp s)`, 897SRW_TAC [][rangevarb_def,selfapp_def,IMAGE_FAPPLY_FDOM]); 898 899(���b2. b2 IN sob2 ��� ���b1. b1 IN sob1 ��� mlt1 R b2 b1) ��� (mlt1 R)^+ (BIG_BAG_UNION sob2) (BIG_BAG_UNION sob1) 900 901val TC_vR_selfapp = Q.store_thm( 902"TC_vR_selfapp", 903`(vR (selfapp s))^+ v u ��� vR s v u ��� v NOTIN FDOM s ��� (���n. NRC (vR s) (SUC (SUC n)) v u)`, 904EQ_TAC THEN1 ( 905 MAP_EVERY Q.ID_SPEC_TAC [`u`,`v`] THEN 906 HO_MATCH_MP_TAC TC_INDUCT THEN 907 SRW_TAC [][vR_selfapp] 908 THEN1 SRW_TAC [][] 909 THEN1 ( 910 DISJ2_TAC THEN Q.EXISTS_TAC `0` THEN 911 ASM_SIMP_TAC (srw_ss()) [] ) 912 THEN1 ( 913 DISJ2_TAC THEN Q.EXISTS_TAC `0` THEN 914 ASM_SIMP_TAC (srw_ss()) [NRC] THEN 915 METIS_TAC [] ) 916 THEN1 ( 917 IMP_RES_TAC NRC_1 THEN 918 IMP_RES_TAC NRC_ADD_I THEN 919 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM ADD_SUC] THEN 920 METIS_TAC [] ) 921 THEN1 ( 922 IMP_RES_TAC NRC_1 THEN 923 IMP_RES_TAC NRC_ADD_I THEN 924 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM ADD_SUC,ADD_SYM] THEN 925 METIS_TAC [] ) 926 THEN1 ( 927 IMP_RES_TAC NRC_ADD_I THEN 928 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM ADD_SUC] THEN 929 METIS_TAC [] ) ) THEN 930SRW_TAC [][] THEN1 ( 931 MATCH_MP_TAC TC_SUBSET THEN 932 SRW_TAC [][vR_selfapp] ) THEN 933 934 935SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN 936HO_MATCH_MP_TAC TC_INDUCT THEN 937SRW_TAC [][] THEN1 ( 938 Cases_on `���n. NRC (vR s) (SUC (SUC n)) y x'` THEN1 ( 939 FULL_SIMP_TAC (srw_ss()) [] THEN 940 MATCH_MP_TAC TC_SUBSET THEN 941 SRW_TAC [][vR_selfapp] THEN 942 METIS_TAC [] ) THEN 943 RES_TAC 944 945 946 SRW_TAC [][] THEN 947 IMP_RES_TAC TC_RULES THEN 948 IMP_RES_TAC TC_RULES THEN 949 `NRC (vR s) 2 y x'` 950 by (Cases_on `2` THEN FULL_SIMP_TAC (srw_ss()) [NRC] THEN METIS_TAC []) THEN 951 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] 952 (Q.MATCH_ABBREV_TAC `R^+ a b` THEN 953 METIS_TAC [TC_RULES]) ORELSE 954 (`NRC (vR s) 2 y x'` 955 by (Cases_on `2` THEN FULL_SIMP_TAC (srw_ss()) [NRC] THEN METIS_TAC []) THEN 956 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [])) 957 SRW_TAC [][vR_selfapp] THEN 958 SRW_TAC [][] THEN (( 959 `NRC (vR s) 2 y x'` 960 by (Cases_on `2` THEN FULL_SIMP_TAC (srw_ss()) [NRC] THEN METIS_TAC []) THEN 961 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) []) ORELSE 962 METIS_TAC [TC_RULES])) 963 964 (( 965 Cases_on `y IN FDOM s` THEN 966 FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN 967 NO_TAC ) ORELSE 968 METIS_TAC [TC_RULES])) THEN 969SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN 970HO_MATCH_MP_TAC TC_INDUCT THEN 971SRW_TAC [][] 972STRIP_TAC 973Q_TAC SUFF_TAC `(���x y. (vR (selfapp s))^+ x y ��� (vR s)^+ x y) ��� 974 (���x y. (vR s)^+ x y ��� (vR (selfapp s))^+ x y)` 975THEN1 (SRW_TAC [][FUN_EQ_THM] THEN METIS_TAC []) THEN 976CONJ_TAC THEN1 ( 977 HO_MATCH_MP_TAC TC_INDUCT THEN 978 SRW_TAC [][vR_selfapp] THEN 979 METIS_TAC [TC_RULES]) THEN 980HO_MATCH_MP_TAC TC_INDUCT THEN 981SRW_TAC [][] 982 ; 983 984 985`(vR1 s RUNION NRC (vR s) (SUC (SUC 0))) y x ��� vR1 s y x ��� ���n. NRC (vR s) (SUC (SUC n)) y x`, 986SRW_TAC [][vR1_def,RUNION,NRC,EQ_IMP_THM] THENL [ 987 SRW_TAC [][], 988 DISJ2_TAC THEN 989 Q.EXISTS_TAC `0` THEN 990 Q.EXISTS_TAC `z` THEN 991 SRW_TAC [][], 992 SRW_TAC [][], 993 false 994 995 996val selfapp_rangevarb_mlt = Q.store_thm( 997"selfapp_rangevarb_mlt", 998`��idempotent s ��� noids s ��� (mlt1 (vR s))^+ (rangevarb (selfapp s)) (rangevarb s)`, 999Q_TAC SUFF_TAC 1000`���b. FINITE_BAG b ��� ���s. (rangevarb s = b) ��� ��idempotent s ��� noids s ��� 1001 (mlt1 (vR s))^+ (rangevarb (selfapp s)) (rangevarb s)` 1002THEN1 SRW_TAC [][] THEN 1003HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN 1004CONJ_TAC THEN1 ( 1005 SRW_TAC [][rangevarb_def,EMPTY_BIG_BAG_UNION] THEN 1006 `~(DISJOINT (FDOM s) (BIGUNION (IMAGE vars (FRANGE s))))` 1007 by METIS_TAC [idempotent_rangevars] THEN 1008 FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF] THEN 1009 Q_TAC SUFF_TAC `varb x = {||}` THEN1 ( 1010 STRIP_TAC THEN 1011 `vars x = {}` 1012 by (SetCases_on `vars x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1013 METIS_TAC [IN_varb_vars,NOT_IN_EMPTY_BAG,IN_INSERT]) THEN 1014 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 1015 FULL_SIMP_TAC (srw_ss()) [DISJOINT_EMPTY]) THEN 1016 FIRST_X_ASSUM MATCH_MP_TAC THEN 1017 Q.EXISTS_TAC `x` THEN SRW_TAC [][] THEN 1018 Q.EXISTS_TAC `x���` THEN SRW_TAC [][]) THEN 1019SRW_TAC [][] 1020 1021 `varb b = {||} 1022 FIRST_X_ASSUM (Q.SPEC_THEN `varb b` MP_TAC) THEN 1023 SRW_TAC [][] 1024 SIMP_TAC (srw_ss()) [rangevarb_def,BIG_BAG_UNION_def,IMAGE_EMPTY] THEN 1025HO_MATCH_MP_TAC FINITE_INDUCT THEN 1026CONJ_TAC THEN1 ( 1027 SRW_TAC [][] THEN 1028 `~(DISJOINT (FDOM s) (BIGUNION (IMAGE vars (FRANGE s))))` 1029 by METIS_TAC [idempotent_rangevars] THEN 1030 FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF] THEN 1031 METIS_TAC [NOT_IN_EMPTY]) THEN 1032SRW_TAC [][] 1033 1034 SRW_TAC [][idempotent_def,FRANGE_DEF,EXTENSION] THEN 1035 Induct_on `t` THEN FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] 1036SRW_TAC [][rangevarb_def,selfapp_def,IMAGE_FAPPLY_FDOM,IMAGE_COMPOSE] THEN 1037o_f_FRANGE 1038FULL_SIMP_TAC (srw_ss()) [] 1039 1040`���s. wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`, 1041WHILE_INDUCTION |> Q.ISPECL [ 1042`��s. �� idempotent s`, 1043`selfapp`, 1044`��ss s. (mlt1 (vR s))^+ (domrangevarb ss) (domrangevarb s)`] |> 1045SIMP_RULE (srw_ss()) [] 1046 1047Q.EXISTS_TAC `��ss s. (mlt1 (vR s))^+ (domrangevarb ss) (domrangevarb s)` THEN 1048SRW_TAC [][] THEN1 ( 1049 SRW_TAC [][WF_EQ_WFP] THEN 1050 MATCH_MP_TAC WFP_RULES THEN 1051 SRW_TAC [][] 1052Q.EXISTS_TAC `inv_image (mlt1 (vR s))^+ domrangevarb` THEN 1053SRW_TAC [][] THEN1 ( 1054 MATCH_MP_TAC WF_inv_image THEN 1055 MATCH_MP_TAC WF_TC THEN 1056 MATCH_MP_TAC WF_mlt1 THEN 1057 FULL_SIMP_TAC (srw_ss()) [wfs_def] ) THEN 1058SRW_TAC [][inv_image_def] THEN 1059SRW_TAC [][FUNPOW_SUC] THEN 1060 1061Q_TAC SUFF_TAC 1062`���s. ��idempotent s ��� noids s ��� (mlt1 (vR s))^+ (domrangevarb (selfapp s)) (domrangevarb s)` 1063METIS_TAC [FUNPOW_exists] 1064METIS_TAC [selfapp_rangevarb_mlt]); 1065 1066val selfappR_def = Define` 1067 selfappR ss s = (mlt1 (vR s)^+)^+ 1068 1069 1070val selfapp_rangevarb_mlt = Q.store_thm( 1071"selfapp_rangevarb_mlt", 1072`��idempotent s ��� noids s ��� (mlt1 (vR s))^+ (domrangevarb (selfapp s)) (domrangevarb s)`, 1073 1074val sources_def = Define` 1075 sources s = {v | v IN FDOM s ��� ���u. (vR s)^+ v u }`; 1076 1077val sources_SUBSET_FDOM = Q.store_thm( 1078"sources_SUBSET_FDOM", 1079`sources s SUBSET FDOM s`, 1080SRW_TAC [][SUBSET_DEF,sources_def]); 1081 1082val sources_selfapp = Q.store_thm( 1083"sources_selfapp", 1084`wfs s ��� sources s ��� {} ��� (sources (selfapp s) PSUBSET sources s)`, 1085SRW_TAC [][sources_def,PSUBSET_DEF,SUBSET_DEF] THEN1 ( 1086 IMP_RES_TAC TC_vR_selfapp THEN1 ( 1087 Cases_on `2 * SUC n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1088 IMP_RES_TAC TC_eq_NRC THEN METIS_TAC [] ) THEN 1089 FULL_SIMP_TAC (srw_ss()) [vR1_def]) THEN 1090FULL_SIMP_TAC (srw_ss()) [EXTENSION,EQ_IMP_THM] THEN 1091Q.EXISTS_TAC `x` THEN SRW_TAC [][] THEN 1092SRW_TAC [][TC_vR_selfapp] 1093 1094val (RTC_path_rules,RTC_path_ind,RTC_path_cases) = Hol_reln` 1095 (RTC_path R []) ��� 1096 (RTC_path R [y]) ��� 1097 (RTC_path R t ��� R x y ��� 1098 RTC_path R (x::y::t))`; 1099 1100val RTC_path_strong_ind = save_thm( 1101"RTC_path_strong_ind", 1102IndDefLib.derive_strong_induction(RTC_path_rules, RTC_path_ind)); 1103 1104val vR_path_bound = Q.store_thm( 1105"vR_path_bound", 1106`wfs s ��� ���ls. RTC_path (vR s) ls ��� LENGTH ls > 1 ��� LENGTH ls ��� CARD (FDOM s)`, 1107STRIP_TAC THEN HO_MATCH_MP_TAC RTC_path_strong_ind THEN 1108SRW_TAC [][] THEN 1109Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) [] 1110 1111val longest_path_def = Define` 1112 longest_path s = MAX_SET {n | ���v u. NRC (vR s) n v u}`; 1113 1114val NRC_vR_set = Q.store_thm( 1115"NRC_vR_set", 1116`wfs s ��� ���n v u. NRC (vR s) n v u ��� ���vs. vs SUBSET FDOM s ��� (CARD vs = n) ��� v NOTIN vs`, 1117STRIP_TAC THEN Induct THEN SRW_TAC [][] THEN1 ( 1118 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) THEN 1119FULL_SIMP_TAC (srw_ss()) [NRC] THEN 1120RES_TAC THEN 1121Q.EXISTS_TAC `z INSERT vs` THEN 1122FULL_SIMP_TAC (srw_ss()) [wfs_no_cycles] THEN 1123Cases_on `v = z` THEN1 ( 1124 FULL_SIMP_TAC (srw_ss()) [] THEN 1125 IMP_RES_TAC TC_SUBSET THEN 1126 RES_TAC ) THEN 1127 1128SRW_TAC [][] THENL [ 1129 Cases_on `z IN FDOM s` THEN 1130 FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF], 1131 IMP_RES_TAC FDOM_FINITE THEN 1132 IMP_RES_TAC SUBSET_FINITE 1133 SRW_TAC [][CARD_INSERT] 1134FULL_SIMP_TAC (srw_ss()) [vR_def,wfs_no_cycles,FLOOKUP_DEF] 1135 1136 1137val wfs_max_path = Q.store_thm( 1138"wfs_max_path", 1139`wfs s ��� ���n v u. NRC (vR s) n v u ��� n ��� CARD (FDOM s)`, 1140STRIP_TAC THEN Induct THEN SRW_TAC [][] THEN 1141FULL_SIMP_TAC (srw_ss()) [NRC] THEN 1142RES_TAC THEN 1143Cases_on `n = CARD (FDOM s)` THEN 1144FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] 1145 1146val vR_FUNPOW_selfapp = Q.store_thm( 1147"vR_FUNPOW_selfapp", 1148`���n s v u. vR (FUNPOW selfapp n s) v u ��� ���m. 1 ��� m ��� m ��� n + 1 ��� NRC (vR s) m v u ��� 1149 (m ��� n ��� v NOTIN FDOM s)`, 1150Induct THEN SRW_TAC [][] THEN1 ( 1151 SRW_TAC [][EQ_IMP_THM] THEN1 ( 1152 Q.EXISTS_TAC `1` THEN SRW_TAC [][] ) THEN 1153 `m = 1` by DECIDE_TAC THEN 1154 FULL_SIMP_TAC (srw_ss()) [] ) THEN 1155SRW_TAC [][EQ_IMP_THM,FUNPOW_SUC,vR_selfapp,RUNION] THENL [ 1156 FULL_SIMP_TAC (srw_ss()) [vR1_def] THEN 1157 RES_TAC THEN Q.EXISTS_TAC `m` THEN SRW_TAC [][] THEN 1158 DECIDE_TAC, 1159 ..., 1160 Cases_on `m ��� SUC n` THENL [ 1161 SRW_TAC [][vR1_def] THEN 1162 DISJ1_TAC THEN 1163 Q.EXISTS_TAC `m` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1164 DECIDE_TAC, 1165 `m = SUC (SUC n)` by DECIDE_TAC THEN 1166 SRW_TAC [][] THEN 1167 FULL_SIMP_TAC (srw_ss()) [NRC] THEN 1168 SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 1169 1170 1171 FULL_SIMP_TAC (srw_ss()) [] 1172 RES_TAC 1173 FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 1174 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1175 Q.EXISTS_TAC `2` THEN SRW_TAC [][] THEN 1176 SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 1177 METIS_TAC [] ) THEN 1178 FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC] THEN 1179 FULL_SIMP_TAC (srw_ss()) [vR_selfapp,RUNION] 1180 RES_TAC THEN IMP_RES_TAC NRC_ADD_I THEN 1181 Q.EXISTS_TAC `m' + m` THEN SRW_TAC [][] THENL [ 1182 DECIDE_TAC, 1183 FULL_SIMP_TAC (srw_ss()) [ADD1] 1184 1185 1186completeInduct_on `n` THEN SRW_TAC [][EQ_IMP_THM] THENL [ 1187 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1188 Q.EXISTS_TAC `1` THEN SRW_TAC [][] ) THEN 1189 FIRST_X_ASSUM (Q.SPEC_THEN `n'` MP_TAC) THEN 1190 SRW_TAC [][] THEN 1191 FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC,vR_selfapp,RUNION] THEN1 ( 1192 FULL_SIMP_TAC (srw_ss()) [vR1_def] THEN 1193 Q.EXISTS_TAC `m'` THEN SRW_TAC [][] THEN 1194 DECIDE_TAC ) THEN 1195 FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN 1196 RES_TAC 1197`���n. vR (FUNPOW selfapp (SUC n) s) = vR1 s RUNION NRC (vR s) (2 * (SUC n))`, 1198Induct THEN SRW_TAC [][vR_selfapp] THEN 1199FULL_SIMP_TAC (srw_ss()) [vR_selfapp,FUNPOW_SUC,vR1_selfapp] THEN 1200FULL_SIMP_TAC (srw_ss()) [RUNION,FUN_EQ_THM,vR1_def,EQ_IMP_THM,vR_selfapp,O_DEF] THEN 1201SRW_TAC [][] THENL [ 1202 RES_TAC THEN SRW_TAC [][] THEN 1203 1204`��idempotent (selfapp s) ��� ���v u. NRC (vR s) 2 v u`, 1205SRW_TAC [][idempotent_def,selfapp_eq_iter_APPLY] THEN 1206Induct_on `t` THEN SRW_TAC [][] THEN1 ( 1207 1208`��idempotent s ��� ���v u. vR s v u ��� v IN FDOM s`, 1209SRW_TAC [][idempotent_def,vR_def] THEN 1210REVERSE (Induct_on `t`) THEN SRW_TAC [][] THEN RES_TAC 1211THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN 1212Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1213POP_ASSUM (K ALL_TAC) THEN 1214Induct_on `x` THEN SRW_TAC [][] THEN1 ( 1215 MAP_EVERY Q.EXISTS_TAC [`n'`,`n`] THEN 1216 SRW_TAC [][] THEN 1217 Cases_on `FLOOKUP s n'` THEN 1218 FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] ) THEN 1219Cases_on `n IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) [] 1220 1221`idempotent (FUNPOW selfapp n s) ��� ���v u. NRC (vR s) n v u`, 1222 1223`���n. idempotent (FUNPOW selfapp n s) ��� ���v u. NRC (vR s) n v u`, 1224Induct THEN SRW_TAC [][] THEN1 ( 1225 IMP_RES_TAC idempotent_selfapp THEN 1226 SRW_TAC [][FUNPOW_SUC] ) THEN 1227Cases_on `idempotent (FUNPOW selfapp (SUC n) s)` THEN 1228SRW_TAC [][NRC,idempotent_def,FUNPOW_SUC,selfapp_eq_iter_APPLY] 1229 1230val vRn_def = Define` 1231 vRn s n y x = NRC (vR s) n y x ��� y NOTIN FDOM s`; 1232 1233val wfs_IMP_fixpoint = Q.store_thm( 1234"wfs_IMP_fixpoint", 1235`wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`, 1236 1237SRW_TAC [][wfs_no_cycles,domrangevarb_idempotent] THEN 1238SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 1239FULL_SIMP_TAC (srw_ss()) [domrangevarb_def,BAG_FILTER_EQ_EMPTY,rangevarb_def,BAG_IN_BIG_BAG_UNION] THEN 1240`���n. wfs (FUNPOW selfapp n s)` 1241by (MATCH_MP_TAC FUNPOW_extends_mono THEN 1242 SRW_TAC [][Once wfs_selfapp]) THEN 1243`���n. FDOM (FUNPOW selfapp n s) = FDOM s` 1244by ( (FUNPOW_extends_mono |> Q.ISPEC `��s'. FDOM s' = FDOM s` |> 1245 SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC ) THEN 1246 SRW_TAC [][]) THEN 1247FULL_SIMP_TAC (srw_ss()) [SKOLEM_THM,FORALL_AND_THM] THEN 1248TC_vR_selfapp 1249TC_vR_vars_FRANGE 1250SRW_TAC [][wfs_def,domrangevarb_idempotent] THEN 1251SRW_TAC [][BAG_EXTENSION] 1252WF_INDUCTION_THM |> Q.ISPEC `vR (s:subst)` |> UNDISCH |> HO_MATCH_MP_TAC 1253SRW_TAC [][domrangevarb_idempotent] 1254 1255STRIP_TAC THEN 1256`���n. wfs (FUNPOW selfapp n s)` 1257by (MATCH_MP_TAC FUNPOW_extends_mono THEN 1258 SRW_TAC [][Once wfs_selfapp]) THEN 1259`���n. noids (FUNPOW selfapp n s)` 1260by METIS_TAC [wfs_noids] THEN 1261`���n. FDOM (FUNPOW selfapp n s) = FDOM s` 1262by ( (FUNPOW_extends_mono |> Q.ISPEC `��s'. FDOM s' = FDOM s` |> 1263 SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC ) THEN 1264 SRW_TAC [][]) THEN 1265SRW_TAC [][] THEN HO_MATCH_MP_TAC FUNPOW_exists THEN 1266Q.EXISTS_TAC `inv_image (mlt1 (vR s)^+)^+ domrangevarb` THEN 1267CONJ_TAC THEN1 ( 1268 MATCH_MP_TAC WF_inv_image THEN 1269 MATCH_MP_TAC WF_TC THEN 1270 MATCH_MP_TAC WF_mlt1 THEN 1271 MATCH_MP_TAC WF_TC THEN 1272 FULL_SIMP_TAC (srw_ss()) [wfs_def] ) THEN 1273Induct THEN FULL_SIMP_TAC (srw_ss()) [inv_image_def] THEN1 ( 1274 STRIP_TAC THEN 1275 (domrangevarb_idempotent |> EQ_IMP_RULE |> snd |> CONTRAPOS |> 1276 SIMP_RULE (srw_ss()) [] |> IMP_RES_TAC) 1277 1278*) 1279 1280val _ = export_theory (); 1281