author | wenzelm |
Wed, 13 Jun 2007 00:01:57 +0200 | |
changeset 23354 | a189707c1d76 |
parent 23238 | 3de6e253efc4 |
child 23357 | 16e0ec4bcd81 |
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 |
23238 | 11 |
val is_atomic: term -> bool |
18762 | 12 |
val dest_all: term -> typ * term |
18181 | 13 |
val mk_equals: term * term -> term |
14 |
val dest_equals: term -> term * term |
|
15 |
val mk_implies: term * term -> term |
|
16 |
val dest_implies: term -> term * term |
|
17 |
val list_implies: term list * term -> term |
|
18 |
val strip_imp_prems: term -> term list |
|
19 |
val strip_imp_concl: term -> term |
|
20 |
val strip_prems: int * term list * term -> term list * term |
|
21576 | 21 |
val count_prems: term -> int |
18181 | 22 |
val nth_prem: int * term -> term |
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
23 |
val conjunction: term |
18181 | 24 |
val mk_conjunction: term * term -> term |
12757 | 25 |
val mk_conjunction_list: term list -> term |
18499 | 26 |
val mk_conjunction_list2: term list list -> term |
18469 | 27 |
val dest_conjunction: term -> term * term |
19425 | 28 |
val dest_conjunction_list: term -> term list |
18469 | 29 |
val dest_conjunctions: term -> term list |
18181 | 30 |
val strip_horn: term -> term list * term |
21520 | 31 |
val mk_type: typ -> term |
18938 | 32 |
val dest_type: term -> typ |
21520 | 33 |
val type_map: (term -> term) -> typ -> typ |
18938 | 34 |
val const_of_class: class -> string |
35 |
val class_of_const: string -> class |
|
36 |
val mk_inclass: typ * class -> term |
|
37 |
val dest_inclass: term -> typ * class |
|
20630 | 38 |
val name_classrel: string * string -> string |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
39 |
val mk_classrel: class * class -> term |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
40 |
val dest_classrel: term -> class * class |
20630 | 41 |
val name_arities: arity -> string list |
42 |
val name_arity: string * sort list * class -> string |
|
43 |
val mk_arities: arity -> term list |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
44 |
val dest_arity: term -> string * sort list * class |
18938 | 45 |
val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) -> |
46 |
term -> (term * term) * term |
|
47 |
val abs_def: term -> term * term |
|
18181 | 48 |
val mk_defpair: term * term -> string * term |
49 |
val protectC: term |
|
50 |
val protect: term -> term |
|
51 |
val unprotect: term -> term |
|
19775 | 52 |
val mk_term: term -> term |
53 |
val dest_term: term -> term |
|
18181 | 54 |
val occs: term * term -> bool |
55 |
val close_form: term -> term |
|
18938 | 56 |
val combound: term * int * int -> term |
57 |
val rlist_abs: (string * typ) list * term -> term |
|
18181 | 58 |
val incr_indexes: typ list * int -> term -> term |
59 |
val incr_tvar: int -> typ -> typ |
|
60 |
val lift_abs: int -> term -> term -> term |
|
61 |
val lift_all: int -> term -> term -> term |
|
62 |
val strip_assums_hyp: term -> term list |
|
9460 | 63 |
val strip_assums_concl: term -> term |
18181 | 64 |
val strip_params: term -> (string * typ) list |
65 |
val has_meta_prems: term -> int -> bool |
|
66 |
val flatten_params: int -> term -> term |
|
67 |
val auto_rename: bool ref |
|
68 |
val set_rename_prefix: string -> unit |
|
0 | 69 |
val list_rename_params: string list * term -> term |
18181 | 70 |
val assum_pairs: int * term -> (term*term)list |
19806 | 71 |
val varifyT: typ -> typ |
72 |
val unvarifyT: typ -> typ |
|
18181 | 73 |
val varify: term -> term |
74 |
val unvarify: term -> term |
|
19806 | 75 |
val legacy_varifyT: typ -> typ |
76 |
val legacy_unvarifyT: typ -> typ |
|
77 |
val legacy_varify: term -> term |
|
78 |
val legacy_unvarify: term -> term |
|
18181 | 79 |
val get_goal: term -> int -> term |
80 |
val goal_params: term -> int -> term * term list |
|
81 |
val prems_of_goal: term -> int -> term list |
|
82 |
val concl_of_goal: term -> int -> term |
|
4345 | 83 |
end; |
0 | 84 |
|
1500 | 85 |
structure Logic : LOGIC = |
0 | 86 |
struct |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
87 |
|
4345 | 88 |
|
0 | 89 |
(*** Abstract syntax operations on the meta-connectives ***) |
90 |
||
23238 | 91 |
fun is_atomic (Const ("==>", _) $ _ $ _) = false |
92 |
| is_atomic (Const ("all", _) $ _) = false |
|
93 |
| is_atomic _ = true; |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
94 |
|
23238 | 95 |
|
96 |
(** all **) |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
97 |
|
18762 | 98 |
fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A) |
99 |
| dest_all t = raise TERM ("dest_all", [t]); |
|
100 |
||
101 |
||
0 | 102 |
(** equality **) |
103 |
||
20883 | 104 |
fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u; |
0 | 105 |
|
20883 | 106 |
fun dest_equals (Const ("==", _) $ t $ u) = (t, u) |
107 |
| dest_equals t = raise TERM ("dest_equals", [t]); |
|
637 | 108 |
|
109 |
||
0 | 110 |
(** implies **) |
111 |
||
20883 | 112 |
fun mk_implies (A, B) = implies $ A $ B; |
0 | 113 |
|
20883 | 114 |
fun dest_implies (Const ("==>", _) $ A $ B) = (A, B) |
115 |
| dest_implies A = raise TERM ("dest_implies", [A]); |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
116 |
|
4822 | 117 |
|
0 | 118 |
(** nested implications **) |
119 |
||
120 |
(* [A1,...,An], B goes to A1==>...An==>B *) |
|
18181 | 121 |
fun list_implies ([], B) = B |
122 |
| list_implies (A::As, B) = implies $ A $ list_implies(As,B); |
|
0 | 123 |
|
124 |
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) |
|
125 |
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B |
|
126 |
| strip_imp_prems _ = []; |
|
127 |
||
128 |
(* A1==>...An==>B goes to B, where B is not an implication *) |
|
129 |
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B |
|
130 |
| strip_imp_concl A = A : term; |
|
131 |
||
132 |
(*Strip and return premises: (i, [], A1==>...Ai==>B) |
|
9460 | 133 |
goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) |
0 | 134 |
if i<0 or else i too big then raises TERM*) |
9460 | 135 |
fun strip_prems (0, As, B) = (As, B) |
136 |
| strip_prems (i, As, Const("==>", _) $ A $ B) = |
|
137 |
strip_prems (i-1, A::As, B) |
|
0 | 138 |
| strip_prems (_, As, A) = raise TERM("strip_prems", A::As); |
139 |
||
16130 | 140 |
(*Count premises -- quicker than (length o strip_prems) *) |
21576 | 141 |
fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B |
142 |
| count_prems _ = 0; |
|
0 | 143 |
|
16130 | 144 |
(*Select Ai from A1 ==>...Ai==>B*) |
145 |
fun nth_prem (1, Const ("==>", _) $ A $ _) = A |
|
146 |
| nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B) |
|
147 |
| nth_prem (_, A) = raise TERM ("nth_prem", [A]); |
|
148 |
||
13659
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
149 |
(*strip a proof state (Horn clause): |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
150 |
B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *) |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
151 |
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
|
152 |
|
4822 | 153 |
|
12137 | 154 |
(** conjunction **) |
155 |
||
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
156 |
val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT); |
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
157 |
|
18499 | 158 |
(*A && B*) |
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
159 |
fun mk_conjunction (A, B) = conjunction $ A $ B; |
12137 | 160 |
|
18499 | 161 |
(*A && B && C -- improper*) |
12757 | 162 |
fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) |
163 |
| mk_conjunction_list ts = foldr1 mk_conjunction ts; |
|
12137 | 164 |
|
18499 | 165 |
(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*) |
166 |
fun mk_conjunction_list2 tss = |
|
167 |
mk_conjunction_list (map mk_conjunction_list (filter_out null tss)); |
|
168 |
||
169 |
(*A && B*) |
|
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
170 |
fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B) |
18469 | 171 |
| dest_conjunction t = raise TERM ("dest_conjunction", [t]); |
172 |
||
19425 | 173 |
(*A && B && C -- improper*) |
174 |
fun dest_conjunction_list t = |
|
175 |
(case try dest_conjunction t of |
|
176 |
NONE => [t] |
|
177 |
| SOME (A, B) => A :: dest_conjunction_list B); |
|
178 |
||
18499 | 179 |
(*((A && B) && C) && D && E -- flat*) |
18469 | 180 |
fun dest_conjunctions t = |
181 |
(case try dest_conjunction t of |
|
182 |
NONE => [t] |
|
183 |
| SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); |
|
184 |
||
185 |
||
12137 | 186 |
|
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
187 |
(** types as terms **) |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
188 |
|
19391 | 189 |
fun mk_type ty = Const ("TYPE", Term.itselfT ty); |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
190 |
|
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
191 |
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
|
192 |
| 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
|
193 |
|
21520 | 194 |
fun type_map f = dest_type o f o mk_type; |
195 |
||
4822 | 196 |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
197 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
198 |
(** type classes **) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
199 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
200 |
(* const names *) |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
201 |
|
18938 | 202 |
val classN = "_class"; |
203 |
||
204 |
val const_of_class = suffix classN; |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
205 |
|
18938 | 206 |
fun class_of_const c = unsuffix classN c |
207 |
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); |
|
208 |
||
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
209 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
210 |
(* class constraints *) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
211 |
|
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
212 |
fun mk_inclass (ty, c) = |
19391 | 213 |
Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty; |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
214 |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
215 |
fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
216 |
| 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
|
217 |
|
0 | 218 |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
219 |
(* class relations *) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
220 |
|
20630 | 221 |
fun name_classrel (c1, c2) = |
222 |
NameSpace.base c1 ^ "_" ^ NameSpace.base c2; |
|
223 |
||
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
224 |
fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2); |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
225 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
226 |
fun dest_classrel tm = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
227 |
(case dest_inclass tm of |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
228 |
(TVar (_, [c1]), c2) => (c1, c2) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
229 |
| _ => raise TERM ("dest_classrel", [tm])); |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
230 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
231 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
232 |
(* type arities *) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
233 |
|
20630 | 234 |
fun name_arities (t, _, S) = |
235 |
let val b = NameSpace.base t |
|
236 |
in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end; |
|
237 |
||
238 |
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); |
|
239 |
||
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
240 |
fun mk_arities (t, Ss, S) = |
20078
f4122d7494f3
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19879
diff
changeset
|
241 |
let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss)) |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
242 |
in map (fn c => mk_inclass (T, c)) S end; |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
243 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
244 |
fun dest_arity tm = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
245 |
let |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
246 |
fun err () = raise TERM ("dest_arity", [tm]); |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
247 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
248 |
val (ty, c) = dest_inclass tm; |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
249 |
val (t, tvars) = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
250 |
(case ty of |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
251 |
Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
252 |
| _ => err ()); |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
253 |
val Ss = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
254 |
if has_duplicates (eq_fst (op =)) tvars then err () |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
255 |
else map snd tvars; |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
256 |
in (t, Ss, c) end; |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
257 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
258 |
|
18938 | 259 |
|
260 |
(** definitions **) |
|
261 |
||
19103 | 262 |
fun term_kind (Const _) = "existing constant " |
263 |
| term_kind (Free _) = "free variable " |
|
264 |
| term_kind (Bound _) = "bound variable " |
|
265 |
| term_kind _ = ""; |
|
266 |
||
18938 | 267 |
(*c x == t[x] to !!x. c x == t[x]*) |
268 |
fun dest_def pp check_head is_fixed is_fixedT eq = |
|
269 |
let |
|
270 |
fun err msg = raise TERM (msg, [eq]); |
|
19071
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
271 |
val eq_vars = Term.strip_all_vars eq; |
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
272 |
val eq_body = Term.strip_all_body eq; |
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
273 |
|
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
274 |
val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars); |
18938 | 275 |
val display_types = commas_quote o map (Pretty.string_of_typ pp); |
276 |
||
19071
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
277 |
val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)"; |
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
278 |
val lhs = Envir.beta_eta_contract raw_lhs; |
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
279 |
val (head, args) = Term.strip_comb lhs; |
18938 | 280 |
val head_tfrees = Term.add_tfrees head []; |
281 |
||
282 |
fun check_arg (Bound _) = true |
|
283 |
| check_arg (Free (x, _)) = not (is_fixed x) |
|
284 |
| check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true |
|
285 |
| check_arg _ = false; |
|
286 |
fun close_arg (Bound _) t = t |
|
287 |
| close_arg x t = Term.all (Term.fastype_of x) $ lambda x t; |
|
288 |
||
289 |
val lhs_bads = filter_out check_arg args; |
|
18964 | 290 |
val lhs_dups = duplicates (op aconv) args; |
18938 | 291 |
val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => |
292 |
if is_fixed x orelse member (op aconv) args v then I |
|
293 |
else insert (op aconv) v | _ => I) rhs []; |
|
294 |
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => |
|
295 |
if is_fixedT a orelse member (op =) head_tfrees (a, S) then I |
|
296 |
else insert (op =) v | _ => I)) rhs []; |
|
297 |
in |
|
298 |
if not (check_head head) then |
|
19103 | 299 |
err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) |
18938 | 300 |
else if not (null lhs_bads) then |
301 |
err ("Bad arguments on lhs: " ^ display_terms lhs_bads) |
|
302 |
else if not (null lhs_dups) then |
|
303 |
err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) |
|
304 |
else if not (null rhs_extras) then |
|
305 |
err ("Extra variables on rhs: " ^ display_terms rhs_extras) |
|
306 |
else if not (null rhs_extrasT) then |
|
307 |
err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) |
|
308 |
else if exists_subterm (fn t => t aconv head) rhs then |
|
309 |
err "Entity to be defined occurs on rhs" |
|
19071
fdffd7c40864
dest_def: actually return beta-eta contracted equation;
wenzelm
parents:
18964
diff
changeset
|
310 |
else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs))))) |
18938 | 311 |
end; |
312 |
||
313 |
(*!!x. c x == t[x] to c == %x. t[x]*) |
|
314 |
fun abs_def eq = |
|
315 |
let |
|
316 |
val body = Term.strip_all_body eq; |
|
317 |
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); |
|
318 |
val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body)); |
|
319 |
val (lhs', args) = Term.strip_comb lhs; |
|
320 |
val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs); |
|
321 |
in (lhs', rhs') end; |
|
322 |
||
22893 | 323 |
fun mk_defpair (lhs, rhs) = |
18938 | 324 |
(case Term.head_of lhs of |
325 |
Const (name, _) => |
|
22893 | 326 |
(NameSpace.base name ^ "_def", mk_equals (lhs, rhs)) |
18938 | 327 |
| _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); |
328 |
||
329 |
||
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
330 |
|
19775 | 331 |
(** protected propositions and embedded terms **) |
9460 | 332 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
333 |
val protectC = Const ("prop", propT --> propT); |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
334 |
fun protect t = protectC $ t; |
9460 | 335 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
336 |
fun unprotect (Const ("prop", _) $ t) = t |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
337 |
| unprotect t = raise TERM ("unprotect", [t]); |
9460 | 338 |
|
339 |
||
19775 | 340 |
fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t; |
341 |
||
342 |
fun dest_term (Const ("ProtoPure.term", _) $ t) = t |
|
343 |
| dest_term t = raise TERM ("dest_term", [t]); |
|
344 |
||
345 |
||
18181 | 346 |
|
0 | 347 |
(*** Low-level term operations ***) |
348 |
||
349 |
(*Does t occur in u? Or is alpha-convertible to u? |
|
350 |
The term t must contain no loose bound variables*) |
|
16846 | 351 |
fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
0 | 352 |
|
353 |
(*Close up a formula over all free variables by quantification*) |
|
354 |
fun close_form A = |
|
19425 | 355 |
Term.list_all_free (rev (Term.add_frees A []), A); |
0 | 356 |
|
357 |
||
18938 | 358 |
|
0 | 359 |
(*** Specialized operations for resolution... ***) |
360 |
||
18938 | 361 |
(*computes t(Bound(n+k-1),...,Bound(n)) *) |
362 |
fun combound (t, n, k) = |
|
363 |
if k>0 then combound (t,n+1,k-1) $ (Bound n) else t; |
|
364 |
||
365 |
(* ([xn,...,x1], t) ======> (x1,...,xn)t *) |
|
366 |
fun rlist_abs ([], body) = body |
|
367 |
| rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); |
|
368 |
||
369 |
||
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
370 |
local exception SAME in |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
371 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
372 |
fun incrT k = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
373 |
let |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
374 |
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
|
375 |
| incr (Type (a, Ts)) = Type (a, incrs Ts) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
376 |
| incr _ = raise SAME |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
377 |
and incrs (T :: Ts) = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
378 |
(incr T :: (incrs Ts handle SAME => Ts) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
379 |
handle SAME => T :: incrs Ts) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
380 |
| incrs [] = raise SAME; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
381 |
in incr end; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
382 |
|
0 | 383 |
(*For all variables in the term, increment indexnames and lift over the Us |
384 |
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *) |
|
17120 | 385 |
fun incr_indexes ([], 0) t = t |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
386 |
| incr_indexes (Ts, k) t = |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
387 |
let |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
388 |
val n = length Ts; |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
389 |
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
|
390 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
391 |
fun incr lev (Var ((x, i), T)) = |
18938 | 392 |
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
|
393 |
| incr lev (Abs (x, T, body)) = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
394 |
(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
|
395 |
handle SAME => Abs (x, T, incr (lev + 1) body)) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
396 |
| incr lev (t $ u) = |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
397 |
(incr lev t $ (incr lev u handle SAME => u) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
398 |
handle SAME => t $ incr lev u) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
399 |
| incr _ (Const (c, T)) = Const (c, incrT T) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
400 |
| incr _ (Free (x, T)) = Free (x, incrT T) |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
401 |
| incr _ (t as Bound _) = t; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
402 |
in incr 0 t handle SAME => t end; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
403 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
404 |
fun incr_tvar 0 T = T |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
405 |
| 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
|
406 |
|
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
407 |
end; |
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
408 |
|
0 | 409 |
|
18248 | 410 |
(* Lifting functions from subgoal and increment: |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
411 |
lift_abs operates on terms |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
412 |
lift_all operates on propositions *) |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
413 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
414 |
fun lift_abs inc = |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
415 |
let |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
416 |
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t |
18248 | 417 |
| lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
418 |
| 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
|
419 |
in lift [] end; |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
420 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
421 |
fun lift_all inc = |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
422 |
let |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
423 |
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t |
18248 | 424 |
| lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
425 |
| 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
|
426 |
in lift [] end; |
0 | 427 |
|
428 |
(*Strips assumptions in goal, yielding list of hypotheses. *) |
|
21016
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
429 |
fun strip_assums_hyp B = |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
430 |
let |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
431 |
fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
432 |
| strip Hs (Const ("all", _) $ Abs (a, T, t)) = |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
433 |
strip (map (incr_boundvars 1) Hs) t |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
434 |
| strip Hs B = rev Hs |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
435 |
in strip [] B end; |
0 | 436 |
|
437 |
(*Strips assumptions in goal, yielding conclusion. *) |
|
438 |
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B |
|
439 |
| strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t |
|
440 |
| strip_assums_concl B = B; |
|
441 |
||
442 |
(*Make a list of all the parameters in a subgoal, even if nested*) |
|
443 |
fun strip_params (Const("==>", _) $ H $ B) = strip_params B |
|
444 |
| strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t |
|
445 |
| strip_params B = []; |
|
446 |
||
9667 | 447 |
(*test for meta connectives in prems of a 'subgoal'*) |
448 |
fun has_meta_prems prop i = |
|
449 |
let |
|
450 |
fun is_meta (Const ("==>", _) $ _ $ _) = true |
|
10442 | 451 |
| is_meta (Const ("==", _) $ _ $ _) = true |
9667 | 452 |
| is_meta (Const ("all", _) $ _) = true |
453 |
| is_meta _ = false; |
|
454 |
in |
|
13659
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
455 |
(case strip_prems (i, [], prop) of |
9667 | 456 |
(B :: _, _) => exists is_meta (strip_assums_hyp B) |
457 |
| _ => false) handle TERM _ => false |
|
458 |
end; |
|
9483 | 459 |
|
0 | 460 |
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, |
9460 | 461 |
where j is the total number of parameters (precomputed) |
0 | 462 |
If n>0 then deletes assumption n. *) |
9460 | 463 |
fun remove_params j n A = |
0 | 464 |
if j=0 andalso n<=0 then A (*nothing left to do...*) |
465 |
else case A of |
|
9460 | 466 |
Const("==>", _) $ H $ B => |
467 |
if n=1 then (remove_params j (n-1) B) |
|
468 |
else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) |
|
0 | 469 |
| Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t |
470 |
| _ => if n>0 then raise TERM("remove_params", [A]) |
|
471 |
else A; |
|
472 |
||
473 |
(** Auto-renaming of parameters in subgoals **) |
|
474 |
||
475 |
val auto_rename = ref false |
|
476 |
and rename_prefix = ref "ka"; |
|
477 |
||
478 |
(*rename_prefix is not exported; it is set by this function.*) |
|
479 |
fun set_rename_prefix a = |
|
4693 | 480 |
if a<>"" andalso forall Symbol.is_letter (Symbol.explode a) |
0 | 481 |
then (rename_prefix := a; auto_rename := true) |
482 |
else error"rename prefix must be nonempty and consist of letters"; |
|
483 |
||
484 |
(*Makes parameters in a goal have distinctive names (not guaranteed unique!) |
|
485 |
A name clash could cause the printer to rename bound vars; |
|
486 |
then res_inst_tac would not work properly.*) |
|
487 |
fun rename_vars (a, []) = [] |
|
488 |
| rename_vars (a, (_,T)::vars) = |
|
12902 | 489 |
(a,T) :: rename_vars (Symbol.bump_string a, vars); |
0 | 490 |
|
491 |
(*Move all parameters to the front of the subgoal, renaming them apart; |
|
492 |
if n>0 then deletes assumption n. *) |
|
493 |
fun flatten_params n A = |
|
494 |
let val params = strip_params A; |
|
9460 | 495 |
val vars = if !auto_rename |
496 |
then rename_vars (!rename_prefix, params) |
|
20078
f4122d7494f3
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19879
diff
changeset
|
497 |
else ListPair.zip (Name.variant_list [] (map #1 params), |
9460 | 498 |
map #2 params) |
0 | 499 |
in list_all (vars, remove_params (length vars) n A) |
500 |
end; |
|
501 |
||
502 |
(*Makes parameters in a goal have the names supplied by the list cs.*) |
|
503 |
fun list_rename_params (cs, Const("==>", _) $ A $ B) = |
|
504 |
implies $ A $ list_rename_params (cs, B) |
|
9460 | 505 |
| list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = |
0 | 506 |
all T $ Abs(c, T, list_rename_params (cs, t)) |
507 |
| list_rename_params (cs, B) = B; |
|
508 |
||
19806 | 509 |
(*** Treatment of "assume", "erule", etc. ***) |
0 | 510 |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
511 |
(*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
|
512 |
HS = [Hn,...,H1], params = [xm,...,x1], and B, |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
513 |
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
|
514 |
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
|
515 |
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
|
516 |
will be regarded as belonging to the conclusion, and left untouched. |
15454 | 517 |
Used ONLY by assum_pairs. |
518 |
Unless nasms<0, it can terminate the recursion early; that allows |
|
519 |
erule to work on assumptions of the form P==>Q.*) |
|
520 |
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
|
521 |
| strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = |
15454 | 522 |
strip_assums_imp (nasms-1, H::Hs, B) |
523 |
| strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) |
|
524 |
||
0 | 525 |
|
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
526 |
(*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
|
527 |
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
|
528 |
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
|
529 |
| strip_assums_all (params, B) = (params, B); |
0 | 530 |
|
531 |
(*Produces disagreement pairs, one for each assumption proof, in order. |
|
532 |
A is the first premise of the lifted rule, and thus has the form |
|
15454 | 533 |
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B). |
534 |
nasms is the number of assumptions in the original subgoal, needed when B |
|
535 |
has the form B1 ==> B2: it stops B1 from being taken as an assumption. *) |
|
536 |
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
|
537 |
let val (params, A') = strip_assums_all ([],A) |
15454 | 538 |
val (Hs,B) = strip_assums_imp (nasms,[],A') |
18938 | 539 |
fun abspar t = rlist_abs(params, t) |
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
540 |
val D = abspar B |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
541 |
fun pairrev ([], pairs) = pairs |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
542 |
| 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
|
543 |
in pairrev (Hs,[]) |
0 | 544 |
end; |
545 |
||
19806 | 546 |
|
547 |
(* global schematic variables *) |
|
548 |
||
549 |
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); |
|
550 |
fun bad_fixed x = "Illegal fixed variable: " ^ quote x; |
|
551 |
||
552 |
fun varifyT ty = ty |> Term.map_atyps |
|
553 |
(fn TFree (a, S) => TVar ((a, 0), S) |
|
554 |
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); |
|
555 |
||
556 |
fun unvarifyT ty = ty |> Term.map_atyps |
|
557 |
(fn TVar ((a, 0), S) => TFree (a, S) |
|
558 |
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) |
|
559 |
| TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); |
|
0 | 560 |
|
19806 | 561 |
fun varify tm = |
562 |
tm |> Term.map_aterms |
|
563 |
(fn Free (x, T) => Var ((x, 0), T) |
|
564 |
| Var (xi, _) => raise TERM (bad_schematic xi, [tm]) |
|
565 |
| t => t) |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset
|
566 |
|> Term.map_types varifyT |
19879 | 567 |
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); |
19806 | 568 |
|
569 |
fun unvarify tm = |
|
570 |
tm |> Term.map_aterms |
|
571 |
(fn Var ((x, 0), T) => Free (x, T) |
|
572 |
| Var (xi, _) => raise TERM (bad_schematic xi, [tm]) |
|
573 |
| Free (x, _) => raise TERM (bad_fixed x, [tm]) |
|
574 |
| t => t) |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset
|
575 |
|> Term.map_types unvarifyT |
19879 | 576 |
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); |
19806 | 577 |
|
578 |
val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T); |
|
579 |
val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T); |
|
580 |
||
581 |
val legacy_varify = |
|
582 |
Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #> |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset
|
583 |
Term.map_types legacy_varifyT; |
19806 | 584 |
|
585 |
val legacy_unvarify = |
|
586 |
Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #> |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset
|
587 |
Term.map_types legacy_unvarifyT; |
546 | 588 |
|
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
589 |
|
16862 | 590 |
(* goal states *) |
591 |
||
592 |
fun get_goal st i = nth_prem (i, st) |
|
593 |
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
|
594 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
595 |
(*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
|
596 |
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
|
597 |
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
|
598 |
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
|
599 |
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
|
600 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
601 |
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
|
602 |
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
|
603 |
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
|
604 |
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
|
605 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
606 |
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
|
607 |
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
|
608 |
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
|
609 |
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
|
610 |
|
0 | 611 |
end; |