1structure jrhUtils :> jrhUtils= 2struct 3 4(* Standard libs *) 5open HolKernel boolLib liteLib numLib reduceLib 6 pairTheory prim_recTheory numTheory arithmeticTheory; 7 8infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 9 10 11val ERR = mk_HOL_ERR "jrhUtils"; 12 13(*---------------------------------------------------------------------------*) 14(* Various utilities useful in building the theories. *) 15(*---------------------------------------------------------------------------*) 16 17fun HALF_MK_ABS qth = 18 let val (x,body) = dest_forall (concl qth) 19 val t = rhs body 20 val gv = genvar (type_of x) 21 val tfun = mk_abs(x,t) in 22 EXT (GEN gv (* |- !gv. u gv =< (\x.t) gv *) 23 (TRANS (SPEC gv qth) 24 (SYM (BETA_CONV (mk_comb(tfun,gv)))))) end; 25 26 27 28(*===========================================================================*) 29(* Various useful tactics, conversions etc. *) 30(*===========================================================================*) 31 32(*---------------------------------------------------------------------------*) 33(* Proves tautologies: handy for propositional lemmas *) 34(*---------------------------------------------------------------------------*) 35 36val TAUT_CONV = tautLib.TAUT_PROVE; 37 38(*---------------------------------------------------------------------------*) 39(* More concise way to get an AC rewrite lemma *) 40(*---------------------------------------------------------------------------*) 41 42fun AC thp tm = EQT_ELIM(AC_CONV thp tm); 43 44(*---------------------------------------------------------------------------*) 45(* GEN_PAIR_TAC - Like GEN_TAC but "pairs" the relevant variable *) 46(*---------------------------------------------------------------------------*) 47 48val GEN_PAIR_TAC = 49 W(curry op THEN GEN_TAC o SUBST1_TAC o SYM o 50 C ISPEC PAIR o fst o dest_forall o snd); 51 52(*---------------------------------------------------------------------------*) 53(* MK_COMB_TAC - reduces ?- f x = g y to ?- f = g and ?- x = y *) 54(*---------------------------------------------------------------------------*) 55 56fun MK_COMB_TAC (asl,w) = 57 let val (l,r) = dest_eq w 58 val (l1,l2) = dest_comb l 59 val (r1,r2) = dest_comb r in 60 ([(asl,mk_eq(l1,r1)), (asl,mk_eq(l2,r2))],end_itlist (curry MK_COMB)) end; 61 62 63(*---------------------------------------------------------------------------*) 64(* BINOP_TAC - reduces "$op x y = $op u v" to "x = u" and "y = v" *) 65(*---------------------------------------------------------------------------*) 66 67val BINOP_TAC = MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC]; 68 69(*---------------------------------------------------------------------------*) 70(* SYM_CANON_CONV - Canonicalizes single application of symmetric operator *) 71(* Rewrites "so as to make f true", e.g. fn = $<< or fn = curry$= "1" o fst *) 72(*---------------------------------------------------------------------------*) 73 74fun SYM_CANON_CONV sym f = 75 REWR_CONV sym o assert (op not o f o ((snd o dest_comb) ## I) o dest_comb); 76 77(*---------------------------------------------------------------------------*) 78(* IMP_SUBST_TAC - Implicational substitution for deepest matchable term *) 79(*---------------------------------------------------------------------------*) 80 81fun IMP_SUBST_TAC th (asl,w) = 82 case (sort free_in 83 (find_terms (can (PART_MATCH (lhs o snd o dest_imp) th)) w)) 84 of [] => raise ERR "IMP_SUBST_TAC" "" 85 | tm1::_ => 86 let val th1 = PART_MATCH (lhs o snd o dest_imp) th tm1 87 val (a,conseq) = dest_imp (concl th1) 88 val (l,r) = dest_eq conseq 89 val gv = genvar (type_of l) 90 val pat = subst[l |-> gv] w 91 in 92 ([(asl,a), (asl,subst[gv |-> r] pat)], 93 fn [t1,t2] => SUBST[gv |-> SYM(MP th1 t1)] pat t2 94 | _ => raise ERR "IMP_SUBST_TAC" "") 95 end; 96 97(*---------------------------------------------------------------------------*) 98(* Tactic to introduce an abbreviation *) 99(* *) 100(* N.B. Just "ABBREV_TAC = CHOOSE_TAC o DEF_EXISTS_RULE" doesn't work if RHS *) 101(* has free variables. *) 102(*---------------------------------------------------------------------------*) 103 104fun ABBREV_TAC tm = 105 let val (v,t) = dest_eq tm in 106 CHOOSE_THEN (fn th => SUBST_ALL_TAC th THEN ASSUME_TAC th) 107 (EXISTS(mk_exists(v,mk_eq(t,v)),t) (REFL t)) end; 108 109(*---------------------------------------------------------------*) 110(* EXT_CONV "!x. f x = g x" = |- (!x. f x = g x) = (f = g) *) 111(*---------------------------------------------------------------*) 112 113val EXT_CONV = SYM o uncurry X_FUN_EQ_CONV o 114 (I ## (mk_eq o (rator ## rator) o dest_eq)) o dest_forall; 115 116(*---------------------------------------------------------------------------*) 117(* (\x. s[x]) = (\y. t[y]) *) 118(* ========================= ABS_TAC *) 119(* s[x] = t[x] *) 120(*---------------------------------------------------------------------------*) 121 122fun ABS_TAC (asl,w) = 123 let val (l,r) = dest_eq w 124 val (v1,b1) = dest_abs l 125 val (v2,b2) = dest_abs r 126 val v = variant (free_varsl (w::asl)) v1 127 val subg = mk_eq(subst[v1 |-> v] b1,subst[v2 |-> v] b2) in 128 ([(asl,subg)],CONV_RULE(LAND_CONV(ALPHA_CONV v1)) o 129 CONV_RULE(RAND_CONV(ALPHA_CONV v2)) o ABS v o hd) end; 130 131(*---------------------------------------------------------------------------*) 132(* EQUAL_TAC - Strip down to unequal core (usually too enthusiastic) *) 133(*---------------------------------------------------------------------------*) 134 135val EQUAL_TAC = REPEAT(FIRST [AP_TERM_TAC, AP_THM_TAC, ABS_TAC]); 136 137(*---------------------------------------------------------------------------*) 138(* X_BETA_CONV "v" "tm[v]" = |- tm[v] = (\v. tm[v]) v *) 139(*---------------------------------------------------------------------------*) 140 141fun X_BETA_CONV v tm = SYM(BETA_CONV(mk_comb(mk_abs(v,tm),v))); 142 143(*---------------------------------------------------------------------------*) 144(* EXACT_CONV - Rewrite with theorem matching exactly one in a list *) 145(*---------------------------------------------------------------------------*) 146 147val EXACT_CONV = 148 ONCE_DEPTH_CONV o FIRST_CONV o 149 map (fn t => K t o assert(aconv (lhs(concl t)))); 150 151(*---------------------------------------------------------------------------*) 152(* Rather ad-hoc higher-order fiddling conversion *) 153(* |- (\x. f t1[x] ... tn[x]) = (\x. f ((\x. t1[x]) x) ... ((\x. tn[x]) x)) *) 154(*---------------------------------------------------------------------------*) 155 156fun HABS_CONV tm = 157 let val (v,bod) = dest_abs tm 158 val (hop,pl) = strip_comb bod 159 val eql = rev(map (X_BETA_CONV v) pl) in 160 ABS v (itlist (C(curry MK_COMB)) eql (REFL hop)) end; 161 162 163(*---------------------------------------------------------------------------*) 164(* Expand an abbreviation *) 165(*---------------------------------------------------------------------------*) 166 167fun EXPAND_TAC s = FIRST_ASSUM(SUBST1_TAC o SYM o 168 assert(curry op = s o fst o dest_var o rhs o concl)) THEN BETA_TAC; 169 170 171(*--------------------------------------------------------------------------- 172 * Added by Konrad, to make his life easier when installing the rewriting 173 * upgrade 27.7.94. 174 *---------------------------------------------------------------------------*) 175 176val GEN_REWR_TAC = Lib.C Rewrite.GEN_REWRITE_TAC Rewrite.empty_rewrites; 177 178end 179