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