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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (hide 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 jyh 2032 (*
2     * Regular logic connectives.
3     *
4 jyh 2456 * ----------------------------------------------------------------
5     *
6 jyh 2494 * This file is part of MetaPRL, a modular, higher order
7 jyh 2456 * 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 jyh 2525 *
15 jyh 2456 * 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 jyh 2525 *
20 jyh 2456 * 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 jyh 2525 *
25 jyh 2456 * 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 jyh 2525 *
29 jyh 2456 * Author: Jason Hickey
30     * jyh@cs.cornell.edu
31     *
32 jyh 2032 *)
33    
34     include Itt_equal
35 jyh 2376 include Itt_rfun
36     include Itt_dfun
37     include Itt_fun
38 jyh 2032 include Itt_dprod
39 jyh 2376 include Itt_prod
40 jyh 2032 include Itt_union
41     include Itt_void
42 jyh 2047 include Itt_unit
43 jyh 2325 include Itt_struct
44 jyh 2032
45 jyh 2152 open Printf
46 jyh 2494 open Mp_debug
47 jyh 2209 open Refiner.Refiner
48 jyh 2190 open Refiner.Refiner.Term
49 nogin 2347 open Refiner.Refiner.TermType
50 jyh 2209 open Refiner.Refiner.TermOp
51     open Refiner.Refiner.TermMan
52 jyh 2325 open Refiner.Refiner.TermSubst
53     open Refiner.Refiner.Refine
54 jyh 2283 open Refiner.Refiner.RefineError
55 jyh 2494 open Mp_resource
56 nogin 2356 open Simple_print
57 jyh 2150
58 jyh 2743 open Tactic_type
59     open Tactic_type.Tacticals
60     open Tactic_type.Conversionals
61 jyh 2494 open Mptop
62 jyh 2376 open Var
63 jyh 2325
64     open Base_auto_tactic
65     open Base_dtactic
66    
67     open Itt_squash
68     open Itt_void
69 jyh 2150 open Itt_equal
70 jyh 2325 open Itt_rfun
71     open Itt_dprod
72     open Itt_struct
73 jyh 2150
74 jyh 2152 (*
75     * Show that the file is loading.
76     *)
77     let _ =
78 nogin 2822 show_loading "Loading Itt_logic%t"
79 jyh 2152
80 jyh 2325 let debug_auto =
81     create_debug (**)
82     { debug_name = "auto";
83     debug_description = "Display auto tactic operations";
84     debug_value = false
85     }
86    
87 jyh 2032 (************************************************************************
88     * REWRITES *
89     ************************************************************************)
90    
91 nogin 2674 declare "prop"[i:l]
92 jyh 2244
93 jyh 2047 declare "true"
94     declare "false"
95 jyh 2032 declare "not"{'a}
96 jyh 2309 declare "iff"{'a; 'b}
97 jyh 2032 declare "implies"{'a; 'b}
98     declare "and"{'a; 'b}
99     declare "or"{'a; 'b}
100 jyh 2380 declare "cand"{'a; 'b}
101     declare "cor"{'a; 'b}
102 jyh 2032 declare "all"{'A; x. 'B['x]}
103     declare "exists"{'A; x. 'B['x]}
104    
105 nogin 2674 prim_rw unfold_prop : "prop"[i:l] <--> "univ"[i:l]
106 jyh 2032
107 jyh 2669 prim_rw unfold_true : "true" <--> unit
108     prim_rw unfold_false : "false" <--> void
109 jyh 2743 prim_rw unfold_not : "not"{'a} <--> ('a -> void)
110     prim_rw unfold_implies : ('a => 'b) <--> ('a -> 'b)
111 jyh 2669 prim_rw unfold_iff : "iff"{'a; 'b} <--> (('a -> 'b) & ('b -> 'a))
112 jyh 2743 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 jyh 2669 prim_rw unfold_cor : "cor"{'a; 'b} <--> "or"{'a; ."cand"{."not"{'a}; 'b}}
116 jyh 2743 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 jyh 2244
119 jyh 2669 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 jyh 2244
131 jyh 2032 (************************************************************************
132 jyh 2314 * RULES *
133     ************************************************************************)
134    
135     (*
136 jyh 2376 * True and false.
137     *)
138 jyh 2743 interactive true_univ {| intro_resource []; eqcd_resource |} 'H :
139 nogin 2674 sequent ['ext] { 'H >- "true" = "true" in univ[i:l] }
140 jyh 2376
141 jyh 2775 interactive true_member {| intro_resource [] |} 'H :
142     sequent ['ext] { 'H >- member{univ[i:l]; ."true"} }
143    
144 jyh 2743 interactive true_type {| intro_resource [] |} 'H :
145 jyh 2376 sequent ['ext] { 'H >- "type"{."true"} }
146    
147 jyh 2743 interactive true_intro {| intro_resource [] |} 'H :
148 jyh 2376 sequent ['ext] { 'H >- "true" }
149    
150 jyh 2743 interactive false_univ {| intro_resource []; eqcd_resource |} 'H :
151 nogin 2674 sequent ['ext] { 'H >- "false" = "false" in univ[i:l] }
152 jyh 2376
153 jyh 2775 interactive false_member {| intro_resource [] |} 'H :
154     sequent ['ext] { 'H >- "member"{univ[i:l]; ."false"} }
155    
156 jyh 2743 interactive false_type {| intro_resource [] |} 'H :
157 jyh 2376 sequent ['ext] { 'H >- "type"{."false"} }
158    
159 jyh 2753 interactive false_elim {| elim_resource [ThinOption thinT] |} 'H 'J :
160 jyh 2376 sequent ['ext] { 'H; x: "false"; 'J['x] >- 'C['x] }
161    
162 jyh 2525 interactive false_squash 'H :
163     sequent [squash] { 'H >- "false" } -->
164     sequent ['ext] { 'H >- "false" }
165    
166 jyh 2376 (*
167     * Negation.
168     *)
169 jyh 2743 interactive not_univ {| intro_resource []; eqcd_resource |} 'H :
170     [wf] sequent [squash] { 'H >- 't1 = 't2 in univ[i:l] } -->
171 nogin 2674 sequent ['ext] { 'H >- "not"{'t1} = "not"{'t2} in univ[i:l] }
172 jyh 2376
173 jyh 2775 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 jyh 2743 interactive not_type {| intro_resource [] |} 'H :
178     [wf] sequent [squash] { 'H >- "type"{'t} } -->
179 jyh 2376 sequent ['ext] { 'H >- "type"{."not"{'t}} }
180    
181 jyh 2743 interactive not_intro {| intro_resource [] |} 'H 'x :
182     [wf] sequent [squash] { 'H >- "type"{'t} } -->
183     [main] sequent ['ext] { 'H; x: 't >- "false" } -->
184 jyh 2376 sequent ['ext] { 'H >- "not"{'t} }
185    
186 jyh 2753 interactive not_elim {| elim_resource [] |} 'H 'J :
187 jyh 2743 [assertion] sequent ['ext] { 'H; x: "not"{'t}; 'J['x] >- 't } -->
188 jyh 2376 sequent ['ext] { 'H; x: "not"{'t}; 'J['x] >- 'C }
189    
190     (*
191     * Conjunction.
192     *)
193 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "and"{'a1; 'a2} = "and"{'b1; 'b2} in univ[i:l] }
197 jyh 2376
198 jyh 2775 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 jyh 2743 interactive and_type {| intro_resource [] |} 'H :
204     [wf] sequent [squash] { 'H >- "type"{'a1} } -->
205     [wf] sequent [squash] { 'H >- "type"{'a2} } -->
206 jyh 2376 sequent ['ext] { 'H >- "type"{."and"{'a1; 'a2}} }
207    
208 jyh 2743 interactive and_intro {| intro_resource [] |} 'H :
209     [wf] sequent ['ext] { 'H >- 'a1 } -->
210     [wf] sequent ['ext] { 'H >- 'a2 } -->
211 jyh 2376 sequent ['ext] { 'H >- "and"{'a1; 'a2} }
212    
213 jyh 2753 interactive and_elim {| elim_resource [] |} 'H 'J 'y 'z :
214 jyh 2743 [main] sequent ['ext] { 'H; y: 'a1; z: 'a2; 'J['y, 'z] >- 'C['y, 'z] } -->
215 jyh 2376 sequent ['ext] { 'H; x: "and"{'a1; 'a2}; 'J['x] >- 'C['x] }
216    
217     (*
218     * Disjunction.
219     *)
220 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "or"{'a1; 'a2} = "or"{'b1; 'b2} in univ[i:l] }
224 jyh 2376
225 jyh 2775 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 jyh 2743 interactive or_type {| intro_resource [] |} 'H :
231     [wf] sequent [squash] { 'H >- "type"{'a1} } -->
232     [wf] sequent [squash] { 'H >- "type"{'a2} } -->
233 jyh 2376 sequent ['ext] { 'H >- "type"{."or"{'a1; 'a2}} }
234    
235 jyh 2743 interactive or_intro_left {| intro_resource [SelectOption 1] |} 'H :
236     [wf] sequent [squash] { 'H >- "type"{.'a2} } -->
237     [main] sequent ['ext] { 'H >- 'a1 } -->
238 jyh 2376 sequent ['ext] { 'H >- "or"{'a1; 'a2} }
239    
240 jyh 2743 interactive or_intro_right {| intro_resource [SelectOption 2] |} 'H :
241     [wf] sequent [squash] { 'H >- "type"{.'a1} } -->
242     [main] sequent ['ext] { 'H >- 'a2 } -->
243 jyh 2376 sequent ['ext] { 'H >- "or"{'a1; 'a2} }
244    
245 jyh 2753 interactive or_elim {| elim_resource [] |} 'H 'J 'y :
246 jyh 2743 [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 jyh 2376 sequent ['ext] { 'H; x: "or"{'a1; 'a2}; 'J['x] >- 'C['x] }
249    
250     (*
251     * Implication.
252     *)
253 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "implies"{'a1; 'a2} = "implies"{'b1; 'b2} in univ[i:l] }
257 jyh 2376
258 jyh 2775 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 jyh 2743 interactive implies_type {| intro_resource [] |} 'H :
264     [wf] sequent [squash] { 'H >- "type"{'a1} } -->
265     [wf] sequent [squash] { 'H >- "type"{'a2} } -->
266 jyh 2376 sequent ['ext] { 'H >- "type"{."implies"{'a1; 'a2}} }
267    
268 jyh 2743 interactive implies_intro {| intro_resource [] |} 'H 'x :
269     [wf] sequent [squash] { 'H >- "type"{'a1} } -->
270     [main] sequent ['ext] { 'H; x: 'a1 >- 'a2 } -->
271 jyh 2376 sequent ['ext] { 'H >- "implies"{'a1; 'a2} }
272    
273 jyh 2753 interactive implies_elim {| elim_resource [ThinOption thinT] |} 'H 'J 'y :
274 jyh 2743 [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 jyh 2376 sequent ['ext] { 'H; x: "implies"{'a1; 'a2}; 'J['x] >- 'C['x] }
277    
278     (*
279     * Bi-implication.
280     *)
281 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "iff"{'a1; 'a2} = "iff"{'b1; 'b2} in univ[i:l] }
285 jyh 2376
286 jyh 2775 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 jyh 2743 interactive iff_type {| intro_resource [] |} 'H :
292     [wf] sequent [squash] { 'H >- "type"{'a1} } -->
293     [wf] sequent [squash] { 'H >- "type"{'a2} } -->
294 jyh 2376 sequent ['ext] { 'H >- "type"{."iff"{'a1; 'a2}} }
295    
296 jyh 2743 interactive iff_intro {| intro_resource [] |} 'H :
297     [wf] sequent ['ext] { 'H >- 'a1 => 'a2 } -->
298     [wf] sequent ['ext] { 'H >- 'a2 => 'a1 } -->
299 jyh 2376 sequent ['ext] { 'H >- "iff"{'a1; 'a2} }
300    
301 jyh 2753 interactive iff_elim {| elim_resource [] |} 'H 'J 'y 'z :
302 jyh 2376 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 jyh 2380 * Conjunction.
307     *)
308 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "cand"{'a1; 'a2} = "cand"{'b1; 'b2} in univ[i:l] }
312 jyh 2380
313 jyh 2775 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 jyh 2743 interactive cand_type {| intro_resource [] |} 'H 'x :
319     [wf] sequent [squash] { 'H >- "type"{'a1} } -->
320     [wf] sequent [squash] { 'H; x: 'a1 >- "type"{'a2} } -->
321 jyh 2380 sequent ['ext] { 'H >- "type"{."cand"{'a1; 'a2}} }
322    
323 jyh 2743 interactive cand_intro {| intro_resource [] |} 'H 'x :
324     [main] sequent ['ext] { 'H >- 'a1 } -->
325     [main] sequent ['ext] { 'H; x: 'a1 >- 'a2 } -->
326 jyh 2380 sequent ['ext] { 'H >- "cand"{'a1; 'a2} }
327    
328 jyh 2753 interactive cand_elim {| elim_resource [] |} 'H 'J 'y 'z :
329 jyh 2743 [main] sequent ['ext] { 'H; y: 'a1; z: 'a2; 'J['y, 'z] >- 'C['y, 'z] } -->
330 jyh 2380 sequent ['ext] { 'H; x: "cand"{'a1; 'a2}; 'J['x] >- 'C['x] }
331    
332     (*
333     * Disjunction.
334     *)
335 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "cor"{'a1; 'a2} = "cor"{'b1; 'b2} in univ[i:l] }
339 jyh 2380
340 jyh 2775 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 jyh 2743 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 jyh 2380 sequent ['ext] { 'H >- "type"{."cor"{'a1; 'a2}} }
349    
350 jyh 2743 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 jyh 2380 sequent ['ext] { 'H >- "cor"{'a1; 'a2} }
354    
355 jyh 2743 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 jyh 2380 sequent ['ext] { 'H >- "cor"{'a1; 'a2} }
360    
361 jyh 2753 interactive cor_elim {| elim_resource [] |} 'H 'J 'u 'v :
362 jyh 2743 [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 jyh 2380 sequent ['ext] { 'H; x: "cor"{'a1; 'a2}; 'J['x] >- 'C['x] }
365    
366     (*
367 jyh 2325 * All elimination performs a thinning
368     *)
369 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "all"{'t1; x1. 'b1['x1]} = "all"{'t2; x2. 'b2['x2]} in univ[i:l] }
373 jyh 2376
374 jyh 2775 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 jyh 2743 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 jyh 2376 sequent ['ext] { 'H >- "type"{."all"{'t; v. 'b['v]}} }
383    
384 jyh 2743 interactive all_intro {| intro_resource [] |} 'H 'x :
385     [wf] sequent [squash] { 'H >- "type"{'t} } -->
386     [main] sequent ['ext] { 'H; x: 't >- 'b['x] } -->
387 jyh 2376 sequent ['ext] { 'H >- "all"{'t; v. 'b['v]} }
388    
389 jyh 2753 interactive all_elim {| elim_resource [ThinOption thinT] |} 'H 'J 'w 'z :
390 jyh 2743 [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 jyh 2325 sequent ['ext] { 'H; x: all a: 'A. 'B['a]; 'J['x] >- 'C['x] }
393    
394     (*
395 jyh 2376 * Existential.
396 jyh 2314 *)
397 jyh 2743 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 nogin 2674 sequent ['ext] { 'H >- "exists"{'t1; x1. 'b1['x1]} = "exists"{'t2; x2. 'b2['x2]} in univ[i:l] }
401 jyh 2314
402 jyh 2775 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 jyh 2743 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 jyh 2376 sequent ['ext] { 'H >- "type"{."exists"{'t; v. 'b['v]}} }
411    
412 jyh 2743 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 jyh 2376 sequent ['ext] { 'H >- "exists"{'t; v. 'b['v]} }
417    
418 jyh 2753 interactive exists_elim {| elim_resource [] |} 'H 'J 'y 'z :
419 jyh 2743 [main] sequent ['ext] { 'H; y: 'a; z: 'b['y]; 'J['y, 'z] >- 'C['y, 'z] } -->
420 jyh 2376 sequent ['ext] { 'H; x: exst v: 'a. 'b['v]; 'J['x] >- 'C['x] }
421    
422 jyh 2314 (************************************************************************
423 jyh 2032 * DISPLAY FORMS *
424     ************************************************************************)
425    
426 jyh 2309 prec prec_iff
427 jyh 2032 prec prec_implies
428     prec prec_and
429     prec prec_or
430 jyh 2529 prec prec_not
431 jyh 2032 prec prec_quant
432    
433 jyh 2309 prec prec_implies < prec_iff
434     prec prec_iff < prec_or
435 jyh 2268 prec prec_or < prec_and
436 jyh 2529 prec prec_and < prec_not
437 jyh 2309 prec prec_quant < prec_iff
438 jyh 2268
439 jyh 2209 dform true_df1 : mode[src] :: "true" = `"True"
440 jyh 2047
441 jyh 2209 dform false_df1 : mode[src] :: "false" = `"False"
442 jyh 2047
443 jyh 2209 dform not_df1 : mode[src] :: parens :: "prec"[prec_implies] :: "not"{'a} =
444 eli 2677 `"not " slot["le"]{'a}
445 jyh 2032
446 jyh 2209 dform implies_df1 : mode[src] :: parens :: "prec"[prec_implies] :: implies{'a; 'b} =
447 eli 2677 slot["le"]{'a} `" => " slot["lt"]{'b}
448 jyh 2209
449 jyh 2309 dform iff_df1 : mode[src] :: parens :: "prec"[prec_iff] :: iff{'a; 'b} =
450 eli 2677 slot["le"]{'a} `" <==> " slot["lt"]{'b}
451 jyh 2309
452 jyh 2209 dform and_df1 : mode[src] :: parens :: "prec"[prec_and] :: "and"{'a; 'b} =
453 nogin 2773 slot["le"]{'a} `" or " slot["lt"]{'b}
454 jyh 2209
455     dform or_df1 : mode[src] :: parens :: "prec"[prec_or] :: "or"{'a; 'b} =
456 nogin 2773 slot["le"]{'a} `" and " slot["lt"]{'b}
457 jyh 2209
458 jyh 2272 dform all_df1 : mode[src] :: parens :: "prec"[prec_quant] :: "all"{'A; x. 'B} =
459     `"all " slot{'x} `": " slot{'A}`"." slot{'B}
460 jyh 2032
461 jyh 2272 dform exists_df1 : mode[src] :: parens :: "prec"[prec_quant] :: "exists"{'A; x. 'B} =
462     `"exists " slot{'x} `": " slot{'A} `"." slot{'B}
463 jyh 2032
464 jyh 2808 dform true_df2 : "true" =
465 jyh 2325 `"True"
466    
467 jyh 2808 dform false_df2 : "false" =
468 jyh 2325 `"False"
469    
470 jyh 2808 dform not_df2 : parens :: "prec"[prec_not] :: "not"{'a} =
471 eli 2677 Nuprl_font!tneg slot["le"]{'a}
472 jyh 2209
473 jyh 2808 dform implies_df2 : parens :: "prec"[prec_implies] :: implies{'a; 'b} =
474 eli 2677 slot["le"]{'a} " " Nuprl_font!Rightarrow " " slot["lt"]{'b}
475 jyh 2209
476 jyh 2808 dform iff_df2 : parens :: "prec"[prec_iff] :: iff{'a; 'b} =
477 eli 2677 slot["le"]{'a} " " Nuprl_font!Leftrightarrow " " slot["lt"]{'b}
478 jyh 2309
479 jyh 2376 (*
480     * Disjunction.
481     *)
482     declare or_df{'a}
483    
484 nogin 2773 dform or_df2 : parens :: "prec"[prec_or] :: "or"{'a; 'b} =
485 jyh 2529 szone pushm[0] slot["le"]{'a} or_df{'b} popm ezone
486 jyh 2209
487 nogin 2773 dform or_df3 : or_df{."or"{'a; 'b}} =
488 jyh 2529 hspace Nuprl_font!vee " " slot["le"]{'a} or_df{'b}
489 jyh 2376
490 nogin 2773 dform or_df4 : or_df{'a} =
491 jyh 2376 hspace Nuprl_font!vee " " slot{'a}
492    
493     (*
494 jyh 2775 * 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 jyh 2376 * Quantifiers.
509     *)
510 nogin 2773 dform all_df2 : parens :: "prec"[prec_quant] :: "all"{'A; x. 'B} =
511 jyh 2272 pushm[3] Nuprl_font!forall slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
512 jyh 2032
513 jyh 2808 dform exists_df2 : parens :: "prec"[prec_quant] :: "exists"{'A; x. 'B} =
514 jyh 2314 pushm[3] Nuprl_font!"exists" slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
515 jyh 2032
516     (************************************************************************
517     * TACTICS *
518     ************************************************************************)
519 jyh 2047
520     let true_term = << "true" >>
521 jyh 2531 let true_opname = opname_of_term true_term
522     let is_true_term = is_no_subterms_term true_opname
523 jyh 2047
524     let false_term = << "false" >>
525 jyh 2531 let false_opname = opname_of_term false_term
526     let is_false_term = is_no_subterms_term false_opname
527 jyh 2047
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 jyh 2209
534 jyh 2061 let exists_term = << exst x: 'A. 'B['x] >>
535 jyh 2047 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 jyh 2209
540 jyh 2047 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 jyh 2209
546 jyh 2047 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 jyh 2209
552 jyh 2380 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 jyh 2047 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 jyh 2209
570 jyh 2309 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 jyh 2320 let not_term = << "not"{'a} >>
577 jyh 2047 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 jyh 2209
582 jyh 2032 (*
583 jyh 2525 * Squash elimination.
584     *)
585     let squash_falseT p =
586     false_squash (Sequent.hyp_count_addr p) p
587    
588 jyh 2047 (************************************************************************
589     * TYPE INFERENCE *
590     ************************************************************************)
591    
592 jyh 2032 (*
593 jyh 2047 * Type of true, false.
594     *)
595     let inf_univ1 _ decl _ = decl, univ1_term
596    
597 jyh 2629 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 jyh 2047
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 jyh 2420 let decl'', b' = f (add_unify_subst v a decl') b in
607 jyh 2283 let le1, le2 = dest_univ a', dest_univ b' in
608 jyh 2669 decl'', Itt_equal.mk_univ_term (max_level_exp le1 le2 0)
609 jyh 2047
610 jyh 2629 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 jyh 2047
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 jyh 2283 let le1, le2 = dest_univ a', dest_univ b' in
621 jyh 2669 decl'', Itt_equal.mk_univ_term (max_level_exp le1 le2 0)
622 jyh 2047
623 jyh 2629 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 jyh 2047
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 jyh 2629 let typeinf_resource = Mp_resource.improve typeinf_resource (not_term, inf_not)
636 jyh 2047
637 jyh 2325 (************************************************************************
638     * AUTOMATION *
639     ************************************************************************)
640    
641 jyh 2047 (*
642 jyh 2333 * 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 jyh 2743 let { sequent_hyps = hyps } = Sequent.explode_sequent p in
656 nogin 2347 let len = SeqHyp.length hyps in
657 jyh 2337 let rec collect i vars indices =
658     if i > len then
659 jyh 2333 indices
660 jyh 2337 else
661 nogin 2347 match SeqHyp.get hyps (i - 1) with
662 jyh 2337 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 jyh 2333 in
670     let rec tac indices goal =
671     match indices with
672     (i, v, hyp) :: tl ->
673 nogin 2905 if is_var_free v goal then
674 jyh 2333 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 jyh 2525 thenLT [memberAssumT i; nthHypT (len + 2)]]
679 jyh 2333
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 jyh 2337 tac (collect 1 vars []) (Sequent.concl p) p
689 jyh 2333
690     let moveToConclT i p =
691 jyh 2743 let v, _ = Sequent.nth_hyp p i in
692 jyh 2333 moveToConclVarsT [v] p
693    
694     (*
695 jyh 2325 * Decompose universal formulas.
696     *)
697 jyh 2743 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 jyh 2325
711 jyh 2743 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 jyh 2325
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 jyh 2743 let _, hyp = Sequent.nth_hyp p i in
738 jyh 2325 let tailT args =
739     if firstp then
740 jyh 2743 inst ((Sequent.hyp_count p) + 1) false args
741 jyh 2325 else
742     thinT i thenT inst i false args
743     in
744 jyh 2333 if is_all_term hyp then
745 jyh 2325 (withT arg (dT i) thenMT tailT args') p
746 jyh 2333 else if is_dfun_term hyp then
747     (withT arg (dT i) thenMT (thinT (-1) thenT tailT args')) p
748 jyh 2325 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 jyh 2775 thinningT false (inst i true args)
754 jyh 2325
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 nogin 2356 eprintf "\tAllTerm %s: %a\n" v SimplePrint.print_simple_term_fp t
771 jyh 2325 | 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 nogin 2356 eprintf "check_subst: checking %s/%a%t" v SimplePrint.print_simple_term_fp t eflush;
801 jyh 2325 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 nogin 2356 eprintf "\t%s: %a%t" v SimplePrint.print_simple_term_fp t eflush
816 jyh 2325 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 jyh 2743 [idT; tac args ((Sequent.hyp_count p) + 1) false]
891 jyh 2325 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 jyh 2743 let _, hyp = Sequent.nth_hyp p i in
905 jyh 2325 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 jyh 2775 thinningT false (tac info i true) p
913 jyh 2325
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 jyh 2337 let rec last_match last_con hyp_index hyps =
933     if hyp_index > len then
934 jyh 2325 last_con
935 jyh 2337 else
936 nogin 2347 match SeqHyp.get hyps (hyp_index - 1) with
937 jyh 2325 Hypothesis _ ->
938 jyh 2337 last_match last_con (hyp_index + 1) hyps
939 jyh 2325 | Context _ ->
940 jyh 2380 last_match (hyp_index + 1) (hyp_index + 1) hyps
941 jyh 2325 in
942     let { sequent_hyps = hyps } = TermMan.explode_sequent assum in
943     let index = last_match 1 1 hyps in
944 jyh 2380 let _ =
945     if !debug_auto then
946     eprintf "Last_match: %d%t" index eflush
947     in
948 jyh 2325
949     (* Construct the assumption as a universal formula *)
950     let rec collect j =
951 jyh 2380 if j > len then
952     TermMan.nth_concl assum 1
953 jyh 2325 else
954     let v, hyp = TermMan.nth_hyp assum j in
955 jyh 2333 let goal = collect (j + 1) in
956 nogin 2905 if is_var_free v goal then
957 jyh 2333 mk_all_term v hyp goal
958     else
959     mk_implies_term hyp goal
960 jyh 2325 in
961     let form = collect index in
962     let _ =
963     if !debug_auto then
964 jyh 2380 eprintf "Found assumption: %a%t" debug_print form eflush
965 jyh 2325 in
966    
967     (* Call intro form on each arg *)
968     let rec introT j p =
969 jyh 2380 if j > len then
970 jyh 2325 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 jyh 2380 thenLT [thinAllT index (TermMan.num_hyps goal) thenT introT index;
984 jyh 2325 addHiddenLabelT "main"]) p
985    
986     (*
987     * Now try backchaining through the assumption.
988     *)
989     let backThruAssumT i p =
990 jyh 2743 let j = Sequent.hyp_count p + 1 in
991 jyh 2325 (assumT i thenMT (backThruHypT j thenT thinT j)) p
992    
993 jyh 2786 (*
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 nogin 2790 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 jyh 2786 if is_var_term t_var then
1019 nogin 2790 mk_all_term (dest_var t_var) t_type t
1020 jyh 2786 else
1021     let v = maybe_new_vars1 p "v" in
1022 nogin 2790 mk_all_term v t_type (var_subst t t_var v)
1023     else mk_implies_term t' t
1024 jyh 2786 in
1025 nogin 2790 let t = make_gen_term (TermMan.nth_concl goal 1) indices in
1026     (assertT t thenMT (backThruHypT (-1) thenT autoT) ) p
1027 jyh 2786
1028 jyh 2325 (************************************************************************
1029     * AUTO TACTIC *
1030     ************************************************************************)
1031    
1032     (*
1033     * In auto tactic, Ok to decompose product hyps.
1034     *)
1035     let logic_trivT i p =
1036 jyh 2743 let _, hyp = Sequent.nth_hyp p i in
1037 jyh 2325 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 jyh 2629 Mp_resource.improve trivial_resource (**)
1044 jyh 2325 { 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 jyh 2743 let _, hyp = Sequent.nth_hyp p i in
1054 jyh 2325 if is_and_term hyp
1055     or is_prod_term hyp
1056     or is_dprod_term hyp
1057 jyh 2326 or is_exists_term hyp
1058 jyh 2325 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 jyh 2629 Mp_resource.improve auto_resource (**)
1069 jyh 2325 { auto_name = "logic_autoT";
1070     auto_prec = logic_prec;
1071     auto_tac = auto_wrap (onSomeHypT logic_autoT)
1072     }
1073    
1074     let auto_resource =
1075 jyh 2629 Mp_resource.improve auto_resource (**)
1076 jyh 2325 { 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 jyh 2380 let goal = TermMan.nth_concl goal 1 in
1087 jyh 2325 let assum = List.nth assums (i - 1) in
1088 jyh 2380 let goal' = TermMan.nth_concl assum 1 in
1089 nogin 2578 try let _ = match_terms [] goal' goal in
1090 jyh 2669 true
1091 nogin 2578 with RefineError _ ->
1092     false
1093 jyh 2325
1094     let auto_resource =
1095 jyh 2629 Mp_resource.improve auto_resource (**)
1096 jyh 2325 { auto_name = "backThruSomeAssumT";
1097     auto_prec = back_assum_prec;
1098     auto_tac = auto_assum_progress assum_test backThruAssumT
1099     }
1100    
1101 steph 2880
1102    
1103    
1104     (************ logic instance for j-prover in refiner/reflib/jall.ml **********)
1105    
1106 lolorigo 2922 open Nuprl5
1107 steph 2880
1108 lolorigo 2922 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 steph 2880 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 lolorigo 2922 module ITT_JProver = Jall.JProver(Itt_JLogic) (* replace Itt_JLogic with Nuprl_JLogic for nv5 edd *)
1143 steph 2880
1144 steph 2921 let jtest t s c = ITT_JProver.test t s c
1145 steph 2880
1146 steph 2921
1147     let jprover t = ITT_JProver.prover t
1148    
1149    
1150     (* sequent calculus, another argumnet for proof reconstruction *)
1151    
1152 jyh 2325 (*
1153 jyh 2032 * -*-
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