1open HolKernel boolLib bossLib Parse finite_mapTheory relationTheory termTheory substTheory alistTheory arithmeticTheory pred_setTheory rich_listTheory listTheory ramanaLib 2 3val _ = new_theory "walk" 4val _ = metisTools.limit := { time = NONE, infs = SOME 1 } 5 6fun vwalk_wfs_hyp th = 7let val th = 8 Q.INST [`R` |-> `vR s`] th 9in 10 foldl (fn (h,th) => PROVE_HYP h th) th 11 (map 12 (UNDISCH o (fn t => prove (``wfs s ==> ^t``, SRW_TAC [] [wfs_def,vR_def]))) 13 (hyp th)) 14end 15 16val vwalk_def = save_thm("vwalk_def",vwalk_wfs_hyp 17(TotalDefn.xDefineSchema "pre_vwalk" 18 `vwalk v = 19 case FLOOKUP s v of 20 SOME (Var u) => vwalk u 21 | SOME t => t 22 | NONE => Var v`) |> DISCH_ALL) 23val vwalk_ind = save_thm("vwalk_ind",vwalk_wfs_hyp (theorem "pre_vwalk_ind")) 24 25val _ = store_term_thm("vwalk_def_print", 26TermWithCase` 27 wfs s ��� 28 (vwalk s v = 29 case FLOOKUP s v of 30 SOME (Var u) => vwalk s u 31 | SOME t => t 32 | NONE => Var v)`) 33 34val NOT_FDOM_vwalk = Q.store_thm( 35 "NOT_FDOM_vwalk", 36 `wfs s /\ v NOTIN FDOM s ==> (vwalk s v = Var v)`, 37 SRW_TAC [] [Once vwalk_def, FLOOKUP_DEF]); 38 39val vwalk_to_var = Q.store_thm( 40 "vwalk_to_var", 41 `wfs s ==> !v u. (vwalk s v = Var u) ==> u NOTIN FDOM s`, 42 DISCH_TAC THEN HO_MATCH_MP_TAC vwalk_ind THEN 43 SRW_TAC [][] THEN 44 Cases_on `FLOOKUP s v` THEN1 45 (REPEAT (POP_ASSUM MP_TAC) THEN 46 REPEAT (SRW_TAC [][Once vwalk_def, FLOOKUP_DEF])) THEN 47 `?w.x = Var w` 48 by (Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [Once (UNDISCH vwalk_def)]) THEN 49 FIRST_X_ASSUM (Q.SPEC_THEN `w` MP_TAC) THEN SRW_TAC [][] THEN 50 `vwalk s w = Var u` by (REPEAT (POP_ASSUM MP_TAC) THEN 51 SRW_TAC [] [Once vwalk_def] THEN 52 FULL_SIMP_TAC (srw_ss()) []) THEN 53 FIRST_X_ASSUM (Q.SPEC_THEN `u` MP_TAC) THEN SRW_TAC [][]); 54 55val walk_def = Define` 56 walk s t = case t of Var v => vwalk s v | t => t`; 57 58val walk_thm = RWstore_thm( 59"walk_thm", 60`(walk s (Var v) = vwalk s v) /\ 61 (walk s (Pair t1 t2) = (Pair t1 t2)) /\ 62 (walk s (Const c) = (Const c))`, 63SRW_TAC [][walk_def]); 64 65val walk_FEMPTY = RWstore_thm( 66"walk_FEMPTY", 67`(walk FEMPTY t = t) /\ 68 (vwalk FEMPTY v = Var v)`, 69Cases_on `t` THEN NTAC 2 (SRW_TAC [][Once(DISCH_ALL vwalk_def)])); 70 71val walk_var_vwalk = Q.store_thm( 72"walk_var_vwalk", 73`wfs s ==> (walk s t = Var v) 74 ==> ?u.(t = Var u) /\ (vwalk s u = Var v)`, 75SRW_TAC [][walk_def] THEN 76Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) []); 77 78val walk_to_var = Q.store_thm( 79"walk_to_var", 80`wfs s /\ (walk s t = Var v) ==> 81 v NOTIN FDOM s /\ ?u.(t = Var u)`, 82Cases_on `t` THEN SRW_TAC [][] THEN 83METIS_TAC [vwalk_to_var]); 84 85val vwalk_vR = Q.store_thm( 86"vwalk_vR", 87`wfs s ==> !v u. u IN vars (vwalk s v) /\ vwalk s v <> Var v ==> 88 (vR s)^+ u v`, 89DISCH_TAC THEN HO_MATCH_MP_TAC vwalk_ind THEN SRW_TAC [][] THEN 90`(FLOOKUP s v = NONE) \/ ?t. FLOOKUP s v = SOME t` 91 by (Cases_on `FLOOKUP s v` THEN SRW_TAC [][]) THEN1 92(`vwalk s v = Var v` by (ONCE_REWRITE_TAC [UNDISCH vwalk_def] THEN 93 SRW_TAC [][])) THEN 94Cases_on `t` THENL [ 95 `vwalk s v = vwalk s n` by (SRW_TAC [][Once vwalk_def]) THEN 96 `vR s n v` by SRW_TAC [][vR_def] THEN 97 Cases_on `vwalk s n = Var n` THENL [ 98 `u = n` by FULL_SIMP_TAC (srw_ss()) [] THEN 99 SRW_TAC [][TC_SUBSET], 100 `(vR s)^+ u n` by METIS_TAC [] THEN 101 MATCH_MP_TAC 102 (GEN_ALL (CONJUNCT2 (SPEC_ALL TC_RULES))) THEN 103 METIS_TAC [TC_SUBSET] 104 ], 105 `vwalk s v = Pair t' t0` by (SRW_TAC [][Once vwalk_def]) THEN 106 MATCH_MP_TAC TC_SUBSET THEN 107 SRW_TAC [][vR_def] THEN FULL_SIMP_TAC (srw_ss()) [], 108 Q.MATCH_ASSUM_RENAME_TAC `FLOOKUP s v = SOME (Const c)` THEN 109 `vwalk s v = Const c` by (SRW_TAC [] [Once vwalk_def]) THEN 110 FULL_SIMP_TAC (srw_ss()) [] 111]); 112 113val vwalk_IN_FRANGE = Q.store_thm( 114"vwalk_IN_FRANGE", 115`wfs s ��� v ��� FDOM s ��� vwalk s v ��� FRANGE s`, 116SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN 117STRIP_TAC THEN Q.ID_SPEC_TAC `v` THEN 118HO_MATCH_MP_TAC vwalk_ind THEN SRW_TAC [][] THEN 119SRW_TAC [][Once vwalk_def] THEN 120FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN 121Cases_on `s ' v` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 122 Cases_on `n ��� FDOM s` THEN SRW_TAC [][NOT_FDOM_vwalk], 123 ALL_TAC, ALL_TAC ] THEN 124SRW_TAC [][FRANGE_DEF] THEN METIS_TAC []); 125 126val walk_IN_FRANGE = Q.store_thm( 127"walk_IN_FRANGE", 128`wfs s ��� walk s t ��� t ��� walk s t ��� FRANGE s`, 129Cases_on `t` THEN SRW_TAC [][] THEN 130`n ��� FDOM s` by METIS_TAC [NOT_FDOM_vwalk] THEN 131SRW_TAC [][vwalk_IN_FRANGE]); 132 133val vwalk_SUBMAP = Q.store_thm( 134"vwalk_SUBMAP", 135`wfs sx ==> !v s.s SUBMAP sx ==> 136 (case vwalk s v of Var u => (vwalk sx v = vwalk sx u) 137 | t => (vwalk sx v = t))`, 138STRIP_TAC THEN HO_MATCH_MP_TAC (Q.INST[`s`|->`sx`]vwalk_ind) THEN 139SRW_TAC [][] THEN 140`wfs s` by METIS_TAC [wfs_SUBMAP] THEN 141POP_ASSUM MP_TAC THEN 142SIMP_TAC (srw_ss())[Once vwalk_def] THEN 143Cases_on `FLOOKUP s v` THEN SRW_TAC [][] THEN 144Cases_on `x` THEN SRW_TAC [][] THENL [ 145 `FLOOKUP sx v = SOME (Var n)` 146 by METIS_TAC [FLOOKUP_SUBMAP] THEN 147 `vwalk sx v = vwalk sx n` 148 by SRW_TAC [][Once (DISCH_ALL vwalk_def), SimpLHS] THEN 149 METIS_TAC [], 150 `FLOOKUP sx v = SOME (Pair t t0)` by METIS_TAC [FLOOKUP_SUBMAP] THEN 151 SRW_TAC [][Once (DISCH_ALL vwalk_def)], 152 Q.MATCH_ASSUM_RENAME_TAC `FLOOKUP s v = SOME (Const c)` THEN 153 `FLOOKUP sx v = SOME (Const c)` by METIS_TAC [FLOOKUP_SUBMAP] THEN 154 SRW_TAC [][Once (DISCH_ALL vwalk_def)] 155]); 156 157val vwalk_no_cycles = store_thm("vwalk_no_cycles", 158 ``wfs s ��� ���v u. (vwalk s v = Var u) ��� v ��� FDOM s ��� (v ��� u)``, 159 strip_tac >> 160 HO_MATCH_MP_TAC vwalk_ind >> 161 rw[FLOOKUP_DEF] >> 162 Cases_on`v ��� FDOM s` >> rw[] >> 163 rw[Once vwalk_def,FLOOKUP_DEF] >> 164 Cases_on`s ' v` >> rw[] >> 165 spose_not_then strip_assume_tac >> 166 qspecl_then[`n`,`v`]mp_tac(UNDISCH vwalk_vR)>> 167 simp[] >> 168 Cases_on`v=n`>>fs[]>> 169 spose_not_then strip_assume_tac >> 170 `(vR s)^+ v v` by ( 171 match_mp_tac (CONJUNCT2(SPEC_ALL(TC_RULES))) >> 172 qexists_tac`n` >> simp[] >> 173 match_mp_tac TC_SUBSET >> 174 simp[vR_def,FLOOKUP_DEF] ) >> 175 METIS_TAC[wfs_no_cycles]) 176 177(* vwalk with concrete alists *) 178 179val _ = overload_on("vwalk_al", ``��al. vwalk (alist_to_fmap al)``); 180val _ = overload_on("vwalk_al", ``vwalk_al``); 181 182val vwalk_al_thm = Q.store_thm( 183"vwalk_al_thm", 184`wfs (alist_to_fmap al) ==> 185 (vwalk_al al v = 186 case ALOOKUP al v of 187 NONE => Var v | 188 SOME (Var u) => vwalk_al al u | 189 SOME t => t)`, 190METIS_TAC [fmap_to_alist_to_fmap,vwalk_def,ALOOKUP_EQ_FLOOKUP]); 191 192val vwalk_al_eq_vwalk = Q.store_thm( 193"vwalk_al_eq_vwalk", 194`vwalk s = vwalk_al (fmap_to_alist s)`, 195METIS_TAC [fmap_to_alist_to_fmap]); 196 197(* vwalk with rhs check *) 198 199val vwalk_rhs_q = ` 200 (vwalk_rhs s [] v = Var v) ��� 201 (vwalk_rhs s ((x,Var u)::t) v = 202 if u = v then Var v 203 else if x = v then vwalk_rhs s s u 204 else vwalk_rhs s t v) ��� 205 (vwalk_rhs s ((x,y)::t) v = 206 if x = v then y 207 else vwalk_rhs s t v)`; 208 209val ELENGTH_def = Define` 210 (ELENGTH (v, []) = 0) ��� 211 (ELENGTH (v, (h::t)) = if SND h = Var v then 0 else 1 + ELENGTH (v, t))`; 212val _ = export_rewrites ["ELENGTH_def"]; 213 214val vwalk_rhsR_q = ` 215 inv_image 216 (measure (��b. if b then 0 else 1) LEX 217 measure ELENGTH LEX measure LENGTH) 218 (��(s0,s1,v). ((���pr. (s0 = pr ++ s1) ��� 219 ���e. MEM e pr ��� FST e ��� v ��� SND e ��� Var v), 220 (v, s0), s1))`; 221 222val vwalk_rhs_def = tDefine "vwalk_rhs" vwalk_rhs_q 223(WF_REL_TAC vwalk_rhsR_q THEN 224SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 225SRW_TAC [][] THEN RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 226Induct_on `pr` THEN SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] THEN 227Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 228METIS_TAC []); 229 230val _ = store_term_thm("vwalk_rhsR", Term vwalk_rhsR_q); 231val _ = store_term_thm("vwalk_rhs_defn_print", Term vwalk_rhs_q); 232 233val vwalk_rhs_ind = theorem "vwalk_rhs_ind"; 234 235open lcsymtacs 236 237val example1 = Q.prove( 238`(y ��� x) ��� (vwalk_al [(y,Var x);(x,Const c)] x = Const c)`, 239strip_tac >> 240Q.MATCH_ABBREV_TAC `vwalk_al s x = Const c` >> 241`wfs (alist_to_fmap s)` by ( 242 srw_tac [][wfs_no_cycles] >> 243 SPOSE_NOT_THEN STRIP_ASSUME_TAC >> 244 imp_res_tac TC_CASES1_E >> 245 full_simp_tac (srw_ss()) [vR_def] >> 246 full_simp_tac std_ss [GSYM (CONJUNCT1 ALOOKUP_EQ_FLOOKUP)] >> 247 full_simp_tac (srw_ss()) [Abbr`s`] >- ( 248 Cases_on `y = v` >> full_simp_tac (srw_ss()) [] >> 249 Cases_on `x = v` >> full_simp_tac (srw_ss()) [] ) >> 250 Cases_on `y = y'` >> full_simp_tac (srw_ss()) [] >> srw_tac [][] >- ( 251 POP_ASSUM (K ALL_TAC) >> 252 imp_res_tac TC_CASES2_E >> 253 full_simp_tac (srw_ss()) [vR_def] >> 254 fsrw_tac [][FLOOKUP_UPDATE] >> pop_assum mp_tac >> srw_tac [][] ) >> 255 Cases_on `x = y'` >> full_simp_tac (srw_ss()) [] ) >> 256srw_tac [][Once vwalk_al_thm] >> 257srw_tac [][Abbr`s`]) 258 259val example2 = Q.prove( 260`(y ��� x) ��� (vwalk_rhs [(y,Var x);(x,Const c)] [(y,Var x);(x,Const c)] x = Var x)`, 261srw_tac [][Once vwalk_rhs_def]) 262 263val vwalk_rhs_ALOOKUP_NONE = Q.store_thm( 264"vwalk_rhs_ALOOKUP_NONE", 265`���a0 al v. (ALOOKUP al v = NONE) ��� (vwalk_rhs a0 al v = Var v)`, 266ho_match_mp_tac vwalk_rhs_ind >> srw_tac [][vwalk_rhs_def]) 267 268(* 269val vwalk_rhs_ALOOKUP_SOME_nonvar = Q.store_thm( 270"vwalk_rhs_ALOOKUP_SOME_nonvar", 271`���al a0 v t. (ALOOKUP al v = SOME t) ��� (���u. t ��� Var u) ��� (vwalk_rhs a0 al v = t)`, 272Induct >> srw_tac [][] >> 273Cases_on `h` >> Cases_on `r` >> srw_tac [][vwalk_rhs_def] 274ho_match_mp_tac vwalk_rhs_ind >> 275srw_tac [][] >> 276srw_tac [][vwalk_rhs_def] >> 277Cases_on `t` >> srw_tac [][] 278FALSE 279 280val submaps_def = RWDefine` 281 (submaps [] = T) ��� 282 (submaps ((x,Var v)::t) = v ��� set (MAP FST t) ��� submaps t) ��� 283 (submaps (h::t) = submaps t)`; THIS IS PROBABLY WRONG 284 285val submaps_thm = Q.store_thm( 286"submaps_thm", 287`submaps al ��� ���l1 l2. (al = l1 ++ l2) ��� (alist_to_fmap l2) SUBMAP (alist_to_fmap al)`, 288Induct_on `al` >> srw_tac [][] >> 289Cases_on `h` >> Cases_on `r` >> srw_tac [][] >- ( 290 srw_tac [][EQ_IMP_THM] >- ( 291 Cases_on `l1` >> full_simp_tac (srw_ss()) [] >> 292 srw_tac [][] >> 293 POP_ASSUM (Q.SPECL_THEN [`t`,`l2`] mp_tac) >> 294 srw_tac [][] >> 295 match_mp_tac SUBMAP_TRANS >> 296 qexists_tac `alist_to_fmap (t ++ l2)` >> srw_tac [][] >> 297 Q.MATCH_ABBREV_TAC `f SUBMAP g` >> 298 qsuff_tac `!k v. (FLOOKUP f k = SOME v) ��� (FLOOKUP g k = SOME v)` >- ( 299 srw_tac [][FLOOKUP_DEF,SUBMAP_DEF] ) >> 300 srw_tac [][Abbr`g`,Abbr`f`,GSYM (CONJUNCT1 ALOOKUP_EQ_FLOOKUP)] 301 302val vwalk_rhs_eq_vwalk_al = Q.store_thm( 303"vwalk_rhs_eq_vwalk" 304`wfs (alist_to_fmap al) ��� submaps al ��� (vwalk_rhs al al v = vwalk_al al v)` 305*) 306 307val _ = export_theory (); 308