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
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% FILE: list_imec_tactics.ml %
% EDITOR: Paul Curzon %
% DATE: July 1991 %
% DESCRIPTION: Some tactics and conversion for rewriting equalities and %
% inequalities of naturals %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% File: list_imec_tactics.ml %
% %
% Author: Wim Ploegaerts %
% %
% Organization: Imec vzw. %
% Kapeldreef 75 %
% 3030 Leuven, Belgium %
% %
% Date: 14-6-1990 %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%< several "translation" conversions >%
%< The same as for integers >%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
let (NUM_LESS_EQ_PLUS_CONV, NUM_EQ_PLUS_CONV, NUM_LESS_PLUS_CONV) =
letrec PROTECT_GSPEC tml th =
let wl,w = dest_thm th in
if is_forall w then
let tm = fst(dest_forall w) in
let tm' = (mem tm tml) => (genvar (type_of tm)) | tm in
PROTECT_GSPEC tml (SPEC tm' th)
else th
in let PROTECT_PART_MATCH tml partfn th =
let pth = PROTECT_GSPEC tml (GEN_ALL th) in
let pat = partfn(concl pth) in
let matchfn = match pat in
\tm. INST_TY_TERM (matchfn tm) pth
in let PROTECT_REWRITE_CONV tml =
set_fail_prefix `PROTECT_REWRITE_CONV`
(PROTECT_PART_MATCH tml (fst o dest_eq))
in let NUM_TRANSLATION_LEQ_EQ =
((GENL ["p:num";"m:num";"n:num"])
o SYM o SPEC_ALL) LESS_EQ_MONO_ADD_EQ
in let NUM_TRANSLATION_LESS_EQ =
((GENL ["p:num";"m:num";"n:num"])
o SYM o SPEC_ALL) LESS_MONO_ADD_EQ
in let NUM_TRANSLATION_EQ_EQ =
((GENL ["p:num";"m:num";"n:num"])
o SYM o SPEC_ALL) EQ_MONO_ADD_EQ
in
((\t. PROTECT_REWRITE_CONV []
(SPEC t NUM_TRANSLATION_LEQ_EQ)),
(\t. PROTECT_REWRITE_CONV []
(SPEC t NUM_TRANSLATION_EQ_EQ)),
(\t. PROTECT_REWRITE_CONV []
(SPEC t NUM_TRANSLATION_LESS_EQ)));;
|
