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