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