1structure reductionEval :> reductionEval = 2struct 3 4open HolKernel Parse boolLib simpLib Traverse BasicProvers 5open chap3Theory normal_orderTheory termSyntax 6 7structure Parse = struct 8val (Type,Term) = parse_from_grammars normal_orderTheory.normal_order_grammars 9end 10 11fun ERR f msg = mk_HOL_ERR "reductionEval" f msg 12val betastar_t = ``(-b->*)`` 13val normorderstar_t = ``(-n->*)`` 14val beta_t = ``(-b->)`` 15val normorder_t = ``(-n->)`` 16val lameq_t = ``(==) : term -> term -> bool`` 17 18fun rtc_po t = let 19 open relationTheory Travrules 20 infix |> fun x |> f = f x 21 fun rwt th = th |> REWRITE_RULE [reflexive_def, transitive_def] 22 |> ISPEC t 23in 24 mk_preorder (rwt transitive_RTC, rwt reflexive_RTC) 25end 26 27val [lameq_beta,lameq_refl,lameq_sym,lameq_trans, 28 lameq_APPl, lameq_APPr, lameq_LAM] = CONJUNCTS chap2Theory.lameq_rules 29 30val lameq_APPcong = chap2Theory.lameq_app_cong 31 32val lameq_po = let 33 open relationTheory Travrules 34in 35 mk_preorder (lameq_trans, lameq_refl) 36end 37 38fun dest_binop t = let 39 val (fx,y) = dest_comb t 40 val (f,x) = dest_comb fx 41in 42 (f,x,y) 43end 44 45 46val betastar_po = rtc_po beta_t 47val normstar_po = rtc_po ``(-n->)`` 48 49val equality_po = let 50 open Travrules 51 val TRAVRULES {relations,...} = EQ_tr 52in 53 hd relations 54end 55 56 57(* ---------------------------------------------------------------------- 58 A reducer for beta-reduction. 59 ---------------------------------------------------------------------- *) 60 61 62val congs = [lameq_APPcong, SPEC_ALL lameq_LAM, 63 chap2Theory.Yf_cong, 64 REWRITE_RULE [GSYM AND_IMP_INTRO] 65 (last (CONJUNCTS chap2Theory.lemma2_12))] 66 67val user_rewrites = ref (SSFRAG {dprocs = [], ac = [], rewrs = [], 68 congs = [], filter = NONE, 69 name = SOME "betasimps", convs = []}) 70fun add_rwts (ths : (KernelSig.kernelname * thm) list) = 71 user_rewrites := 72 simpLib.merge_ss [!user_rewrites, simpLib.rewrites (map #2 ths)] 73 74open chap2Theory head_reductionTheory 75val BETA_rsd = {refl = GEN_ALL lameq_refl, trans = lameq_trans, 76 weakenings = [lameq_weaken_cong, lameq_has_bnf_cong, 77 lameq_bnf_of_cong], 78 subsets = [ccbeta_lameq, betastar_lameq, whstar_lameq, 79 normorder_lameq, nstar_lameq], 80 rewrs = [lameq_S, lameq_K, lameq_I, lameq_C, 81 lameq_B, lameq_beta]} 82 83val BETA_CONG_ss = 84 SSFRAG {dprocs = [], ac = [], rewrs = [], congs = congs, filter = NONE, 85 name = NONE, convs = []} 86val BETA_RWTS_ss = rewrites [termTheory.lemma14b, 87 normal_orderTheory.nstar_betastar_bnf, 88 betastar_lameq_bnf, lameq_refl] 89 90val BETA_ss = 91 simpLib.merge_ss [relsimp_ss BETA_rsd, BETA_CONG_ss, BETA_RWTS_ss] 92 93fun betafy ss = 94 simpLib.add_relsimp BETA_rsd ss ++ BETA_RWTS_ss ++ 95 !user_rewrites ++ BETA_CONG_ss 96fun bsrw_ss() = betafy(srw_ss()) 97 98val {export = export_betarwt,...} = 99 ThmSetData.new_exporter { 100 settype = "betasimp", 101 efns = {add = (fn {named_thm,...} => add_rwts [named_thm]), 102 remove = (fn _ => ())} 103 } 104fun bstore_thm (trip as (n,t,tac)) = store_thm trip before export_betarwt n 105 106(* ---------------------------------------------------------------------- 107 A reducer for weak head reduction. 108 ---------------------------------------------------------------------- *) 109 110fun whfy ss = let 111 open relationTheory head_reductionTheory termTheory 112 val congs = [wh_app_congL, whstar_substitutive] 113in 114 add_relsimp {refl = RTC_REFL 115 |> INST_TYPE [alpha |-> termSyntax.term_ty] 116 |> Q.INST [`R` |-> `(-w->)`] 117 |> Q.GEN `x`, 118 trans = transitive_RTC 119 |> REWRITE_RULE [transitive_def] 120 |> Q.ISPEC `(-w->)`, 121 weakenings = [wh_weaken_cong], 122 subsets = [], 123 rewrs = [MATCH_MP RTC_SINGLE 124 (SPEC_ALL (CONJUNCT1 weak_head_rules))]} ss ++ 125 SSFRAG {dprocs = [], ac = [], 126 rewrs = [(SOME {Thy = "term", Name = "lemma14b"}, lemma14b), 127 (SOME {Thy = "head_reduction", Name = "bnf_whnf"},bnf_whnf)], 128 congs = congs, filter = NONE, name = NONE, convs = []} 129end 130 131(* ---------------------------------------------------------------------- 132 normorder_step 133 134 Given a term t of type ``:term``, try to deduce a normal order reduction 135 step, returning a thm looking like 136 137 |- t -n-> t' 138 139 raises a HOL_ERR if it can't do it. This may mean t is in bnf. 140 ---------------------------------------------------------------------- *) 141 142open termSyntax 143val [nbeta,nlam_cong,nleft,nright] = CONJUNCTS normorder_rules 144val is_abs_t = mk_thy_const{Thy = "chap2", Name = "is_abs", 145 Ty = term_ty --> bool} 146val bnf_t = mk_thy_const{Thy = "chap2", Name = "bnf", 147 Ty = term_ty --> bool} 148 149fun normorder_step solver t = let 150 val _ = Trace.trace (2, Trace.LZ_TEXT (fn () => "Attempting no1 on "^ 151 term_to_string t)) 152in 153 case total dest_APP t of 154 NONE => let 155 in 156 case total dest_LAM t of 157 NONE => raise ERR "normorder_step" "No visible reduction" 158 | SOME (v,bdy) => let 159 val subth = normorder_step solver bdy 160 in 161 MP (SPECL [v,bdy,rand(concl subth)] nlam_cong) subth 162 end 163 end 164 | SOME(M1,M2) => let 165 in 166 case total dest_LAM M1 of 167 NONE => let 168 val isnt_ABS_th = solver (mk_neg(mk_comb(is_abs_t,M1))) 169 in 170 case total (normorder_step solver) M1 of 171 NONE => let 172 val bnf_th = solver (mk_comb(bnf_t,M1)) 173 val subth = normorder_step solver M2 174 in 175 MP (SPECL [M1,M2,rand (concl subth)] nright) 176 (LIST_CONJ [subth,bnf_th,isnt_ABS_th]) 177 end 178 | SOME subth => 179 MP (SPECL [M1,rand(concl subth),M2] nleft) 180 (CONJ subth isnt_ABS_th) 181 end 182 | SOME(v,body) => SPECL [v,body,M2] nbeta 183 end 184end 185 186 187 188val [noredLAM, noredbeta, noredAPP, noredVAR] = CONJUNCTS noreduct_thm 189val noreduct_t = mk_thy_const{Name = "noreduct", Thy = "normal_order", 190 Ty = term_ty --> optionSyntax.mk_option term_ty} 191val (opmap_SOME,opmap_NONE) = CONJ_PAIR optionTheory.OPTION_MAP_DEF 192val Mv_t = mk_var("M", term_ty) 193val Nv_t = mk_var("N", term_ty) 194 195fun noreduct_CONV solver t = let 196 val (f,arg) = dest_comb t 197 val _ = same_const noreduct_t f orelse 198 raise ERR "noreduct_CONV" "Inapplicable" 199 fun recurse t = 200 case total dest_LAM t of 201 SOME (v, body) => let 202 val subth = recurse body 203 val c = REWR_CONV noredLAM THENC 204 RAND_CONV (K subth) THENC 205 FIRST_CONV [REWR_CONV opmap_SOME, REWR_CONV opmap_NONE] 206 in 207 c (mk_comb(noreduct_t, t)) 208 end 209 | NONE => let 210 in 211 case total dest_APP t of 212 NONE => if is_VAR t then REWR_CONV noredVAR (mk_comb(noreduct_t, t)) 213 else raise ERR "noreduct_CONV" "No good normorder reduct" 214 | SOME (M1, M2) => let 215 in 216 case total dest_LAM M1 of 217 SOME (v, body) => REWR_CONV noredbeta (mk_comb(noreduct_t, t)) 218 | NONE => let 219 val isnt_ABS = solver (mk_neg(mk_comb(is_abs_t, M1))) 220 val M1th = recurse M1 221 val eqn = MP (INST [Mv_t |-> M1, Nv_t |-> M2] noredAPP') 222 isnt_ABS 223 val c = REWRITE_CONV [optionTheory.option_case_def, 224 M1th] 225 val eqn' = CONV_RULE (RAND_CONV c) eqn 226 in 227 if is_comb (rand (concl M1th)) then 228 CONV_RULE (RAND_CONV BETA_CONV) eqn' 229 else let 230 val M2th = recurse M2 231 in 232 CONV_RULE 233 (RAND_CONV 234 (REWRITE_CONV [optionTheory.OPTION_MAP_DEF, 235 M2th])) 236 eqn' 237 end 238 end 239 end 240 end 241in 242 recurse arg 243end 244 245val nopath_t = prim_mk_const{Thy = "normal_order", Name = "nopath"} 246fun nopath_CONV solver t = let 247 val (f, x) = dest_comb t 248 val _ = aconv f nopath_t orelse raise ERR "nopath_CONV" "Inapplicable" 249 val subth = noreduct_CONV solver (mk_comb(noreduct_t, x)) 250in 251 REWR_CONV nopath_def THENC 252 REWRITE_CONV [subth, optionTheory.option_case_def] THENC 253 TRY_CONV BETA_CONV 254end t 255 256val bnf_imp_noreduct = GEN_ALL (#2 (EQ_IMP_RULE noreduct_bnf)) 257val nstar_imp_memnopath = GEN_ALL (#1 (EQ_IMP_RULE normstar_nopath)) 258fun normstar_filter (th,c) = 259 [(th,c), (EQT_INTRO (MATCH_MP bnf_imp_noreduct (EQT_ELIM th)),c)] 260 handle HOL_ERR _ => 261 [(th,c), (EQT_INTRO (MATCH_MP nstar_imp_memnopath (EQT_ELIM th)),c)] 262 handle HOL_ERR _ => [(th,c)] 263 264fun mngcnv cnv solver stack t = cnv (solver stack) t 265val NORMSTAR_ss = SSFRAG { 266 ac = [], congs = [], 267 convs = [{conv = mngcnv nopath_CONV, key = SOME([], mk_comb(nopath_t, Mv_t)), 268 name = "nopath_CONV", trace = 2}, 269 {conv = mngcnv noreduct_CONV, 270 key = SOME([], mk_comb(noreduct_t, Mv_t)), 271 name = "noreduct_CONV", trace = 2}], 272 filter = SOME normstar_filter, dprocs = [], name = SOME "NORMSTAR_ss", 273 rewrs = [(SOME{Thy = "normal_order", Name = "normstar_nopath"}, 274 normstar_nopath), 275 (SOME{Thy = "term", Name = "lemma14b"}, termTheory.lemma14b)]}; 276 277(* ---------------------------------------------------------------------- 278 unvarify_tac 279 280 Turns a goal of the form M -b->* N into one where free term variables 281 in N have turned into lambda-variables (i.e., HOL terms of the form 282 VAR s). This may put N into bnf, allowing the betastar reduction 283 congruence to fire. If the resulting goal is provable, so too was 284 the original because of substitutivity of beta-reduction. 285 ---------------------------------------------------------------------- *) 286 287fun goalnames (asl, w) = let 288 val fvs = FVL (w::asl) empty_tmset 289 fun foldthis(t,acc) = HOLset.add(acc, #1 (dest_var t)) 290in 291 HOLset.listItems (HOLset.foldl foldthis (HOLset.empty String.compare) fvs) 292end 293 294fun unvarify_tac th (w as (asl,g)) = let 295 val (f,x,y) = dest_binop g 296 val y_fvs = free_vars y 297 val y_fvs = filter (fn t => type_of t = term_ty) y_fvs 298 val (strs, sets) = 299 List.foldl binderLib.find_avoids (empty_tmset, empty_tmset) (g::asl) 300 val finite_sets = List.mapPartial (total pred_setSyntax.dest_finite) asl 301 fun filterthis t = not (is_var t) orelse tmem t finite_sets 302 val sets = List.filter filterthis (HOLset.listItems sets) 303 fun do_them (strs,sets) ys (w as (asl,g)) = 304 case ys of 305 [] => ALL_TAC w 306 | y::rest => let 307 val newname = Lexis.gen_variant Lexis.tmvar_vary 308 (goalnames w) 309 (#1 (dest_var y) ^ "s") 310 val sets = List.filter (fn t => rand t !~ y) sets 311 val new_tac = let 312 open pred_setSyntax 313 in 314 if null sets then 315 if HOLset.isEmpty strs then ALL_TAC 316 else let 317 val avoid_t = mk_set (HOLset.listItems strs) 318 in 319 binderLib.NEW_TAC newname avoid_t 320 end 321 else if HOLset.isEmpty strs then let 322 val avoid_t = List.foldl mk_union (hd sets) (tl sets) 323 in 324 binderLib.NEW_TAC newname avoid_t 325 end 326 else let 327 val base = mk_set (HOLset.listItems strs) 328 val avoid_t = List.foldl mk_union base sets 329 in 330 binderLib.NEW_TAC newname avoid_t 331 end 332 end 333 val newname_t = mk_var(newname, stringSyntax.string_ty) 334 val inst1 = [y |-> mk_comb(VAR_t, newname_t)] 335 val (_, M, N) = dest_binop g 336 val x'_base = Term.subst inst1 M 337 val y'_base = Term.subst inst1 N 338 val x' = list_mk_comb(SUB_t, [y,newname_t,x'_base]) 339 val y' = list_mk_comb(SUB_t, [y,newname_t,y'_base]) 340 val g' = list_mk_comb(f, [x',y']) 341 in 342 new_tac THEN SUBGOAL_THEN (mk_eq(g,g')) SUBST1_TAC THENL [ 343 ASM_SIMP_TAC (srw_ss()) [termTheory.lemma14b], 344 MATCH_MP_TAC th THEN 345 do_them (HOLset.add(strs,newname_t), sets) rest 346 ] 347 end w 348in 349 do_them (strs,sets) y_fvs 350end w 351 352 353end 354