author | wenzelm |
Fri, 08 Dec 2023 14:59:22 +0100 | |
changeset 79204 | 64aca92fcd0f |
parent 79201 | 5d27271701a2 |
child 79205 | a159cb82afe7 |
permissions | -rw-r--r-- |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/zterm.ML |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
3 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
4 |
Tight representation of types / terms / proof terms, notably for proof recording. |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
5 |
*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
6 |
|
79124 | 7 |
(*** global ***) |
8 |
||
9 |
(* types and terms *) |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
10 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
11 |
datatype ztyp = |
79119 | 12 |
ZTVar of indexname * sort (*free: index ~1*) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
13 |
| ZFun of ztyp * ztyp |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
14 |
| ZProp |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
15 |
| ZItself of ztyp |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
16 |
| ZType0 of string (*type constant*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
17 |
| ZType1 of string * ztyp (*type constructor: 1 argument*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
18 |
| ZType of string * ztyp list (*type constructor: >= 2 arguments*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
19 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
20 |
datatype zterm = |
79119 | 21 |
ZVar of indexname * ztyp (*free: index ~1*) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
22 |
| ZBound of int |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
23 |
| ZConst0 of string (*monomorphic constant*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
24 |
| ZConst1 of string * ztyp (*polymorphic constant: 1 type argument*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
25 |
| ZConst of string * ztyp list (*polymorphic constant: >= 2 type arguments*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
26 |
| ZAbs of string * ztyp * zterm |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
27 |
| ZApp of zterm * zterm |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
28 |
| ZClass of ztyp * class (*OFCLASS proposition*) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
29 |
|
79124 | 30 |
structure ZTerm = |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
31 |
struct |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
32 |
|
79119 | 33 |
(* fold *) |
34 |
||
35 |
fun fold_tvars f (ZTVar v) = f v |
|
36 |
| fold_tvars f (ZFun (T, U)) = fold_tvars f T #> fold_tvars f U |
|
37 |
| fold_tvars f (ZItself T) = fold_tvars f T |
|
38 |
| fold_tvars f (ZType1 (_, T)) = fold_tvars f T |
|
39 |
| fold_tvars f (ZType (_, Ts)) = fold (fold_tvars f) Ts |
|
40 |
| fold_tvars _ _ = I; |
|
41 |
||
42 |
fun fold_aterms f (ZApp (t, u)) = fold_aterms f t #> fold_aterms f u |
|
43 |
| fold_aterms f (ZAbs (_, _, t)) = fold_aterms f t |
|
44 |
| fold_aterms f a = f a; |
|
45 |
||
46 |
fun fold_types f (ZVar (_, T)) = f T |
|
47 |
| fold_types f (ZConst1 (_, T)) = f T |
|
48 |
| fold_types f (ZConst (_, As)) = fold f As |
|
49 |
| fold_types f (ZAbs (_, T, b)) = f T #> fold_types f b |
|
50 |
| fold_types f (ZApp (t, u)) = fold_types f t #> fold_types f u |
|
51 |
| fold_types f (ZClass (T, _)) = f T |
|
52 |
| fold_types _ _ = I; |
|
53 |
||
54 |
||
79124 | 55 |
(* ordering *) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
56 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
57 |
local |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
58 |
|
79119 | 59 |
fun cons_nr (ZTVar _) = 0 |
60 |
| cons_nr (ZFun _) = 1 |
|
61 |
| cons_nr ZProp = 2 |
|
62 |
| cons_nr (ZItself _) = 3 |
|
63 |
| cons_nr (ZType0 _) = 4 |
|
64 |
| cons_nr (ZType1 _) = 5 |
|
65 |
| cons_nr (ZType _) = 6; |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
66 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
67 |
val fast_indexname_ord = Term_Ord.fast_indexname_ord; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
68 |
val sort_ord = Term_Ord.sort_ord; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
69 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
70 |
in |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
71 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
72 |
fun ztyp_ord TU = |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
73 |
if pointer_eq TU then EQUAL |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
74 |
else |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
75 |
(case TU of |
79119 | 76 |
(ZTVar (a, A), ZTVar (b, B)) => |
77 |
(case fast_indexname_ord (a, b) of EQUAL => sort_ord (A, B) | ord => ord) |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
78 |
| (ZFun (T, T'), ZFun (U, U')) => |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
79 |
(case ztyp_ord (T, U) of EQUAL => ztyp_ord (T', U') | ord => ord) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
80 |
| (ZProp, ZProp) => EQUAL |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
81 |
| (ZItself T, ZItself U) => ztyp_ord (T, U) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
82 |
| (ZType0 a, ZType0 b) => fast_string_ord (a, b) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
83 |
| (ZType1 (a, T), ZType1 (b, U)) => |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
84 |
(case fast_string_ord (a, b) of EQUAL => ztyp_ord (T, U) | ord => ord) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
85 |
| (ZType (a, Ts), ZType (b, Us)) => |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
86 |
(case fast_string_ord (a, b) of EQUAL => dict_ord ztyp_ord (Ts, Us) | ord => ord) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
87 |
| (T, U) => int_ord (cons_nr T, cons_nr U)); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
88 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
89 |
end; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
90 |
|
79124 | 91 |
end; |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
92 |
|
79124 | 93 |
|
94 |
(* term items *) |
|
95 |
||
79163 | 96 |
structure ZTypes = Table(type key = ztyp val ord = ZTerm.ztyp_ord); |
97 |
||
79124 | 98 |
structure ZTVars: |
99 |
sig |
|
100 |
include TERM_ITEMS |
|
101 |
val add_tvarsT: ztyp -> set -> set |
|
102 |
val add_tvars: zterm -> set -> set |
|
103 |
end = |
|
104 |
struct |
|
105 |
open TVars; |
|
106 |
val add_tvarsT = ZTerm.fold_tvars add_set; |
|
107 |
val add_tvars = ZTerm.fold_types add_tvarsT; |
|
108 |
end; |
|
109 |
||
110 |
structure ZVars: |
|
111 |
sig |
|
112 |
include TERM_ITEMS |
|
113 |
val add_vars: zterm -> set -> set |
|
114 |
end = |
|
115 |
struct |
|
116 |
||
117 |
structure Term_Items = Term_Items |
|
118 |
( |
|
119 |
type key = indexname * ztyp; |
|
120 |
val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord ZTerm.ztyp_ord); |
|
121 |
); |
|
122 |
open Term_Items; |
|
123 |
||
124 |
val add_vars = ZTerm.fold_aterms (fn ZVar v => add_set v | _ => I); |
|
125 |
||
126 |
end; |
|
127 |
||
128 |
||
129 |
(* proofs *) |
|
130 |
||
79126 | 131 |
datatype zproof_name = |
132 |
ZAxiom of string |
|
133 |
| ZOracle of string |
|
134 |
| ZBox of serial; |
|
135 |
||
79124 | 136 |
datatype zproof = |
137 |
ZDummy (*dummy proof*) |
|
79126 | 138 |
| ZConstP of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table |
79124 | 139 |
| ZBoundP of int |
140 |
| ZHyp of zterm |
|
141 |
| ZAbst of string * ztyp * zproof |
|
142 |
| ZAbsP of string * zterm * zproof |
|
143 |
| ZAppt of zproof * zterm |
|
144 |
| ZAppP of zproof * zproof |
|
79126 | 145 |
| ZClassP of ztyp * class; (*OFCLASS proof from sorts algebra*) |
79124 | 146 |
|
147 |
||
148 |
||
149 |
(*** local ***) |
|
150 |
||
151 |
signature ZTERM = |
|
152 |
sig |
|
153 |
datatype ztyp = datatype ztyp |
|
154 |
datatype zterm = datatype zterm |
|
155 |
datatype zproof = datatype zproof |
|
156 |
val fold_tvars: (indexname * sort -> 'a -> 'a) -> ztyp -> 'a -> 'a |
|
157 |
val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a |
|
158 |
val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a |
|
159 |
val ztyp_ord: ztyp * ztyp -> order |
|
160 |
val aconv_zterm: zterm * zterm -> bool |
|
79200 | 161 |
val incr_bv_same: int -> int -> zterm Same.operation |
162 |
val incr_bv: int -> int -> zterm -> zterm |
|
163 |
val incr_boundvars: int -> zterm -> zterm |
|
79124 | 164 |
val ztyp_of: typ -> ztyp |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
165 |
val zterm_cache_consts: Consts.T -> {zterm: term -> zterm, ztyp: typ -> ztyp} |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
166 |
val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp} |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
167 |
val zterm_of: theory -> term -> zterm |
79124 | 168 |
val typ_of: ztyp -> typ |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
169 |
val term_of_consts: Consts.T -> zterm -> term |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
170 |
val term_of: theory -> zterm -> term |
79200 | 171 |
val norm_type: Type.tyenv -> ztyp -> ztyp |
172 |
val norm_term: theory -> Envir.env -> zterm -> zterm |
|
79124 | 173 |
val dummy_proof: 'a -> zproof |
174 |
val todo_proof: 'a -> zproof |
|
79126 | 175 |
val axiom_proof: theory -> string -> term -> zproof |
176 |
val oracle_proof: theory -> string -> term -> zproof |
|
79124 | 177 |
val assume_proof: theory -> term -> zproof |
178 |
val trivial_proof: theory -> term -> zproof |
|
179 |
val implies_intr_proof: theory -> term -> zproof -> zproof |
|
180 |
val forall_intr_proof: theory -> typ -> string * term -> zproof -> zproof |
|
181 |
val forall_elim_proof: theory -> term -> zproof -> zproof |
|
79128 | 182 |
val of_class_proof: typ * class -> zproof |
79124 | 183 |
val reflexive_proof: theory -> typ -> term -> zproof |
184 |
val symmetric_proof: theory -> typ -> term -> term -> zproof -> zproof |
|
185 |
val transitive_proof: theory -> typ -> term -> term -> term -> zproof -> zproof -> zproof |
|
186 |
val equal_intr_proof: theory -> term -> term -> zproof -> zproof -> zproof |
|
187 |
val equal_elim_proof: theory -> term -> term -> zproof -> zproof -> zproof |
|
188 |
val abstract_rule_proof: theory -> typ -> typ -> string * term -> term -> term -> zproof -> zproof |
|
189 |
val combination_proof: theory -> typ -> typ -> term -> term -> term -> term -> |
|
190 |
zproof -> zproof -> zproof |
|
79133 | 191 |
val generalize_proof: Names.set * Names.set -> int -> zproof -> zproof |
79149 | 192 |
val instantiate_proof: theory -> |
193 |
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> zproof -> zproof |
|
79135 | 194 |
val varifyT_proof: ((string * sort) * (indexname * sort)) list -> zproof -> zproof |
79152 | 195 |
val legacy_freezeT_proof: term -> zproof -> zproof |
79150 | 196 |
val incr_indexes_proof: int -> zproof -> zproof |
79155 | 197 |
val rotate_proof: theory -> term list -> term -> (string * typ) list -> |
198 |
term list -> int -> zproof -> zproof |
|
199 |
val permute_prems_proof: theory -> term list -> int -> int -> zproof -> zproof |
|
79124 | 200 |
end; |
201 |
||
202 |
structure ZTerm: ZTERM = |
|
203 |
struct |
|
204 |
||
205 |
datatype ztyp = datatype ztyp; |
|
206 |
datatype zterm = datatype zterm; |
|
207 |
datatype zproof = datatype zproof; |
|
208 |
||
209 |
open ZTerm; |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
210 |
|
79119 | 211 |
fun aconv_zterm (tm1, tm2) = |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
212 |
pointer_eq (tm1, tm2) orelse |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
213 |
(case (tm1, tm2) of |
79119 | 214 |
(ZApp (t1, u1), ZApp (t2, u2)) => aconv_zterm (t1, t2) andalso aconv_zterm (u1, u2) |
215 |
| (ZAbs (_, T1, t1), ZAbs (_, T2, t2)) => aconv_zterm (t1, t2) andalso T1 = T2 |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
216 |
| (a1, a2) => a1 = a2); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
217 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
218 |
|
79155 | 219 |
(* derived operations *) |
220 |
||
221 |
val mk_ZAbst = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf)); |
|
222 |
val mk_ZAbsP = fold_rev (fn t => fn prf => ZAbsP ("H", t, prf)); |
|
223 |
||
224 |
val mk_ZAppt = Library.foldl ZAppt; |
|
225 |
val mk_ZAppP = Library.foldl ZAppP; |
|
226 |
||
227 |
||
79200 | 228 |
(* substitution of bound variables *) |
229 |
||
230 |
fun incr_bv_same inc = |
|
231 |
if inc = 0 then fn _ => Same.same |
|
232 |
else |
|
233 |
let |
|
234 |
fun term lev (ZBound i) = if i >= lev then ZBound (i + inc) else raise Same.SAME |
|
235 |
| term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t) |
|
236 |
| term lev (ZApp (t, u)) = |
|
237 |
(ZApp (term lev t, Same.commit (term lev) u) handle Same.SAME => |
|
238 |
ZApp (t, term lev u)) |
|
239 |
| term _ _ = raise Same.SAME; |
|
240 |
in term end; |
|
241 |
||
242 |
fun incr_bv inc lev = Same.commit (incr_bv_same inc lev); |
|
243 |
||
244 |
fun incr_boundvars inc = incr_bv inc 0; |
|
245 |
||
246 |
fun subst_bound arg body = |
|
247 |
let |
|
248 |
fun term lev (ZBound i) = |
|
249 |
if i < lev then raise Same.SAME (*var is locally bound*) |
|
250 |
else if i = lev then incr_boundvars lev arg |
|
251 |
else ZBound (i - 1) (*loose: change it*) |
|
252 |
| term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t) |
|
253 |
| term lev (ZApp (t, u)) = |
|
254 |
(ZApp (term lev t, Same.commit (term lev) u) |
|
255 |
handle Same.SAME => ZApp (t, term lev u)) |
|
256 |
| term _ _ = raise Same.SAME; |
|
257 |
in Same.commit (term 0) body end; |
|
258 |
||
259 |
||
260 |
(* direct substitution *) |
|
79132 | 261 |
|
262 |
fun subst_type_same tvar = |
|
263 |
let |
|
264 |
fun typ (ZTVar x) = tvar x |
|
265 |
| typ (ZFun (T, U)) = (ZFun (typ T, Same.commit typ U) handle Same.SAME => ZFun (T, typ U)) |
|
266 |
| typ ZProp = raise Same.SAME |
|
267 |
| typ (ZItself T) = ZItself (typ T) |
|
268 |
| typ (ZType0 _) = raise Same.SAME |
|
269 |
| typ (ZType1 (a, T)) = ZType1 (a, typ T) |
|
270 |
| typ (ZType (a, Ts)) = ZType (a, Same.map typ Ts); |
|
271 |
in typ end; |
|
272 |
||
273 |
fun subst_term_same typ var = |
|
274 |
let |
|
275 |
fun term (ZVar (x, T)) = |
|
276 |
let val (T', same) = Same.commit_id typ T in |
|
277 |
(case Same.catch var (x, T') of |
|
278 |
NONE => if same then raise Same.SAME else ZVar (x, T') |
|
279 |
| SOME t' => t') |
|
280 |
end |
|
281 |
| term (ZBound _) = raise Same.SAME |
|
282 |
| term (ZConst0 _) = raise Same.SAME |
|
283 |
| term (ZConst1 (a, T)) = ZConst1 (a, typ T) |
|
284 |
| term (ZConst (a, Ts)) = ZConst (a, Same.map typ Ts) |
|
285 |
| term (ZAbs (a, T, t)) = |
|
286 |
(ZAbs (a, typ T, Same.commit term t) handle Same.SAME => ZAbs (a, T, term t)) |
|
287 |
| term (ZApp (t, u)) = |
|
288 |
(ZApp (term t, Same.commit term u) handle Same.SAME => ZApp (t, term u)) |
|
289 |
| term (ZClass (T, c)) = ZClass (typ T, c); |
|
290 |
in term end; |
|
291 |
||
79145 | 292 |
fun map_insts_same typ term (instT, inst) = |
293 |
let |
|
294 |
val changed = Unsynchronized.ref false; |
|
79146
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
295 |
fun apply f x = |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
296 |
(case Same.catch f x of |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
297 |
NONE => NONE |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
298 |
| some => (changed := true; some)); |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
299 |
|
79145 | 300 |
val instT' = |
301 |
(instT, instT) |-> ZTVars.fold (fn (v, T) => |
|
79146
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
302 |
(case apply typ T of |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
303 |
NONE => I |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
304 |
| SOME T' => ZTVars.update (v, T'))); |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
305 |
|
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
306 |
val vars' = |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
307 |
(inst, ZVars.empty) |-> ZVars.fold (fn ((v, T), _) => |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
308 |
(case apply typ T of |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
309 |
NONE => I |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
310 |
| SOME T' => ZVars.add ((v, T), (v, T')))); |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
311 |
|
79145 | 312 |
val inst' = |
79146
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
313 |
if ZVars.is_empty vars' then |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
314 |
(inst, inst) |-> ZVars.fold (fn (v, t) => |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
315 |
(case apply term t of |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
316 |
NONE => I |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
317 |
| SOME t' => ZVars.update (v, t'))) |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
318 |
else |
79145 | 319 |
ZVars.dest inst |
79146
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
320 |
|> map (fn (v, t) => (the_default v (ZVars.lookup vars' v), the_default t (apply term t))) |
feb94ac5df41
more accurate treatment of term variables after instantiation of type variables;
wenzelm
parents:
79145
diff
changeset
|
321 |
|> ZVars.make_strict; |
79145 | 322 |
in if ! changed then (instT', inst') else raise Same.SAME end; |
323 |
||
79132 | 324 |
fun map_proof_same typ term = |
325 |
let |
|
326 |
fun proof ZDummy = raise Same.SAME |
|
327 |
| proof (ZConstP (a, A, instT, inst)) = |
|
79148
99201e7b1d94
proper treatment of ZConstP: term represents body of closure;
wenzelm
parents:
79147
diff
changeset
|
328 |
let val (instT', inst') = map_insts_same typ term (instT, inst) |
99201e7b1d94
proper treatment of ZConstP: term represents body of closure;
wenzelm
parents:
79147
diff
changeset
|
329 |
in ZConstP (a, A, instT', inst') end |
79132 | 330 |
| proof (ZBoundP _) = raise Same.SAME |
331 |
| proof (ZHyp h) = ZHyp (term h) |
|
332 |
| proof (ZAbst (a, T, p)) = |
|
333 |
(ZAbst (a, typ T, Same.commit proof p) handle Same.SAME => ZAbst (a, T, proof p)) |
|
334 |
| proof (ZAbsP (a, t, p)) = |
|
335 |
(ZAbsP (a, term t, Same.commit proof p) handle Same.SAME => ZAbsP (a, t, proof p)) |
|
336 |
| proof (ZAppt (p, t)) = |
|
337 |
(ZAppt (proof p, Same.commit term t) handle Same.SAME => ZAppt (p, term t)) |
|
338 |
| proof (ZAppP (p, q)) = |
|
339 |
(ZAppP (proof p, Same.commit proof q) handle Same.SAME => ZAppP (p, proof q)) |
|
340 |
| proof (ZClassP (T, c)) = ZClassP (typ T, c); |
|
341 |
in proof end; |
|
342 |
||
79144 | 343 |
fun map_proof_types_same typ = |
344 |
map_proof_same typ (subst_term_same typ Same.same); |
|
345 |
||
79124 | 346 |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
347 |
(* convert ztyp / zterm vs. regular typ / term *) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
348 |
|
79119 | 349 |
fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
350 |
| ztyp_of (TVar v) = ZTVar v |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
351 |
| ztyp_of (Type ("fun", [T, U])) = ZFun (ztyp_of T, ztyp_of U) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
352 |
| ztyp_of (Type (c, [])) = if c = "prop" then ZProp else ZType0 c |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
353 |
| ztyp_of (Type (c, [T])) = if c = "itself" then ZItself (ztyp_of T) else ZType1 (c, ztyp_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
354 |
| ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
355 |
|
79163 | 356 |
fun ztyp_cache () = Typtab.unsynchronized_cache ztyp_of; |
357 |
||
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
358 |
fun zterm_cache_consts consts = |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
359 |
let |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
360 |
val typargs = Consts.typargs consts; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
361 |
|
79163 | 362 |
val ztyp = ztyp_cache (); |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
363 |
|
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
364 |
fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp T) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
365 |
| zterm (Var (xi, T)) = ZVar (xi, ztyp T) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
366 |
| zterm (Bound i) = ZBound i |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
367 |
| zterm (Const (c, T)) = |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
368 |
(case typargs (c, T) of |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
369 |
[] => ZConst0 c |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
370 |
| [T] => ZConst1 (c, ztyp T) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
371 |
| Ts => ZConst (c, map ztyp Ts)) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
372 |
| zterm (Abs (a, T, b)) = ZAbs (a, ztyp T, zterm b) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
373 |
| zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) = |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
374 |
if String.isSuffix Logic.class_suffix c then |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
375 |
ZClass (ztyp (Logic.dest_type u), Logic.class_of_const c) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
376 |
else ZApp (zterm t, zterm u) |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
377 |
| zterm (t $ u) = ZApp (zterm t, zterm u); |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
378 |
in {ztyp = ztyp, zterm = zterm} end; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
379 |
|
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
380 |
val zterm_cache = zterm_cache_consts o Sign.consts_of; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
381 |
val zterm_of = #zterm o zterm_cache; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
382 |
|
79119 | 383 |
fun typ_of (ZTVar ((a, ~1), S)) = TFree (a, S) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
384 |
| typ_of (ZTVar v) = TVar v |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
385 |
| typ_of (ZFun (T, U)) = typ_of T --> typ_of U |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
386 |
| typ_of ZProp = propT |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
387 |
| typ_of (ZItself T) = Term.itselfT (typ_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
388 |
| typ_of (ZType0 c) = Type (c, []) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
389 |
| typ_of (ZType1 (c, T)) = Type (c, [typ_of T]) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
390 |
| typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
391 |
|
79201 | 392 |
fun typ_cache () = ZTypes.unsynchronized_cache typ_of; |
393 |
||
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
394 |
fun term_of_consts consts = |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
395 |
let |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
396 |
val instance = Consts.instance consts; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
397 |
fun const (c, Ts) = Const (c, instance (c, Ts)); |
79119 | 398 |
fun term (ZVar ((x, ~1), T)) = Free (x, typ_of T) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
399 |
| term (ZVar (xi, T)) = Var (xi, typ_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
400 |
| term (ZBound i) = Bound i |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
401 |
| term (ZConst0 c) = const (c, []) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
402 |
| term (ZConst1 (c, T)) = const (c, [typ_of T]) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
403 |
| term (ZConst (c, Ts)) = const (c, map typ_of Ts) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
404 |
| term (ZAbs (a, T, b)) = Abs (a, typ_of T, term b) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
405 |
| term (ZApp (t, u)) = term t $ term u |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
406 |
| term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
407 |
in term end; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
408 |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
409 |
val term_of = term_of_consts o Sign.consts_of; |
79113
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
410 |
|
79119 | 411 |
|
79200 | 412 |
(* beta normalization wrt. environment *) |
413 |
||
414 |
local |
|
415 |
||
416 |
fun norm_type_same ztyp tyenv = |
|
417 |
if Vartab.is_empty tyenv then Same.same |
|
418 |
else |
|
419 |
let |
|
420 |
fun norm (ZTVar v) = |
|
421 |
(case Type.lookup tyenv v of |
|
422 |
SOME U => Same.commit norm (ztyp U) |
|
423 |
| NONE => raise Same.SAME) |
|
424 |
| norm (ZFun (T, U)) = |
|
425 |
(ZFun (norm T, Same.commit norm U) |
|
426 |
handle Same.SAME => ZFun (T, norm U)) |
|
427 |
| norm ZProp = raise Same.SAME |
|
428 |
| norm (ZItself T) = ZItself (norm T) |
|
429 |
| norm (ZType0 _) = raise Same.SAME |
|
430 |
| norm (ZType1 (a, T)) = ZType1 (a, norm T) |
|
431 |
| norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts); |
|
432 |
in norm end; |
|
433 |
||
79204 | 434 |
fun norm_term_same thy (envir as Envir.Envir {tyenv, tenv, ...}) = |
79200 | 435 |
if Envir.is_empty envir then Same.same |
436 |
else |
|
437 |
let |
|
79204 | 438 |
val {ztyp, zterm} = zterm_cache_consts (Sign.consts_of thy); |
79201 | 439 |
val typ = typ_cache (); |
79200 | 440 |
|
441 |
val lookup = |
|
442 |
if Vartab.is_empty tenv then K NONE |
|
443 |
else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm); |
|
444 |
||
445 |
val normT = norm_type_same ztyp tyenv; |
|
446 |
||
447 |
fun norm (ZVar (xi, T)) = |
|
448 |
(case lookup (xi, T) of |
|
449 |
SOME u => Same.commit norm u |
|
450 |
| NONE => ZVar (xi, normT T)) |
|
451 |
| norm (ZBound _) = raise Same.SAME |
|
452 |
| norm (ZConst0 _) = raise Same.SAME |
|
453 |
| norm (ZConst1 (a, T)) = ZConst1 (a, normT T) |
|
454 |
| norm (ZConst (a, Ts)) = ZConst (a, Same.map normT Ts) |
|
455 |
| norm (ZAbs (a, T, t)) = |
|
456 |
(ZAbs (a, normT T, Same.commit norm t) |
|
457 |
handle Same.SAME => ZAbs (a, T, norm t)) |
|
458 |
| norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_bound t body) |
|
459 |
| norm (ZApp (f, t)) = |
|
460 |
((case norm f of |
|
461 |
ZAbs (_, _, body) => Same.commit norm (subst_bound t body) |
|
462 |
| nf => ZApp (nf, Same.commit norm t)) |
|
463 |
handle Same.SAME => ZApp (f, norm t)) |
|
464 |
| norm _ = raise Same.SAME; |
|
465 |
in norm end; |
|
466 |
||
467 |
in |
|
468 |
||
469 |
fun norm_type tyenv = |
|
79201 | 470 |
Same.commit (norm_type_same (ztyp_cache ()) tyenv); |
79200 | 471 |
|
79204 | 472 |
fun norm_term thy envir = |
473 |
Same.commit (norm_term_same thy envir); |
|
79200 | 474 |
|
475 |
end; |
|
476 |
||
477 |
||
79119 | 478 |
|
479 |
(** proof construction **) |
|
79113
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
480 |
|
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
481 |
fun dummy_proof _ = ZDummy; |
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
482 |
val todo_proof = dummy_proof; |
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
483 |
|
79124 | 484 |
|
79161 | 485 |
(* constants *) |
79124 | 486 |
|
79126 | 487 |
fun const_proof thy a A = |
79119 | 488 |
let |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
489 |
val t = zterm_of thy A; |
79154 | 490 |
val instT = |
491 |
ZTVars.build (t |> (fold_types o fold_tvars) (fn v => fn tab => |
|
492 |
if ZTVars.defined tab v then tab else ZTVars.update (v, ZTVar v) tab)); |
|
493 |
val inst = |
|
494 |
ZVars.build (t |> fold_aterms (fn a => fn tab => |
|
495 |
(case a of |
|
496 |
ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab |
|
497 |
| _ => tab))); |
|
79126 | 498 |
in ZConstP (a, t, instT, inst) end; |
499 |
||
79161 | 500 |
fun map_const_proof (f, g) prf = |
501 |
(case prf of |
|
502 |
ZConstP (a, A, instT, inst) => |
|
503 |
let |
|
504 |
val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT; |
|
505 |
val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst; |
|
506 |
in ZConstP (a, A, instT', inst') end |
|
507 |
| _ => prf); |
|
508 |
||
509 |
||
510 |
(* basic logic *) |
|
511 |
||
512 |
fun axiom_proof thy name = |
|
513 |
const_proof thy (ZAxiom name); |
|
514 |
||
515 |
fun oracle_proof thy name = |
|
516 |
const_proof thy (ZOracle name); |
|
79119 | 517 |
|
518 |
fun assume_proof thy A = |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
519 |
ZHyp (zterm_of thy A); |
79119 | 520 |
|
521 |
fun trivial_proof thy A = |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
522 |
ZAbsP ("H", zterm_of thy A, ZBoundP 0); |
79119 | 523 |
|
524 |
fun implies_intr_proof thy A prf = |
|
525 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
526 |
val h = zterm_of thy A; |
79157 | 527 |
fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else raise Same.SAME |
528 |
| proof i (ZAbst (x, T, p)) = ZAbst (x, T, proof i p) |
|
529 |
| proof i (ZAbsP (x, t, p)) = ZAbsP (x, t, proof (i + 1) p) |
|
530 |
| proof i (ZAppt (p, t)) = ZAppt (proof i p, t) |
|
531 |
| proof i (ZAppP (p, q)) = |
|
532 |
(ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME => |
|
533 |
ZAppP (p, proof i q)) |
|
534 |
| proof _ _ = raise Same.SAME; |
|
535 |
in ZAbsP ("H", h, Same.commit (proof 0) prf) end; |
|
79119 | 536 |
|
79124 | 537 |
fun forall_intr_proof thy T (a, x) prf = |
79119 | 538 |
let |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
539 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
540 |
val Z = ztyp T; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
541 |
val z = zterm x; |
79119 | 542 |
|
79157 | 543 |
fun term i b = |
79119 | 544 |
if aconv_zterm (b, z) then ZBound i |
545 |
else |
|
546 |
(case b of |
|
79157 | 547 |
ZAbs (x, T, t) => ZAbs (x, T, term (i + 1) t) |
79156 | 548 |
| ZApp (t, u) => |
79157 | 549 |
(ZApp (term i t, Same.commit (term i) u) handle Same.SAME => |
550 |
ZApp (t, term i u)) |
|
79156 | 551 |
| _ => raise Same.SAME); |
79119 | 552 |
|
79157 | 553 |
fun proof i (ZAbst (x, T, prf)) = ZAbst (x, T, proof (i + 1) prf) |
554 |
| proof i (ZAbsP (x, t, prf)) = |
|
555 |
(ZAbsP (x, term i t, Same.commit (proof i) prf) handle Same.SAME => |
|
556 |
ZAbsP (x, t, proof i prf)) |
|
557 |
| proof i (ZAppt (p, t)) = |
|
558 |
(ZAppt (proof i p, Same.commit (term i) t) handle Same.SAME => |
|
559 |
ZAppt (p, term i t)) |
|
560 |
| proof i (ZAppP (p, q)) = |
|
561 |
(ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME => |
|
562 |
ZAppP (p, proof i q)) |
|
563 |
| proof _ _ = raise Same.SAME; |
|
79119 | 564 |
|
79157 | 565 |
in ZAbst (a, Z, Same.commit (proof 0) prf) end; |
79119 | 566 |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
567 |
fun forall_elim_proof thy t p = ZAppt (p, zterm_of thy t); |
79119 | 568 |
|
79128 | 569 |
fun of_class_proof (T, c) = ZClassP (ztyp_of T, c); |
570 |
||
79124 | 571 |
|
572 |
(* equality *) |
|
573 |
||
574 |
local |
|
575 |
||
576 |
val thy0 = |
|
577 |
Context.the_global_context () |
|
578 |
|> Sign.add_types_global [(Binding.name "fun", 2, NoSyn), (Binding.name "prop", 0, NoSyn)] |
|
579 |
|> Sign.local_path |
|
580 |
|> Sign.add_consts |
|
581 |
[(Binding.name "all", (Term.aT [] --> propT) --> propT, NoSyn), |
|
582 |
(Binding.name "imp", propT --> propT --> propT, NoSyn), |
|
583 |
(Binding.name "eq", Term.aT [] --> Term.aT [] --> propT, NoSyn)]; |
|
584 |
||
585 |
val [reflexive_axiom, symmetric_axiom, transitive_axiom, equal_intr_axiom, equal_elim_axiom, |
|
586 |
abstract_rule_axiom, combination_axiom] = |
|
79126 | 587 |
Theory.equality_axioms |> map (fn (b, t) => axiom_proof thy0 (Sign.full_name thy0 b) t); |
79124 | 588 |
|
589 |
in |
|
590 |
||
591 |
val is_reflexive_proof = |
|
79126 | 592 |
fn ZConstP (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false; |
79124 | 593 |
|
594 |
fun reflexive_proof thy T t = |
|
595 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
596 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
597 |
val A = ztyp T; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
598 |
val x = zterm t; |
79126 | 599 |
in map_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end; |
79124 | 600 |
|
601 |
fun symmetric_proof thy T t u prf = |
|
602 |
if is_reflexive_proof prf then prf |
|
603 |
else |
|
604 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
605 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
606 |
val A = ztyp T; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
607 |
val x = zterm t; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
608 |
val y = zterm u; |
79126 | 609 |
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom; |
79124 | 610 |
in ZAppP (ax, prf) end; |
611 |
||
612 |
fun transitive_proof thy T t u v prf1 prf2 = |
|
613 |
if is_reflexive_proof prf1 then prf2 |
|
614 |
else if is_reflexive_proof prf2 then prf1 |
|
615 |
else |
|
616 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
617 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
618 |
val A = ztyp T; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
619 |
val x = zterm t; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
620 |
val y = zterm u; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
621 |
val z = zterm v; |
79126 | 622 |
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom; |
79124 | 623 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
624 |
||
625 |
fun equal_intr_proof thy t u prf1 prf2 = |
|
626 |
let |
|
79160 | 627 |
val {zterm, ...} = zterm_cache thy; |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
628 |
val A = zterm t; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
629 |
val B = zterm u; |
79126 | 630 |
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom; |
79124 | 631 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
632 |
||
633 |
fun equal_elim_proof thy t u prf1 prf2 = |
|
634 |
let |
|
79160 | 635 |
val {zterm, ...} = zterm_cache thy; |
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
636 |
val A = zterm t; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
637 |
val B = zterm u; |
79126 | 638 |
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom; |
79124 | 639 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
640 |
||
641 |
fun abstract_rule_proof thy T U x t u prf = |
|
642 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
643 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
644 |
val A = ztyp T; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
645 |
val B = ztyp U; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
646 |
val f = zterm t; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
647 |
val g = zterm u; |
79126 | 648 |
val ax = |
649 |
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g) |
|
650 |
abstract_rule_axiom; |
|
79124 | 651 |
in ZAppP (ax, forall_intr_proof thy T x prf) end; |
652 |
||
653 |
fun combination_proof thy T U f g t u prf1 prf2 = |
|
654 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
655 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
656 |
val A = ztyp T; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
657 |
val B = ztyp U; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
658 |
val f' = zterm f; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
659 |
val g' = zterm g; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
660 |
val x = zterm t; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
661 |
val y = zterm u; |
79124 | 662 |
val ax = |
79126 | 663 |
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y) |
79124 | 664 |
combination_axiom; |
665 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
|
666 |
||
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
667 |
end; |
79124 | 668 |
|
79133 | 669 |
|
670 |
(* substitution *) |
|
671 |
||
672 |
fun generalize_proof (tfrees, frees) idx prf = |
|
673 |
let |
|
674 |
val typ = |
|
675 |
if Names.is_empty tfrees then Same.same else |
|
79163 | 676 |
ZTypes.unsynchronized_cache |
677 |
(subst_type_same (fn ((a, i), S) => |
|
678 |
if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S) |
|
679 |
else raise Same.SAME)); |
|
79136 | 680 |
val term = |
79147 | 681 |
subst_term_same typ (fn ((x, i), T) => |
682 |
if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T) |
|
683 |
else raise Same.SAME); |
|
79136 | 684 |
in Same.commit (map_proof_same typ term) prf end; |
79133 | 685 |
|
79149 | 686 |
fun instantiate_proof thy (Ts, ts) prf = |
687 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
688 |
val {ztyp, zterm} = zterm_cache thy; |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
689 |
val instT = ZTVars.build (Ts |> fold (fn (v, T) => ZTVars.add (v, ztyp T))); |
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
690 |
val inst = ZVars.build (ts |> fold (fn ((v, T), t) => ZVars.add ((v, ztyp T), zterm t))); |
79149 | 691 |
val typ = |
692 |
if ZTVars.is_empty instT then Same.same |
|
79163 | 693 |
else ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))); |
79149 | 694 |
val term = subst_term_same typ (Same.function (ZVars.lookup inst)); |
695 |
in Same.commit (map_proof_same typ term) prf end; |
|
696 |
||
79135 | 697 |
fun varifyT_proof names prf = |
698 |
if null names then prf |
|
699 |
else |
|
700 |
let |
|
701 |
val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b))); |
|
79136 | 702 |
val typ = |
79163 | 703 |
ZTypes.unsynchronized_cache (subst_type_same (fn v => |
79136 | 704 |
(case ZTVars.lookup tab v of |
705 |
NONE => raise Same.SAME |
|
79163 | 706 |
| SOME w => ZTVar w))); |
79144 | 707 |
in Same.commit (map_proof_types_same typ) prf end; |
79135 | 708 |
|
79152 | 709 |
fun legacy_freezeT_proof t prf = |
710 |
(case Type.legacy_freezeT t of |
|
711 |
NONE => prf |
|
712 |
| SOME f => |
|
713 |
let |
|
714 |
val tvar = ztyp_of o Same.function f; |
|
79163 | 715 |
val typ = ZTypes.unsynchronized_cache (subst_type_same tvar); |
79152 | 716 |
in Same.commit (map_proof_types_same typ) prf end); |
717 |
||
79150 | 718 |
fun incr_indexes_proof inc prf = |
719 |
let |
|
720 |
fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME; |
|
721 |
fun var ((x, i), T) = if i >= 0 then ZVar ((x, i + inc), T) else raise Same.SAME; |
|
79163 | 722 |
val typ = ZTypes.unsynchronized_cache (subst_type_same tvar); |
79150 | 723 |
val term = subst_term_same typ var; |
724 |
in Same.commit (map_proof_same typ term) prf end; |
|
725 |
||
79155 | 726 |
|
727 |
(* permutations *) |
|
728 |
||
729 |
fun rotate_proof thy Bs Bi' params asms m prf = |
|
730 |
let |
|
79158
3c7ab17380a8
performance tuning: cache for ztyp_of within zterm_of;
wenzelm
parents:
79157
diff
changeset
|
731 |
val {ztyp, zterm} = zterm_cache thy; |
79155 | 732 |
val i = length asms; |
733 |
val j = length Bs; |
|
734 |
in |
|
735 |
mk_ZAbsP (map zterm Bs @ [zterm Bi']) (mk_ZAppP (prf, map ZBoundP |
|
736 |
(j downto 1) @ [mk_ZAbst (map (apsnd ztyp) params) (mk_ZAbsP (map zterm asms) |
|
737 |
(mk_ZAppP (mk_ZAppt (ZBoundP i, map ZBound ((length params - 1) downto 0)), |
|
738 |
map ZBoundP (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))])) |
|
739 |
end; |
|
740 |
||
741 |
fun permute_prems_proof thy prems' j k prf = |
|
742 |
let |
|
79160 | 743 |
val {zterm, ...} = zterm_cache thy; |
79155 | 744 |
val n = length prems'; |
745 |
in |
|
746 |
mk_ZAbsP (map zterm prems') |
|
747 |
(mk_ZAppP (prf, map ZBoundP ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k)))) |
|
748 |
end; |
|
749 |
||
79124 | 750 |
end; |