author | haftmann |
Mon, 07 Nov 2005 12:06:11 +0100 (2005-11-07) | |
changeset 18103 | 7a524bfa8d65 |
parent 18029 | 19f1ad18bece |
child 18181 | 644d3e609db8 |
permissions | -rw-r--r-- |
9460 | 1 |
(* Title: Pure/logic.ML |
0 | 2 |
ID: $Id$ |
9460 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright Cambridge University 1992 |
5 |
||
9460 | 6 |
Abstract syntax operations of the Pure meta-logic. |
0 | 7 |
*) |
8 |
||
9460 | 9 |
signature LOGIC = |
4345 | 10 |
sig |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
11 |
val is_all : term -> bool |
9460 | 12 |
val mk_equals : term * term -> term |
13 |
val dest_equals : term -> term * term |
|
3963
29c5ec9ecbaa
Corrected alphabetical order of entries in signature.
nipkow
parents:
3915
diff
changeset
|
14 |
val is_equals : term -> bool |
9460 | 15 |
val mk_implies : term * term -> term |
16 |
val dest_implies : term -> term * term |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
17 |
val is_implies : term -> bool |
9460 | 18 |
val list_implies : term list * term -> term |
19 |
val strip_imp_prems : term -> term list |
|
20 |
val strip_imp_concl : term -> term |
|
21 |
val strip_prems : int * term list * term -> term list * term |
|
22 |
val count_prems : term * int -> int |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
23 |
val nth_prem : int * term -> term |
12137 | 24 |
val mk_conjunction : term * term -> term |
12757 | 25 |
val mk_conjunction_list: term list -> term |
13659
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
26 |
val strip_horn : term -> term list * term |
9460 | 27 |
val mk_cond_defpair : term list -> term * term -> string * term |
28 |
val mk_defpair : term * term -> string * term |
|
29 |
val mk_type : typ -> term |
|
30 |
val dest_type : term -> typ |
|
31 |
val mk_inclass : typ * class -> term |
|
32 |
val dest_inclass : term -> typ * class |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
33 |
val protectC : term |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
34 |
val protect : term -> term |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
35 |
val unprotect : term -> term |
9460 | 36 |
val occs : term * term -> bool |
37 |
val close_form : term -> term |
|
38 |
val incr_indexes : typ list * int -> term -> term |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
39 |
val incr_tvar : int -> typ -> typ |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
40 |
val lift_abs : int -> term -> term -> term |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
41 |
val lift_all : int -> term -> term -> term |
9460 | 42 |
val strip_assums_hyp : term -> term list |
43 |
val strip_assums_concl: term -> term |
|
44 |
val strip_params : term -> (string * typ) list |
|
9667 | 45 |
val has_meta_prems : term -> int -> bool |
9460 | 46 |
val flatten_params : int -> term -> term |
47 |
val auto_rename : bool ref |
|
48 |
val set_rename_prefix : string -> unit |
|
0 | 49 |
val list_rename_params: string list * term -> term |
15454 | 50 |
val assum_pairs : int * term -> (term*term)list |
9460 | 51 |
val varify : term -> term |
52 |
val unvarify : term -> term |
|
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
53 |
val get_goal : term -> int -> term |
14107 | 54 |
val goal_params : term -> int -> term * term list |
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
55 |
val prems_of_goal : term -> int -> term list |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
56 |
val concl_of_goal : term -> int -> term |
4345 | 57 |
end; |
0 | 58 |
|
1500 | 59 |
structure Logic : LOGIC = |
0 | 60 |
struct |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
61 |
|
4345 | 62 |
|
0 | 63 |
(*** Abstract syntax operations on the meta-connectives ***) |
64 |
||
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
65 |
(** all **) |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
66 |
|
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
67 |
fun is_all (Const ("all", _) $ _) = true |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
68 |
| is_all _ = false; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
69 |
|
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
70 |
|
0 | 71 |
(** equality **) |
72 |
||
1835 | 73 |
(*Make an equality. DOES NOT CHECK TYPE OF u*) |
64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset
|
74 |
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; |
0 | 75 |
|
76 |
fun dest_equals (Const("==",_) $ t $ u) = (t,u) |
|
77 |
| dest_equals t = raise TERM("dest_equals", [t]); |
|
78 |
||
637 | 79 |
fun is_equals (Const ("==", _) $ _ $ _) = true |
80 |
| is_equals _ = false; |
|
81 |
||
82 |
||
0 | 83 |
(** implies **) |
84 |
||
85 |
fun mk_implies(A,B) = implies $ A $ B; |
|
86 |
||
87 |
fun dest_implies (Const("==>",_) $ A $ B) = (A,B) |
|
88 |
| dest_implies A = raise TERM("dest_implies", [A]); |
|
89 |
||
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
90 |
fun is_implies (Const ("==>", _) $ _ $ _) = true |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
91 |
| is_implies _ = false; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
92 |
|
4822 | 93 |
|
0 | 94 |
(** nested implications **) |
95 |
||
96 |
(* [A1,...,An], B goes to A1==>...An==>B *) |
|
97 |
fun list_implies ([], B) = B : term |
|
98 |
| list_implies (A::AS, B) = implies $ A $ list_implies(AS,B); |
|
99 |
||
100 |
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) |
|
101 |
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B |
|
102 |
| strip_imp_prems _ = []; |
|
103 |
||
104 |
(* A1==>...An==>B goes to B, where B is not an implication *) |
|
105 |
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B |
|
106 |
| strip_imp_concl A = A : term; |
|
107 |
||
108 |
(*Strip and return premises: (i, [], A1==>...Ai==>B) |
|
9460 | 109 |
goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) |
0 | 110 |
if i<0 or else i too big then raises TERM*) |
9460 | 111 |
fun strip_prems (0, As, B) = (As, B) |
112 |
| strip_prems (i, As, Const("==>", _) $ A $ B) = |
|
113 |
strip_prems (i-1, A::As, B) |
|
0 | 114 |
| strip_prems (_, As, A) = raise TERM("strip_prems", A::As); |
115 |
||
16130 | 116 |
(*Count premises -- quicker than (length o strip_prems) *) |
0 | 117 |
fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) |
118 |
| count_prems (_,n) = n; |
|
119 |
||
16130 | 120 |
(*Select Ai from A1 ==>...Ai==>B*) |
121 |
fun nth_prem (1, Const ("==>", _) $ A $ _) = A |
|
122 |
| nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B) |
|
123 |
| nth_prem (_, A) = raise TERM ("nth_prem", [A]); |
|
124 |
||
13659
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
125 |
(*strip a proof state (Horn clause): |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
126 |
B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *) |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
127 |
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
128 |
|
4822 | 129 |
|
12137 | 130 |
(** conjunction **) |
131 |
||
132 |
fun mk_conjunction (t, u) = |
|
133 |
Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0)); |
|
134 |
||
12757 | 135 |
fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) |
136 |
| mk_conjunction_list ts = foldr1 mk_conjunction ts; |
|
12137 | 137 |
|
138 |
||
4822 | 139 |
(** definitions **) |
140 |
||
141 |
fun mk_cond_defpair As (lhs, rhs) = |
|
142 |
(case Term.head_of lhs of |
|
143 |
Const (name, _) => |
|
144 |
(Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs))) |
|
145 |
| _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); |
|
146 |
||
147 |
fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; |
|
148 |
||
149 |
||
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
150 |
(** types as terms **) |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
151 |
|
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
152 |
fun mk_type ty = Const ("TYPE", itselfT ty); |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
153 |
|
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
154 |
fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
155 |
| dest_type t = raise TERM ("dest_type", [t]); |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
156 |
|
4822 | 157 |
|
447 | 158 |
(** class constraints **) |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
159 |
|
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
160 |
fun mk_inclass (ty, c) = |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
161 |
Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty; |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
162 |
|
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
163 |
fun dest_inclass (t as Const (c_class, _) $ ty) = |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
164 |
((dest_type ty, Sign.class_of_const c_class) |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
165 |
handle TERM _ => raise TERM ("dest_inclass", [t])) |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
166 |
| dest_inclass t = raise TERM ("dest_inclass", [t]); |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
167 |
|
0 | 168 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
169 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
170 |
(** protected propositions **) |
9460 | 171 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
172 |
val protectC = Const ("prop", propT --> propT); |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
173 |
fun protect t = protectC $ t; |
9460 | 174 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
175 |
fun unprotect (Const ("prop", _) $ t) = t |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
176 |
| unprotect t = raise TERM ("unprotect", [t]); |
9460 | 177 |
|
178 |
||
0 | 179 |
(*** Low-level term operations ***) |
180 |
||
181 |
(*Does t occur in u? Or is alpha-convertible to u? |
|
182 |
The term t must contain no loose bound variables*) |
|
16846 | 183 |
fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
0 | 184 |
|
185 |
(*Close up a formula over all free variables by quantification*) |
|
186 |
fun close_form A = |
|
4443 | 187 |
list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A); |
0 | 188 |
|
189 |
||
190 |
(*** Specialized operations for resolution... ***) |
|
191 |
||
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
192 |
local exception SAME in |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
193 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
194 |
fun incrT k = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
195 |
let |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
196 |
fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
197 |
| incr (Type (a, Ts)) = Type (a, incrs Ts) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
198 |
| incr _ = raise SAME |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
199 |
and incrs (T :: Ts) = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
200 |
(incr T :: (incrs Ts handle SAME => Ts) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
201 |
handle SAME => T :: incrs Ts) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
202 |
| incrs [] = raise SAME; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
203 |
in incr end; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
204 |
|
0 | 205 |
(*For all variables in the term, increment indexnames and lift over the Us |
206 |
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *) |
|
17120 | 207 |
fun incr_indexes ([], 0) t = t |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
208 |
| incr_indexes (Ts, k) t = |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
209 |
let |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
210 |
val n = length Ts; |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
211 |
val incrT = if k = 0 then I else incrT k; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
212 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
213 |
fun incr lev (Var ((x, i), T)) = |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
214 |
Unify.combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n) |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
215 |
| incr lev (Abs (x, T, body)) = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
216 |
(Abs (x, incrT T, incr (lev + 1) body handle SAME => body) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
217 |
handle SAME => Abs (x, T, incr (lev + 1) body)) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
218 |
| incr lev (t $ u) = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
219 |
(incr lev t $ (incr lev u handle SAME => u) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
220 |
handle SAME => t $ incr lev u) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
221 |
| incr _ (Const (c, T)) = Const (c, incrT T) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
222 |
| incr _ (Free (x, T)) = Free (x, incrT T) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
223 |
| incr _ (t as Bound _) = t; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
224 |
in incr 0 t handle SAME => t end; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
225 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
226 |
fun incr_tvar 0 T = T |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
227 |
| incr_tvar k T = incrT k T handle SAME => T; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
228 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
229 |
end; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
230 |
|
0 | 231 |
|
232 |
(*Make lifting functions from subgoal and increment. |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
233 |
lift_abs operates on terms |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
234 |
lift_all operates on propositions *) |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
235 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
236 |
fun lift_abs inc = |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
237 |
let |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
238 |
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
239 |
| lift Ts (Const ("all", _) $ Abs (a, T, b)) t = Abs (a, T, lift (T :: Ts) b t) |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
240 |
| lift Ts _ t = incr_indexes (rev Ts, inc) t; |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
241 |
in lift [] end; |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
242 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
243 |
fun lift_all inc = |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
244 |
let |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
245 |
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
246 |
| lift Ts ((c as Const ("all", _)) $ Abs (a, T, b)) t = c $ Abs (a, T, lift (T :: Ts) b t) |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
247 |
| lift Ts _ t = incr_indexes (rev Ts, inc) t; |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
248 |
in lift [] end; |
0 | 249 |
|
250 |
(*Strips assumptions in goal, yielding list of hypotheses. *) |
|
251 |
fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B |
|
252 |
| strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t |
|
253 |
| strip_assums_hyp B = []; |
|
254 |
||
255 |
(*Strips assumptions in goal, yielding conclusion. *) |
|
256 |
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B |
|
257 |
| strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t |
|
258 |
| strip_assums_concl B = B; |
|
259 |
||
260 |
(*Make a list of all the parameters in a subgoal, even if nested*) |
|
261 |
fun strip_params (Const("==>", _) $ H $ B) = strip_params B |
|
262 |
| strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t |
|
263 |
| strip_params B = []; |
|
264 |
||
9667 | 265 |
(*test for meta connectives in prems of a 'subgoal'*) |
266 |
fun has_meta_prems prop i = |
|
267 |
let |
|
268 |
fun is_meta (Const ("==>", _) $ _ $ _) = true |
|
10442 | 269 |
| is_meta (Const ("==", _) $ _ $ _) = true |
9667 | 270 |
| is_meta (Const ("all", _) $ _) = true |
271 |
| is_meta _ = false; |
|
272 |
in |
|
13659
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
273 |
(case strip_prems (i, [], prop) of |
9667 | 274 |
(B :: _, _) => exists is_meta (strip_assums_hyp B) |
275 |
| _ => false) handle TERM _ => false |
|
276 |
end; |
|
9483 | 277 |
|
0 | 278 |
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, |
9460 | 279 |
where j is the total number of parameters (precomputed) |
0 | 280 |
If n>0 then deletes assumption n. *) |
9460 | 281 |
fun remove_params j n A = |
0 | 282 |
if j=0 andalso n<=0 then A (*nothing left to do...*) |
283 |
else case A of |
|
9460 | 284 |
Const("==>", _) $ H $ B => |
285 |
if n=1 then (remove_params j (n-1) B) |
|
286 |
else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) |
|
0 | 287 |
| Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t |
288 |
| _ => if n>0 then raise TERM("remove_params", [A]) |
|
289 |
else A; |
|
290 |
||
291 |
(** Auto-renaming of parameters in subgoals **) |
|
292 |
||
293 |
val auto_rename = ref false |
|
294 |
and rename_prefix = ref "ka"; |
|
295 |
||
296 |
(*rename_prefix is not exported; it is set by this function.*) |
|
297 |
fun set_rename_prefix a = |
|
4693 | 298 |
if a<>"" andalso forall Symbol.is_letter (Symbol.explode a) |
0 | 299 |
then (rename_prefix := a; auto_rename := true) |
300 |
else error"rename prefix must be nonempty and consist of letters"; |
|
301 |
||
302 |
(*Makes parameters in a goal have distinctive names (not guaranteed unique!) |
|
303 |
A name clash could cause the printer to rename bound vars; |
|
304 |
then res_inst_tac would not work properly.*) |
|
305 |
fun rename_vars (a, []) = [] |
|
306 |
| rename_vars (a, (_,T)::vars) = |
|
12902 | 307 |
(a,T) :: rename_vars (Symbol.bump_string a, vars); |
0 | 308 |
|
309 |
(*Move all parameters to the front of the subgoal, renaming them apart; |
|
310 |
if n>0 then deletes assumption n. *) |
|
311 |
fun flatten_params n A = |
|
312 |
let val params = strip_params A; |
|
9460 | 313 |
val vars = if !auto_rename |
314 |
then rename_vars (!rename_prefix, params) |
|
315 |
else ListPair.zip (variantlist(map #1 params,[]), |
|
316 |
map #2 params) |
|
0 | 317 |
in list_all (vars, remove_params (length vars) n A) |
318 |
end; |
|
319 |
||
320 |
(*Makes parameters in a goal have the names supplied by the list cs.*) |
|
321 |
fun list_rename_params (cs, Const("==>", _) $ A $ B) = |
|
322 |
implies $ A $ list_rename_params (cs, B) |
|
9460 | 323 |
| list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = |
0 | 324 |
all T $ Abs(c, T, list_rename_params (cs, t)) |
325 |
| list_rename_params (cs, B) = B; |
|
326 |
||
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
327 |
(*** Treatmsent of "assume", "erule", etc. ***) |
0 | 328 |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
329 |
(*Strips assumptions in goal yielding |
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
330 |
HS = [Hn,...,H1], params = [xm,...,x1], and B, |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
331 |
where x1...xm are the parameters. This version (21.1.2005) REQUIRES |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
332 |
the the parameters to be flattened, but it allows erule to work on |
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
333 |
assumptions of the form !!x. phi. Any !! after the outermost string |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
334 |
will be regarded as belonging to the conclusion, and left untouched. |
15454 | 335 |
Used ONLY by assum_pairs. |
336 |
Unless nasms<0, it can terminate the recursion early; that allows |
|
337 |
erule to work on assumptions of the form P==>Q.*) |
|
338 |
fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*) |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
339 |
| strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = |
15454 | 340 |
strip_assums_imp (nasms-1, H::Hs, B) |
341 |
| strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) |
|
342 |
||
0 | 343 |
|
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
344 |
(*Strips OUTER parameters only, unlike similar legacy versions.*) |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
345 |
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) = |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
346 |
strip_assums_all ((a,T)::params, t) |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
347 |
| strip_assums_all (params, B) = (params, B); |
0 | 348 |
|
349 |
(*Produces disagreement pairs, one for each assumption proof, in order. |
|
350 |
A is the first premise of the lifted rule, and thus has the form |
|
15454 | 351 |
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B). |
352 |
nasms is the number of assumptions in the original subgoal, needed when B |
|
353 |
has the form B1 ==> B2: it stops B1 from being taken as an assumption. *) |
|
354 |
fun assum_pairs(nasms,A) = |
|
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
355 |
let val (params, A') = strip_assums_all ([],A) |
15454 | 356 |
val (Hs,B) = strip_assums_imp (nasms,[],A') |
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
357 |
fun abspar t = Unify.rlist_abs(params, t) |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
358 |
val D = abspar B |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
359 |
fun pairrev ([], pairs) = pairs |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
360 |
| pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs) |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
361 |
in pairrev (Hs,[]) |
0 | 362 |
end; |
363 |
||
364 |
(*Converts Frees to Vars and TFrees to TVars so that axioms can be written |
|
365 |
without (?) everywhere*) |
|
16862 | 366 |
fun varify (Const(a, T)) = Const (a, Type.varifyT T) |
367 |
| varify (Free (a, T)) = Var ((a, 0), Type.varifyT T) |
|
368 |
| varify (Var (ixn, T)) = Var (ixn, Type.varifyT T) |
|
369 |
| varify (t as Bound _) = t |
|
370 |
| varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body) |
|
371 |
| varify (f $ t) = varify f $ varify t; |
|
0 | 372 |
|
546 | 373 |
(*Inverse of varify. Converts axioms back to their original form.*) |
16862 | 374 |
fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T) |
375 |
| unvarify (Free (a, T)) = Free (a, Type.unvarifyT T) |
|
376 |
| unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T) |
|
377 |
| unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T) (*non-0 index!*) |
|
378 |
| unvarify (t as Bound _) = t |
|
379 |
| unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body) |
|
380 |
| unvarify (f $ t) = unvarify f $ unvarify t; |
|
546 | 381 |
|
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
382 |
|
16862 | 383 |
(* goal states *) |
384 |
||
385 |
fun get_goal st i = nth_prem (i, st) |
|
386 |
handle TERM _ => error "Goal number out of range"; |
|
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
387 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
388 |
(*reverses parameters for substitution*) |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
389 |
fun goal_params st i = |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
390 |
let val gi = get_goal st i |
14137
c57ec95e7763
Removed extraneous rev in function goal_params (the list of parameters
berghofe
parents:
14107
diff
changeset
|
391 |
val rfrees = map Free (rename_wrt_term gi (strip_params gi)) |
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
392 |
in (gi, rfrees) end; |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
393 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
394 |
fun concl_of_goal st i = |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
395 |
let val (gi, rfrees) = goal_params st i |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
396 |
val B = strip_assums_concl gi |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
397 |
in subst_bounds (rfrees, B) end; |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
398 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
399 |
fun prems_of_goal st i = |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
400 |
let val (gi, rfrees) = goal_params st i |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
401 |
val As = strip_assums_hyp gi |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
402 |
in map (fn A => subst_bounds (rfrees, A)) As end; |
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
403 |
|
0 | 404 |
end; |