1open HolKernel boolLib bossLib ramanaLib Parse stringTheory arithmeticTheory finite_mapTheory pred_setTheory bagTheory relationTheory prim_recTheory pairTheory termTheory substTheory walkTheory walkstarTheory 2 3val _ = new_theory "unifDef"; 4val _ = monadsyntax.temp_add_monadsyntax() 5val _ = metisTools.limit := { time = NONE, infs = SOME 5000 }; 6val _ = overload_on("monad_bind",``OPTION_BIND``); 7 8val vR_update = Q.prove( 9 `v NOTIN FDOM s /\ x <> v ==> (vR (s |+ (v,t)) y x <=> vR s y x)`, 10 SRW_TAC [][vR_def] THEN 11 Cases_on `x IN FDOM s` THEN 12 SRW_TAC [][FLOOKUP_DEF,FAPPLY_FUPDATE_THM]); 13 14val TC_vR_update = Q.prove( 15`!y x. (vR (s |+ (v,t)))^+ y x ==> v NOTIN FDOM s ==> 16 (vR s)^+ y x \/ ?u. (vR s)^* v x /\ u IN vars t /\ (vR s)^* y u`, 17HO_MATCH_MP_TAC TC_STRONG_INDUCT THEN 18CONJ_TAC 19THENL [ 20 MAP_EVERY Q.X_GEN_TAC [`y`,`x`] THEN SRW_TAC [][] THEN 21 Cases_on `x = v` THENL [ 22 DISJ2_TAC THEN 23 FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN 24 Q.EXISTS_TAC `y` THEN SRW_TAC [] [], 25 METIS_TAC [vR_update,TC_RULES] 26 ], 27 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] 28 THEN1 METIS_TAC [TC_RULES] THEN 29 DISJ2_TAC THEN Q.EXISTS_TAC `u` THEN 30 METIS_TAC [TC_RTC,RTC_TRANSITIVE,transitive_def] 31]); 32 33val wfs_extend = Q.store_thm( 34 "wfs_extend", 35 `wfs s /\ v NOTIN FDOM s /\ v NOTIN vars (walkstar s t) ==> 36 wfs (s |+ (v, t))`, 37 SRW_TAC [boolSimps.CONJ_ss][oc_eq_vars_walkstar, wfs_no_cycles] THEN 38 STRIP_TAC THEN 39 `!u. u IN vars t ==> ~(vR s)^+ v u` 40 by METIS_TAC [TC_vR_vars_walkstar, wfs_no_cycles] THEN 41 `?u. (vR s)^* v v' /\ u IN vars t /\ (vR s)^* v' u` 42 by METIS_TAC [TC_vR_update] THEN 43 FULL_SIMP_TAC (srw_ss()) [RTC_CASES_TC] THEN 44 METIS_TAC [NOT_FDOM_walkstar,wfs_no_cycles,TC_RULES] 45); 46 47val vwalk_FDOM = Q.store_thm( 48"vwalk_FDOM", 49`wfs s ==> (vwalk s v = t) ==> 50 (v NOTIN FDOM s /\ (t = Var v)) \/ 51 (v IN FDOM s /\ (t <> Var v) /\ 52 ?u.(vwalk s v = vwalk s u) /\ (FLOOKUP s u = SOME t))`, 53REVERSE (Cases_on `v IN FDOM s`) 54THEN1 METIS_TAC [NOT_FDOM_vwalk] THEN 55REPEAT STRIP_TAC THEN 56Q.PAT_X_ASSUM `v IN FDOM s` MP_TAC THEN 57Q.PAT_X_ASSUM `vwalk s v = t` MP_TAC THEN 58Q.ID_SPEC_TAC `v` THEN 59HO_MATCH_MP_TAC vwalk_ind THEN 60REPEAT (GEN_TAC ORELSE STRIP_TAC) THEN 61ASM_SIMP_TAC (srw_ss()) [] THEN 62Cases_on `FLOOKUP s v` 63 THEN1 (POP_ASSUM MP_TAC THEN SRW_TAC [][FLOOKUP_DEF]) THEN 64`x = s ' v` by (POP_ASSUM MP_TAC THEN SRW_TAC [][FLOOKUP_DEF]) THEN 65Cases_on `s ' v` THENL [ 66 `vwalk s v = vwalk s n` 67 by FULL_SIMP_TAC (srw_ss()) [Once(UNDISCH vwalk_def), FLOOKUP_DEF] THEN 68 SRW_TAC [][] THENL [ 69 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 70 Q_TAC SUFF_TAC `n = v` THEN1 METIS_TAC [] THEN 71 REVERSE (Cases_on `n IN FDOM s`) 72 THEN1 METIS_TAC [NOT_FDOM_vwalk,term_11] THEN 73 `vwalk s n <> Var n` by METIS_TAC [] THEN 74 `v IN vars (vwalk s n)` by METIS_TAC [IN_INSERT,vars_def] THEN 75 `(vR s)^+ v n` by METIS_TAC [vwalk_vR] THEN 76 `vR s n v` by FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 77 `(vR s)^+ n n` by METIS_TAC [TC_RULES] THEN 78 METIS_TAC [wfs_no_cycles], 79 Cases_on `n IN FDOM s` THEN1 METIS_TAC [] THEN 80 `vwalk s v = Var n` by METIS_TAC [NOT_FDOM_vwalk] THEN 81 METIS_TAC [] 82 ], 83 `vwalk s v = x` by SRW_TAC [][Once vwalk_def,FLOOKUP_DEF] THEN METIS_TAC [], 84 `vwalk s v = x` by SRW_TAC [][Once vwalk_def,FLOOKUP_DEF] THEN METIS_TAC [] 85]); 86 87val allvars_def = Define` 88 allvars s (t1:'a term) (t2:'a term) = vars t1 ��� vars t2 ��� substvars s`; 89 90val FINITE_allvars = RWstore_thm( 91"FINITE_allvars", 92`FINITE (allvars s t1 t2)`, 93SRW_TAC [][allvars_def]); 94 95val allvars_sym = Q.store_thm( 96"allvars_sym", 97`allvars s t1 t2 = allvars s t2 t1`, 98SRW_TAC [][allvars_def,UNION_COMM]); 99 100val uR_def = Define` 101uR (sx,c1,c2) (s,t1,t2) = 102wfs sx ��� s SUBMAP sx 103��� allvars sx c1 c2 SUBSET allvars s t1 t2 104��� measure (pair_count o (walkstar sx)) c1 t1` 105 106val FDOM_allvars = prove( 107 ``FDOM s ��� allvars s t1 t2``, 108 SRW_TAC [][allvars_def, substvars_def, SUBSET_DEF]); 109val intro = SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [AND_IMP_INTRO] 110 111val uR_lambda = let 112 val c = concl (SPEC_ALL uR_def) 113 val args = #2 (strip_comb (lhs c)) 114 val rhs' = pairSyntax.list_mk_pabs(args, rhs c) 115in 116 prove(``uR = ^rhs'``, 117 SIMP_TAC (srw_ss()) [FUN_EQ_THM, FORALL_PROD, uR_def]) 118end 119 120val uR_lex_def = Define` 121 uR_lex = inv_image ((��s1 s2. s2 SUBMAP s1 ��� s2 ��� s1) LEX (��s1 s2. s1 PSUBSET s2 ��� FINITE s2) LEX (measure pair_count)) 122 (��(s,t1,t2). (s,allvars s t1 t2,walk* s t1))` 123 124open lcsymtacs 125 126val uR_RSUBSET_uR_lex = Q.store_thm( 127"uR_RSUBSET_uR_lex", 128`uR RSUBSET uR_lex`, 129srw_tac [][RSUBSET] >> 130PairCases_on`x` >> PairCases_on`y` >> 131Q.MATCH_RENAME_TAC `uR_lex (sx,c1,c2) (s,t1,t2)` >> 132FULL_SIMP_TAC (srw_ss()) [uR_def,uR_lex_def,measure_thm,inv_image_def,LEX_DEF] >> 133Cases_on `sx = s` >> srw_tac [][PSUBSET_DEF]) 134 135val WF_FINITE_PSUBSET = Q.store_thm( 136"WF_FINITE_PSUBSET", 137`WF (��s1 s2. s1 PSUBSET s2 ��� FINITE s2)`, 138srw_tac [][WF_EQ_WFP] >> 139REVERSE (Cases_on `FINITE x`) >- ( 140 srw_tac [][WFP_DEF] ) >> 141POP_ASSUM mp_tac >> 142Q.ID_SPEC_TAC `x` >> 143match_mp_tac FINITE_COMPLETE_INDUCTION >> 144srw_tac [][] >> 145match_mp_tac WFP_RULES >> 146srw_tac [][]) 147 148val WF_uR = Q.store_thm( 149"WF_uR", 150`WF uR`, 151SRW_TAC [][WF_IFF_WELLFOUNDED,wellfounded_def,uR_lambda,UNCURRY, 152 EXISTS_OR_THM] THEN 153SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 154Q.ABBREV_TAC `f1 = \n. FST (f n)` THEN 155`!n. FST (f n) = f1 n` by SRW_TAC [][Abbr`f1`] THEN 156Q.ABBREV_TAC `f2 = \n. FST (SND (f n))` THEN 157`!n. FST (SND (f n)) = f2 n` by SRW_TAC [][Abbr`f2`] THEN 158Q.ABBREV_TAC `f3 = \n. SND (SND (f n))` THEN 159`!n. SND (SND (f n)) = f3 n` by SRW_TAC [][Abbr`f3`] THEN 160FULL_SIMP_TAC (srw_ss()) [] THEN 161REPEAT (Q.PAT_X_ASSUM `Abbrev B` (K ALL_TAC)) THEN 162Q.ISPECL_THEN [`��x y. y:num set SUBSET x`, 163 `��n. allvars (f1 n) (f2 n) (f3 n)`] 164 MP_TAC 165 transitive_monotone THEN 166DISCH_THEN 167 (fn th => th |> SIMP_RULE (srw_ss()) [transitive_def,GSYM AND_IMP_INTRO] 168 |> UNDISCH 169 |> (fn th => PROVE_HYP (prove(hd(hyp th), 170 METIS_TAC [SUBSET_TRANS])) th) 171 |> MP_TAC) THEN 172`���m n. m < n ��� f1 m ��� f1 n` 173 by (CONV_TAC (STRIP_QUANT_CONV 174 (RAND_CONV (RAND_CONV (UNBETA_CONV ``n:num``) THENC 175 LAND_CONV (UNBETA_CONV ``m:num``)))) THEN 176 MATCH_MP_TAC transitive_monotone THEN 177 SRW_TAC [][transitive_def] THEN METIS_TAC [SUBMAP_TRANS]) THEN 178SRW_TAC [][] THEN 179SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 180`?m.!n. m < n ==> 181 (allvars (f1 n) (f2 n) (f3 n) = allvars (f1 m) (f2 m) (f3 m))` 182 by (SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 183 FULL_SIMP_TAC (srw_ss()) [SKOLEM_THM] THEN 184 `!m. m < f' m /\ 185 allvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m)) 186 PSUBSET 187 allvars (f1 m) (f2 m) (f3 m)` 188 by METIS_TAC [PSUBSET_DEF] THEN 189 `!m. measure CARD 190 (allvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m))) 191 (allvars (f1 m) (f2 m) (f3 m))` 192 by METIS_TAC [measure_thm,FINITE_allvars,CARD_PSUBSET] THEN 193 `WF (measure (CARD:((num -> bool) -> num)))` by SRW_TAC [][] THEN 194 FULL_SIMP_TAC bool_ss [WF_IFF_WELLFOUNDED,wellfounded_def] THEN 195 POP_ASSUM (Q.SPEC_THEN 196 `\n. let t = FUNPOW f' n 0 197 in allvars (f1 t) (f2 t) (f3 t)` 198 MP_TAC) THEN 199 FULL_SIMP_TAC (srw_ss()) [LET_THM,FUNPOW_SUC]) THEN 200`?m.!n.m < n ==> (f1 m = f1 n)` 201by (Q.ISPECL_THEN 202 [`f1`, 203 `\n. allvars (f1 n) (f2 n) (f3 n) DIFF (FDOM(f1 n))`, `m`] 204 (MATCH_MP_TAC o GSYM o SIMP_RULE (srw_ss()) []) 205 commonUnifTheory.extension_chain THEN 206 SRW_TAC [][DISJOINT_DEF] THENL [ 207 SRW_TAC [][EXTENSION] THEN METIS_TAC [], 208 METIS_TAC [UNION_DIFF,allvars_def,substvars_def,SUBSET_UNION,SUBSET_TRANS] 209 ]) THEN 210Q.ABBREV_TAC `z = MAX m m'` THEN 211`!n. z < n ==> (f1 n = f1 m')` by METIS_TAC [MAX_LT] THEN 212`!n. z < n ==> measure (pair_count o (walkstar (f1 m'))) 213 (f2 (SUC n)) (f2 n)` 214 by (SRW_TAC [][] THEN METIS_TAC [LESS_SUC]) THEN 215`WF (measure (pair_count o (walkstar (f1 m'))))` by SRW_TAC [][] THEN 216FULL_SIMP_TAC bool_ss [WF_IFF_WELLFOUNDED,wellfounded_def] THEN 217POP_ASSUM (Q.SPEC_THEN `\n. f2 (z+n+1)` MP_TAC) THEN 218SRW_TAC [][] THEN 219Q.PAT_X_ASSUM `!n.z < n ==> measure X Y Z` (Q.SPEC_THEN `z+n+1` MP_TAC) THEN 220SRW_TAC [ARITH_ss][ADD1]); 221 222val tunify_defn_q =` 223 tunify s t1 t2 = 224 if wfs s then 225 case (walk s t1, walk s t2) of 226 (Var v1, Var v2) => SOME if (v1 = v2) then s else (s |+ (v1,Var v2)) 227 | (Var v1, t2) => if oc s t2 v1 then NONE else SOME (s |+ (v1,t2)) 228 | (t1, Var v2) => if oc s t1 v2 then NONE else SOME (s |+ (v2,t1)) 229 | (Pair t1a t1d, Pair t2a t2d) => 230 do sx <- tunify s t1a t2a; tunify sx t1d t2d od 231 | (Const c1, Const c2) => if (c1 = c2) then SOME s else NONE 232 | _ => NONE 233else ARB`; 234 235val tunify_defn = Hol_defn "tunify" tunify_defn_q; 236 237val _ = store_term_thm("tunify_defn", TermWithCase tunify_defn_q); 238 239val [tc0,tc1,tc2] = map (SIMP_TERM (srw_ss()) []) (Defn.tcs_of tunify_defn); 240val _ = store_term_thm("tunify_tcd", tc0); 241val _ = store_term_thm("tunify_tca", tc1); 242val _ = store_term_thm("tunify_tc_WF", tc2); 243 244val vwalk_to_Pair_SUBSET_rangevars = Q.store_thm( 245"vwalk_to_Pair_SUBSET_rangevars", 246`wfs s /\ (vwalk s v = Pair t1 t2) 247 ==> (vars t1 SUBSET (rangevars s)) /\ 248 (vars t2 SUBSET (rangevars s))`, 249STRIP_TAC THEN 250`v ��� FDOM s` by METIS_TAC [NOT_FDOM_vwalk,term_distinct] THEN 251IMP_RES_TAC vwalk_IN_FRANGE THEN 252IMP_RES_TAC IN_FRANGE_rangevars THEN 253POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) []); 254 255val allvars_SUBSET = Q.store_thm( 256"allvars_SUBSET", 257`wfs s /\ 258 (walk s t1 = Pair t1a t1d) /\ 259 (walk s t2 = Pair t2a t2d) ==> 260 allvars s t1a t2a SUBSET allvars s t1 t2 /\ 261 allvars s t1d t2d SUBSET allvars s t1 t2`, 262SRW_TAC [][walk_def,allvars_def] THEN 263Cases_on `t1` THEN Cases_on `t2` THEN 264FULL_SIMP_TAC (srw_ss()) [] THEN 265METIS_TAC [vwalk_to_Pair_SUBSET_rangevars,substvars_def,SUBSET_TRANS,SUBSET_UNION]); 266 267val walkstar_subterm_smaller = Q.store_thm( 268"walkstar_subterm_smaller", 269`wfs s /\ (walk s t1 = Pair t1a t1d) ==> 270 pair_count (walkstar s t1a) < pair_count (walkstar s t1) /\ 271 pair_count (walkstar s t1d) < pair_count (walkstar s t1)`, 272SRW_TAC [][walk_def] THEN 273Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 274FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []); 275 276val tca_thm = Q.store_thm( 277"tca_thm", 278`wfs s /\ 279 (walk s t1 = Pair t1a t1d) /\ 280 (walk s t2 = Pair t2a t2d) ==> 281 uR (s,t1a,t2a) (s,t1,t2)`, 282SRW_TAC [][uR_def,SUBMAP_REFL] THEN 283METIS_TAC [allvars_SUBSET,walkstar_subterm_smaller]); 284 285val met = METIS_TAC [SUBSET_UNION,SUBSET_TRANS]; 286 287val allvars_SUBSET_FUPDATE = Q.store_thm( 288"allvars_SUBSET_FUPDATE", 289`(walk s t1 = Pair t1a t1d) /\ (walk s t2 = Pair t2a t2d) /\ 290 (walk s t1a = Var v) /\ wfs s ==> 291 allvars (s |+ (v,walk s t2a)) t1d t2d SUBSET allvars s t1 t2`, 292SRW_TAC [][allvars_def] THEN1 ( 293 Cases_on `walk s t1 = t1` THEN1 ( 294 FULL_SIMP_TAC (srw_ss()) [] THEN met) THEN 295 IMP_RES_TAC walk_IN_FRANGE THEN 296 IMP_RES_TAC IN_FRANGE_rangevars THEN 297 Q.PAT_X_ASSUM `walk s t1 = X` ASSUME_TAC THEN 298 FULL_SIMP_TAC (srw_ss()) [substvars_def] THEN met ) 299THEN1 ( 300 Cases_on `walk s t2 = t2` THEN1 ( 301 FULL_SIMP_TAC (srw_ss()) [] THEN met) THEN 302 IMP_RES_TAC walk_IN_FRANGE THEN 303 IMP_RES_TAC IN_FRANGE_rangevars THEN 304 Q.PAT_X_ASSUM `walk s t2 = X` ASSUME_TAC THEN 305 FULL_SIMP_TAC (srw_ss()) [substvars_def] THEN met ) THEN 306IMP_RES_TAC walk_to_var THEN SRW_TAC [][] THEN 307ASM_SIMP_TAC (srw_ss()) [substvars_def,rangevars_FUPDATE] THEN 308CONJ_TAC THEN1 ( 309 REVERSE CONJ_TAC THEN1 met THEN 310 Cases_on `u = v` THEN SRW_TAC [][] THEN1 ( 311 Cases_on `walk s t1 = t1` THEN 312 FULL_SIMP_TAC (srw_ss()) [] THEN 313 IMP_RES_TAC walk_IN_FRANGE THEN 314 IMP_RES_TAC IN_FRANGE_rangevars THEN 315 Q.PAT_X_ASSUM `walk s t1 = X` ASSUME_TAC THEN 316 FULL_SIMP_TAC (srw_ss()) [] ) THEN 317 FULL_SIMP_TAC (srw_ss()) [] THEN 318 `u ��� FDOM s` by METIS_TAC [NOT_FDOM_vwalk,term_11] THEN 319 IMP_RES_TAC vwalk_IN_FRANGE THEN 320 IMP_RES_TAC IN_FRANGE_rangevars THEN 321 Q.PAT_X_ASSUM `vwalk s u = X` ASSUME_TAC THEN 322 FULL_SIMP_TAC (srw_ss()) [] ) THEN 323CONJ_TAC THEN1 met THEN 324Cases_on `walk s t2a = t2a` THEN 325FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 326 Cases_on `walk s t2 = t2` THEN 327 FULL_SIMP_TAC (srw_ss()) [] THEN1 met THEN 328 IMP_RES_TAC walk_IN_FRANGE THEN 329 IMP_RES_TAC IN_FRANGE_rangevars THEN 330 Q.PAT_X_ASSUM `walk s t2 = X` ASSUME_TAC THEN 331 FULL_SIMP_TAC (srw_ss()) [] THEN met ) THEN 332IMP_RES_TAC walk_IN_FRANGE THEN 333IMP_RES_TAC IN_FRANGE_rangevars THEN met ); 334 335val walkstar_subterm_FUPDATE = Q.store_thm( 336"walkstar_subterm_FUPDATE", 337`wfs s /\ v NOTIN FDOM s /\ v NOTIN vars (walkstar s t) /\ 338 (walk s t1 = Pair t1a t1d) ==> 339 pair_count (walkstar (s |+ (v,t)) t1d) < 340 pair_count (walkstar (s |+ (v,t)) t1)`, 341SRW_TAC [][] THEN 342`wfs (s |+ (v,t))` by METIS_TAC [wfs_extend] THEN 343`s SUBMAP (s |+ (v,t))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 344`walk (s |+ (v,t)) t1 = Pair t1a t1d` 345 by (Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [walk_def] THEN 346 Q.MATCH_ABBREV_TAC `vwalk (s|+(v,t)) s' = Pair t1a t1d` THEN 347 MP_TAC(Q.SPECL[`s'`,`s`](Q.INST[`sx`|->`(s |+ (v,t))`](UNDISCH 348 vwalk_SUBMAP))) THEN 349 SRW_TAC [][]) THEN 350Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [walk_def] THEN 351SRW_TAC [ARITH_ss][measure_thm,walkstar_thm] 352); 353 354val SOME tunify_aux_defn = Defn.aux_defn tunify_defn; 355 356val aux_def = 357SIMP_RULE std_ss [] 358(MATCH_MP 359 (MATCH_MP WFREC_COROLLARY 360 (Q.SPEC`uR`(definition"tunify_tupled_AUX_def"))) 361 WF_uR); 362 363val uR_subterm = Q.store_thm( 364"uR_subterm", 365`wfs s /\ 366 (walk s t1 = Pair t1a t1d) /\ 367 (walk s t2 = Pair t2a t2d) ==> 368 uR (s,t1a,t2a) (s,t1,t2) /\ 369 uR (s,t1d,t2d) (s,t1,t2)`, 370REPEAT STRIP_TAC THEN 371SRW_TAC [][uR_def,SUBMAP_REFL] THEN 372METIS_TAC [allvars_SUBSET,walkstar_subterm_smaller] 373); 374 375val uR_subterm_FUPDATE = Q.store_thm( 376"uR_subterm_FUPDATE", 377`(walk s t1 = Pair t1a t1d) /\ 378 (walk s t2 = Pair t2a t2d) /\ 379 ((walk s t1a = Var v) /\ (walk s t2a = t) ��� 380 (walk s t2a = Var v) ��� (walk s t1a = t)) ��� 381 wfs s /\ 382 v NOTIN FDOM s /\ 383 v NOTIN vars (walk* s t) ==> 384 uR (s |+ (v,t), t1d, t2d) (s,t1,t2)`, 385STRIP_TAC THEN 386`wfs (s |+ (v,t))` by METIS_TAC [wfs_extend] THEN 387`s SUBMAP (s|+(v,t))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 388(SRW_TAC [][uR_def] THEN1 METIS_TAC [allvars_SUBSET_FUPDATE,allvars_sym] THEN 389METIS_TAC [walkstar_subterm_FUPDATE]) 390); 391 392val uR_ind = save_thm("uR_ind",WF_INDUCTION_THM |> Q.ISPEC `uR` |> SIMP_RULE (srw_ss()) [WF_uR] 393|> Q.SPEC `\(a,b,c).P a b c` |> SIMP_RULE std_ss [FORALL_PROD] |> Q.GEN`P`); 394 395val uP_def = Define` 396uP sx s t1 t2 = wfs sx /\ s SUBMAP sx /\ substvars sx SUBSET allvars s t1 t2`; 397 398val uP_sym = Q.store_thm( 399"uP_sym", 400`uP sx s t1 t2 ��� uP sx s t2 t1`, 401SRW_TAC [][uP_def,allvars_sym]); 402 403val uP_FUPDATE = Q.store_thm( 404"uP_FUPDATE", 405`wfs s /\ 406 v NOTIN FDOM s /\ 407 v NOTIN vars (walkstar s t2) /\ 408 (walk s t1 = Var v) ==> 409 uP (s |+ (v,walk s t2)) s t1 t2`, 410STRIP_TAC THEN 411`wfs (s |+ (v,walk s t2))` by METIS_TAC [wfs_extend,walkstar_walk] THEN 412`s SUBMAP (s|+(v,walk s t2))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 413SRW_TAC [][uP_def,allvars_def] THEN 414Cases_on `walk s t2 = t2` THEN 415FULL_SIMP_TAC (srw_ss()) [] THEN 416FULL_SIMP_TAC (srw_ss()) [substvars_def,rangevars_FUPDATE] THEN 417Cases_on `walk s t1 = t1` THEN 418FULL_SIMP_TAC (srw_ss()) [] THEN1 met THEN 419IMP_RES_TAC walk_IN_FRANGE THEN 420IMP_RES_TAC IN_FRANGE_rangevars THEN 421Q.PAT_X_ASSUM `walk s t1 = X` ASSUME_TAC THEN 422FULL_SIMP_TAC (srw_ss()) [] THEN met); 423 424val walk_SUBMAP = Q.store_thm( 425"walk_SUBMAP", 426`wfs sx /\ s SUBMAP sx ==> 427 case walk s t of 428 Var u => walk sx t = walk sx (Var u) 429 | u => walk sx t = u`, 430Cases_on `t` THEN SRW_TAC [][walk_def] THEN 431MP_TAC (Q.SPECL [`n`,`s`] (UNDISCH vwalk_SUBMAP)) THEN 432SRW_TAC [][]) 433 434val uR_IMP_uP = Q.store_thm( 435"uR_IMP_uP", 436`uR (sx,c1,c2) (s,t1,t2) ==> uP sx s t1 t2`, 437SRW_TAC [][uR_def,uP_def,allvars_def]) 438 439val uP_IMP_subterm_uR = Q.store_thm( 440"uP_IMP_subterm_uR", 441`wfs s /\ 442 (walk s t1 = Pair t1a t1d) /\ 443 (walk s t2 = Pair t2a t2d) /\ 444 (uP sx s t1a t2a \/ uP sx s t1d t2d) ==> 445 uR (sx,t1d,t2d) (s,t1,t2)`, 446SRW_TAC [][] THEN ( 447`allvars s t1a t2a SUBSET allvars s t1 t2 /\ 448 allvars s t1d t2d SUBSET allvars s t1 t2` 449 by METIS_TAC [allvars_SUBSET] THEN 450FULL_SIMP_TAC (srw_ss()) [uR_def,uP_def] THEN 451`substvars sx SUBSET allvars s t1 t2` by METIS_TAC [SUBSET_TRANS] THEN 452SRW_TAC [][] THENL [ 453 SRW_TAC [][Once allvars_def] THEN 454 METIS_TAC [allvars_def,SUBSET_UNION,SUBSET_TRANS], 455 `walk sx t1 = walk s t1` 456 by (MP_TAC (Q.INST [`t`|->`t1`] walk_SUBMAP) THEN 457 SRW_TAC [][]) THEN 458 Cases_on `t1` THEN 459 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [measure_thm,walk_def] 460])) 461 462val aux_uP = Q.store_thm( 463"aux_uP", 464`!s t1 t2 sx. 465 wfs s /\ (tunify_tupled_aux uR (s,t1,t2) = SOME sx) ==> 466 uP sx s t1 t2`, 467HO_MATCH_MP_TAC uR_ind THEN 468REPEAT (GEN_TAC ORELSE (DISCH_THEN STRIP_ASSUME_TAC)) THEN 469POP_ASSUM MP_TAC THEN 470ASM_SIMP_TAC (srw_ss()) [aux_def] THEN 471Cases_on `walk s t1` THEN Cases_on `walk s t2` 472THEN ASM_SIMP_TAC (srw_ss()) [] THENL [ 473 SRW_TAC [][] THEN1 474 (SRW_TAC [][uP_def,SUBMAP_REFL,allvars_def] THEN 475 METIS_TAC [SUBSET_UNION,SUBSET_TRANS]) THEN 476 `n NOTIN FDOM s` 477 by (IMP_RES_TAC walk_var_vwalk THEN 478 IMP_RES_TAC vwalk_to_var THEN 479 IMP_RES_TAC NOT_FDOM_vwalk) THEN 480 `n NOTIN vars (walkstar s (Var n'))` 481 by (IMP_RES_TAC walk_var_vwalk THEN 482 IMP_RES_TAC vwalk_to_var THEN 483 IMP_RES_TAC NOT_FDOM_vwalk THEN 484 SRW_TAC [][walkstar_thm]) THEN 485 METIS_TAC [uP_FUPDATE,walkstar_walk], 486 SRW_TAC [][] THEN 487 `n NOTIN FDOM s` 488 by (IMP_RES_TAC walk_var_vwalk THEN 489 IMP_RES_TAC vwalk_to_var THEN 490 IMP_RES_TAC NOT_FDOM_vwalk) THEN 491 `n NOTIN vars (walkstar s (Pair t t0))` 492 by (`~(n IN oc s t \/ n IN oc s t0)` by METIS_TAC [IN_DEF] THEN 493 SRW_TAC [][walkstar_thm] THEN 494 METIS_TAC [oc_eq_vars_walkstar]) THEN 495 METIS_TAC [uP_FUPDATE,walkstar_walk], 496 SRW_TAC [][] THEN 497 `n NOTIN FDOM s` 498 by (IMP_RES_TAC walk_var_vwalk THEN 499 IMP_RES_TAC vwalk_to_var THEN 500 IMP_RES_TAC NOT_FDOM_vwalk) THEN 501 Q.MATCH_ASSUM_RENAME_TAC `walk s _ = Const c` THEN 502 `n NOTIN vars (walkstar s (Const c))` 503 by (SRW_TAC [][walkstar_thm]) THEN 504 METIS_TAC [uP_FUPDATE,walkstar_walk], 505 SRW_TAC [][] THEN 506 `n NOTIN FDOM s` 507 by (IMP_RES_TAC walk_var_vwalk THEN 508 IMP_RES_TAC vwalk_to_var THEN 509 IMP_RES_TAC NOT_FDOM_vwalk) THEN 510 `n NOTIN vars (walkstar s (Pair t t0))` 511 by (`~(n IN oc s t \/ n IN oc s t0)` by METIS_TAC [IN_DEF] THEN 512 SRW_TAC [][walkstar_thm] THEN 513 METIS_TAC [oc_eq_vars_walkstar]) THEN 514 METIS_TAC [uP_FUPDATE,walkstar_walk,uP_sym], 515 `uR (s,t,t') (s,t1,t2)` by METIS_TAC [uR_subterm] THEN 516 ASM_SIMP_TAC (srw_ss()) [RESTRICT_LEMMA] THEN 517 Cases_on `tunify_tupled_aux uR (s,t,t')` THEN 518 FULL_SIMP_TAC (srw_ss()) [] THEN 519 `uP x s t t'` 520 by (FIRST_ASSUM (Q.SPECL_THEN [`s`,`t`,`t'`] ASSUME_TAC) 521 THEN RES_TAC) THEN 522 `uR (x,t0,t0') (s,t1,t2)` 523 by METIS_TAC [uP_IMP_subterm_uR] THEN 524 ASM_SIMP_TAC (srw_ss()) [RESTRICT_LEMMA] THEN 525 STRIP_TAC THEN 526 `wfs x` by FULL_SIMP_TAC (srw_ss()) [uP_def] THEN 527 `uP sx x t0 t0'` by METIS_TAC [] THEN 528 FULL_SIMP_TAC (srw_ss()) [uP_def,uR_def] THEN 529 METIS_TAC [SUBMAP_TRANS,SUBSET_TRANS], 530 SRW_TAC [][] THEN 531 `n NOTIN FDOM s` 532 by (IMP_RES_TAC walk_var_vwalk THEN 533 IMP_RES_TAC vwalk_to_var THEN 534 IMP_RES_TAC NOT_FDOM_vwalk) THEN 535 Q.MATCH_ASSUM_RENAME_TAC `walk s _ = Const c` THEN 536 `n NOTIN vars (walkstar s (Const c))` 537 by (SRW_TAC [][walkstar_thm]) THEN 538 METIS_TAC [uP_FUPDATE,walkstar_walk,uP_sym], 539 SRW_TAC [][uP_def,allvars_def,SUBMAP_REFL] THEN 540 METIS_TAC [SUBSET_UNION,SUBSET_TRANS] 541]) 542 543val tcd_thm = Q.store_thm( 544"tcd_thm", 545`wfs s /\ 546 (walk s t1 = Pair t1a t1d) /\ 547 (walk s t2 = Pair t2a t2d) /\ 548 (tunify_tupled_aux uR (s,t1a,t2a) = SOME sx) ==> 549 uR (sx,t1d,t2d) (s,t1,t2)`, 550METIS_TAC [aux_uP, uP_IMP_subterm_uR]) 551 552val (tunify_def,tunify_ind) = Defn.tprove ( 553tunify_defn, 554WF_REL_TAC `uR` THEN METIS_TAC [WF_uR,tca_thm,tcd_thm] 555) 556 557val [aux_eqn0] = Defn.eqns_of tunify_aux_defn 558val aux_eqn = aux_eqn0 |> Q.INST[`R`|->`uR`] |> 559 PROVE_HYP WF_uR |> 560 (fn th => PROVE_HYP 561 (prove(hd(hyp th),SRW_TAC[][tcd_thm])) th) |> 562 (fn th => PROVE_HYP 563 (prove(hd(hyp th),SRW_TAC[][tca_thm])) th) 564 565val aux_eq_tunify = Q.store_thm( 566"aux_eq_tunify", 567`!s t1 t2. tunify_tupled_aux uR (s,t1,t2) = tunify s t1 t2`, 568HO_MATCH_MP_TAC tunify_ind THEN 569REPEAT STRIP_TAC THEN 570SRW_TAC [][Once aux_eqn] THEN 571SRW_TAC [][Once tunify_def,SimpRHS] THEN 572Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN 573SRW_TAC [][] THEN 574Cases_on `tunify s t t'` THEN SRW_TAC [][] 575) 576 577val ext_s_check_def = RWDefine` 578ext_s_check s v t = if oc s t v then NONE else SOME (s |+ (v,t))` 579 580val unify_exists = prove( 581``?unify.!s t1 t2.wfs s ==> (unify s t1 t2 = 582 case (walk s t1, walk s t2) of 583 (Var v1, Var v2) => SOME if (v1 = v2) then s else (s |+ (v1,Var v2)) 584 | (Var v1, t2) => ext_s_check s v1 t2 585 | (t1, Var v2) => ext_s_check s v2 t1 586 | (Pair t1a t1d, Pair t2a t2d) => 587 do sx <- unify s t1a t2a; unify sx t1d t2d od 588 | (Const c1, Const c2) => if (c1 = c2) then SOME s else NONE 589 | _ => NONE)``, 590Q.EXISTS_TAC `tunify` THEN 591SRW_TAC [][Once tunify_def,SimpLHS] THEN 592Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN 593SRW_TAC [][]) 594 595val unify_def = new_specification("unify_def",["unify"],unify_exists) 596 597val _ = store_type_thm("unify_type",type_of``unify``) 598 599val unify_eq_tunify = Q.store_thm( 600"unify_eq_tunify", 601`!s t1 t2. wfs s ==> (unify s t1 t2 = tunify s t1 t2)`, 602HO_MATCH_MP_TAC tunify_ind THEN 603REPEAT STRIP_TAC THEN 604SRW_TAC [][Once tunify_def,SimpRHS] THEN 605SRW_TAC [][Once unify_def,SimpLHS] THEN 606Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN 607SRW_TAC [][] THEN 608Cases_on `tunify s t t'` THEN SRW_TAC [][] THEN 609`wfs x` by METIS_TAC [aux_eq_tunify,uP_def,aux_uP] THEN 610METIS_TAC []) 611 612val _ = metisTools.limit := { time = NONE, infs = NONE } 613val unify_ind = Q.store_thm( 614"unify_ind", 615`!P. 616 (!s t1 t2. 617 (!t1a t1d t2a t2d sx. 618 wfs s /\ 619 (walk s t1 = Pair t1a t1d) /\ 620 (walk s t2 = Pair t2a t2d) /\ 621 (unify s t1a t2a = SOME sx) ==> 622 P sx t1d t2d) /\ 623 (!t1a t1d t2a t2d. 624 wfs s /\ 625 (walk s t1 = Pair t1a t1d) /\ 626 (walk s t2 = Pair t2a t2d) ==> 627 P s t1a t2a) ==> 628 P s t1 t2) ==> 629 !v v1 v2. P v v1 v2`, 630METIS_TAC [unify_eq_tunify,tunify_ind]) 631 632val unify_uP = Q.store_thm( 633"unify_uP", 634`wfs s /\ (unify s t1 t2 = SOME sx) ==> 635 uP sx s t1 t2`, 636METIS_TAC [unify_eq_tunify,aux_eq_tunify,aux_uP]) 637 638val _ = export_theory () 639