|
1 |
|
2 open Goals; |
|
3 open Unify; |
|
4 open USyntax; |
|
5 open Utils; |
|
6 open Envir; |
|
7 open Tfl; |
|
8 open Rules; |
|
9 |
|
10 goal Main.thy "A -->A"; |
|
11 by Auto_tac; |
|
12 qed "foo"; |
|
13 |
|
14 |
|
15 val Mainsign = #sign (rep_thm foo); |
|
16 |
|
17 |
|
18 |
|
19 (*val myhol = sign_of thy;*) |
|
20 |
|
21 val myenv = empty 0; |
|
22 |
|
23 |
|
24 val gcounter = ref 0; |
|
25 |
|
26 exception NOMATES; |
|
27 exception UNMATEABLE; |
|
28 exception NOTSOME; |
|
29 exception UNSPANNED; |
|
30 |
|
31 fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; |
|
32 |
|
33 fun dest_neg(Const("Not",_) $ M) = M |
|
34 | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; |
|
35 |
|
36 fun is_abs t = can dest_abs t; |
|
37 fun is_comb t = can dest_comb t; |
|
38 |
|
39 fun iscomb a = if is_Free a then |
|
40 false |
|
41 else if is_Var a then |
|
42 false |
|
43 else if is_conj a then |
|
44 false |
|
45 else if is_disj a then |
|
46 false |
|
47 else if is_forall a then |
|
48 false |
|
49 else if is_exists a then |
|
50 false |
|
51 else |
|
52 true; |
|
53 fun getstring (Var (v,T)) = fst v |
|
54 |getstring (Free (v,T))= v; |
|
55 |
|
56 |
|
57 fun getindexstring ((a:string),(b:int))= a; |
|
58 |
|
59 fun getstrings (a,b) = let val astring = getstring a |
|
60 val bstring = getstring b in |
|
61 (astring,bstring) |
|
62 end; |
|
63 |
|
64 |
|
65 fun alltrue [] = true |
|
66 |alltrue (true::xs) = true andalso (alltrue xs) |
|
67 |alltrue (false::xs) = false; |
|
68 |
|
69 fun allfalse [] = true |
|
70 |allfalse (false::xs) = true andalso (allfalse xs) |
|
71 |allfalse (true::xs) = false; |
|
72 |
|
73 fun not_empty [] = false |
|
74 | not_empty _ = true; |
|
75 |
|
76 fun twoisvar (a,b) = is_Var b; |
|
77 fun twoisfree (a,b) = is_Free b; |
|
78 fun twoiscomb (a,b) = iscomb b; |
|
79 |
|
80 fun strequalfirst a (b,c) = (getstring a) = (getstring b); |
|
81 |
|
82 fun fstequal a b = a = fst b; |
|
83 |
|
84 fun takeout (i,[]) = [] |
|
85 | takeout (i,(x::xs)) = if (i>0) then |
|
86 (x::(takeout(i-1,xs))) |
|
87 else |
|
88 []; |
|
89 |
|
90 |
|
91 |
|
92 (* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *) |
|
93 fun is_Abs (Abs _) = true |
|
94 | is_Abs _ = false; |
|
95 fun is_Bound (Bound _) = true |
|
96 | is_Bound _ = false; |
|
97 |
|
98 |
|
99 |
|
100 |
|
101 fun is_hol_tm t = |
|
102 if (is_Free t) then |
|
103 true |
|
104 else if (is_Var t) then |
|
105 true |
|
106 else if (is_Const t) then |
|
107 true |
|
108 else if (is_Abs t) then |
|
109 true |
|
110 else if (is_Bound t) then |
|
111 true |
|
112 else |
|
113 let val (f, args) = strip_comb t in |
|
114 if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then |
|
115 true (* should be is_const *) |
|
116 else |
|
117 false |
|
118 end; |
|
119 |
|
120 fun is_hol_fm f = if is_neg f then |
|
121 let val newf = dest_neg f in |
|
122 is_hol_fm newf |
|
123 end |
|
124 |
|
125 else if is_disj f then |
|
126 let val {disj1,disj2} = dest_disj f in |
|
127 (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *) |
|
128 end |
|
129 else if is_conj f then |
|
130 let val {conj1,conj2} = dest_conj f in |
|
131 (is_hol_fm conj1) andalso (is_hol_fm conj2) |
|
132 end |
|
133 else if (is_forall f) then |
|
134 let val {Body, Bvar} = dest_forall f in |
|
135 is_hol_fm Body |
|
136 end |
|
137 else if (is_exists f) then |
|
138 let val {Body, Bvar} = dest_exists f in |
|
139 is_hol_fm Body |
|
140 end |
|
141 else if (iscomb f) then |
|
142 let val (P, args) = strip_comb f in |
|
143 ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args)) |
|
144 end |
|
145 else |
|
146 is_hol_tm f; (* should be is_const, nee |
|
147 d to check args *) |
|
148 |
|
149 |
|
150 fun hol_literal t = (is_hol_fm t) andalso ( not ((is_conj t) orelse (is_disj t) orelse (is_forall t) orelse (is_exists t))); |
|
151 |
|
152 |
|
153 |
|
154 |
|
155 (*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *) |
|
156 fun getcombvar a = let val {Rand = rand, Rator = rator} = dest_comb a in |
|
157 if (iscomb rand) then |
|
158 getcombvar rand |
|
159 else |
|
160 rand |
|
161 end; |
|
162 |
|
163 |
|
164 |
|
165 fun free2var v = let val thing = dest_Free v |
|
166 val (name,vtype) = thing |
|
167 val index = (name,0) in |
|
168 Var (index,vtype) |
|
169 end; |
|
170 |
|
171 fun var2free v = let val (index, tv) = dest_Var v |
|
172 val istr = fst index in |
|
173 Free (istr,tv) |
|
174 end; |
|
175 |
|
176 fun inlist v [] = false |
|
177 | inlist v (first::rest) = if first = v then |
|
178 true |
|
179 else inlist v rest; |
|
180 |
|
181 (*fun in_vars v [] = false |
|
182 | in_vars v ((a,b)::rest) = if v = a then |
|
183 true |
|
184 else if v = b then |
|
185 true |
|
186 else in_vars v rest;*) |
|
187 |
|
188 fun in_vars v [] = false |
|
189 | in_vars v (a::rest) = if (fst v) = a then |
|
190 true |
|
191 |
|
192 else in_vars v rest; |
|
193 |
|
194 fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then |
|
195 true |
|
196 else if (a,b) = (d,c) then |
|
197 true |
|
198 else false; |
|
199 |
|
200 |
|
201 fun is_empty_seq thisseq = case Seq.chop (1, thisseq) of |
|
202 ([],_) => true |
|
203 | _ => false |
|
204 |
|
205 fun getnewenv thisseq = |
|
206 let val seqlist = Seq.list_of thisseq |
|
207 val envpair =hd seqlist in |
|
208 fst envpair |
|
209 end; |
|
210 |
|
211 fun getnewsubsts thisseq = let val seqlist = Seq.list_of thisseq |
|
212 val envpair =hd seqlist in |
|
213 snd envpair |
|
214 end; |
|
215 |
|
216 fun readnewenv thisenv =let val seqlist = Seq.list_of thisenv |
|
217 val envpair = hd seqlist |
|
218 val env = fst envpair |
|
219 val envlist = alist_of env in |
|
220 hd envlist |
|
221 end; |
|
222 |
|
223 |
|
224 fun readenv thisenv = let val envlist = alist_of thisenv in |
|
225 |
|
226 hd envlist |
|
227 end; |
|
228 |
|
229 |
|
230 |
|
231 |
|
232 |
|
233 fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]); |
|
234 |
|
235 fun oneofthree (a,b,c) = a; |
|
236 |
|
237 fun twoofthree (a,b,c) = b; |
|
238 |
|
239 fun threeofthree (a,b,c) = c; |
|
240 |
|
241 val my_simps = map prover |
|
242 [ "(x=x) = True", |
|
243 "(~ ~ P) = P", |
|
244 "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))", |
|
245 |
|
246 "(P | P) = P", "(P | (P | Q)) = (P | Q)", |
|
247 "((~P) = (~Q)) = (P=Q)" ]; |
|
248 |
|
249 |
|
250 (*val myss = HOL_basic_ss addsimps (my_simps@[not_all, not_ex, de_Morgan_conj, de_Morgan_disj, U_def, intersect_def, setEq_def, proposEq_def, hashset_def, subset_def]@ex_simps @ all_simps); |
|
251 |
|
252 *) |
|
253 |
|
254 (*--------------------------*) |
|
255 (* NNF stuff from meson_tac *) |
|
256 (*--------------------------*) |
|
257 |
|
258 |
|
259 (*Prove theorems using fast_tac*) |
|
260 fun prove_fun s = |
|
261 prove_goal HOL.thy s |
|
262 (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]); |
|
263 |
|
264 (*------------------------------------------------------------------------*) |
|
265 (* Renaming all the bound vars in the term - sort of fake `Skolemisation' *) |
|
266 (*------------------------------------------------------------------------*) |
|
267 fun mygenvar ty thisenv = |
|
268 let val count = !gcounter |
|
269 val genstring = "GEN"^(string_of_int count)^"VAR" in |
|
270 gcounter := count + 1; |
|
271 genvar genstring (thisenv,ty) |
|
272 end; |
|
273 |
|
274 fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then |
|
275 t |
|
276 |
|
277 else if is_forall t then |
|
278 let val {Body, Bvar} = dest_forall t |
|
279 val newvarenv = mygenvar(type_of Bvar) thisenv |
|
280 val newvar = snd(newvarenv) |
|
281 val newbod = subst_free [(Bvar,newvar)] Body |
|
282 val newbod2 = renameBounds newbod thisenv in |
|
283 mk_forall{Body = newbod2, Bvar = newvar} |
|
284 end |
|
285 else if is_exists t then |
|
286 let val {Body, Bvar} =dest_exists t |
|
287 val newvarenv = mygenvar(type_of Bvar) thisenv |
|
288 val newvar = snd(newvarenv) |
|
289 val newbod = subst_free [(Bvar,newvar)] Body |
|
290 val newbod2 = renameBounds newbod thisenv in |
|
291 mk_exists{Body = newbod2, Bvar = newvar} |
|
292 end |
|
293 else if is_conj t then |
|
294 let val {conj1,conj2} = dest_conj t |
|
295 val vpl = renameBounds conj1 thisenv |
|
296 val vpr = renameBounds conj2 thisenv in |
|
297 mk_conj {conj1 = vpl, conj2 = vpr} |
|
298 end |
|
299 else |
|
300 let val {disj1, disj2} = dest_disj t |
|
301 val vpl = renameBounds disj1 thisenv |
|
302 val vpr = renameBounds disj2 thisenv in |
|
303 mk_disj {disj1 = vpl,disj2= vpr} |
|
304 end; |
|
305 |
|
306 |
|
307 (*-----------------*) |
|
308 (* from hologic.ml *) |
|
309 (*-----------------*) |
|
310 val boolT = Type ("bool", []); |
|
311 |
|
312 val Trueprop = Const ("Trueprop", boolT --> propT); |
|
313 |
|
314 fun mk_Trueprop P = Trueprop $ P; |
|
315 |
|
316 fun eq_const T = Const ("op =", [T, T] ---> boolT); |
|
317 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
|
318 |
|
319 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P |
|
320 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
|
321 |
|
322 |
|
323 (*-----------------------------------------------------------------------*) |
|
324 (* Making a THM from a subgoal and other such things *) |
|
325 (*-----------------------------------------------------------------------*) |
|
326 |
|
327 fun thmfromgoal goalnum = let val mygoal = getgoal goalnum |
|
328 val mycgoal = cterm_of Mainsign mygoal in |
|
329 assume mycgoal |
|
330 end; |
|
331 |
|
332 fun termfromgoal goalnum = let val mygoal = getgoal goalnum |
|
333 val {Rand = myra, Rator = myrat} = dest_comb mygoal in |
|
334 myra |
|
335 end; |
|
336 |
|
337 fun thmfromterm t = let val propterm = mk_Trueprop t |
|
338 val mycterm = cterm_of Mainsign propterm in |
|
339 assume mycterm |
|
340 end; |
|
341 |
|
342 fun termfromthm t = let val conc = concl_of t |
|
343 val {Rand = myra, Rator = myrat} = dest_comb conc in |
|
344 myra |
|
345 end; |
|
346 |
|
347 fun goalfromterm t = let val pterm = mk_Trueprop t |
|
348 val ct = cterm_of Mainsign pterm in |
|
349 goalw_cterm [] ct |
|
350 end; |
|
351 |
|
352 fun termfromgoalimp goalnum = let val mygoal = getgoal goalnum |
|
353 val {Rand = myra1, Rator = myrat1} = dest_comb mygoal |
|
354 val {Rand = myra, Rator = myrat} = dest_comb myra1 in |
|
355 myra |
|
356 end; |
|
357 |
|
358 |
|
359 fun mkvars (a,b:term) = let val thetype = type_of b |
|
360 val stringa =( fst a) |
|
361 val newa = Free (stringa, thetype) in |
|
362 (newa,b) |
|
363 end; |
|
364 |
|
365 fun glue [] thestring = thestring |
|
366 |glue (""::[]) thestring = thestring |
|
367 |glue (a::[]) thestring = thestring^" "^a |
|
368 |glue (a::rest) thestring = let val newstring = thestring^" "^a in |
|
369 glue rest newstring |
|
370 end; |
|
371 |
|
372 exception STRINGEXCEP; |
|
373 |
|
374 fun getvstring (Var (v,T)) = fst v |
|
375 |getvstring (Free (v,T))= v; |
|
376 |
|
377 |
|
378 fun getindexstring ((a:string),(b:int))= a; |
|
379 |
|
380 fun getstrings (a,b) = let val astring = getstring a |
|
381 val bstring = getstring b in |
|
382 (astring,bstring) |
|
383 end; |
|
384 (* |
|
385 fun getvstrings (a,b) = let val astring = getvstring a |
|
386 val bstring = getvstring b in |
|
387 (astring,bstring) |
|
388 end; |
|
389 *) |
|
390 |
|
391 |
|
392 |
|
393 (*------------------------------------------------------------------------*) |
|
394 (* Renaming all the bound vars in the term - sort of fake `Skolemisation' *) |
|
395 (*------------------------------------------------------------------------*) |
|
396 fun mygenvar ty thisenv = |
|
397 let val count = !gcounter |
|
398 val genstring = "GEN"^(string_of_int count)^"VAR" in |
|
399 gcounter := count + 1; |
|
400 genvar genstring (thisenv,ty) |
|
401 end; |
|
402 |
|
403 fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then |
|
404 t |
|
405 |
|
406 else if is_forall t then |
|
407 let val {Body, Bvar} = dest_forall t |
|
408 val newvarenv = mygenvar(type_of Bvar) thisenv |
|
409 val newvar = snd(newvarenv) |
|
410 val newbod = subst_free [(Bvar,newvar)] Body |
|
411 val newbod2 = renameBounds newbod thisenv in |
|
412 mk_forall{Body = newbod2, Bvar = newvar} |
|
413 end |
|
414 else if is_exists t then |
|
415 let val {Body, Bvar} =dest_exists t |
|
416 val newvarenv = mygenvar(type_of Bvar) thisenv |
|
417 val newvar = snd(newvarenv) |
|
418 val newbod = subst_free [(Bvar,newvar)] Body |
|
419 val newbod2 = renameBounds newbod thisenv in |
|
420 mk_exists{Body = newbod2, Bvar = newvar} |
|
421 end |
|
422 else if is_conj t then |
|
423 let val {conj1,conj2} = dest_conj t |
|
424 val vpl = renameBounds conj1 thisenv |
|
425 val vpr = renameBounds conj2 thisenv in |
|
426 mk_conj {conj1 = vpl, conj2 = vpr} |
|
427 end |
|
428 else |
|
429 let val {disj1, disj2} = dest_disj t |
|
430 val vpl = renameBounds disj1 thisenv |
|
431 val vpr = renameBounds disj2 thisenv in |
|
432 mk_disj {disj1 = vpl,disj2= vpr} |
|
433 end; |
|
434 |
|
435 |
|
436 |
|
437 exception VARFORM_PROBLEM; |
|
438 |
|
439 fun varform t = if (hol_literal t) then |
|
440 t |
|
441 |
|
442 else if is_forall t then |
|
443 let val {Body, Bvar} = dest_forall t |
|
444 (* need to subst schematic vars for Bvar here, e.g. x becomes ?x *) |
|
445 val newB = free2var Bvar |
|
446 val newBody = subst_free[(Bvar, newB)] Body in |
|
447 varform newBody |
|
448 end |
|
449 else if is_exists t then |
|
450 (* Shouldn't really be any exists in term due to Skolemisation*) |
|
451 let val {Body, Bvar} =dest_exists t in |
|
452 varform Body |
|
453 end |
|
454 else if is_conj t then |
|
455 let val {conj1,conj2} = dest_conj t |
|
456 val vpl = varform conj1 |
|
457 val vpr = varform conj2 in |
|
458 mk_conj {conj1 = vpl, conj2 = vpr} |
|
459 end |
|
460 else if is_disj t then |
|
461 let val {disj1, disj2} = dest_disj t |
|
462 val vpl = varform disj1 |
|
463 val vpr = varform disj2 in |
|
464 mk_disj {disj1 = vpl,disj2= vpr} |
|
465 end |
|
466 else |
|
467 raise VARFORM_PROBLEM; |
|
468 |
|
469 |
|
470 exception ASSERTION of string; |