author | paulson |
Wed, 07 Sep 2005 09:54:31 +0200 | |
changeset 17305 | 6cef3aedd661 |
parent 16803 | 014090d1e64b |
permissions | -rw-r--r-- |
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
1 |
(* ID: $Id$ |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
2 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
3 |
Copyright 2004 University of Cambridge |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
4 |
*) |
15642 | 5 |
|
16803 | 6 |
structure ReconPrelim = |
7 |
struct |
|
15642 | 8 |
|
9 |
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; |
|
10 |
||
11 |
fun dest_neg(Const("Not",_) $ M) = M |
|
12 |
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; |
|
13 |
||
16803 | 14 |
fun iscomb a = |
15 |
if is_Free a then |
|
16 |
false |
|
17 |
else if is_Var a then |
|
18 |
false |
|
19 |
else if USyntax.is_conj a then |
|
20 |
false |
|
21 |
else if USyntax.is_disj a then |
|
22 |
false |
|
23 |
else if USyntax.is_forall a then |
|
24 |
false |
|
25 |
else if USyntax.is_exists a then |
|
26 |
false |
|
27 |
else |
|
28 |
true; |
|
15642 | 29 |
|
30 |
fun getstring (Var (v,T)) = fst v |
|
31 |
|getstring (Free (v,T))= v; |
|
32 |
||
33 |
fun twoisvar (a,b) = is_Var b; |
|
34 |
fun twoisfree (a,b) = is_Free b; |
|
35 |
fun twoiscomb (a,b) = iscomb b; |
|
36 |
||
37 |
fun strequalfirst a (b,c) = (getstring a) = (getstring b); |
|
38 |
||
39 |
fun fstequal a b = a = fst b; |
|
40 |
||
41 |
(* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *) |
|
42 |
fun is_Abs (Abs _) = true |
|
43 |
| is_Abs _ = false; |
|
44 |
fun is_Bound (Bound _) = true |
|
45 |
| is_Bound _ = false; |
|
46 |
||
47 |
fun is_hol_tm t = |
|
16803 | 48 |
if (is_Free t) then |
49 |
true |
|
50 |
else if (is_Var t) then |
|
51 |
true |
|
52 |
else if (is_Const t) then |
|
53 |
true |
|
54 |
else if (is_Abs t) then |
|
55 |
true |
|
56 |
else if (is_Bound t) then |
|
57 |
true |
|
58 |
else |
|
59 |
let val (f, args) = strip_comb t in |
|
60 |
if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then |
|
61 |
true (* should be is_const *) |
|
62 |
else |
|
63 |
false |
|
64 |
end; |
|
15642 | 65 |
|
16803 | 66 |
fun is_hol_fm f = |
67 |
if USyntax.is_neg f then |
|
68 |
let val newf = USyntax.dest_neg f in |
|
69 |
is_hol_fm newf |
|
70 |
end |
|
71 |
else if USyntax.is_disj f then |
|
72 |
let val {disj1,disj2} = USyntax.dest_disj f in |
|
73 |
(is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *) |
|
74 |
end |
|
75 |
else if USyntax.is_conj f then |
|
76 |
let val {conj1,conj2} = USyntax.dest_conj f in |
|
77 |
(is_hol_fm conj1) andalso (is_hol_fm conj2) |
|
78 |
end |
|
79 |
else if (USyntax.is_forall f) then |
|
80 |
let val {Body, Bvar} = USyntax.dest_forall f in |
|
81 |
is_hol_fm Body |
|
82 |
end |
|
83 |
else if (USyntax.is_exists f) then |
|
84 |
let val {Body, Bvar} = USyntax.dest_exists f in |
|
85 |
is_hol_fm Body |
|
86 |
end |
|
87 |
else if (iscomb f) then |
|
88 |
let val (P, args) = strip_comb f in |
|
89 |
((is_hol_tm P)) andalso (forall is_hol_fm args) |
|
90 |
end |
|
91 |
else |
|
92 |
is_hol_tm f; (* should be is_const, need to check args *) |
|
15642 | 93 |
|
16803 | 94 |
fun hol_literal t = |
95 |
is_hol_fm t andalso |
|
96 |
(not (USyntax.is_conj t orelse USyntax.is_disj t orelse USyntax.is_forall t |
|
97 |
orelse USyntax.is_exists t)); |
|
15642 | 98 |
|
99 |
||
100 |
(*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *) |
|
16803 | 101 |
fun getcombvar a = |
102 |
let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in |
|
103 |
if (iscomb rand) then |
|
104 |
getcombvar rand |
|
105 |
else |
|
106 |
rand |
|
107 |
end; |
|
15642 | 108 |
|
16803 | 109 |
fun free2var v = |
110 |
let val (name, vtype) = dest_Free v |
|
111 |
in Var ((name, 0), vtype) end; |
|
15642 | 112 |
|
16803 | 113 |
fun var2free v = |
114 |
let val ((x, _), tv) = dest_Var v |
|
115 |
in Free (x, tv) end; |
|
15642 | 116 |
|
16803 | 117 |
val is_empty_seq = is_none o Seq.pull; |
15642 | 118 |
|
16803 | 119 |
fun getnewenv seq = fst (fst (the (Seq.pull seq))); |
120 |
fun getnewsubsts seq = snd (fst (the (Seq.pull seq))); |
|
15642 | 121 |
|
122 |
fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]); |
|
123 |
||
16803 | 124 |
val no_lines = filter_out (equal "\n"); |
125 |
||
15680 | 126 |
exception ASSERTION of string; |
16803 | 127 |
|
128 |
end; |