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
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% FILE: minmax.ml %
% EDITOR: Paul Curzon %
% DATE: June 1991 %
% DESCRIPTION: Maximum and Minimum %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%********************************* HISTORY ********************************%
% %
% This file is part of the more_arithmetic theory in the bags library by %
% Philippe Leveilley %
% Conversion to HOL12 and editing was done by %
% Wim Ploegaerts %
% %
%****************************************************************************%
% %
% PC 21/4/93 %
% Removed dependencies on several external files/theories %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
system `rm -f min_max.th`;;
new_theory `min_max`;;
% PC 22-4-92 No longer used%
%loadf `tools`;;%
%============================================================================%
% %
% MIN AND MAX by PL %
% %
%============================================================================%
let MAX_DEF = new_definition
(`MAX_DEF`,
"MAX n p = ((n <= p) => p | n)"
);;
let MAX_0 = prove_thm
(`MAX_0`,
"!n. MAX 0 n = n",
REWRITE_TAC [MAX_DEF; ZERO_LESS_EQ]
);;
let MAX_SYM = prove_thm
(`MAX_SYM`,
"!n p. MAX n p = MAX p n",
REPEAT GEN_TAC THEN
ASM_CASES_TAC "n:num=p" THENL
[ % n = p %
ASM_REWRITE_TAC []
; % ~ n = p %
REWRITE_TAC [MAX_DEF] THEN
ASM_CASES_TAC "n <= p" THEN
ASM_REWRITE_TAC [LESS_OR_EQ] THEN
POP_ASSUM_LIST (\ [T1;T2].
REWRITE_TAC [GSYM T2; REWRITE_RULE [GSYM NOT_LESS] T1])
]
);;
let MAX_REFL = prove_thm
(`MAX_REFL`,
"!n. MAX n n = n",
REWRITE_TAC [MAX_DEF; LESS_OR_EQ]
);;
let MAX_SUC = prove_thm
(`MAX_SUC`,
"!n. MAX n (SUC n) = SUC n",
REWRITE_TAC [MAX_DEF; LESS_EQ_SUC_REFL]
);;
let SUC_MAX = prove_thm
(`SUC_MAX`,
"!n p. MAX (SUC n) (SUC p) = SUC (MAX n p)",
REPEAT GEN_TAC THEN
REWRITE_TAC [MAX_DEF; LESS_EQ_MONO] THEN
COND_CASES_TAC THEN
ASM_REWRITE_TAC[]
);;
let MIN_DEF = new_definition
(`MIN_DEF`,
"MIN n p = ((n <= p) => n | p)"
);;
let MIN_0 = prove_thm
(`MIN_0`,
"!n. MIN 0 n = 0",
REWRITE_TAC [MIN_DEF; ZERO_LESS_EQ]
);;
let MIN_SYM = prove_thm
(`MIN_SYM`,
"!n p. MIN n p = MIN p n",
REPEAT GEN_TAC THEN
ASM_CASES_TAC "n:num=p" THENL
[ % n = p %
ASM_REWRITE_TAC []
; % ~ n = p %
REWRITE_TAC [MIN_DEF] THEN
ASM_CASES_TAC "n <= p" THEN
ASM_REWRITE_TAC [LESS_OR_EQ] THEN
POP_ASSUM_LIST (\ [T1;T2].
REWRITE_TAC [GSYM T2; REWRITE_RULE [GSYM NOT_LESS] T1])
]
);;
let MIN_REFL = prove_thm
(`MIN_REFL`,
"!n. MIN n n = n",
REWRITE_TAC [MIN_DEF; LESS_OR_EQ]
);;
let MIN_SUC = prove_thm
(`MIN_SUC`,
"!n. MIN n (SUC n) = n",
REWRITE_TAC [MIN_DEF; LESS_EQ_SUC_REFL]
);;
let SUC_MIN = prove_thm
(`SUC_MIN`,
"!n p. MIN (SUC n) (SUC p) = SUC (MIN n p)",
REPEAT GEN_TAC THEN
REWRITE_TAC [MIN_DEF; LESS_EQ_MONO] THEN
COND_CASES_TAC THEN
ASM_REWRITE_TAC[]
);;
close_theory();;
|
