/[mojave]/metaprl/theories/itt/itt_logic.ml
ViewVC logotype

Contents of /metaprl/theories/itt/itt_logic.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (show annotations) (download)
Thu Mar 16 19:52:02 2000 UTC (21 years, 4 months ago) by lolorigo
File size: 39029 byte(s)
added/improved functionality for metaprl/jprover/nuprl5 io

1 (*
2 * Regular logic connectives.
3 *
4 * ----------------------------------------------------------------
5 *
6 * This file is part of MetaPRL, a modular, higher order
7 * logical framework that provides a logical programming
8 * environment for OCaml and other languages.
9 *
10 * See the file doc/index.html for information on Nuprl,
11 * OCaml, and more information about this system.
12 *
13 * Copyright (C) 1998 Jason Hickey, Cornell University
14 *
15 * This program is free software; you can redistribute it and/or
16 * modify it under the terms of the GNU General Public License
17 * as published by the Free Software Foundation; either version 2
18 * of the License, or (at your option) any later version.
19 *
20 * This program is distributed in the hope that it will be useful,
21 * but WITHOUT ANY WARRANTY; without even the implied warranty of
22 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
23 * GNU General Public License for more details.
24 *
25 * You should have received a copy of the GNU General Public License
26 * along with this program; if not, write to the Free Software
27 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28 *
29 * Author: Jason Hickey
30 * jyh@cs.cornell.edu
31 *
32 *)
33
34 include Itt_equal
35 include Itt_rfun
36 include Itt_dfun
37 include Itt_fun
38 include Itt_dprod
39 include Itt_prod
40 include Itt_union
41 include Itt_void
42 include Itt_unit
43 include Itt_struct
44
45 open Printf
46 open Mp_debug
47 open Refiner.Refiner
48 open Refiner.Refiner.Term
49 open Refiner.Refiner.TermType
50 open Refiner.Refiner.TermOp
51 open Refiner.Refiner.TermMan
52 open Refiner.Refiner.TermSubst
53 open Refiner.Refiner.Refine
54 open Refiner.Refiner.RefineError
55 open Mp_resource
56 open Simple_print
57
58 open Tactic_type
59 open Tactic_type.Tacticals
60 open Tactic_type.Conversionals
61 open Mptop
62 open Var
63
64 open Base_auto_tactic
65 open Base_dtactic
66
67 open Itt_squash
68 open Itt_void
69 open Itt_equal
70 open Itt_rfun
71 open Itt_dprod
72 open Itt_struct
73
74 (*
75 * Show that the file is loading.
76 *)
77 let _ =
78 show_loading "Loading Itt_logic%t"
79
80 let debug_auto =
81 create_debug (**)
82 { debug_name = "auto";
83 debug_description = "Display auto tactic operations";
84 debug_value = false
85 }
86
87 (************************************************************************
88 * REWRITES *
89 ************************************************************************)
90
91 declare "prop"[i:l]
92
93 declare "true"
94 declare "false"
95 declare "not"{'a}
96 declare "iff"{'a; 'b}
97 declare "implies"{'a; 'b}
98 declare "and"{'a; 'b}
99 declare "or"{'a; 'b}
100 declare "cand"{'a; 'b}
101 declare "cor"{'a; 'b}
102 declare "all"{'A; x. 'B['x]}
103 declare "exists"{'A; x. 'B['x]}
104
105 prim_rw unfold_prop : "prop"[i:l] <--> "univ"[i:l]
106
107 prim_rw unfold_true : "true" <--> unit
108 prim_rw unfold_false : "false" <--> void
109 prim_rw unfold_not : "not"{'a} <--> ('a -> void)
110 prim_rw unfold_implies : ('a => 'b) <--> ('a -> 'b)
111 prim_rw unfold_iff : "iff"{'a; 'b} <--> (('a -> 'b) & ('b -> 'a))
112 prim_rw unfold_and : ('a & 'b) <--> ('a * 'b)
113 prim_rw unfold_or : ('a or 'b) <--> ('a + 'b)
114 prim_rw unfold_cand : "cand"{'a; 'b} <--> ('a & 'b)
115 prim_rw unfold_cor : "cor"{'a; 'b} <--> "or"{'a; ."cand"{."not"{'a}; 'b}}
116 prim_rw unfold_all : (all x: 'A. 'B['x]) <--> (x:'A -> 'B['x])
117 prim_rw unfold_exists : (exst x: 'A. 'B['x]) <--> (x:'A * 'B['x])
118
119 let fold_true = makeFoldC << "true" >> unfold_true
120 let fold_false = makeFoldC << "false" >> unfold_false
121 let fold_not = makeFoldC << not{'a} >> unfold_not
122 let fold_implies = makeFoldC << 'a => 'b >> unfold_implies
123 let fold_iff = makeFoldC << "iff"{'a; 'b} >> unfold_iff
124 let fold_and = makeFoldC << 'a & 'b >> unfold_and
125 let fold_or = makeFoldC << 'a or 'b >> unfold_or
126 let fold_cand = makeFoldC << "cand"{'a; 'b} >> unfold_cand
127 let fold_cor = makeFoldC << "cor"{'a; 'b} >> unfold_cor
128 let fold_all = makeFoldC << all x: 'A. 'B['x] >> unfold_all
129 let fold_exists = makeFoldC << exst x: 'A. 'B['x] >> unfold_exists
130
131 (************************************************************************
132 * RULES *
133 ************************************************************************)
134
135 (*
136 * True and false.
137 *)
138 interactive true_univ {| intro_resource []; eqcd_resource |} 'H :
139 sequent ['ext] { 'H >- "true" = "true" in univ[i:l] }
140
141 interactive true_member {| intro_resource [] |} 'H :
142 sequent ['ext] { 'H >- member{univ[i:l]; ."true"} }
143
144 interactive true_type {| intro_resource [] |} 'H :
145 sequent ['ext] { 'H >- "type"{."true"} }
146
147 interactive true_intro {| intro_resource [] |} 'H :
148 sequent ['ext] { 'H >- "true" }
149
150 interactive false_univ {| intro_resource []; eqcd_resource |} 'H :
151 sequent ['ext] { 'H >- "false" = "false" in univ[i:l] }
152
153 interactive false_member {| intro_resource [] |} 'H :
154 sequent ['ext] { 'H >- "member"{univ[i:l]; ."false"} }
155
156 interactive false_type {| intro_resource [] |} 'H :
157 sequent ['ext] { 'H >- "type"{."false"} }
158
159 interactive false_elim {| elim_resource [ThinOption thinT] |} 'H 'J :
160 sequent ['ext] { 'H; x: "false"; 'J['x] >- 'C['x] }
161
162 interactive false_squash 'H :
163 sequent [squash] { 'H >- "false" } -->
164 sequent ['ext] { 'H >- "false" }
165
166 (*
167 * Negation.
168 *)
169 interactive not_univ {| intro_resource []; eqcd_resource |} 'H :
170 [wf] sequent [squash] { 'H >- 't1 = 't2 in univ[i:l] } -->
171 sequent ['ext] { 'H >- "not"{'t1} = "not"{'t2} in univ[i:l] }
172
173 interactive not_member {| intro_resource [] |} 'H :
174 [wf] sequent [squash] { 'H >- member{univ[i:l]; 't} } -->
175 sequent ['ext] { 'H >- member{univ[i:l]; ."not"{'t}} }
176
177 interactive not_type {| intro_resource [] |} 'H :
178 [wf] sequent [squash] { 'H >- "type"{'t} } -->
179 sequent ['ext] { 'H >- "type"{."not"{'t}} }
180
181 interactive not_intro {| intro_resource [] |} 'H 'x :
182 [wf] sequent [squash] { 'H >- "type"{'t} } -->
183 [main] sequent ['ext] { 'H; x: 't >- "false" } -->
184 sequent ['ext] { 'H >- "not"{'t} }
185
186 interactive not_elim {| elim_resource [] |} 'H 'J :
187 [assertion] sequent ['ext] { 'H; x: "not"{'t}; 'J['x] >- 't } -->
188 sequent ['ext] { 'H; x: "not"{'t}; 'J['x] >- 'C }
189
190 (*
191 * Conjunction.
192 *)
193 interactive and_univ {| intro_resource []; eqcd_resource |} 'H :
194 [wf] sequent [squash] { 'H >- 'a1 = 'b1 in univ[i:l] } -->
195 [wf] sequent [squash] { 'H >- 'a2 = 'b2 in univ[i:l] } -->
196 sequent ['ext] { 'H >- "and"{'a1; 'a2} = "and"{'b1; 'b2} in univ[i:l] }
197
198 interactive and_member {| intro_resource [] |} 'H :
199 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a1} } -->
200 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a2} } -->
201 sequent ['ext] { 'H >- member{univ[i:l]; ."and"{'a1; 'a2}} }
202
203 interactive and_type {| intro_resource [] |} 'H :
204 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
205 [wf] sequent [squash] { 'H >- "type"{'a2} } -->
206 sequent ['ext] { 'H >- "type"{."and"{'a1; 'a2}} }
207
208 interactive and_intro {| intro_resource [] |} 'H :
209 [wf] sequent ['ext] { 'H >- 'a1 } -->
210 [wf] sequent ['ext] { 'H >- 'a2 } -->
211 sequent ['ext] { 'H >- "and"{'a1; 'a2} }
212
213 interactive and_elim {| elim_resource [] |} 'H 'J 'y 'z :
214 [main] sequent ['ext] { 'H; y: 'a1; z: 'a2; 'J['y, 'z] >- 'C['y, 'z] } -->
215 sequent ['ext] { 'H; x: "and"{'a1; 'a2}; 'J['x] >- 'C['x] }
216
217 (*
218 * Disjunction.
219 *)
220 interactive or_univ {| intro_resource []; eqcd_resource |} 'H :
221 [wf] sequent [squash] { 'H >- 'a1 = 'b1 in univ[i:l] } -->
222 [wf] sequent [squash] { 'H >- 'a2 = 'b2 in univ[i:l] } -->
223 sequent ['ext] { 'H >- "or"{'a1; 'a2} = "or"{'b1; 'b2} in univ[i:l] }
224
225 interactive or_member {| intro_resource [] |} 'H :
226 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a1} } -->
227 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a2} } -->
228 sequent ['ext] { 'H >- member{univ[i:l]; ."or"{'a1; 'a2}} }
229
230 interactive or_type {| intro_resource [] |} 'H :
231 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
232 [wf] sequent [squash] { 'H >- "type"{'a2} } -->
233 sequent ['ext] { 'H >- "type"{."or"{'a1; 'a2}} }
234
235 interactive or_intro_left {| intro_resource [SelectOption 1] |} 'H :
236 [wf] sequent [squash] { 'H >- "type"{.'a2} } -->
237 [main] sequent ['ext] { 'H >- 'a1 } -->
238 sequent ['ext] { 'H >- "or"{'a1; 'a2} }
239
240 interactive or_intro_right {| intro_resource [SelectOption 2] |} 'H :
241 [wf] sequent [squash] { 'H >- "type"{.'a1} } -->
242 [main] sequent ['ext] { 'H >- 'a2 } -->
243 sequent ['ext] { 'H >- "or"{'a1; 'a2} }
244
245 interactive or_elim {| elim_resource [] |} 'H 'J 'y :
246 [main] sequent ['ext] { 'H; y: 'a1; 'J[inl{'y}] >- 'C[inl{'y}] } -->
247 [main] sequent ['ext] { 'H; y: 'a2; 'J[inr{'y}] >- 'C[inr{'y}] } -->
248 sequent ['ext] { 'H; x: "or"{'a1; 'a2}; 'J['x] >- 'C['x] }
249
250 (*
251 * Implication.
252 *)
253 interactive implies_univ {| intro_resource []; eqcd_resource |} 'H :
254 [wf] sequent [squash] { 'H >- 'a1 = 'b1 in univ[i:l] } -->
255 [wf] sequent [squash] { 'H >- 'a2 = 'b2 in univ[i:l] } -->
256 sequent ['ext] { 'H >- "implies"{'a1; 'a2} = "implies"{'b1; 'b2} in univ[i:l] }
257
258 interactive implies_member {| intro_resource [] |} 'H :
259 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a1} } -->
260 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a2} } -->
261 sequent ['ext] { 'H >- member{univ[i:l]; ."implies"{'a1; 'a2}} }
262
263 interactive implies_type {| intro_resource [] |} 'H :
264 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
265 [wf] sequent [squash] { 'H >- "type"{'a2} } -->
266 sequent ['ext] { 'H >- "type"{."implies"{'a1; 'a2}} }
267
268 interactive implies_intro {| intro_resource [] |} 'H 'x :
269 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
270 [main] sequent ['ext] { 'H; x: 'a1 >- 'a2 } -->
271 sequent ['ext] { 'H >- "implies"{'a1; 'a2} }
272
273 interactive implies_elim {| elim_resource [ThinOption thinT] |} 'H 'J 'y :
274 [assertion] sequent ['ext] { 'H; x: "implies"{'a1; 'a2}; 'J['x] >- 'a1 } -->
275 [main] sequent ['ext] { 'H; x: "implies"{'a1; 'a2}; 'J['x]; y: 'a2 >- 'C['x] } -->
276 sequent ['ext] { 'H; x: "implies"{'a1; 'a2}; 'J['x] >- 'C['x] }
277
278 (*
279 * Bi-implication.
280 *)
281 interactive iff_univ {| intro_resource []; eqcd_resource |} 'H :
282 [wf] sequent [squash] { 'H >- 'a1 = 'b1 in univ[i:l] } -->
283 [wf] sequent [squash] { 'H >- 'a2 = 'b2 in univ[i:l] } -->
284 sequent ['ext] { 'H >- "iff"{'a1; 'a2} = "iff"{'b1; 'b2} in univ[i:l] }
285
286 interactive iff_member {| intro_resource [] |} 'H :
287 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a1} } -->
288 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a2} } -->
289 sequent ['ext] { 'H >- member{univ[i:l]; ."iff"{'a1; 'a2}} }
290
291 interactive iff_type {| intro_resource [] |} 'H :
292 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
293 [wf] sequent [squash] { 'H >- "type"{'a2} } -->
294 sequent ['ext] { 'H >- "type"{."iff"{'a1; 'a2}} }
295
296 interactive iff_intro {| intro_resource [] |} 'H :
297 [wf] sequent ['ext] { 'H >- 'a1 => 'a2 } -->
298 [wf] sequent ['ext] { 'H >- 'a2 => 'a1 } -->
299 sequent ['ext] { 'H >- "iff"{'a1; 'a2} }
300
301 interactive iff_elim {| elim_resource [] |} 'H 'J 'y 'z :
302 sequent ['ext] { 'H; y: "implies"{'a1; 'a2}; z: "implies"{'a2; 'a1}; 'J['y, 'z] >- 'C['y, 'z] } -->
303 sequent ['ext] { 'H; x: "iff"{'a1; 'a2}; 'J['x] >- 'C['x] }
304
305 (*
306 * Conjunction.
307 *)
308 interactive cand_univ {| intro_resource []; eqcd_resource |} 'H 'x :
309 [wf] sequent [squash] { 'H >- 'a1 = 'b1 in univ[i:l] } -->
310 [wf] sequent [squash] { 'H; x: 'a1 >- 'a2 = 'b2 in univ[i:l] } -->
311 sequent ['ext] { 'H >- "cand"{'a1; 'a2} = "cand"{'b1; 'b2} in univ[i:l] }
312
313 interactive cand_member {| intro_resource [] |} 'H 'x :
314 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a1} } -->
315 [wf] sequent [squash] { 'H; x: 'a1 >- member{univ[i:l]; 'a2} } -->
316 sequent ['ext] { 'H >- member{univ[i:l]; ."cand"{'a1; 'a2}} }
317
318 interactive cand_type {| intro_resource [] |} 'H 'x :
319 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
320 [wf] sequent [squash] { 'H; x: 'a1 >- "type"{'a2} } -->
321 sequent ['ext] { 'H >- "type"{."cand"{'a1; 'a2}} }
322
323 interactive cand_intro {| intro_resource [] |} 'H 'x :
324 [main] sequent ['ext] { 'H >- 'a1 } -->
325 [main] sequent ['ext] { 'H; x: 'a1 >- 'a2 } -->
326 sequent ['ext] { 'H >- "cand"{'a1; 'a2} }
327
328 interactive cand_elim {| elim_resource [] |} 'H 'J 'y 'z :
329 [main] sequent ['ext] { 'H; y: 'a1; z: 'a2; 'J['y, 'z] >- 'C['y, 'z] } -->
330 sequent ['ext] { 'H; x: "cand"{'a1; 'a2}; 'J['x] >- 'C['x] }
331
332 (*
333 * Disjunction.
334 *)
335 interactive cor_univ {| intro_resource []; eqcd_resource |} 'H 'x :
336 [wf] sequent [squash] { 'H >- 'a1 = 'b1 in univ[i:l] } -->
337 [wf] sequent [squash] { 'H; x: "not"{'a1} >- 'a2 = 'b2 in univ[i:l] } -->
338 sequent ['ext] { 'H >- "cor"{'a1; 'a2} = "cor"{'b1; 'b2} in univ[i:l] }
339
340 interactive cor_member {| intro_resource [] |} 'H 'x :
341 [wf] sequent [squash] { 'H >- member{univ[i:l]; 'a1} } -->
342 [wf] sequent [squash] { 'H; x: "not"{'a1} >- member{univ[i:l]; 'a2} } -->
343 sequent ['ext] { 'H >- member{univ[i:l]; ."cor"{'a1; 'a2}} }
344
345 interactive cor_type {| intro_resource [] |} 'H 'x :
346 [wf] sequent [squash] { 'H >- "type"{'a1} } -->
347 [wf] sequent [squash] { 'H; x: "not"{'a1} >- "type"{'a2} } -->
348 sequent ['ext] { 'H >- "type"{."cor"{'a1; 'a2}} }
349
350 interactive cor_intro_left {| intro_resource [SelectOption 1] |} 'H 'x :
351 [wf] sequent [squash] { 'H; x: "not"{'a1} >- "type"{.'a2} } -->
352 [main] sequent ['ext] { 'H >- 'a1 } -->
353 sequent ['ext] { 'H >- "cor"{'a1; 'a2} }
354
355 interactive cor_intro_right {| intro_resource [SelectOption 2] |} 'H 'x :
356 [wf] sequent [squash] { 'H >- "type"{.'a1} } -->
357 [main] sequent ['ext] { 'H >- "not"{'a1} } -->
358 [main] sequent ['ext] { 'H; x: "not"{'a1} >- 'a2 } -->
359 sequent ['ext] { 'H >- "cor"{'a1; 'a2} }
360
361 interactive cor_elim {| elim_resource [] |} 'H 'J 'u 'v :
362 [main] sequent ['ext] { 'H; u: 'a1; 'J[inl{'u}] >- 'C[inl{'u}] } -->
363 [main] sequent ['ext] { 'H; u: "not"{'a1}; v: 'a2; 'J[inr{'u, 'v}] >- 'C[inr{'u, 'v}] } -->
364 sequent ['ext] { 'H; x: "cor"{'a1; 'a2}; 'J['x] >- 'C['x] }
365
366 (*
367 * All elimination performs a thinning
368 *)
369 interactive all_univ {| intro_resource []; eqcd_resource |} 'H 'x :
370 [wf] sequent [squash] { 'H >- 't1 = 't2 in univ[i:l] } -->
371 [wf] sequent [squash] { 'H; x : 't1 >- 'b1['x] = 'b2['x] in univ[i:l] } -->
372 sequent ['ext] { 'H >- "all"{'t1; x1. 'b1['x1]} = "all"{'t2; x2. 'b2['x2]} in univ[i:l] }
373
374 interactive all_member {| intro_resource [] |} 'H 'x :
375 [wf] sequent [squash] { 'H >- member{univ[i:l]; 't} } -->
376 [wf] sequent [squash] { 'H; x: 't >- member{univ[i:l]; 'b['x]} } -->
377 sequent ['ext] { 'H >- member{univ[i:l]; ."all"{'t; v. 'b['v]}} }
378
379 interactive all_type {| intro_resource [] |} 'H 'x :
380 [wf] sequent [squash] { 'H >- "type"{'t} } -->
381 [wf] sequent [squash] { 'H; x: 't >- "type"{'b['x]} } -->
382 sequent ['ext] { 'H >- "type"{."all"{'t; v. 'b['v]}} }
383
384 interactive all_intro {| intro_resource [] |} 'H 'x :
385 [wf] sequent [squash] { 'H >- "type"{'t} } -->
386 [main] sequent ['ext] { 'H; x: 't >- 'b['x] } -->
387 sequent ['ext] { 'H >- "all"{'t; v. 'b['v]} }
388
389 interactive all_elim {| elim_resource [ThinOption thinT] |} 'H 'J 'w 'z :
390 [wf] sequent [squash] { 'H; x: all a: 'A. 'B['a]; 'J['x] >- member{'A; 'z} } -->
391 [main] sequent ['ext] { 'H; x: all a: 'A. 'B['a]; 'J['x]; w: 'B['z] >- 'C['x] } -->
392 sequent ['ext] { 'H; x: all a: 'A. 'B['a]; 'J['x] >- 'C['x] }
393
394 (*
395 * Existential.
396 *)
397 interactive exists_univ {| intro_resource []; eqcd_resource |} 'H 'x :
398 [wf] sequent [squash] { 'H >- 't1 = 't2 in univ[i:l] } -->
399 [wf] sequent [squash] { 'H; x : 't1 >- 'b1['x] = 'b2['x] in univ[i:l] } -->
400 sequent ['ext] { 'H >- "exists"{'t1; x1. 'b1['x1]} = "exists"{'t2; x2. 'b2['x2]} in univ[i:l] }
401
402 interactive exists_member {| intro_resource [] |} 'H 'x :
403 [wf] sequent [squash] { 'H >- member{univ[i:l]; 't} } -->
404 [wf] sequent [squash] { 'H; x: 't >- member{univ[i:l]; 'b['x]} } -->
405 sequent ['ext] { 'H >- member{univ[i:l]; ."exists"{'t; v. 'b['v]}} }
406
407 interactive exists_type {| intro_resource [] |} 'H 'x :
408 [wf] sequent [squash] { 'H >- "type"{'t} } -->
409 [wf] sequent [squash] { 'H; x: 't >- "type"{'b['x]} } -->
410 sequent ['ext] { 'H >- "type"{."exists"{'t; v. 'b['v]}} }
411
412 interactive exists_intro {| intro_resource [] |} 'H 'z 'x :
413 [wf] sequent [squash] { 'H >- member{'t; 'z} } -->
414 [main] sequent ['ext] { 'H >- 'b['z] } -->
415 [wf] sequent [squash] { 'H; x: 't >- "type"{'b['x]} } -->
416 sequent ['ext] { 'H >- "exists"{'t; v. 'b['v]} }
417
418 interactive exists_elim {| elim_resource [] |} 'H 'J 'y 'z :
419 [main] sequent ['ext] { 'H; y: 'a; z: 'b['y]; 'J['y, 'z] >- 'C['y, 'z] } -->
420 sequent ['ext] { 'H; x: exst v: 'a. 'b['v]; 'J['x] >- 'C['x] }
421
422 (************************************************************************
423 * DISPLAY FORMS *
424 ************************************************************************)
425
426 prec prec_iff
427 prec prec_implies
428 prec prec_and
429 prec prec_or
430 prec prec_not
431 prec prec_quant
432
433 prec prec_implies < prec_iff
434 prec prec_iff < prec_or
435 prec prec_or < prec_and
436 prec prec_and < prec_not
437 prec prec_quant < prec_iff
438
439 dform true_df1 : mode[src] :: "true" = `"True"
440
441 dform false_df1 : mode[src] :: "false" = `"False"
442
443 dform not_df1 : mode[src] :: parens :: "prec"[prec_implies] :: "not"{'a} =
444 `"not " slot["le"]{'a}
445
446 dform implies_df1 : mode[src] :: parens :: "prec"[prec_implies] :: implies{'a; 'b} =
447 slot["le"]{'a} `" => " slot["lt"]{'b}
448
449 dform iff_df1 : mode[src] :: parens :: "prec"[prec_iff] :: iff{'a; 'b} =
450 slot["le"]{'a} `" <==> " slot["lt"]{'b}
451
452 dform and_df1 : mode[src] :: parens :: "prec"[prec_and] :: "and"{'a; 'b} =
453 slot["le"]{'a} `" or " slot["lt"]{'b}
454
455 dform or_df1 : mode[src] :: parens :: "prec"[prec_or] :: "or"{'a; 'b} =
456 slot["le"]{'a} `" and " slot["lt"]{'b}
457
458 dform all_df1 : mode[src] :: parens :: "prec"[prec_quant] :: "all"{'A; x. 'B} =
459 `"all " slot{'x} `": " slot{'A}`"." slot{'B}
460
461 dform exists_df1 : mode[src] :: parens :: "prec"[prec_quant] :: "exists"{'A; x. 'B} =
462 `"exists " slot{'x} `": " slot{'A} `"." slot{'B}
463
464 dform true_df2 : "true" =
465 `"True"
466
467 dform false_df2 : "false" =
468 `"False"
469
470 dform not_df2 : parens :: "prec"[prec_not] :: "not"{'a} =
471 Nuprl_font!tneg slot["le"]{'a}
472
473 dform implies_df2 : parens :: "prec"[prec_implies] :: implies{'a; 'b} =
474 slot["le"]{'a} " " Nuprl_font!Rightarrow " " slot["lt"]{'b}
475
476 dform iff_df2 : parens :: "prec"[prec_iff] :: iff{'a; 'b} =
477 slot["le"]{'a} " " Nuprl_font!Leftrightarrow " " slot["lt"]{'b}
478
479 (*
480 * Disjunction.
481 *)
482 declare or_df{'a}
483
484 dform or_df2 : parens :: "prec"[prec_or] :: "or"{'a; 'b} =
485 szone pushm[0] slot["le"]{'a} or_df{'b} popm ezone
486
487 dform or_df3 : or_df{."or"{'a; 'b}} =
488 hspace Nuprl_font!vee " " slot["le"]{'a} or_df{'b}
489
490 dform or_df4 : or_df{'a} =
491 hspace Nuprl_font!vee " " slot{'a}
492
493 (*
494 * Disjunction.
495 *)
496 declare and_df{'a}
497
498 dform and_df2 : parens :: "prec"[prec_and] :: "and"{'a; 'b} =
499 szone pushm[0] slot["le"]{'a} and_df{'b} popm ezone
500
501 dform and_df3 : and_df{."and"{'a; 'b}} =
502 hspace Nuprl_font!wedge " " slot["le"]{'a} and_df{'b}
503
504 dform and_df4 : and_df{'a} =
505 hspace Nuprl_font!wedge " " slot{'a}
506
507 (*
508 * Quantifiers.
509 *)
510 dform all_df2 : parens :: "prec"[prec_quant] :: "all"{'A; x. 'B} =
511 pushm[3] Nuprl_font!forall slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
512
513 dform exists_df2 : parens :: "prec"[prec_quant] :: "exists"{'A; x. 'B} =
514 pushm[3] Nuprl_font!"exists" slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
515
516 (************************************************************************
517 * TACTICS *
518 ************************************************************************)
519
520 let true_term = << "true" >>
521 let true_opname = opname_of_term true_term
522 let is_true_term = is_no_subterms_term true_opname
523
524 let false_term = << "false" >>
525 let false_opname = opname_of_term false_term
526 let is_false_term = is_no_subterms_term false_opname
527
528 let all_term = << all x: 'A. 'B['x] >>
529 let all_opname = opname_of_term all_term
530 let is_all_term = is_dep0_dep1_term all_opname
531 let dest_all = dest_dep0_dep1_term all_opname
532 let mk_all_term = mk_dep0_dep1_term all_opname
533
534 let exists_term = << exst x: 'A. 'B['x] >>
535 let exists_opname = opname_of_term exists_term
536 let is_exists_term = is_dep0_dep1_term exists_opname
537 let dest_exists = dest_dep0_dep1_term exists_opname
538 let mk_exists_term = mk_dep0_dep1_term exists_opname
539
540 let or_term = << 'A or 'B >>
541 let or_opname = opname_of_term or_term
542 let is_or_term = is_dep0_dep0_term or_opname
543 let dest_or = dest_dep0_dep0_term or_opname
544 let mk_or_term = mk_dep0_dep0_term or_opname
545
546 let and_term = << 'A and 'B >>
547 let and_opname = opname_of_term and_term
548 let is_and_term = is_dep0_dep0_term and_opname
549 let dest_and = dest_dep0_dep0_term and_opname
550 let mk_and_term = mk_dep0_dep0_term and_opname
551
552 let cor_term = << "cor"{'A; 'B} >>
553 let cor_opname = opname_of_term cor_term
554 let is_cor_term = is_dep0_dep0_term cor_opname
555 let dest_cor = dest_dep0_dep0_term cor_opname
556 let mk_cor_term = mk_dep0_dep0_term cor_opname
557
558 let cand_term = << "cand"{'A; 'B} >>
559 let cand_opname = opname_of_term cand_term
560 let is_cand_term = is_dep0_dep0_term cand_opname
561 let dest_cand = dest_dep0_dep0_term cand_opname
562 let mk_cand_term = mk_dep0_dep0_term cand_opname
563
564 let implies_term = << 'A => 'B >>
565 let implies_opname = opname_of_term implies_term
566 let is_implies_term = is_dep0_dep0_term implies_opname
567 let dest_implies = dest_dep0_dep0_term implies_opname
568 let mk_implies_term = mk_dep0_dep0_term implies_opname
569
570 let iff_term = << "iff"{'A; 'B} >>
571 let iff_opname = opname_of_term iff_term
572 let is_iff_term = is_dep0_dep0_term iff_opname
573 let dest_iff = dest_dep0_dep0_term iff_opname
574 let mk_iff_term = mk_dep0_dep0_term iff_opname
575
576 let not_term = << "not"{'a} >>
577 let not_opname = opname_of_term not_term
578 let is_not_term = is_dep0_term not_opname
579 let dest_not = dest_dep0_term not_opname
580 let mk_not_term = mk_dep0_term not_opname
581
582 (*
583 * Squash elimination.
584 *)
585 let squash_falseT p =
586 false_squash (Sequent.hyp_count_addr p) p
587
588 (************************************************************************
589 * TYPE INFERENCE *
590 ************************************************************************)
591
592 (*
593 * Type of true, false.
594 *)
595 let inf_univ1 _ decl _ = decl, univ1_term
596
597 let typeinf_resource = Mp_resource.improve typeinf_resource (true_term, inf_univ1)
598 let typeinf_resource = Mp_resource.improve typeinf_resource (false_term, inf_univ1)
599
600 (*
601 * Type of quantifiers.
602 *)
603 let inf_d dest f decl t =
604 let v, a, b = dest t in
605 let decl', a' = f decl a in
606 let decl'', b' = f (add_unify_subst v a decl') b in
607 let le1, le2 = dest_univ a', dest_univ b' in
608 decl'', Itt_equal.mk_univ_term (max_level_exp le1 le2 0)
609
610 let typeinf_resource = Mp_resource.improve typeinf_resource (all_term, inf_d dest_all)
611 let typeinf_resource = Mp_resource.improve typeinf_resource (exists_term, inf_d dest_exists)
612
613 (*
614 * Type of propositions.
615 *)
616 let inf_nd dest f decl t =
617 let a, b = dest t in
618 let decl', a' = f decl a in
619 let decl'', b' = f decl' b in
620 let le1, le2 = dest_univ a', dest_univ b' in
621 decl'', Itt_equal.mk_univ_term (max_level_exp le1 le2 0)
622
623 let typeinf_resource = Mp_resource.improve typeinf_resource (or_term, inf_nd dest_or)
624 let typeinf_resource = Mp_resource.improve typeinf_resource (and_term, inf_nd dest_and)
625 let typeinf_resource = Mp_resource.improve typeinf_resource (implies_term, inf_nd dest_implies)
626 let typeinf_resource = Mp_resource.improve typeinf_resource (iff_term, inf_nd dest_iff)
627
628 (*
629 * Type of all.
630 *)
631 let inf_not f decl t =
632 let a = dest_not t in
633 f decl a
634
635 let typeinf_resource = Mp_resource.improve typeinf_resource (not_term, inf_not)
636
637 (************************************************************************
638 * AUTOMATION *
639 ************************************************************************)
640
641 (*
642 * Move hyps dependeing on the var to the conclusion.
643 *)
644 let rec intersects vars fv =
645 match vars with
646 [] ->
647 false
648 | v :: tl ->
649 if List.mem v fv then
650 true
651 else
652 intersects tl fv
653
654 let moveToConclVarsT vars p =
655 let { sequent_hyps = hyps } = Sequent.explode_sequent p in
656 let len = SeqHyp.length hyps in
657 let rec collect i vars indices =
658 if i > len then
659 indices
660 else
661 match SeqHyp.get hyps (i - 1) with
662 Hypothesis (v, hyp) ->
663 if List.mem v vars or intersects vars (free_vars hyp) then
664 collect (i + 1) (v :: vars) ((i, v, hyp) :: indices)
665 else
666 collect (i + 1) vars indices
667 | _ ->
668 collect (i + 1) vars indices
669 in
670 let rec tac indices goal =
671 match indices with
672 (i, v, hyp) :: tl ->
673 if is_var_free v goal then
674 let goal' = mk_all_term v hyp goal in
675 assertT goal'
676 thenLT [thinT i thenT tac tl goal';
677 withT (mk_var_term v) (dT (len + 1)) (**)
678 thenLT [memberAssumT i; nthHypT (len + 2)]]
679
680 else
681 let goal' = mk_implies_term hyp goal in
682 assertT goal'
683 thenLT [thinT i thenT tac tl goal';
684 (dT (len + 1)) thenLT [nthHypT i; nthHypT (-1)]]
685 | [] ->
686 idT
687 in
688 tac (collect 1 vars []) (Sequent.concl p) p
689
690 let moveToConclT i p =
691 let v, _ = Sequent.nth_hyp p i in
692 moveToConclVarsT [v] p
693
694 (*
695 * Decompose universal formulas.
696 *)
697 let univCDT =
698 let rec tac p =
699 let concl = Sequent.concl p in
700 if is_all_term concl
701 or is_dfun_term concl
702 or is_implies_term concl
703 or is_fun_term concl
704 then
705 (dT 0 thenMT tac) p
706 else
707 idT p
708 in
709 tac
710
711 let genUnivCDT =
712 let rec tac p =
713 let concl = Sequent.concl p in
714 if is_all_term concl
715 or is_dfun_term concl
716 or is_implies_term concl
717 or is_fun_term concl
718 or is_and_term concl
719 or is_prod_term concl
720 or is_iff_term concl
721 then
722 (dT 0 thenMT tac) p
723 else
724 idT p
725 in
726 tac
727
728 (*
729 * Instantiate a hyp with some arguments.
730 *)
731 let instHypT args i =
732 let rec inst i firstp args p =
733 match args with
734 [] ->
735 idT p
736 | arg :: args' ->
737 let _, hyp = Sequent.nth_hyp p i in
738 let tailT args =
739 if firstp then
740 inst ((Sequent.hyp_count p) + 1) false args
741 else
742 thinT i thenT inst i false args
743 in
744 if is_all_term hyp then
745 (withT arg (dT i) thenMT tailT args') p
746 else if is_dfun_term hyp then
747 (withT arg (dT i) thenMT (thinT (-1) thenT tailT args')) p
748 else if is_implies_term hyp or is_fun_term hyp then
749 (dT i thenMT tailT args) p
750 else
751 raise (RefineError ("instHypT", StringTermError ("hyp is not quantified", hyp)))
752 in
753 thinningT false (inst i true args)
754
755 (*
756 * This type is used to collect the arguments to instantiate.
757 *)
758 type formula_args =
759 AllTerm of string * term
760 | ImpliesTerm
761 | IffLeft
762 | IffRight
763
764 (*
765 * Print an info list.
766 *)
767 let eprint_info info =
768 let print_item = function
769 AllTerm (v, t) ->
770 eprintf "\tAllTerm %s: %a\n" v SimplePrint.print_simple_term_fp t
771 | ImpliesTerm ->
772 eprintf "\tImpliesTerm\n"
773 | IffLeft ->
774 eprintf "\tIffLeft\n"
775 | IffRight ->
776 eprintf "\tIffRight\n"
777 in
778 List.iter print_item info;
779 eprintf "\t.%t" eflush
780
781 (*
782 * Lookup and remove a value from an association list.
783 *)
784 let rec assoc v = function
785 (v', t) :: tl ->
786 if v' = v then
787 t, tl
788 else
789 let t', tl = assoc v tl in
790 t', (v', t) :: tl
791 | [] ->
792 raise Not_found
793
794 (*
795 * Check for exact matches.
796 *)
797 let check_subst subst =
798 let check (v, t) =
799 if !debug_auto then
800 eprintf "check_subst: checking %s/%a%t" v SimplePrint.print_simple_term_fp t eflush;
801 if not (is_var_term t & dest_var t = v) then
802 raise (RefineError ("check_subst", StringError "bad match"))
803 in
804 List.iter check subst
805
806 (*
807 * Instantiate the vars with the values in the substitution.
808 * If any vars in the subst don't match, they are global,
809 * and they should match exactly.
810 *)
811 let instantiate_vars args subst =
812 if !debug_auto then
813 begin
814 let print_subst (v, t) =
815 eprintf "\t%s: %a%t" v SimplePrint.print_simple_term_fp t eflush
816 in
817 eprintf "instantiate_vars: got subst\n";
818 List.iter print_subst subst
819 end;
820 let rec collect result args subst =
821 match args with
822 [] ->
823 check_subst subst;
824 result
825 | hd::tl ->
826 match hd with
827 AllTerm (v, t) ->
828 if !debug_auto then
829 eprintf "instantiate_vars: looking for %s%t" v eflush;
830 let t', subst' = assoc v subst in
831 collect (AllTerm (v, t') :: result) tl subst'
832 | ImpliesTerm
833 | IffLeft
834 | IffRight ->
835 collect (hd :: result) tl subst
836 in
837 collect [] args subst
838
839 (*
840 * Walk down an implication and look for the goal.
841 *)
842 let rec match_goal args form goal =
843 try
844 if !debug_auto then
845 eprintf "Matching form%t" eflush;
846 let subst = match_terms [] form goal in
847 let info = instantiate_vars args subst in
848 if !debug_auto then
849 eprintf "Form matched%t" eflush;
850 info
851 with
852 RefineError _ ->
853 if is_all_term form then
854 let v, v_T, v_P = dest_all form in
855 match_goal (AllTerm (v, v_T) :: args) v_P goal
856 else if is_dfun_term form then
857 let v, v_T, v_P = dest_dfun form in
858 match_goal (AllTerm (v, v_T) :: args) v_P goal
859 else if is_implies_term form then
860 let v_T, v_P = dest_implies form in
861 match_goal (ImpliesTerm :: args) v_P goal
862 else if is_fun_term form then
863 let v_T, v_P = dest_fun form in
864 match_goal (ImpliesTerm :: args) v_P goal
865 else if is_iff_term form then
866 let left, right = dest_iff form in
867 try match_goal (IffLeft :: args) left goal with
868 RefineError _ ->
869 match_goal (IffRight :: args) right goal
870 else
871 raise (RefineError ("match_goal", StringError "no match"))
872 | Not_found ->
873 raise (RefineError ("match_goal", StringError "no match"))
874
875 (*
876 * Try the universal #1.
877 *)
878 let backThruHypT i p =
879 if !debug_auto then
880 eprintf "Starting backThruHyp %d%t" i eflush;
881 let rec tac info i firstp p =
882 (match info with
883 [] ->
884 nthHypT i
885 | hd :: args ->
886 if !debug_auto then
887 eprintf "\tbackThruHyp step%t" eflush;
888 let tailT =
889 if firstp then
890 [idT; tac args ((Sequent.hyp_count p) + 1) false]
891 else
892 [thinT i; thinT i thenT tac args i false]
893 in
894 match hd with
895 ImpliesTerm ->
896 dT i thenLT tailT
897 | IffRight ->
898 dT i thenT thinT (i + 1) thenT dT i thenLT tailT
899 | IffLeft ->
900 dT i thenT thinT i thenT dT i thenLT tailT
901 | AllTerm (v, t) ->
902 withT t (dT i) thenLT tailT) p
903 in
904 let _, hyp = Sequent.nth_hyp p i in
905 let goal = Sequent.concl p in
906 let info = match_goal [] hyp goal in
907 if !debug_auto then
908 begin
909 eprintf "backThruHyp %d%t" i eflush;
910 eprint_info info
911 end;
912 thinningT false (tac info i true) p
913
914 (*
915 * We can also backchain through assumptions by pulling them
916 * in as universally quantified formulas.
917 * We assum that we can thin enough.
918 *
919 * This next function adds the assumption as a universlly
920 * quantified formula.
921 *)
922 let assumT i p =
923 let goal, assums = dest_msequent (Sequent.msequent p) in
924 let assum = List.nth assums (i - 1) in
925 let len = TermMan.num_hyps assum in
926
927 (*
928 * Compute the number of matching hyps.
929 * This is approximate. Right now, we look
930 * for the last context hyp.
931 *)
932 let rec last_match last_con hyp_index hyps =
933 if hyp_index > len then
934 last_con
935 else
936 match SeqHyp.get hyps (hyp_index - 1) with
937 Hypothesis _ ->
938 last_match last_con (hyp_index + 1) hyps
939 | Context _ ->
940 last_match (hyp_index + 1) (hyp_index + 1) hyps
941 in
942 let { sequent_hyps = hyps } = TermMan.explode_sequent assum in
943 let index = last_match 1 1 hyps in
944 let _ =
945 if !debug_auto then
946 eprintf "Last_match: %d%t" index eflush
947 in
948
949 (* Construct the assumption as a universal formula *)
950 let rec collect j =
951 if j > len then
952 TermMan.nth_concl assum 1
953 else
954 let v, hyp = TermMan.nth_hyp assum j in
955 let goal = collect (j + 1) in
956 if is_var_free v goal then
957 mk_all_term v hyp goal
958 else
959 mk_implies_term hyp goal
960 in
961 let form = collect index in
962 let _ =
963 if !debug_auto then
964 eprintf "Found assumption: %a%t" debug_print form eflush
965 in
966
967 (* Call intro form on each arg *)
968 let rec introT j p =
969 if j > len then
970 let goal, assums = dest_msequent (Sequent.msequent p) in
971 let assum = List.nth assums (i - 1) in
972 if is_squash_sequent goal then
973 if is_squash_sequent assum then
974 nthAssumT i p
975 else
976 (unsquashT (get_squash_arg assum) thenT nthAssumT i) p
977 else
978 nthAssumT i p
979 else
980 (dT 0 thenMT introT (j + 1)) p
981 in
982 (assertT form
983 thenLT [thinAllT index (TermMan.num_hyps goal) thenT introT index;
984 addHiddenLabelT "main"]) p
985
986 (*
987 * Now try backchaining through the assumption.
988 *)
989 let backThruAssumT i p =
990 let j = Sequent.hyp_count p + 1 in
991 (assumT i thenMT (backThruHypT j thenT thinT j)) p
992
993 (*
994 * Generalize on a membership assumption:
995 * i. sequent [...] { ... >- member{T; t} } -->
996 * ...
997 * sequent [...] { ... >- 'T2 }
998 * BY genAssumT [i; and any others you want to include...]
999 *
1000 * sequent [...] { ... >- all x: T. ...others... => T2 }
1001 *)
1002 let genAssumT indices p =
1003 let goal, assums = dest_msequent (Sequent.msequent p) in
1004 let len = List.length assums in
1005 let _ =
1006 List.iter (fun i ->
1007 if i <= 0 || i > len then
1008 raise (RefineError ("genAssumT", StringIntError ("assum index is out of range", i)))) indices
1009 in
1010 let rec make_gen_term t = function
1011 [] ->
1012 t
1013 | i :: indices ->
1014 let t = make_gen_term t indices in
1015 let t' = TermMan.nth_concl (List.nth assums (pred i)) 1 in
1016 if is_member_term t' then
1017 let t_type, t_var = dest_member t' in
1018 if is_var_term t_var then
1019 mk_all_term (dest_var t_var) t_type t
1020 else
1021 let v = maybe_new_vars1 p "v" in
1022 mk_all_term v t_type (var_subst t t_var v)
1023 else mk_implies_term t' t
1024 in
1025 let t = make_gen_term (TermMan.nth_concl goal 1) indices in
1026 (assertT t thenMT (backThruHypT (-1) thenT autoT) ) p
1027
1028 (************************************************************************
1029 * AUTO TACTIC *
1030 ************************************************************************)
1031
1032 (*
1033 * In auto tactic, Ok to decompose product hyps.
1034 *)
1035 let logic_trivT i p =
1036 let _, hyp = Sequent.nth_hyp p i in
1037 if is_void_term hyp or is_false_term hyp then
1038 dT i p
1039 else
1040 raise (RefineError ("logic_trivT", StringTermError ("nothing known about", hyp)))
1041
1042 let trivial_resource =
1043 Mp_resource.improve trivial_resource (**)
1044 { auto_name = "logic_trivT";
1045 auto_prec = trivial_prec;
1046 auto_tac = onSomeHypT logic_trivT
1047 }
1048
1049 (*
1050 * Backchaining in auto tactic.
1051 *)
1052 let logic_autoT i p =
1053 let _, hyp = Sequent.nth_hyp p i in
1054 if is_and_term hyp
1055 or is_prod_term hyp
1056 or is_dprod_term hyp
1057 or is_exists_term hyp
1058 then
1059 dT i p
1060 else
1061 raise (RefineError ("logic_autoT", StringError "unknown formula"))
1062
1063 let logic_prec = create_auto_prec [trivial_prec] []
1064 let back_hyp_prec = create_auto_prec [logic_prec] []
1065 let back_assum_prec = create_auto_prec [back_hyp_prec] []
1066
1067 let auto_resource =
1068 Mp_resource.improve auto_resource (**)
1069 { auto_name = "logic_autoT";
1070 auto_prec = logic_prec;
1071 auto_tac = auto_wrap (onSomeHypT logic_autoT)
1072 }
1073
1074 let auto_resource =
1075 Mp_resource.improve auto_resource (**)
1076 { auto_name = "backThruHypT";
1077 auto_prec = back_hyp_prec;
1078 auto_tac = auto_hyp_progress (fun _ _ -> true) backThruHypT
1079 }
1080
1081 (*
1082 * Quick test on assumptions.
1083 *)
1084 let assum_test i p =
1085 let goal, assums = dest_msequent (Sequent.msequent p) in
1086 let goal = TermMan.nth_concl goal 1 in
1087 let assum = List.nth assums (i - 1) in
1088 let goal' = TermMan.nth_concl assum 1 in
1089 try let _ = match_terms [] goal' goal in
1090 true
1091 with RefineError _ ->
1092 false
1093
1094 let auto_resource =
1095 Mp_resource.improve auto_resource (**)
1096 { auto_name = "backThruSomeAssumT";
1097 auto_prec = back_assum_prec;
1098 auto_tac = auto_assum_progress assum_test backThruAssumT
1099 }
1100
1101
1102
1103
1104 (************ logic instance for j-prover in refiner/reflib/jall.ml **********)
1105
1106 open Nuprl5
1107
1108 module Nuprl_JLogic =
1109 struct
1110 let is_all_term = nuprl_is_all_term
1111 let dest_all = nuprl_dest_all
1112 let is_exists_term = nuprl_is_exists_term
1113 let dest_exists = nuprl_dest_exists
1114 let is_and_term = nuprl_is_and_term
1115 let dest_and = nuprl_dest_and
1116 let is_or_term = nuprl_is_or_term
1117 let dest_or = nuprl_dest_or
1118 let is_implies_term = nuprl_is_implies_term
1119 let dest_implies = nuprl_dest_implies
1120 let is_not_term = nuprl_is_not_term
1121 let dest_not = nuprl_dest_not
1122 end
1123
1124
1125 module Itt_JLogic =
1126 struct
1127 let is_all_term = is_all_term
1128 let dest_all = dest_all
1129 let is_exists_term = is_exists_term
1130 let dest_exists = dest_exists
1131 let is_and_term = is_and_term
1132 let dest_and = dest_and
1133 let is_or_term = is_or_term
1134 let dest_or = dest_or
1135 let is_implies_term = is_implies_term
1136 let dest_implies = dest_implies
1137 let is_not_term = is_not_term
1138 let dest_not = dest_not
1139 end
1140
1141
1142 module ITT_JProver = Jall.JProver(Itt_JLogic) (* replace Itt_JLogic with Nuprl_JLogic for nv5 edd *)
1143
1144 let jtest t s c = ITT_JProver.test t s c
1145
1146
1147 let jprover t = ITT_JProver.prover t
1148
1149
1150 (* sequent calculus, another argumnet for proof reconstruction *)
1151
1152 (*
1153 * -*-
1154 * Local Variables:
1155 * Caml-master: "prlcomp.run"
1156 * End:
1157 * -*-
1158 *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26