author | wenzelm |
Thu, 16 Jul 2009 21:29:02 +0200 | |
changeset 32023 | 2d071ac5032f |
parent 32020 | 9abf5d66606e |
child 32026 | 9898880061df |
permissions | -rw-r--r-- |
9460 | 1 |
(* Title: Pure/logic.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
29276 | 3 |
Author: Makarius |
0 | 4 |
|
9460 | 5 |
Abstract syntax operations of the Pure meta-logic. |
0 | 6 |
*) |
7 |
||
9460 | 8 |
signature LOGIC = |
4345 | 9 |
sig |
27334 | 10 |
val all: term -> term -> term |
11 |
val is_all: term -> bool |
|
12 |
val dest_all: term -> (string * typ) * term |
|
18181 | 13 |
val mk_equals: term * term -> term |
14 |
val dest_equals: term -> term * term |
|
27334 | 15 |
val implies: term |
18181 | 16 |
val mk_implies: term * term -> term |
17 |
val dest_implies: term -> term * term |
|
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 |
|
21576 | 22 |
val count_prems: term -> int |
18181 | 23 |
val nth_prem: int * term -> term |
23418 | 24 |
val true_prop: term |
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
25 |
val conjunction: term |
18181 | 26 |
val mk_conjunction: term * term -> term |
12757 | 27 |
val mk_conjunction_list: term list -> term |
23418 | 28 |
val mk_conjunction_balanced: term list -> term |
18469 | 29 |
val dest_conjunction: term -> term * term |
19425 | 30 |
val dest_conjunction_list: term -> term list |
23418 | 31 |
val dest_conjunction_balanced: int -> term -> term list |
18469 | 32 |
val dest_conjunctions: term -> term list |
18181 | 33 |
val strip_horn: term -> term list * term |
21520 | 34 |
val mk_type: typ -> term |
18938 | 35 |
val dest_type: term -> typ |
21520 | 36 |
val type_map: (term -> term) -> typ -> typ |
18938 | 37 |
val const_of_class: class -> string |
38 |
val class_of_const: string -> class |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
39 |
val mk_of_class: typ * class -> term |
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
40 |
val dest_of_class: term -> typ * class |
20630 | 41 |
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
|
42 |
val mk_classrel: class * class -> term |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
43 |
val dest_classrel: term -> class * class |
20630 | 44 |
val name_arities: arity -> string list |
45 |
val name_arity: string * sort list * class -> string |
|
46 |
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
|
47 |
val dest_arity: term -> string * sort list * class |
18181 | 48 |
val protectC: term |
49 |
val protect: term -> term |
|
50 |
val unprotect: term -> term |
|
19775 | 51 |
val mk_term: term -> term |
52 |
val dest_term: term -> term |
|
18181 | 53 |
val occs: term * term -> bool |
54 |
val close_form: term -> term |
|
18938 | 55 |
val combound: term * int * int -> term |
56 |
val rlist_abs: (string * typ) list * term -> term |
|
32023 | 57 |
val incr_tvar_same: int -> typ Same.operation |
58 |
val incr_tvar: int -> typ -> typ |
|
18181 | 59 |
val incr_indexes: typ list * int -> term -> term |
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 |
23597 | 65 |
val has_meta_prems: term -> bool |
18181 | 66 |
val flatten_params: int -> term -> term |
0 | 67 |
val list_rename_params: string list * term -> term |
18181 | 68 |
val assum_pairs: int * term -> (term*term)list |
30554
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
69 |
val assum_problems: int * term -> (term -> term) * term list * term |
19806 | 70 |
val varifyT: typ -> typ |
71 |
val unvarifyT: typ -> typ |
|
18181 | 72 |
val varify: term -> term |
73 |
val unvarify: term -> term |
|
74 |
val get_goal: term -> int -> term |
|
75 |
val goal_params: term -> int -> term * term list |
|
76 |
val prems_of_goal: term -> int -> term list |
|
77 |
val concl_of_goal: term -> int -> term |
|
4345 | 78 |
end; |
0 | 79 |
|
1500 | 80 |
structure Logic : LOGIC = |
0 | 81 |
struct |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
82 |
|
4345 | 83 |
|
0 | 84 |
(*** Abstract syntax operations on the meta-connectives ***) |
85 |
||
23238 | 86 |
(** all **) |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
87 |
|
27334 | 88 |
fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t; |
89 |
||
90 |
fun is_all (Const ("all", _) $ Abs _) = true |
|
91 |
| is_all _ = false; |
|
92 |
||
93 |
fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) = |
|
94 |
let val (x, b) = Term.dest_abs abs (*potentially slow*) |
|
95 |
in ((x, T), b) end |
|
18762 | 96 |
| dest_all t = raise TERM ("dest_all", [t]); |
97 |
||
98 |
||
0 | 99 |
(** equality **) |
100 |
||
27334 | 101 |
fun mk_equals (t, u) = |
102 |
let val T = Term.fastype_of t |
|
103 |
in Const ("==", T --> T --> propT) $ t $ u end; |
|
0 | 104 |
|
20883 | 105 |
fun dest_equals (Const ("==", _) $ t $ u) = (t, u) |
106 |
| dest_equals t = raise TERM ("dest_equals", [t]); |
|
637 | 107 |
|
108 |
||
0 | 109 |
(** implies **) |
110 |
||
27334 | 111 |
val implies = Const ("==>", propT --> propT --> propT); |
112 |
||
20883 | 113 |
fun mk_implies (A, B) = implies $ A $ B; |
0 | 114 |
|
20883 | 115 |
fun dest_implies (Const ("==>", _) $ A $ B) = (A, B) |
116 |
| dest_implies A = raise TERM ("dest_implies", [A]); |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset
|
117 |
|
4822 | 118 |
|
0 | 119 |
(** nested implications **) |
120 |
||
121 |
(* [A1,...,An], B goes to A1==>...An==>B *) |
|
18181 | 122 |
fun list_implies ([], B) = B |
123 |
| list_implies (A::As, B) = implies $ A $ list_implies(As,B); |
|
0 | 124 |
|
125 |
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) |
|
126 |
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B |
|
127 |
| strip_imp_prems _ = []; |
|
128 |
||
129 |
(* A1==>...An==>B goes to B, where B is not an implication *) |
|
130 |
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B |
|
131 |
| strip_imp_concl A = A : term; |
|
132 |
||
133 |
(*Strip and return premises: (i, [], A1==>...Ai==>B) |
|
9460 | 134 |
goes to ([Ai, A(i-1),...,A1] , B) (REVERSED) |
0 | 135 |
if i<0 or else i too big then raises TERM*) |
9460 | 136 |
fun strip_prems (0, As, B) = (As, B) |
137 |
| strip_prems (i, As, Const("==>", _) $ A $ B) = |
|
138 |
strip_prems (i-1, A::As, B) |
|
0 | 139 |
| strip_prems (_, As, A) = raise TERM("strip_prems", A::As); |
140 |
||
16130 | 141 |
(*Count premises -- quicker than (length o strip_prems) *) |
21576 | 142 |
fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B |
143 |
| count_prems _ = 0; |
|
0 | 144 |
|
16130 | 145 |
(*Select Ai from A1 ==>...Ai==>B*) |
146 |
fun nth_prem (1, Const ("==>", _) $ A $ _) = A |
|
147 |
| nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B) |
|
148 |
| nth_prem (_, A) = raise TERM ("nth_prem", [A]); |
|
149 |
||
13659
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
150 |
(*strip a proof state (Horn clause): |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
151 |
B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *) |
3cf622f6b0b2
Removed obsolete functions dealing with flex-flex constraints.
berghofe
parents:
12902
diff
changeset
|
152 |
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
|
153 |
|
4822 | 154 |
|
23418 | 155 |
|
12137 | 156 |
(** conjunction **) |
157 |
||
23418 | 158 |
val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)); |
26424 | 159 |
val conjunction = Const ("Pure.conjunction", propT --> propT --> propT); |
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
160 |
|
23418 | 161 |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
162 |
(*A &&& B*) |
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset
|
163 |
fun mk_conjunction (A, B) = conjunction $ A $ B; |
12137 | 164 |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
165 |
(*A &&& B &&& C -- improper*) |
23418 | 166 |
fun mk_conjunction_list [] = true_prop |
12757 | 167 |
| mk_conjunction_list ts = foldr1 mk_conjunction ts; |
12137 | 168 |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
169 |
(*(A &&& B) &&& (C &&& D) -- balanced*) |
23418 | 170 |
fun mk_conjunction_balanced [] = true_prop |
171 |
| mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; |
|
172 |
||
18499 | 173 |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
174 |
(*A &&& B*) |
26424 | 175 |
fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B) |
18469 | 176 |
| dest_conjunction t = raise TERM ("dest_conjunction", [t]); |
177 |
||
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
178 |
(*A &&& B &&& C -- improper*) |
19425 | 179 |
fun dest_conjunction_list t = |
180 |
(case try dest_conjunction t of |
|
181 |
NONE => [t] |
|
182 |
| SOME (A, B) => A :: dest_conjunction_list B); |
|
183 |
||
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
184 |
(*(A &&& B) &&& (C &&& D) -- balanced*) |
23418 | 185 |
fun dest_conjunction_balanced 0 _ = [] |
186 |
| dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t; |
|
187 |
||
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset
|
188 |
(*((A &&& B) &&& C) &&& D &&& E -- flat*) |
18469 | 189 |
fun dest_conjunctions t = |
190 |
(case try dest_conjunction t of |
|
191 |
NONE => [t] |
|
192 |
| SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); |
|
193 |
||
194 |
||
12137 | 195 |
|
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
196 |
(** types as terms **) |
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
197 |
|
19391 | 198 |
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
|
199 |
|
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
200 |
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
|
201 |
| 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
|
202 |
|
21520 | 203 |
fun type_map f = dest_type o f o mk_type; |
204 |
||
4822 | 205 |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
206 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
207 |
(** type classes **) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
208 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
209 |
(* const names *) |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
210 |
|
18938 | 211 |
val classN = "_class"; |
212 |
||
213 |
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
|
214 |
|
18938 | 215 |
fun class_of_const c = unsuffix classN c |
216 |
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); |
|
217 |
||
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
218 |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
219 |
(* class membership *) |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
220 |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
221 |
fun mk_of_class (ty, c) = |
19391 | 222 |
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
|
223 |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
224 |
fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) |
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
225 |
| dest_of_class t = raise TERM ("dest_of_class", [t]); |
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset
|
226 |
|
0 | 227 |
|
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
228 |
(* class relations *) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
229 |
|
20630 | 230 |
fun name_classrel (c1, c2) = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
231 |
Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; |
20630 | 232 |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
233 |
fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2); |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
234 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
235 |
fun dest_classrel tm = |
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
236 |
(case dest_of_class tm of |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
237 |
(TVar (_, [c1]), c2) => (c1, c2) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
238 |
| _ => raise TERM ("dest_classrel", [tm])); |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
239 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
240 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
241 |
(* type arities *) |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
242 |
|
20630 | 243 |
fun name_arities (t, _, S) = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
244 |
let val b = Long_Name.base_name t |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
245 |
in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end; |
20630 | 246 |
|
247 |
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); |
|
248 |
||
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
249 |
fun mk_arities (t, Ss, S) = |
24848 | 250 |
let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss)) |
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
251 |
in map (fn c => mk_of_class (T, c)) S end; |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
252 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
253 |
fun dest_arity tm = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
254 |
let |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
255 |
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
|
256 |
|
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
30554
diff
changeset
|
257 |
val (ty, c) = dest_of_class tm; |
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
258 |
val (t, tvars) = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
259 |
(case ty of |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
260 |
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
|
261 |
| _ => err ()); |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
262 |
val Ss = |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
263 |
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
|
264 |
else map snd tvars; |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
265 |
in (t, Ss, c) end; |
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
266 |
|
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset
|
267 |
|
18938 | 268 |
|
28448 | 269 |
(** protected propositions and embedded terms **) |
9460 | 270 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
271 |
val protectC = Const ("prop", propT --> propT); |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
272 |
fun protect t = protectC $ t; |
9460 | 273 |
|
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
274 |
fun unprotect (Const ("prop", _) $ t) = t |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
275 |
| unprotect t = raise TERM ("unprotect", [t]); |
9460 | 276 |
|
277 |
||
26424 | 278 |
fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t; |
19775 | 279 |
|
26424 | 280 |
fun dest_term (Const ("Pure.term", _) $ t) = t |
19775 | 281 |
| dest_term t = raise TERM ("dest_term", [t]); |
282 |
||
283 |
||
18181 | 284 |
|
0 | 285 |
(*** Low-level term operations ***) |
286 |
||
287 |
(*Does t occur in u? Or is alpha-convertible to u? |
|
288 |
The term t must contain no loose bound variables*) |
|
16846 | 289 |
fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
0 | 290 |
|
291 |
(*Close up a formula over all free variables by quantification*) |
|
292 |
fun close_form A = |
|
19425 | 293 |
Term.list_all_free (rev (Term.add_frees A []), A); |
0 | 294 |
|
295 |
||
18938 | 296 |
|
0 | 297 |
(*** Specialized operations for resolution... ***) |
298 |
||
18938 | 299 |
(*computes t(Bound(n+k-1),...,Bound(n)) *) |
300 |
fun combound (t, n, k) = |
|
301 |
if k>0 then combound (t,n+1,k-1) $ (Bound n) else t; |
|
302 |
||
303 |
(* ([xn,...,x1], t) ======> (x1,...,xn)t *) |
|
304 |
fun rlist_abs ([], body) = body |
|
305 |
| rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); |
|
306 |
||
32023 | 307 |
fun incr_tvar_same k = Term_Subst.map_atypsT_same |
32020 | 308 |
(fn TVar ((a, i), S) => TVar ((a, i + k), S) |
309 |
| _ => raise Same.SAME); |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
310 |
|
32023 | 311 |
fun incr_tvar 0 T = T |
312 |
| incr_tvar k T = incr_tvar_same k T handle Same.SAME => T; |
|
313 |
||
0 | 314 |
(*For all variables in the term, increment indexnames and lift over the Us |
315 |
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *) |
|
17120 | 316 |
fun incr_indexes ([], 0) t = t |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
317 |
| incr_indexes (Ts, k) t = |
32020 | 318 |
let |
319 |
val n = length Ts; |
|
32023 | 320 |
val incrT = if k = 0 then I else incr_tvar_same k; |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
321 |
|
32020 | 322 |
fun incr lev (Var ((x, i), T)) = |
323 |
combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n) |
|
324 |
| incr lev (Abs (x, T, body)) = |
|
325 |
(Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body) |
|
326 |
handle Same.SAME => Abs (x, T, incr (lev + 1) body)) |
|
327 |
| incr lev (t $ u) = |
|
328 |
(incr lev t $ (incr lev u handle Same.SAME => u) |
|
329 |
handle Same.SAME => t $ incr lev u) |
|
330 |
| incr _ (Const (c, T)) = Const (c, incrT T) |
|
331 |
| incr _ (Free (x, T)) = Free (x, incrT T) |
|
332 |
| incr _ (t as Bound _) = t; |
|
333 |
in incr 0 t handle Same.SAME => t end; |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
334 |
|
0 | 335 |
|
18248 | 336 |
(* Lifting functions from subgoal and increment: |
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
337 |
lift_abs operates on terms |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
338 |
lift_all operates on propositions *) |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
339 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
340 |
fun lift_abs inc = |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
341 |
let |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
342 |
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t |
18248 | 343 |
| 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
|
344 |
| 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
|
345 |
in lift [] end; |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
346 |
|
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
347 |
fun lift_all inc = |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
348 |
let |
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset
|
349 |
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t |
18248 | 350 |
| 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
|
351 |
| 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
|
352 |
in lift [] end; |
0 | 353 |
|
354 |
(*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
|
355 |
fun strip_assums_hyp B = |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
356 |
let |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
357 |
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
|
358 |
| strip Hs (Const ("all", _) $ Abs (a, T, t)) = |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
359 |
strip (map (incr_boundvars 1) Hs) t |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
360 |
| strip Hs B = rev Hs |
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset
|
361 |
in strip [] B end; |
0 | 362 |
|
363 |
(*Strips assumptions in goal, yielding conclusion. *) |
|
364 |
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B |
|
365 |
| strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t |
|
366 |
| strip_assums_concl B = B; |
|
367 |
||
368 |
(*Make a list of all the parameters in a subgoal, even if nested*) |
|
369 |
fun strip_params (Const("==>", _) $ H $ B) = strip_params B |
|
370 |
| strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t |
|
371 |
| strip_params B = []; |
|
372 |
||
23597 | 373 |
(*test for nested meta connectives in prems*) |
374 |
val has_meta_prems = |
|
9667 | 375 |
let |
23597 | 376 |
fun is_meta (Const ("==", _) $ _ $ _) = true |
377 |
| is_meta (Const ("==>", _) $ _ $ _) = true |
|
9667 | 378 |
| is_meta (Const ("all", _) $ _) = true |
379 |
| is_meta _ = false; |
|
23597 | 380 |
fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B |
381 |
| ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B |
|
382 |
| ex_meta _ = false; |
|
383 |
in ex_meta end; |
|
9483 | 384 |
|
0 | 385 |
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, |
9460 | 386 |
where j is the total number of parameters (precomputed) |
0 | 387 |
If n>0 then deletes assumption n. *) |
9460 | 388 |
fun remove_params j n A = |
0 | 389 |
if j=0 andalso n<=0 then A (*nothing left to do...*) |
390 |
else case A of |
|
9460 | 391 |
Const("==>", _) $ H $ B => |
392 |
if n=1 then (remove_params j (n-1) B) |
|
393 |
else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B) |
|
0 | 394 |
| Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t |
395 |
| _ => if n>0 then raise TERM("remove_params", [A]) |
|
396 |
else A; |
|
397 |
||
398 |
(*Move all parameters to the front of the subgoal, renaming them apart; |
|
399 |
if n>0 then deletes assumption n. *) |
|
400 |
fun flatten_params n A = |
|
401 |
let val params = strip_params A; |
|
25939 | 402 |
val vars = ListPair.zip (Name.variant_list [] (map #1 params), |
403 |
map #2 params) |
|
0 | 404 |
in list_all (vars, remove_params (length vars) n A) |
405 |
end; |
|
406 |
||
407 |
(*Makes parameters in a goal have the names supplied by the list cs.*) |
|
408 |
fun list_rename_params (cs, Const("==>", _) $ A $ B) = |
|
409 |
implies $ A $ list_rename_params (cs, B) |
|
27334 | 410 |
| list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) = |
411 |
a $ Abs(c, T, list_rename_params (cs, t)) |
|
0 | 412 |
| list_rename_params (cs, B) = B; |
413 |
||
32008 | 414 |
|
415 |
||
19806 | 416 |
(*** Treatment of "assume", "erule", etc. ***) |
0 | 417 |
|
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
418 |
(*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
|
419 |
HS = [Hn,...,H1], params = [xm,...,x1], and B, |
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset
|
420 |
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
|
421 |
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
|
422 |
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
|
423 |
will be regarded as belonging to the conclusion, and left untouched. |
15454 | 424 |
Used ONLY by assum_pairs. |
425 |
Unless nasms<0, it can terminate the recursion early; that allows |
|
426 |
erule to work on assumptions of the form P==>Q.*) |
|
427 |
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
|
428 |
| strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = |
15454 | 429 |
strip_assums_imp (nasms-1, H::Hs, B) |
430 |
| strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) |
|
431 |
||
32008 | 432 |
(*Strips OUTER parameters only.*) |
15451
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
433 |
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
|
434 |
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
|
435 |
| strip_assums_all (params, B) = (params, B); |
0 | 436 |
|
437 |
(*Produces disagreement pairs, one for each assumption proof, in order. |
|
438 |
A is the first premise of the lifted rule, and thus has the form |
|
15454 | 439 |
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B). |
440 |
nasms is the number of assumptions in the original subgoal, needed when B |
|
441 |
has the form B1 ==> B2: it stops B1 from being taken as an assumption. *) |
|
442 |
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
|
443 |
let val (params, A') = strip_assums_all ([],A) |
15454 | 444 |
val (Hs,B) = strip_assums_imp (nasms,[],A') |
18938 | 445 |
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
|
446 |
val D = abspar B |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
447 |
fun pairrev ([], pairs) = pairs |
c6c8786b9921
fixed thin_tac with higher-level assumptions by removing the old code to
paulson
parents:
14137
diff
changeset
|
448 |
| 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
|
449 |
in pairrev (Hs,[]) |
0 | 450 |
end; |
451 |
||
30554
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
452 |
fun assum_problems (nasms, A) = |
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
453 |
let |
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
454 |
val (params, A') = strip_assums_all ([], A) |
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
455 |
val (Hs, B) = strip_assums_imp (nasms, [], A') |
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
456 |
fun abspar t = rlist_abs (params, t) |
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
457 |
in (abspar, rev Hs, B) end; |
73f8bd5f0af8
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset
|
458 |
|
19806 | 459 |
|
460 |
(* global schematic variables *) |
|
461 |
||
462 |
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); |
|
463 |
fun bad_fixed x = "Illegal fixed variable: " ^ quote x; |
|
464 |
||
32020 | 465 |
fun varifyT_same ty = ty |
466 |
|> Term_Subst.map_atypsT_same |
|
467 |
(fn TFree (a, S) => TVar ((a, 0), S) |
|
31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset
|
468 |
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); |
19806 | 469 |
|
32020 | 470 |
fun unvarifyT_same ty = ty |
471 |
|> Term_Subst.map_atypsT_same |
|
472 |
(fn TVar ((a, 0), S) => TFree (a, S) |
|
31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset
|
473 |
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) |
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset
|
474 |
| TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); |
0 | 475 |
|
32020 | 476 |
val varifyT = Same.commit varifyT_same; |
477 |
val unvarifyT = Same.commit unvarifyT_same; |
|
31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset
|
478 |
|
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset
|
479 |
fun varify tm = tm |
32020 | 480 |
|> Same.commit (Term_Subst.map_aterms_same |
481 |
(fn Free (x, T) => Var ((x, 0), T) |
|
19806 | 482 |
| Var (xi, _) => raise TERM (bad_schematic xi, [tm]) |
32020 | 483 |
| _ => raise Same.SAME)) |
484 |
|> Same.commit (Term_Subst.map_types_same varifyT_same) |
|
19879 | 485 |
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); |
19806 | 486 |
|
31981
9c59cbb9c5a2
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
wenzelm
parents:
31943
diff
changeset
|
487 |
fun unvarify tm = tm |
32020 | 488 |
|> Same.commit (Term_Subst.map_aterms_same |
489 |
(fn Var ((x, 0), T) => Free (x, T) |
|
19806 | 490 |
| Var (xi, _) => raise TERM (bad_schematic xi, [tm]) |
491 |
| Free (x, _) => raise TERM (bad_fixed x, [tm]) |
|
32020 | 492 |
| _ => raise Same.SAME)) |
493 |
|> Same.commit (Term_Subst.map_types_same unvarifyT_same) |
|
19879 | 494 |
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); |
19806 | 495 |
|
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
496 |
|
16862 | 497 |
(* goal states *) |
498 |
||
499 |
fun get_goal st i = nth_prem (i, st) |
|
500 |
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
|
501 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
502 |
(*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
|
503 |
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
|
504 |
let val gi = get_goal st i |
29276 | 505 |
val rfrees = map Free (Term.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
|
506 |
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
|
507 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
508 |
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
|
509 |
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
|
510 |
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
|
511 |
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
|
512 |
|
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset
|
513 |
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
|
514 |
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
|
515 |
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
|
516 |
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
|
517 |
|
0 | 518 |
end; |