1structure pairTools :> pairTools = 2struct 3 4open HolKernel Parse boolLib pairSyntax pairTheory PairRules; 5 6val PERR = mk_HOL_ERR "pairTools"; 7 8(* recursively expand variables with pair type *) 9local 10 val name_of = fst o dest_var 11 fun rename_tac v1 v2 = 12 FULL_STRUCT_CASES_TAC 13 (EXISTS (mk_exists(v2,(mk_eq(v1,v2))),v1) (REFL v1)) 14 fun split_tac p a d = 15 FULL_STRUCT_CASES_TAC 16 (CONV_RULE (RENAME_VARS_CONV [name_of a, name_of d]) 17 (ISPEC p pair_CASES)) 18 fun PairCases_common v fvs g = let 19 val mk_var = variant fvs o mk_var 20 val (sv,ty) = dest_var v 21 val n = let val n = ref 0 in fn()=> !n before n := !n+1 end 22 fun split_tacs v tya tyd = let 23 fun try_split s ty = let 24 val v = mk_var((name_of v)^s,ty) 25 in (v, 26 case total dest_prod ty of 27 NONE => 28 (fn()=> rename_tac v (mk_var(sv^(Int.toString(n())),ty))) 29 | SOME (tya, tyd) => 30 (fn()=> split_tacs v tya tyd)) 31 end 32 val (va,ka) = try_split "a" tya 33 val (vd,kd) = try_split "d" tyd 34 in 35 split_tac v va vd 36 THEN ka() THEN kd() 37 end 38 in 39 case total dest_prod (type_of v) of 40 NONE => raise PERR "PairCases_on" "Not of pair type" 41 | SOME (tya, tyd) => split_tacs v tya tyd 42 end g 43in 44 fun PairCases (g as (hyps, w)) = let 45 val fvs = free_varsl (w::hyps) 46 val (v, _) = dest_forall w 47 (* From gen_tac: *) 48 val v' = gen_variant Parse.is_constname "" fvs v 49 in 50 X_GEN_TAC v' THEN PairCases_common v' fvs 51 end g 52 53 fun PairCases_on q (g as (hyps, w)) = let 54 val fvs = free_varsl (w::hyps) 55 val v = parse_in_context fvs q 56 in 57 if is_var v then 58 PairCases_common v fvs g 59 else 60 raise PERR "PairCases_on" "Not a variable" 61 end 62end 63 64(*--------------------------------------------------------------------------- 65 * 66 * (x = (v1,...,vn)) |- M[(v1,...,vn)] 67 * --------------------------------------------- 68 * ?v1 ... vn. x = (v1,...,vn) |- M[x] 69 * 70 *---------------------------------------------------------------------------*) 71 72fun VSTRUCT_ABS bind th = 73 let fun CHOOSER v (tm,thm) = 74 let val ex_tm = mk_exists(v,tm) 75 in (ex_tm, CHOOSE(v, ASSUME ex_tm) thm) 76 end 77 val L = strip_pair (rand bind) 78 in snd(itlist CHOOSER L (bind, SUBS[SYM(ASSUME bind)] th)) 79 end; 80 81 82(*--------------------------------------------------------------------------- 83 * 84 * `x` `<varstruct>` 85 * -------------------------------- 86 * |- ?v1..vn. x = <varstruct> 87 * 88 *---------------------------------------------------------------------------*) 89 90local val pthm = GSYM pairTheory.PAIR 91in 92fun PAIR_EX x vstruct = 93 let fun pair_exists node value thm = 94 if Term.is_var value 95 then EXISTS (mk_exists(value,subst[node|->value] (concl thm)), node) thm 96 else 97 let val (V,(l,r)) = (I##dest_eq)(strip_exists(concl thm)) 98 val v = genvar(type_of node) 99 val template = list_mk_exists(V,mk_eq(l, subst[node|->v] r)) 100 val expansion = ISPEC node pthm 101 val pthm' = Thm.SUBST[v |-> expansion] template thm 102 val (node1, node2) = dest_pair(rhs(concl expansion)) 103 val (value1,value2) = dest_pair value 104 in pair_exists node1 value1 (pair_exists node2 value2 pthm') 105 end 106 handle HOL_ERR _ => raise PERR "PAIR_EX" "" 107 in 108 pair_exists x vstruct (REFL x) 109 end 110end 111 112 113 114(*--------------------------------------------------------------------------- 115 * Generalize a free tuple (vstr) into a universally quantified variable (a). 116 * There must be a faster way! Note however that the notion of "freeness" for 117 * a tuple is different than for a variable: if variables in the tuple also 118 * occur in any other place than an occurrences of the tuple, they aren't 119 * "free" (which is thus probably the wrong word to use). 120 *---------------------------------------------------------------------------*) 121 122fun PGEN a vstr th = 123 GEN a (if is_var vstr 124 then Thm.INST [vstr |-> a] th 125 else PROVE_HYP (PAIR_EX a vstr) (VSTRUCT_ABS (mk_eq(a,vstr)) th)) 126 127fun PGEN_TAC vars (asl:Term.term list,tm) = 128 let val (v,_) = dest_forall tm 129 val tm' = beta_conv(mk_comb(rand tm,vars)) 130 in 131 ([(asl,tm')], fn [th] => PGEN v vars th 132 | _ => raise PERR "PGEN_TAC" "validation") 133 end; 134 135(*--------------------------------------------------------------------------- 136 |- f <vstr> = g <vstr> 137 ------------------------ PFUN_EQ_RULE 138 |- f = g 139 ---------------------------------------------------------------------------*) 140 141local val expected = PERR "PFUN_EQ_RULE" "expected f <vstruct> = g <vstruct>" 142 val SIMP = Rewrite.PURE_ONCE_REWRITE_RULE[GSYM FUN_EQ_THM] 143in 144fun PFUN_EQ_RULE th = 145 let val ((_,v1),(_,v2)) 146 = with_exn ((dest_comb##dest_comb) o dest_eq o concl) th expected 147 in 148 if aconv v1 v2 then SIMP (PGEN (genvar (type_of v1)) v1 th) 149 else raise expected 150 end 151end; 152 153 154(*---------------------------------------------------------------------------* 155 * v (|- !v_1...v_n. M[v_1...v_n]) * 156 * TUPLE ------------------------------------------------- * 157 * !v. M[FST v, FST(SND v), ... SND(SND ... v)] * 158 *---------------------------------------------------------------------------*) 159 160local fun trav tm A = 161 trav (mk_fst tm) (trav (mk_snd tm) A) handle HOL_ERR _ => (tm::A) 162 fun hd1 [th] = th 163 | hd1 _ = raise Bind 164in 165fun TUPLE v thm = GEN v (SPECL (trav v []) thm) 166 167fun TUPLE_TAC vtuple:tactic = fn (asl,w) => 168 let val (Bvar,Body) = dest_forall w 169 val w1 = subst [Bvar |-> vtuple] Body 170 val w2 = list_mk_forall(strip_pair vtuple,w1) 171 in ([(asl,w2)], 172 PURE_REWRITE_RULE[pairTheory.PAIR] o TUPLE Bvar o hd1) 173 end 174end; 175 176 177(*--------------------------------------------------------------------------- 178 * Builds a list of projection terms for "rhs", based on structure 179 * of "tuple". 180 181 fun flat_vstruct0 tuple rhs = 182 if (is_var tuple) then [rhs] 183 else let val {fst,snd} = dest_pair tuple 184 in flat_vstruct0 fst (mk_fst rhs) @ 185 flat_vstruct0 snd (mk_snd rhs) 186 end; 187 188 * That was the clean implementation. Now for the one that gets used, we 189 * add an extra field to the return value, so that it can be made into 190 * an equality. 191 *---------------------------------------------------------------------------*) 192 193fun flat_vstruct tuple rhs = 194 let 195 (* behaviour of mk_fst and mk_snd should match PairedLambda.GEN_BETA_CONV in LET_INTRO *) 196 val mk_fst = fn tm => if is_pair tm then #1 (dest_pair tm) else mk_fst tm 197 val mk_snd = fn tm => if is_pair tm then #2 (dest_pair tm) else mk_snd tm 198 fun flat tuple (v,rhs) = 199 if is_var tuple then [(tuple, rhs)] 200 else let val (fst,snd) = dest_pair tuple 201 in flat fst (v, mk_fst rhs) @ 202 flat snd (v, mk_snd rhs) 203 end 204 in map mk_eq (flat tuple (genvar alpha,rhs)) 205 end; 206 207 208(*--------------------------------------------------------------------------- 209 * 210 * Gamma |- (<vstruct> = M) ==> N 211 * -------------------------------------------------- 212 * Gamma |- let <vstruct> = M in N 213 * 214 *---------------------------------------------------------------------------*) 215 216local val LET_THM1 = GSYM LET_THM 217 val PAIR_RW = PURE_REWRITE_RULE [pairTheory.PAIR] 218 fun lhs_repl th = (lhs(concl th) |-> th) 219in 220fun LET_INTRO thm = 221 let val (ant,conseq) = dest_imp(concl thm) 222 val (lhs,rhs) = dest_eq ant 223 val bindings = flat_vstruct lhs rhs 224 val thl = map ASSUME bindings 225 val th0 = UNDISCH thm 226 val th1 = SUBS thl th0 227 val Bredex = mk_comb(mk_pabs(lhs,conseq),rhs) 228 val th2 = EQ_MP (GSYM(PairedLambda.GEN_BETA_CONV Bredex)) th1 229 val th3 = PURE_ONCE_REWRITE_RULE[LET_THM1] th2 230 val vstruct_thm = SUBST_CONV (map lhs_repl thl) lhs lhs; 231 val th4 = PROVE_HYP (PAIR_RW vstruct_thm) th3 232 in 233 rev_itlist (fn bind => fn th => 234 let val th' = DISCH bind th 235 val (lhs,rhs) = dest_eq bind 236 in MP (Thm.INST [lhs |-> rhs] th') (REFL rhs) end) 237 bindings th4 238 end 239end; 240 241 242(*--------------------------------------------------------------------------- 243 * Returns the variants and the "away" list augmented with the variants. 244 *---------------------------------------------------------------------------*) 245 246fun unpabs tm = 247 let val (vstr,body) = dest_pabs tm 248 val V = free_vars_lr vstr 249 in list_mk_abs(V,body) 250 end; 251 252 253local 254fun dot 0 vstr tm away = (vstr,tm) 255 | dot n vstr tm away = 256 let val (Bvar,Body) = dest_abs tm 257 val v' = variant away Bvar 258 val tm' = beta_conv(mk_comb(tm, v')) 259 val vstr' = subst[Bvar |-> v'] vstr 260 in dot (n-1) vstr' tm' (v'::away) 261 end 262in 263(*--------------------------------------------------------------------------- 264 * Alpha convert to ensure that variables bound by the "let" are not 265 * free in the assumptions of the goal. Alpha-convert in reverse on way 266 * back from achieving the goal. 267 *---------------------------------------------------------------------------*) 268 269val LET_INTRO_TAC :tactic = 270fn (asl,w) => 271 let val (func,arg) = dest_let w 272 val func' = unpabs func 273 val (vstr,body) = dest_pabs func 274 val away0 = Lib.op_union aconv (free_vars func) (free_varsl asl) 275 val (vstr', body') = dot (length (free_vars vstr)) vstr func' away0 276 val bind = mk_eq(vstr', arg) 277 in 278 ([(asl,mk_imp(bind,body'))], 279 fn ths => let val let_thm = LET_INTRO (hd ths) 280 in EQ_MP (ALPHA (concl let_thm) w) let_thm end) 281 end 282end; 283 284(*--------------------------------------------------------------------------- 285 * Test. 286 * 287 set_goal([Term`x:bool`, Term`x':bool`], 288 Term`let (x':bool,(x:bool)) = M in x'' x x' : bool`); 289 * 290 * 291 * g`!P x M N. (!x. x=M ==> P(N x)) ==> P(let (x = M) in N)`; 292 * 293 *---------------------------------------------------------------------------*) 294 295 296fun LET_EQ_TAC thml = 297 Ho_Rewrite.PURE_REWRITE_TAC thml 298 THEN REPEAT (LET_INTRO_TAC THEN DISCH_TAC); 299 300(*--------------------------------------------------------------------------- 301 * Eliminate PABS 302 * 303 304 ----------------------------------- PABS_ELIM_CONV (\<vstr>. P vstr) 305 |- \<vstr>. P <vstr> = \x. P x 306 * 307 *---------------------------------------------------------------------------*) 308 309local 310 fun UNCURRY_ELIM_CONV t = 311 ((REWR_CONV ELIM_UNCURRY) THENC 312 (ABS_CONV ( 313 RATOR_CONV ( 314 ((RATOR_CONV UNCURRY_ELIM_CONV) THENC 315 BETA_CONV THENC 316 UNCURRY_ELIM_CONV)) THENC 317 BETA_CONV))) t 318 handle HOL_ERR _ => raise UNCHANGED; 319in 320 321fun PABS_ELIM_CONV t = 322 if (pairSyntax.is_pabs t) then (UNCURRY_ELIM_CONV t) else raise UNCHANGED; 323 324end 325 326 327(*--------------------------------------------------------------------------- 328 * Introduces PABS 329 * 330 331 ----------------------------------- PABS_ELIM_CONV <vstr> (\x. P x) 332 |- \x. P x = \<vstr>. P vstr 333 * 334 *---------------------------------------------------------------------------*) 335 336fun PABS_INTRO_CONV vstruct tt = let 337 val (vstruct', _) = variant_of_term (free_vars tt) vstruct 338 val new_t = mk_comb (tt, vstruct') 339 val thm0 = (BETA_CONV THENC 340 REWRITE_CONV[pairTheory.FST, pairTheory.SND]) new_t 341 342 val thm1 = PairRules.PABS vstruct' thm0 343 val thm2 = CONV_RULE (LHS_CONV PairRules.PETA_CONV) thm1 344in 345 thm2 346end; 347 348(*--------------------------------------------------------------------------- 349 Eliminate tupled quantification 350 351 ----------------------------------- TUPLED_QUANT_CONV `<Q><vstr>. P` 352 |- <Q><vstr>. P = <Q> v1 ... vn. P 353 354 where <Q> is one of {?,!} and <vstruct> is a varstruct made 355 from the variables v1,...,vn. 356 ---------------------------------------------------------------------------*) 357 358 359val is_uncurry_tm = same_const pairSyntax.uncurry_tm 360val is_universal = same_const boolSyntax.universal 361val is_existential = same_const boolSyntax.existential; 362 363local 364 val ELIM_PEXISTS2 = prove (``(?p:('a#'b). P (FST p) (SND p) p) = ?p1 p2. P p1 p2 (p1,p2)``, 365 CONV_TAC (LHS_CONV (HO_REWR_CONV EXISTS_PROD)) THEN 366 REWRITE_TAC[FST, SND]) 367 val ELIM_PFORALL2 = prove (``(!p:('a#'b). P (FST p) (SND p) p) = !p1 p2. P p1 p2 (p1,p2)``, 368 CONV_TAC (LHS_CONV (HO_REWR_CONV FORALL_PROD)) THEN 369 REWRITE_TAC[FST, SND]); 370 371 val ELIM_PEXISTS_CONV = HO_REWR_CONV ELIM_PEXISTS2; 372 val ELIM_PFORALL_CONV = HO_REWR_CONV ELIM_PFORALL2; 373 374 fun dest_tupled_quant tm = 375 case total dest_comb tm 376 of NONE => NONE 377 | SOME(f,x) => 378 if is_comb x andalso is_uncurry_tm (rator x) 379 then if is_existential f then SOME ELIM_PEXISTS_CONV else 380 if is_universal f then SOME ELIM_PFORALL_CONV 381 else NONE 382 else NONE 383 384 fun PQUANT_ELIM_CONV quant_elim vc = 385 if (is_var vc) then (RAND_CONV (ALPHA_CONV vc)) else 386 let 387 val (vc1, vc2) = pairSyntax.dest_pair vc; 388 val conv = (quant_elim THENC 389 (QUANT_CONV (PQUANT_ELIM_CONV quant_elim vc2)) THENC 390 (PQUANT_ELIM_CONV quant_elim vc1)); 391 in 392 conv 393 end; 394in 395 fun ELIM_TUPLED_QUANT_CONV tm = 396 case dest_tupled_quant tm 397 of NONE => raise PERR "TUPLED_QUANT_CONV" "" 398 | SOME (quant_elim) => 399 ((RAND_CONV PABS_ELIM_CONV) THENC 400 PQUANT_ELIM_CONV quant_elim (fst (dest_pabs(rand tm)))) tm 401 402 fun SPLIT_QUANT_CONV vc tm = 403 let 404 val quant_elim = 405 if is_universal (rator tm) then ELIM_PFORALL_CONV else 406 if is_existential (rator tm) then ELIM_PEXISTS_CONV else 407 raise PERR "SPLIT_QUANT_CONV" "" 408 val (v, _) = dest_abs (rand tm) handle HOL_ERR _ => raise PERR "SPLIT_QUANT_CONV" "" 409 val _ = if (type_of vc = type_of v) then () else raise PERR "SPLIT_QUANT_CONV" ""; 410 in 411 PQUANT_ELIM_CONV quant_elim vc tm 412 end; 413end; 414 415 416 417local 418 val PFORALL_THM2 = prove ( 419 ``!P:'a->'b->bool. (!x. $! (P x)) = $! (UNCURRY P)``, 420 GEN_TAC THEN 421 Q.SUBGOAL_THEN `P = (\x y. P x y)` 422 (fn thm => ONCE_ASM_REWRITE_TAC [thm]) 423 THEN1 (REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC[]) THEN 424 BETA_TAC THEN REWRITE_TAC [PFORALL_THM]); 425 426 val PEXISTS_THM2 = prove ( 427 ``!P:'a->'b->bool. (?x. $? (P x)) = $? (UNCURRY P)``, 428 GEN_TAC THEN 429 Q.SUBGOAL_THEN `P = (\x y. P x y)` 430 (fn thm => ONCE_ASM_REWRITE_TAC [thm]) 431 THEN1 (REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC[]) THEN 432 BETA_TAC THEN REWRITE_TAC [PEXISTS_THM]); 433in 434 fun PEXISTS_INTRO_CONV tm = 435 (((TRY_CONV ELIM_TUPLED_QUANT_CONV) THENC 436 (QUANT_CONV PEXISTS_INTRO_CONV) THENC 437 (HO_REWR_CONV PEXISTS_THM2)) tm) handle HOL_ERR _ => raise UNCHANGED 438 439 fun PFORALL_INTRO_CONV tm = 440 (((TRY_CONV ELIM_TUPLED_QUANT_CONV) THENC 441 (QUANT_CONV PFORALL_INTRO_CONV) THENC 442 (HO_REWR_CONV PFORALL_THM2)) tm) handle HOL_ERR _ => raise UNCHANGED 443 444 fun INTRO_TUPLED_QUANT_CONV tm = 445 if is_universal (rator tm) then PFORALL_INTRO_CONV tm else 446 if is_existential (rator tm) then PEXISTS_INTRO_CONV tm else 447 raise PERR "INTRO_TUPLED_QUANT_CONV" "" 448end; 449 450 451end 452