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
|
(* ====================================================================== *)
(* TESTFORM *)
(* ====================================================================== *)
let rec TESTFORM var interpsigns_thm set_thm fm =
let polys,set,signs = dest_interpsigns interpsigns_thm in
let polys' = dest_list polys in
let signs' = dest_list signs in
if fm = t_tm then BETA_RULE (ISPECL [set] t_thm)
else if fm = f_tm then BETA_RULE (ISPECL [set] f_thm)
else if is_neg fm then
let lam = mk_abs (var,dest_neg fm) in
let thm = TESTFORM var interpsigns_thm set_thm (dest_neg fm) in
if is_pos (concl thm) then
MATCH_MP (BETA_RULE (ISPECL [lam;set] neg_thm_p)) thm
else if is_neg (concl thm) then
MATCH_MP (BETA_RULE (ISPECL [lam;set] neg_thm_n)) thm
else failwith "error"
else if is_conj fm then
let a,b = dest_conj fm in
let a',b' = mk_abs (var,a),mk_abs (var,b) in
let thma = TESTFORM var interpsigns_thm set_thm a in
let thmb = TESTFORM var interpsigns_thm set_thm b in
if is_neg (concl thma) && is_neg (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_nn);set_thm;thma;thmb]
else if is_neg (concl thma) && is_pos (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_np);set_thm;thma;thmb]
else if is_pos (concl thma) && is_neg (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_pn);set_thm;thma;thmb]
else if is_pos (concl thma) && is_pos (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_pp);set_thm;thma;thmb]
else failwith "error"
else if is_disj fm then
let a,b = dest_disj fm in
let a',b' = mk_abs (var,a),mk_abs (var,b) in
let thma = TESTFORM var interpsigns_thm set_thm a in
let thmb = TESTFORM var interpsigns_thm set_thm b in
if is_neg (concl thma) && is_neg (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] or_thm_nn);set_thm;thma;thmb]
else if is_pos (concl thma) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] or_thm_p);set_thm;thma]
else if is_pos (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] or_thm_q);set_thm;thmb]
else failwith "error"
else if is_imp fm then
let a,b = dest_imp fm in
let a',b' = mk_abs (var,a),mk_abs (var,b) in
let thma = TESTFORM var interpsigns_thm set_thm a in
let thmb = TESTFORM var interpsigns_thm set_thm b in
if is_neg (concl thma) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] imp_thm_n);set_thm;thma]
else if is_pos (concl thma) && is_neg (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] imp_thm_pn);set_thm;thma;thmb]
else if is_pos (concl thma) && is_pos (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] imp_thm_pp);set_thm;thmb]
else failwith "error"
else if is_iff fm then
let a,b = dest_eq fm in
let a',b' = mk_abs (var,a),mk_abs (var,b) in
let thma = TESTFORM var interpsigns_thm set_thm a in
let thmb = TESTFORM var interpsigns_thm set_thm b in
if is_neg (concl thma) && is_neg (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_nn);set_thm;thma;thmb]
else if is_neg (concl thma) && is_pos (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_np);set_thm;thma;thmb]
else if is_pos (concl thma) && is_neg (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_pn);set_thm;thma;thmb]
else if is_pos (concl thma) && is_pos (concl thmb) then
MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_pp);set_thm;thma;thmb]
else failwith "error"
else (* an atom *)
let op,p,_ = get_binop fm in
let lam = mk_abs (var,p) in
let ind =
try
index lam polys'
with Failure "index" -> failwith "TESTFORM: Poly not present in list" in
let sign = ith ind signs' in
let thm = ith ind (interpsigns_thms interpsigns_thm) in
let thm_op,thm_p,_ =
get_binop (snd (dest_imp (snd (dest_forall (concl thm))))) in
if op = req then
if thm_op = req then thm
else if thm_op = rlt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_eq_thm);thm]
else if thm_op = rgt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_eq_thm);thm]
else failwith "error"
else if op = rlt then
if thm_op = rlt then thm
else if thm_op = req then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_lt_thm);thm]
else if thm_op = rgt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_lt_thm);thm]
else failwith "error"
else if op = rgt then
if thm_op = rgt then thm
else if thm_op = req then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_gt_thm);thm]
else if thm_op = rlt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_gt_thm);thm]
else failwith "error"
else if op = rle then
if thm_op = rlt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_le_thm);thm]
else if thm_op = req then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_le_thm);thm]
else if thm_op = rgt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_le_thm);thm]
else failwith "error"
else if op = rge then
if thm_op = rlt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_ge_thm);thm]
else if thm_op = req then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_ge_thm);thm]
else if thm_op = rgt then
MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_ge_thm);thm]
else failwith "error"
else failwith "error" ;;
let TESTFORM var interpsigns_thm set_thm fm =
let start_time = Sys.time() in
let res = TESTFORM var interpsigns_thm set_thm fm in
testform_timer +.= (Sys.time() -. start_time);
res;;
let tvar,tmat,tfm = ref `T`,ref TRUTH,ref `T`;;
(*
let var,mat_thm,fm = !tvar,!tmat,!tfm
*)
let COMBINE_TESTFORMS =
let lem1 = TAUT `(T ==> a) <=> a`
and lem2 = TAUT `(T /\ x) <=> x`
and imat_tm = `interpmat` in
fun var mat_thm fm ->
tvar := var;
tmat := mat_thm;
tfm := fm;
(* if not (fst (strip_comb (concl mat_thm)) = imat_tm) then failwith "not a mat thm" else *)
let mat_thm' = (CONV_RULE (RATOR_CONV (RAND_CONV (LIST_CONV (ALPHA_CONV var))))) mat_thm in
let rol_thm,all2_thm = interpmat_thms mat_thm' in
let ord_thms = rol_nonempty_thms rol_thm in
let part_thm = PARTITION_LINE_CONV (snd(dest_comb(concl rol_thm))) in
let isigns_thms = CONJUNCTS(REWRITE_RULE[ALL2;part_thm] all2_thm) in
let ex_thms = map2 (fun x y -> TESTFORM var x y fm) isigns_thms ord_thms in
if exists (fun x -> is_forall(concl x)) ex_thms then
let witness_thm = find (fun x -> is_forall(concl x)) ex_thms in
let i = try index witness_thm ex_thms with _ -> failwith "COMBINE_TESTFORMS: witness not present" in
let ord_thm = ith i ord_thms in
let x,bod = dest_exists (concl ord_thm) in
if bod = t_tm then
let thm1 = ISPEC var witness_thm in
let thm2 = PURE_REWRITE_RULE[lem1] thm1 in
let exists_thm = EXISTS (mk_exists(var,concl thm2),var) thm2 in
EQT_INTRO exists_thm
else
let nv = new_var real_ty in
let ord_thm' = CONV_RULE (RAND_CONV (ALPHA_CONV nv)) ord_thm in
let y,bod = dest_exists (concl ord_thm') in
let ass_thm = ASSUME bod in
let thm = MATCH_MP witness_thm ass_thm in
let exists_thm = EXISTS (mk_exists(y,concl thm) ,y) thm in
let ret = CHOOSE (nv,ord_thm) exists_thm in
EQT_INTRO ret
else
if length ord_thms = 1 && snd(dest_exists(concl (hd ord_thms))) = t_tm then
PURE_REWRITE_RULE[lem2] (EQF_INTRO (hd ex_thms)) else
let ex_thms' = map (MATCH_MP NOT_EXISTS_CONJ_THM) ex_thms in
let len = length ex_thms' in
let first,[t1;t2] = chop_list (len-2) ex_thms' in
let base = MATCH_MPL[testform_itlem;t1;t2] in
let ex_thm = itlist (fun x y -> MATCH_MPL[testform_itlem;x;y]) first base in
let cover_thm = ROL_COVERS rol_thm in
let pre_thm = MATCH_MP ex_thm (ISPEC var cover_thm) in
let gen_thm = GEN var pre_thm in
let ret = MATCH_EQ_MP FORALL_NOT_THM gen_thm in
EQF_INTRO ret;;
let COMBINE_TESTFORMS var mat_thm fm =
let start_time = Sys.time() in
let res = COMBINE_TESTFORMS var mat_thm fm in
combine_testforms_timer +.= (Sys.time() -. start_time);
res;;
(* {{{ Examples *)
(*
let var,mat_thm,fm =
rx,ASSUME `interpsigns [\x. &1 + x * (&0 + x * &1)] (\x. T) [Pos]`,ASSUME `?x:real. T`
let ex_thms = map2 (fun x y -> TESTFORM var x y fm) isigns_thms ord_thms in
TESTFORM ry (hd isigns_thms) (hd ord_thms) fm
TESTFORM ry (hd isigns_thms) (hd ord_thms) `&1 + y * (&0 + x * -- &1) <= &0`
TESTFORM ry (hd isigns_thms) (hd ord_thms) `(&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0`
TESTFORM ry (hd isigns_thms) (hd ord_thms) `(&1 + y * (&0 + x * -- &1) <= &0) /\ (&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0`
let fm = `(&1 + y * (&0 + x * -- &1) <= &0) /\ (&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0`
let var,mat_thm,fm =
ry,
ASSUME `interpmat [] [\y. (&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1); \y. &1 + y * (&0 + x * -- &1)] [[Neg; Pos]]`,
`~((&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0 /\ &1 + y * (&0 + x * -- &1) <= &0)`
let var,mat_thm,fm =
ry,
ASSUME `interpmat [x_354]
[\y. (&1 + x * -- &1) + y * (&0 + x * -- &2); \x. &1 + x * -- &1;
\y. (&1 + x * -- &1) + y * (&0 + x * -- &2)]
[[Neg; Pos; Neg]; [Neg; Zero; Neg]; [Neg; Neg; Neg]]`,
`~(&1 + x * -- &1 < &0 /\ &1 + y * -- &1 < &0
==> (&1 + x * -- &1) + y * (&0 + x * -- &2) < &0)`
*)
(* }}} *)
|
