1open HolKernel boolLib bossLib Parse pred_setTheory relationTheory finite_mapTheory termTheory ramanaLib pairTheory bagTheory prim_recTheory substTheory walkTheory walkstarTheory 2 3val _ = new_theory "redUnif" 4val _ = metisTools.limit := { time = NONE, infs = SOME 5000 } 5 6val istep_def = Define` 7 istep (sl,bl) (sr,br) = 8 (���t. (br + {|(t, t)|} = bl) ��� 9 (sr = sl)) ��� 10 (���t1a t1d t2a t2d. 11 (br + {|(Pair t1a t1d, Pair t2a t2d)|} = {|(t1a,t2a); (t1d,t2d)|} + bl) ��� 12 (sr = sl)) ��� 13 (���v t bi. 14 ((bi + {|(Var v, t)|} = bl) ��� 15 (bi + {|(t, Var v)|} = bl)) ��� 16 v ��� vars t ��� 17 (br = BAG_IMAGE (��(t1,t2). ((FEMPTY|+(v,t)) ��� t1, (FEMPTY|+(v,t)) ��� t2)) bi) ��� 18 (sr = sl |+ (v,t)))`; 19 20val tstep_def = Define` 21 tstep (sl,bl) (sr,br) = 22 (���t1 t2. 23 (walk sl t1 = walk sl t2) ��� 24 (br + {|(t1,t2)|} = bl) ��� 25 (sr = sl)) ��� 26 (���t1 t2 t1a t1d t2a t2d. 27 (walk sl t1 = Pair t1a t1d) ��� (walk sl t2 = Pair t2a t2d) ��� 28 (br + {|(t1,t2)|} = {|(t1a,t2a); (t1d,t2d)|} + bl) ��� 29 (sr = sl)) ��� 30 (���t1 t2 v t. 31 ((walk sl t1 = Var v) ��� (walk sl t2 = t) ��� 32 (walk sl t1 = t) ��� (walk sl t2 = Var v)) ��� 33 �� oc sl t v ��� 34 (br + {|(t1,t2)|} = bl) ��� 35 (sr = sl |+ (v,t)))`; 36 37open unifDefTheory unifPropsTheory; 38 39val wfs_tstep = Q.store_thm( 40"wfs_tstep", 41`wfs sl ��� tstep (sl,bl) (sr,br) ��� wfs sr`, 42SRW_TAC [][tstep_def] THEN SRW_TAC [][] THEN 43IMP_RES_TAC walk_to_var THEN 44Q.PAT_ASSUM `wfs s` ASSUME_TAC THEN 45FULL_SIMP_TAC (srw_ss()) [oc_eq_vars_walkstar,walkstar_walk] THEN 46MATCH_MP_TAC wfs_extend THEN 47METIS_TAC [IN_DEF,walkstar_walk]) 48 49val walks_equal = Q.store_thm( 50"walks_equal", 51`wfs s ��� (walk s t1 = walk s t2) ��� (t1 = t2) ��� ���v. (t1 = Var v) ��� (t2 = Var v)`, 52Cases_on `t1 = t2` THEN ASM_SIMP_TAC (srw_ss()) [] THEN 53SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN STRIP_TAC THEN 54MAP_EVERY Cases_on [`t1`,`t2`] THEN SRW_TAC [][] THEN 55METIS_TAC []); 56 57val NOTIN_vars_walk = Q.store_thm( 58"NOTIN_vars_walk", 59`wfs s ��� (vwalk s v = walk s t) ��� (t ��� Var v) ��� v ��� vars t`, 60Cases_on `t` THEN SRW_TAC [][] THEN 61SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 62`v ��� vars (vwalk s v)` by SRW_TAC [][] THEN 63IMP_RES_TAC vwalk_vR THEN 64Q.PAT_ASSUM `vwalk s v = X` ASSUME_TAC THEN 65FULL_SIMP_TAC (srw_ss()) [wfs_no_cycles] THEN 66RES_TAC); 67 68(* 69val istep_if_tstep = Q.store_thm( 70"istep_if_tstep", (* no! the substitutions won't be equal, they will be equivalent. istep gives an idempotent substitution whereas tstep gives a triangular one! *) 71`wfs sl ��� tstep^* (sl,bl) (sr,br) ��� ���br'. tstep^* (sl,bl) (sr,br')`, 72Q_TAC SUFF_TAC 73`���x y. RTC tstep x y ��� wfs (FST x) ��� ���br. RTC istep x (FST y,br)` 74THEN1 ( SRW_TAC [][] THEN RES_TAC THEN 75 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [] ) THEN 76HO_MATCH_MP_TAC RTC_INDUCT THEN 77SRW_TAC [][] THEN1 ( 78 Q.EXISTS_TAC `SND x` THEN SRW_TAC [][] ) THEN 79Q.MATCH_ASSUM_RENAME_TAC `tstep a b` THEN 80MAP_EVERY Cases_on [`a`,`b`] THEN 81Q.MATCH_ASSUM_RENAME_TAC `tstep (sl,bl) (si,bi)` THEN 82FULL_SIMP_TAC (srw_ss()) [] THEN 83IMP_RES_TAC wfs_tstep THEN 84FULL_SIMP_TAC (srw_ss()) [] THEN 85Q.MATCH_ASSUM_RENAME_TAC `istep^* (si,bi) (FST sr,br)` THEN 86 87FULL_SIMP_TAC (srw_ss()) [tstep_def] THEN 88SRW_TAC [][] THEN1 ( 89 `(t1 = t2) ��� (t1 ��� t2) ��� ���v. (t1 = Var v) ��� (t2 = Var v)` 90 by METIS_TAC [walks_equal] THEN 91 SRW_TAC [][] THEN1 ( 92 Q.EXISTS_TAC `br` THEN 93 Q.MATCH_ABBREV_TAC `RTC istep pi pr` THEN 94 Q_TAC SUFF_TAC `istep pi (si,bi)` 95 THEN1 METIS_TAC [RTC_RULES] THEN 96 SRW_TAC [][istep_def,Abbr`pi`] ) THEN 97 FULL_SIMP_TAC (srw_ss()) [] THEN 98 SRW_TAC [][] THEN 99 TRY (Q.PAT_ASSUM `Var v ��� t2` (ASSUME_TAC o GSYM)) THEN 100 IMP_RES_TAC NOTIN_vars_walk THEN 101 102val tstep_if_istep = Q.store_thm( 103"tstep_if_istep", (* need/want idempotent sl instead? *) 104`wfs sl ��� istep^* (sl,bl) (sr,br) ��� ���br'. tstep^* (sl,bl) (sr,br')`, 105Q_TAC SUFF_TAC 106`���x y. RTC istep x y ��� wfs (FST x) ��� ���br. RTC tstep x (FST y,br)` 107THEN1 ( SRW_TAC [][] THEN RES_TAC THEN 108 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [] ) THEN 109HO_MATCH_MP_TAC RTC_INDUCT THEN 110SRW_TAC [][] THEN1 ( 111 Q.EXISTS_TAC `SND x` THEN SRW_TAC [][] ) THEN 112Q.MATCH_ASSUM_RENAME_TAC `istep a b` THEN 113MAP_EVERY Cases_on [`a`,`b`] THEN 114Q.MATCH_ASSUM_RENAME_TAC `istep (sl,bl) (si,bi)` THEN 115Q.MATCH_ASSUM_RENAME_TAC `tstep^* (si,bi) (FST sr,br)` THEN 116FULL_SIMP_TAC (srw_ss()) [istep_def] THEN 117SRW_TAC [][] THEN1 ( 118 Q.EXISTS_TAC `br` THEN 119 Q.MATCH_ABBREV_TAC `RTC tstep pi pr` THEN 120 Q_TAC SUFF_TAC `tstep pi (si,bi)` 121 THEN1 METIS_TAC [RTC_RULES] THEN 122 SRW_TAC [][tstep_def,Abbr`pi`] ) 123THEN1 ( 124 Q.EXISTS_TAC `br` THEN 125 Q.MATCH_ABBREV_TAC `RTC tstep pi pr` THEN 126 Q_TAC SUFF_TAC `tstep pi (si,bi)` 127 THEN1 METIS_TAC [RTC_RULES] THEN 128 SRW_TAC [][tstep_def,Abbr`pi`] THEN 129 DISJ2_TAC THEN DISJ1_TAC THEN 130 MAP_EVERY Q.EXISTS_TAC [`Pair t1a t1d`,`Pair t2a t2d`,`t1a`,`t1d`,`t2a`,`t2d`] THEN 131 132val tstep_if_unify = Q.store_thm( 133"tstep_if_unify", 134`wfs s ��� (unify s t1 t2 = SOME sx) ��� tstep^+ (s,b+{|(t1,t2)|}) (sx,b)`, 135MAP_EVERY Q.ID_SPEC_TAC [`b`,`sx`,`t2`,`t1`,`s`] THEN 136HO_MATCH_MP_TAC unify_ind THEN 137SRW_TAC [][] THEN 138POP_ASSUM MP_TAC THEN 139ASM_SIMP_TAC (srw_ss()) [Once unify_def] THEN 140Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN SRW_TAC [][] 141THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def]) 142THEN1 ( 143 MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def] THEN 144 DISJ2_TAC THEN 145 MAP_EVERY Q.EXISTS_TAC [`n`,`Var n'`] THEN 146 SRW_TAC [][] THEN 147 Q.PAT_ASSUM `walk s X = Var n'` MP_TAC THEN 148 Cases_on `t2` THEN SRW_TAC [][] THEN 149 IMP_RES_TAC vwalk_to_var THEN 150 SRW_TAC [][NOT_FDOM_vwalk]) 151THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def]) 152THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def]) 153THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def]) 154THEN1 ( 155 Q.PAT_ASSUM `X = SOME sx` ASSUME_TAC THEN 156 Q.PAT_ASSUM `wfs s` ASSUME_TAC THEN 157 Cases_on `unify s t t'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 158 `wfs x` by METIS_TAC [unify_uP,uP_def] THEN 159 FULL_SIMP_TAC (srw_ss()) [] THEN 160 FIRST_X_ASSUM (Q.SPEC_THEN `b+{|(t0,t0')|}` STRIP_ASSUME_TAC) THEN 161 FIRST_X_ASSUM (Q.SPEC_THEN `b` STRIP_ASSUME_TAC) THEN 162 Q.PAT_ASSUM `TC tstep X (x,Y)` MP_TAC THEN 163 Q.MATCH_ABBREV_TAC `TC tstep p2 (x,Y) ��� TC tstep p1 (sx,b)` THEN 164 STRIP_TAC THEN Q_TAC SUFF_TAC `tstep p1 p2` 165 THEN1 METIS_TAC [TC_RULES] THEN 166 SRW_TAC [][tstep_def,Abbr`p2`,Abbr`p1`,Abbr`Y`] THEN 167 DISJ2_TAC THEN DISJ1_TAC THEN 168 MAP_EVERY Q.EXISTS_TAC [`t1`,`t2`,`t`,`t0`,`t'`,`t0'`] THEN 169 SRW_TAC [][ASSOC_BAG_UNION,BAG_INSERT_UNION] THEN 170 METIS_TAC [COMM_BAG_UNION,ASSOC_BAG_UNION] ) 171THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def]) 172THEN1 (MATCH_MP_TAC TC_SUBSET THEN SRW_TAC [][tstep_def]) 173); 174*) 175 176(* 177"unify_if_tstep", 178`tstep^+ (s,{|(t1,t2)|}) (sx,{||}) ��� ���su. (unify s t1 t2 = SOME su) ��� relate sx and su` 179*) 180 181(* The above is more like Urban's paper. The below is following "Term rewriting 182and all that" by Baader and Nipkow. It's messier because of the explicit orient 183step and because the idempotent substitution is supposed to be read off the 184solved form of the state when no reductions are possible. 185val istep_def = Define` 186 istep f el er = 187 (���c. er + {|(Const c, Const c)|} = el) ��� 188 (���t1a t1d t2a t2d. 189 er + {|(Pair t1a t1d, Pair t2a t2d)|} = {|(t1a,t2a); (t1d,t2d)|} + el) ��� 190 (���v t. 191 (���u. t ��� Var u) ��� 192 (er + {|(t,Var v)|} = {|(Var v,t)|} + el)) ��� 193 (���v t. 194 (Var v, t) <: el ��� 195 v ��� vars t ��� 196 �� BAG_EVERY el (��(t1,t2) v ��� vars t1 ��� v ��� vars t2) ��� 197 (er = {|(Var v, t)|} + BAG_IMAGE (el - (Var v, t)) (��(t1,t2). ((FEMPTY|+(v,t)) ��� t1, (FEMPTY|+(v,t)) ��� t2))))`; 198 199val tstep_def = Define` 200 tstep f (sl,el) (sr,er) = 201 (���t1 t2 c. 202 (walk sl t1 = Const c) ��� 203 (walk sl t2 = Const c) ��� 204 (er + {|(t1,t2)|} = el) ��� 205 (sr = sl)) ��� 206 (���t1 t2 t1a t1d t2a t2d. 207 (walk sl t1 = Pair t1a t1d) ��� 208 (walk sl t2 = Pair t2a t2d) ��� 209 (er + {|(t1,t2)|} = {|(t1a,t2a); (t1d,t2d)|} + el) ��� 210 (sr = sl)) ��� 211 (���t1 t2 v t. 212 (walk sl t1 = t) ��� 213 (walk sl t2 = Var v) ��� 214 (���u. t ��� Var u) ��� 215 (er + {|(t1,t2)|} = {|(Var v,t)|} + el) ��� 216 (sr = sl)) ��� 217 (���t1 t2 v t. 218 (walk sl t1 = Var v) ��� 219 (walk sl t2 = t) ��� 220 �� oc sl v t ��� 221 (er + {|(t1,t2)|} = el) ��� 222 (sr = sl |+ (v,t)))`; 223*) 224 225val _ = export_theory (); 226