/usr/share/hol88-2.02.19940316/ml/rewrite.ml is in hol88-source 2.02.19940316-28.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 | %=============================================================================%
% HOL 88 Version 2.0 %
% %
% FILE NAME: rewrite.ml %
% %
% DESCRIPTION: Simple rewriting rules and tactics for HOL %
% %
% USES FILES: basic-hol lisp files, bool.th, genfns.ml, hol-syn.ml, %
% hol-rule.ml, hol-drule.ml, drul.ml, tacticals.ml, %
% conv.ml, hol-net.ml %
% %
% University of Cambridge %
% Hardware Verification Group %
% Computer Laboratory %
% New Museums Site %
% Pembroke Street %
% Cambridge CB2 3QG %
% England %
% %
% COPYRIGHT: University of Edinburgh %
% COPYRIGHT: University of Cambridge %
% COPYRIGHT: INRIA %
% %
% REVISION HISTORY: (none) %
%=============================================================================%
% --------------------------------------------------------------------- %
% Must be compiled in the presence of the hol parser/pretty printer %
% This loads genfns.ml and hol-syn.ml too. %
% Also load hol-rule.ml, hol-drule.ml, drul.ml, tacticals.ml, etc %
% --------------------------------------------------------------------- %
if compiling then (loadf `ml/hol-in-out`;
loadf `ml/hol-rule`;
loadf `ml/hol-drule`;
loadf `ml/drul`;
loadf `ml/tacticals`;
loadf `ml/conv`;
loadf `ml/hol-net`);;
% ===================================================================== %
% Section for defining mk_conv_net [TFM 91.03.17] %
% ===================================================================== %
begin_section mk_conv_net;;
% --------------------------------------------------------------------- %
% Redundant GEN_ALL/SPEC_ALL combinations resulting from applying %
% mk_conv_net to mk_rewrite eliminated as was done by Konrad Slind in %
% HOL90 [JG 92.04.24] %
% --------------------------------------------------------------------- %
% --------------------------------------------------------------------- %
% mk_rewrites: split a theorem into a list of theorems suitable for %
% rewriting by doing: %
% %
% 1. Specialize all variables (SPEC_ALL). %
% %
% 2. Then do the following: %
% %
% |- t1 /\ t2 --> [|- t1 ; |- t2] %
% |- t1 <=> t2 --> [|- t1=t2] %
% %
% 3. Then |- t --> |- t = T and |- ~t --> |- t = F %
% %
% iff case deleted [TFM 91.01.20] %
% optimized [TFM 91.03.17] %
% --------------------------------------------------------------------- %
letrec mk_rewrites th =
(let thm = SPEC_ALL th in
let t = concl thm in
if is_eq t
then [thm] else
if is_conj t then
let (c1,c2) = CONJ_PAIR thm in (mk_rewrites c1 @ mk_rewrites c2) else
if is_neg t then [EQF_INTRO thm]
else [EQT_INTRO thm]) ? failwith `mk_rewrites`;;
% --------------------------------------------------------------------- %
% [th1; ... ; thn] --> (mk_rewrites th1) @ ... @ (mk_rewrites thn) %
% --------------------------------------------------------------------- %
let mk_rewritesl thl = itlist (append o mk_rewrites ) thl [];;
% --------------------------------------------------------------------- %
% Inefficient ML implementation of nets as lists of pairs: %
% %
% let enter_term(t,x)n = (t,x).n %
% and lookup_term n t = %
% mapfilter(\(t',x).if can(match t)t' then x else fail) %
% and nil_term_net = []:(term#*)list;; %
% --------------------------------------------------------------------- %
% --------------------------------------------------------------------- %
% Build a conv net from a list of theorems %
% --------------------------------------------------------------------- %
let mk_conv_net thl =
itlist
enter_term
(map (\th. (lhs(concl th),REWR_CONV th)) (mk_rewritesl thl))
nil_term_net;;
% --------------------------------------------------------------------- %
% Export mk_conv_net outside of section. %
% --------------------------------------------------------------------- %
mk_conv_net;;
end_section mk_conv_net;;
let mk_conv_net = it;;
% ===================================================================== %
% List of basic rewrites (temporarily made assignable to enable %
% experimental changes to be quickly made) %
% ===================================================================== %
% |- !t. (!x.t) = t %
let FORALL_SIMP =
let t = "t:bool"
and x = "x:*"
in
GEN t (IMP_ANTISYM_RULE
(DISCH "!^x.^t" (SPEC x (ASSUME "!^x.^t")))
(DISCH t (GEN x (ASSUME t))));;
% |- !t. (?x.t) = t %
let EXISTS_SIMP =
let t = "t:bool"
and x = "x:*"
in
GEN t (IMP_ANTISYM_RULE
(DISCH "?^x.^t" (CHOOSE("p:*", ASSUME"?^x.^t")(ASSUME t)))
(DISCH t (EXISTS("?^x.^t", "r:*")(ASSUME t))));;
% |- !t1 t2. (\x. t1)t2 = t1 %
let ABS_SIMP = GEN_ALL(BETA_CONV "(\x:*.(t1:**))t2");;
let basic_rewrites =
[REFL_CLAUSE;
EQ_CLAUSES;
NOT_CLAUSES;
AND_CLAUSES;
OR_CLAUSES;
IMP_CLAUSES;
COND_CLAUSES;
% IFF_EQ; |- !t1 t2. (t1<=>t2) = (t1=t2) DELETED [TFM 91.01.20] %
FORALL_SIMP;
EXISTS_SIMP;
ABS_SIMP;
PAIR;
FST;
SND
];;
% ===================================================================== %
% Main rewriting conversion %
% ===================================================================== %
let GEN_REWRITE_CONV =
let RW_CONV net = \tm. FIRST_CONV (lookup_term net tm) tm in
\(rewrite_fun:conv->conv) built_in_rewrites.
let basic_net = mk_conv_net built_in_rewrites in
\thl. rewrite_fun
(RW_CONV (merge_term_nets (mk_conv_net thl) basic_net));;
% --------------------------------------------------------------------- %
% Rewriting conversions. %
% %
% Modified to use special versions of the depth conversions. %
% [RJB 94.02.15] %
% --------------------------------------------------------------------- %
let PURE_REWRITE_CONV = GEN_REWRITE_CONV REW_DEPTH_CONV []
and REWRITE_CONV = GEN_REWRITE_CONV REW_DEPTH_CONV basic_rewrites
and PURE_ONCE_REWRITE_CONV = GEN_REWRITE_CONV ONCE_REW_DEPTH_CONV []
and ONCE_REWRITE_CONV = GEN_REWRITE_CONV ONCE_REW_DEPTH_CONV basic_rewrites;;
%====================================================================== %
% Main rewriting rule %
% OLD version: %
% %
% let GEN_REWRITE_RULE = %
% let REWRITE_CONV net = \tm. FIRST_CONV (lookup_term net tm) tm in %
% \rewrite_fun built_in_rewrites. %
% let basic_net = mk_conv_net built_in_rewrites in %
% \thl. let conv = rewrite_fun %
% (REWRITE_CONV(merge_term_nets (mk_conv_net thl) %
% basic_net)) in %
% \th. EQ_MP (conv (concl th)) th;; %
% %
% New version rewritten using the new GEN_REWRITE_CONV [JG 92.04.07] %
% The code is most simply expressed as follows: %
% %
% let GEN_REWRITE_RULE rewrite_fun built_in_rewrites thl = %
% CONV_RULE (GEN_REWRITE_CONV rewrite_fun built_in_rewrites thl) ;; %
% %
% However, it is optimised below so that the built_in_rewrites gets %
% made into a conv net at compile time. %
% %
% Futher optimized 13.5.93 by JVT to remove the function composition %
% to enhance speed. %
% %
% OLD VERSION: %
% %
% let GEN_REWRITE_RULE rewrite_fun built_in_rewrites = %
% let REWL_CONV = GEN_REWRITE_CONV rewrite_fun built_in_rewrites in %
% CONV_RULE o REWL_CONV ;; %
%====================================================================== %
let GEN_REWRITE_RULE rewrite_fun built_in_rewrites =
let REWL_CONV = GEN_REWRITE_CONV rewrite_fun built_in_rewrites in
\tm. (CONV_RULE (REWL_CONV tm));;
% --------------------------------------------------------------------- %
% Rewriting rules. %
% %
% Modified to use special versions of the depth conversions. %
% [RJB 94.02.15] %
% --------------------------------------------------------------------- %
let PURE_REWRITE_RULE = GEN_REWRITE_RULE REW_DEPTH_CONV []
and REWRITE_RULE = GEN_REWRITE_RULE REW_DEPTH_CONV basic_rewrites
and PURE_ONCE_REWRITE_RULE = GEN_REWRITE_RULE ONCE_REW_DEPTH_CONV []
and ONCE_REWRITE_RULE = GEN_REWRITE_RULE ONCE_REW_DEPTH_CONV
basic_rewrites;;
% --------------------------------------------------------------------- %
% Rewrite a theorem with the help of its assumptions %
% --------------------------------------------------------------------- %
let PURE_ASM_REWRITE_RULE thl th =
PURE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th
and ASM_REWRITE_RULE thl th =
REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th
and PURE_ONCE_ASM_REWRITE_RULE thl th =
PURE_ONCE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th
and ONCE_ASM_REWRITE_RULE thl th =
ONCE_REWRITE_RULE ((map ASSUME (hyp th)) @ thl) th;;
% --------------------------------------------------------------------- %
% Rules that rewrite using those assumptions that satisfy a predicate %
% --------------------------------------------------------------------- %
let FILTER_PURE_ASM_REWRITE_RULE f thl th =
PURE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
and FILTER_ASM_REWRITE_RULE f thl th =
REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
and FILTER_PURE_ONCE_ASM_REWRITE_RULE f thl th =
PURE_ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th
and FILTER_ONCE_ASM_REWRITE_RULE f thl th =
ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th;;
%====================================================================== %
% Main rewriting tactic %
% OLD version: %
% %
% let GEN_REWRITE_TAC = %
% let REWRITE_CONV net = \tm. FIRST_CONV (lookup_term net tm) tm in %
% \rewrite_fun built_in_rewrites. %
% let basic_net = mk_conv_net built_in_rewrites in %
% \thl.let conv = rewrite_fun %
% (REWRITE_CONV(merge_term_nets (mk_conv_net thl) %
% basic_net)) in %
% \(A,t):goal. let th = conv t in %
% let (),right = dest_eq(concl th) in %
% if right="T" %
% then ([], \[]. EQ_MP (SYM th) TRUTH) %
% else ([A,right], \[th']. EQ_MP (SYM th) th');; %
% %
% New version rewritten using the new GEN_REWRITE_CONV [JG 92.04.07] %
% The code is most simply expressed as follows: %
% %
% let GEN_REWRITE_TAC rewrite_fun built_in_rewrites thl = %
% CONV_TAC (GEN_REWRITE_CONV rewrite_fun built_in_rewrites thl) ;; %
% %
% However, it is optimised below so that the built_in_rewrites gets %
% made into a conv net at compile time. %
% %
% Futher optimized 13.5.93 by JVT to remove the function composition %
% to enhance speed. %
% %
% OLD VERSION: %
% %
% let GEN_REWRITE_TAC rewrite_fun built_in_rewrites = %
% let REWL_CONV = GEN_REWRITE_CONV rewrite_fun built_in_rewrites in %
% CONV_TAC o REWL_CONV ;; %
%====================================================================== %
let GEN_REWRITE_TAC rewrite_fun built_in_rewrites =
let REWL_CONV = GEN_REWRITE_CONV rewrite_fun built_in_rewrites in
\tm. (CONV_TAC (REWL_CONV tm));;
% --------------------------------------------------------------------- %
% Rewriting tactics. %
% %
% Modified to use special versions of the depth conversions. %
% [RJB 94.02.15] %
% --------------------------------------------------------------------- %
let PURE_REWRITE_TAC = GEN_REWRITE_TAC REW_DEPTH_CONV []
and REWRITE_TAC = GEN_REWRITE_TAC REW_DEPTH_CONV basic_rewrites
and PURE_ONCE_REWRITE_TAC = GEN_REWRITE_TAC ONCE_REW_DEPTH_CONV []
and ONCE_REWRITE_TAC = GEN_REWRITE_TAC ONCE_REW_DEPTH_CONV
basic_rewrites;;
% --------------------------------------------------------------------- %
% Rewrite a goal with the help of its assumptions %
% --------------------------------------------------------------------- %
let PURE_ASM_REWRITE_TAC thl =
ASSUM_LIST (\asl. PURE_REWRITE_TAC (asl @ thl))
and ASM_REWRITE_TAC thl =
ASSUM_LIST (\asl. REWRITE_TAC (asl @ thl))
and PURE_ONCE_ASM_REWRITE_TAC thl =
ASSUM_LIST (\asl. PURE_ONCE_REWRITE_TAC (asl @ thl))
and ONCE_ASM_REWRITE_TAC thl =
ASSUM_LIST (\asl. ONCE_REWRITE_TAC (asl @ thl));;
% --------------------------------------------------------------------- %
% Tactics that rewrite using those assumptions that satisfy a predicate %
% --------------------------------------------------------------------- %
let FILTER_PURE_ASM_REWRITE_TAC f thl =
ASSUM_LIST (\asl. PURE_REWRITE_TAC ((filter (f o concl) asl) @ thl))
and FILTER_ASM_REWRITE_TAC f thl =
ASSUM_LIST (\asl. REWRITE_TAC ((filter (f o concl) asl) @ thl))
and FILTER_PURE_ONCE_ASM_REWRITE_TAC f thl =
ASSUM_LIST (\asl. PURE_ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl))
and FILTER_ONCE_ASM_REWRITE_TAC f thl =
ASSUM_LIST (\asl. ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl));;
% --------------------------------------------------------------------- %
% Search a sub-term of t matching u %
% --------------------------------------------------------------------- %
let find_match u =
letrec find_mt t =
(match u t
? find_mt(rator t)
? find_mt(rand t)
? find_mt(snd(dest_abs t))
? failwith `find_match`)
in
find_mt;;
%
SUBST_MATCH (|-u=v) th searches for an instance of u in
(the conclusion of) th and then substitutes the corresponding
instance of v. Much faster than rewriting.
%
let SUBST_MATCH eqth th =
let tm_inst,ty_inst = find_match (lhs(concl eqth)) (concl th)
in
SUBS [INST tm_inst (INST_TYPE ty_inst eqth)] th;;
% Possible further simplifications:
|- !t. ((\x.t1) t2) = t1
|- !t P. (!x. t /\ P x) = (t /\ (!x. P x))
| !x:*. (@x'.x'=x) = x
|- !t1 t2 t3. (t1\/t2) ==> t3 = (t1==>t3) /\ (t2==>t3)
|- !t1 t2 t3. (t1\/t2) /\ t3 = (t1/\t3) \/ (t2/\t3)
|- !t1 t2 t3. t3 /\ (t1\/t2) = (t3/\t1) \/ (t3/\t2)
|- !t P. (?x.P x) ==> t = !x'.(P x' ==> t)
|- !t P. (?x.P x) /\ t = ?x'.(P x' /\ t)
|- !t P. t /\ (?x.P x) = ?x'.(t /\ P x')
|- !t1 t2. (t1<=>t2) = (t1==>t2 /\ t2==>t1)
%
|