author | wenzelm |
Tue, 05 Dec 2023 11:37:24 +0100 | |
changeset 79128 | b6f5d4392388 |
parent 79126 | bdb33a2d4167 |
child 79132 | 6d3322477cfd |
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 |
||
96 |
structure ZTVars: |
|
97 |
sig |
|
98 |
include TERM_ITEMS |
|
99 |
val add_tvarsT: ztyp -> set -> set |
|
100 |
val add_tvars: zterm -> set -> set |
|
101 |
end = |
|
102 |
struct |
|
103 |
open TVars; |
|
104 |
val add_tvarsT = ZTerm.fold_tvars add_set; |
|
105 |
val add_tvars = ZTerm.fold_types add_tvarsT; |
|
106 |
end; |
|
107 |
||
108 |
structure ZVars: |
|
109 |
sig |
|
110 |
include TERM_ITEMS |
|
111 |
val add_vars: zterm -> set -> set |
|
112 |
end = |
|
113 |
struct |
|
114 |
||
115 |
structure Term_Items = Term_Items |
|
116 |
( |
|
117 |
type key = indexname * ztyp; |
|
118 |
val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord ZTerm.ztyp_ord); |
|
119 |
); |
|
120 |
open Term_Items; |
|
121 |
||
122 |
val add_vars = ZTerm.fold_aterms (fn ZVar v => add_set v | _ => I); |
|
123 |
||
124 |
end; |
|
125 |
||
126 |
||
127 |
(* proofs *) |
|
128 |
||
79126 | 129 |
datatype zproof_name = |
130 |
ZAxiom of string |
|
131 |
| ZOracle of string |
|
132 |
| ZBox of serial; |
|
133 |
||
79124 | 134 |
datatype zproof = |
135 |
ZDummy (*dummy proof*) |
|
79126 | 136 |
| ZConstP of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table |
79124 | 137 |
| ZBoundP of int |
138 |
| ZHyp of zterm |
|
139 |
| ZAbst of string * ztyp * zproof |
|
140 |
| ZAbsP of string * zterm * zproof |
|
141 |
| ZAppt of zproof * zterm |
|
142 |
| ZAppP of zproof * zproof |
|
79126 | 143 |
| ZClassP of ztyp * class; (*OFCLASS proof from sorts algebra*) |
79124 | 144 |
|
145 |
||
146 |
||
147 |
(*** local ***) |
|
148 |
||
149 |
signature ZTERM = |
|
150 |
sig |
|
151 |
datatype ztyp = datatype ztyp |
|
152 |
datatype zterm = datatype zterm |
|
153 |
datatype zproof = datatype zproof |
|
154 |
val fold_tvars: (indexname * sort -> 'a -> 'a) -> ztyp -> 'a -> 'a |
|
155 |
val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a |
|
156 |
val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a |
|
157 |
val ztyp_ord: ztyp * ztyp -> order |
|
158 |
val aconv_zterm: zterm * zterm -> bool |
|
159 |
val ztyp_of: typ -> ztyp |
|
160 |
val typ_of: ztyp -> typ |
|
161 |
val zterm_of: Consts.T -> term -> zterm |
|
162 |
val term_of: Consts.T -> zterm -> term |
|
163 |
val global_zterm_of: theory -> term -> zterm |
|
164 |
val global_term_of: theory -> zterm -> term |
|
165 |
val dummy_proof: 'a -> zproof |
|
166 |
val todo_proof: 'a -> zproof |
|
79126 | 167 |
val axiom_proof: theory -> string -> term -> zproof |
168 |
val oracle_proof: theory -> string -> term -> zproof |
|
79124 | 169 |
val assume_proof: theory -> term -> zproof |
170 |
val trivial_proof: theory -> term -> zproof |
|
171 |
val implies_intr_proof: theory -> term -> zproof -> zproof |
|
172 |
val forall_intr_proof: theory -> typ -> string * term -> zproof -> zproof |
|
173 |
val forall_elim_proof: theory -> term -> zproof -> zproof |
|
79128 | 174 |
val of_class_proof: typ * class -> zproof |
79124 | 175 |
val reflexive_proof: theory -> typ -> term -> zproof |
176 |
val symmetric_proof: theory -> typ -> term -> term -> zproof -> zproof |
|
177 |
val transitive_proof: theory -> typ -> term -> term -> term -> zproof -> zproof -> zproof |
|
178 |
val equal_intr_proof: theory -> term -> term -> zproof -> zproof -> zproof |
|
179 |
val equal_elim_proof: theory -> term -> term -> zproof -> zproof -> zproof |
|
180 |
val abstract_rule_proof: theory -> typ -> typ -> string * term -> term -> term -> zproof -> zproof |
|
181 |
val combination_proof: theory -> typ -> typ -> term -> term -> term -> term -> |
|
182 |
zproof -> zproof -> zproof |
|
183 |
end; |
|
184 |
||
185 |
structure ZTerm: ZTERM = |
|
186 |
struct |
|
187 |
||
188 |
datatype ztyp = datatype ztyp; |
|
189 |
datatype zterm = datatype zterm; |
|
190 |
datatype zproof = datatype zproof; |
|
191 |
||
192 |
open ZTerm; |
|
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
193 |
|
79119 | 194 |
fun aconv_zterm (tm1, tm2) = |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
195 |
pointer_eq (tm1, tm2) orelse |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
196 |
(case (tm1, tm2) of |
79119 | 197 |
(ZApp (t1, u1), ZApp (t2, u2)) => aconv_zterm (t1, t2) andalso aconv_zterm (u1, u2) |
198 |
| (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
|
199 |
| (a1, a2) => a1 = a2); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
200 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
201 |
|
79124 | 202 |
(* instantiation *) |
203 |
||
204 |
fun init_instT t = ZTVars.build (ZTVars.add_tvars t) |> ZTVars.map (fn v => fn _ => ZTVar v); |
|
205 |
fun init_inst t = ZVars.build (ZVars.add_vars t) |> ZVars.map (fn v => fn _ => ZVar v); |
|
79126 | 206 |
|
207 |
fun map_const_proof (f, g) prf = |
|
208 |
(case prf of |
|
209 |
ZConstP (a, A, instT, inst) => |
|
210 |
let |
|
211 |
val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT; |
|
212 |
val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst; |
|
213 |
in ZConstP (a, A, instT', inst') end |
|
214 |
| _ => prf); |
|
79124 | 215 |
|
216 |
||
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
217 |
(* convert ztyp / zterm vs. regular typ / term *) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
218 |
|
79119 | 219 |
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
|
220 |
| ztyp_of (TVar v) = ZTVar v |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
221 |
| 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
|
222 |
| 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
|
223 |
| 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
|
224 |
| 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
|
225 |
|
79119 | 226 |
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
|
227 |
| typ_of (ZTVar v) = TVar v |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
228 |
| 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
|
229 |
| typ_of ZProp = propT |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
230 |
| typ_of (ZItself T) = Term.itselfT (typ_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
231 |
| typ_of (ZType0 c) = Type (c, []) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
232 |
| typ_of (ZType1 (c, T)) = Type (c, [typ_of T]) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
233 |
| 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
|
234 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
235 |
fun zterm_of consts = |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
236 |
let |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
237 |
val typargs = Consts.typargs consts; |
79119 | 238 |
fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp_of T) |
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
239 |
| zterm (Var (xi, T)) = ZVar (xi, ztyp_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
240 |
| zterm (Bound i) = ZBound i |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
241 |
| zterm (Const (c, T)) = |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
242 |
(case typargs (c, T) of |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
243 |
[] => ZConst0 c |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
244 |
| [T] => ZConst1 (c, ztyp_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
245 |
| Ts => ZConst (c, map ztyp_of Ts)) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
246 |
| zterm (Abs (a, T, b)) = ZAbs (a, ztyp_of T, zterm b) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
247 |
| zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) = |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
248 |
if String.isSuffix Logic.class_suffix c then |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
249 |
ZClass (ztyp_of (Logic.dest_type u), Logic.class_of_const c) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
250 |
else ZApp (zterm t, zterm u) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
251 |
| zterm (t $ u) = ZApp (zterm t, zterm u); |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
252 |
in zterm end; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
253 |
|
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
254 |
fun term_of consts = |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
255 |
let |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
256 |
val instance = Consts.instance consts; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
257 |
fun const (c, Ts) = Const (c, instance (c, Ts)); |
79119 | 258 |
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
|
259 |
| term (ZVar (xi, T)) = Var (xi, typ_of T) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
260 |
| term (ZBound i) = Bound i |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
261 |
| term (ZConst0 c) = const (c, []) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
262 |
| term (ZConst1 (c, T)) = const (c, [typ_of T]) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
263 |
| term (ZConst (c, Ts)) = const (c, map typ_of Ts) |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
264 |
| 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
|
265 |
| term (ZApp (t, u)) = term t $ term u |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
266 |
| 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
|
267 |
in term end; |
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
268 |
|
79119 | 269 |
val global_zterm_of = zterm_of o Sign.consts_of; |
270 |
val global_term_of = term_of o Sign.consts_of; |
|
79113
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
271 |
|
79119 | 272 |
|
273 |
||
274 |
(** proof construction **) |
|
79113
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
275 |
|
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
276 |
fun dummy_proof _ = ZDummy; |
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
277 |
val todo_proof = dummy_proof; |
5109e4b2a292
pro-forma support for optional zproof: no proper content yet;
wenzelm
parents:
79098
diff
changeset
|
278 |
|
79124 | 279 |
|
280 |
(* basic logic *) |
|
281 |
||
79126 | 282 |
fun const_proof thy a A = |
79119 | 283 |
let |
284 |
val t = global_zterm_of thy A; |
|
79126 | 285 |
val instT = init_instT t; |
286 |
val inst = init_inst t; |
|
287 |
in ZConstP (a, t, instT, inst) end; |
|
288 |
||
289 |
fun axiom_proof thy name = const_proof thy (ZAxiom name); |
|
290 |
fun oracle_proof thy name = const_proof thy (ZOracle name); |
|
79119 | 291 |
|
292 |
fun assume_proof thy A = |
|
293 |
ZHyp (global_zterm_of thy A); |
|
294 |
||
295 |
fun trivial_proof thy A = |
|
296 |
ZAbsP ("H", global_zterm_of thy A, ZBoundP 0); |
|
297 |
||
298 |
fun implies_intr_proof thy A prf = |
|
299 |
let |
|
300 |
val h = global_zterm_of thy A; |
|
301 |
fun abs_hyp i (p as ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else p |
|
302 |
| abs_hyp i (ZAbst (x, T, p)) = ZAbst (x, T, abs_hyp i p) |
|
303 |
| abs_hyp i (ZAbsP (x, t, p)) = ZAbsP (x, t, abs_hyp (i + 1) p) |
|
304 |
| abs_hyp i (ZAppt (p, t)) = ZAppt (abs_hyp i p, t) |
|
305 |
| abs_hyp i (ZAppP (p, q)) = ZAppP (abs_hyp i p, abs_hyp i q) |
|
306 |
| abs_hyp _ p = p; |
|
307 |
in ZAbsP ("H", h, abs_hyp 0 prf) end; |
|
308 |
||
79124 | 309 |
fun forall_intr_proof thy T (a, x) prf = |
79119 | 310 |
let |
79124 | 311 |
val Z = ztyp_of T; |
79119 | 312 |
val z = global_zterm_of thy x; |
313 |
||
314 |
fun abs_term i b = |
|
315 |
if aconv_zterm (b, z) then ZBound i |
|
316 |
else |
|
317 |
(case b of |
|
318 |
ZAbs (x, T, t) => ZAbs (x, T, abs_term (i + 1) t) |
|
319 |
| ZApp (t, u) => ZApp (abs_term i t, abs_term i u) |
|
320 |
| _ => b); |
|
321 |
||
79124 | 322 |
fun abs_proof i (ZAbst (x, T, prf)) = ZAbst (x, T, abs_proof (i + 1) prf) |
323 |
| abs_proof i (ZAbsP (x, t, prf)) = ZAbsP (x, abs_term i t, abs_proof i prf) |
|
324 |
| abs_proof i (ZAppt (p, t)) = ZAppt (abs_proof i p, abs_term i t) |
|
325 |
| abs_proof i (ZAppP (p, q)) = ZAppP (abs_proof i p, abs_proof i q) |
|
326 |
| abs_proof _ p = p; |
|
79119 | 327 |
|
79124 | 328 |
in ZAbst (a, Z, abs_proof 0 prf) end; |
79119 | 329 |
|
330 |
fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t); |
|
331 |
||
79128 | 332 |
fun of_class_proof (T, c) = ZClassP (ztyp_of T, c); |
333 |
||
79124 | 334 |
|
335 |
(* equality *) |
|
336 |
||
337 |
local |
|
338 |
||
339 |
val thy0 = |
|
340 |
Context.the_global_context () |
|
341 |
|> Sign.add_types_global [(Binding.name "fun", 2, NoSyn), (Binding.name "prop", 0, NoSyn)] |
|
342 |
|> Sign.local_path |
|
343 |
|> Sign.add_consts |
|
344 |
[(Binding.name "all", (Term.aT [] --> propT) --> propT, NoSyn), |
|
345 |
(Binding.name "imp", propT --> propT --> propT, NoSyn), |
|
346 |
(Binding.name "eq", Term.aT [] --> Term.aT [] --> propT, NoSyn)]; |
|
347 |
||
348 |
val [reflexive_axiom, symmetric_axiom, transitive_axiom, equal_intr_axiom, equal_elim_axiom, |
|
349 |
abstract_rule_axiom, combination_axiom] = |
|
79126 | 350 |
Theory.equality_axioms |> map (fn (b, t) => axiom_proof thy0 (Sign.full_name thy0 b) t); |
79124 | 351 |
|
352 |
in |
|
353 |
||
354 |
val is_reflexive_proof = |
|
79126 | 355 |
fn ZConstP (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false; |
79124 | 356 |
|
357 |
fun reflexive_proof thy T t = |
|
358 |
let |
|
359 |
val A = ztyp_of T; |
|
360 |
val x = global_zterm_of thy t; |
|
79126 | 361 |
in map_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end; |
79124 | 362 |
|
363 |
fun symmetric_proof thy T t u prf = |
|
364 |
if is_reflexive_proof prf then prf |
|
365 |
else |
|
366 |
let |
|
367 |
val A = ztyp_of T; |
|
368 |
val x = global_zterm_of thy t; |
|
369 |
val y = global_zterm_of thy u; |
|
79126 | 370 |
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom; |
79124 | 371 |
in ZAppP (ax, prf) end; |
372 |
||
373 |
fun transitive_proof thy T t u v prf1 prf2 = |
|
374 |
if is_reflexive_proof prf1 then prf2 |
|
375 |
else if is_reflexive_proof prf2 then prf1 |
|
376 |
else |
|
377 |
let |
|
378 |
val A = ztyp_of T; |
|
379 |
val x = global_zterm_of thy t; |
|
380 |
val y = global_zterm_of thy u; |
|
381 |
val z = global_zterm_of thy v; |
|
79126 | 382 |
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom; |
79124 | 383 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
384 |
||
385 |
fun equal_intr_proof thy t u prf1 prf2 = |
|
386 |
let |
|
387 |
val A = global_zterm_of thy t; |
|
388 |
val B = global_zterm_of thy u; |
|
79126 | 389 |
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom; |
79124 | 390 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
391 |
||
392 |
fun equal_elim_proof thy t u prf1 prf2 = |
|
393 |
let |
|
394 |
val A = global_zterm_of thy t; |
|
395 |
val B = global_zterm_of thy u; |
|
79126 | 396 |
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom; |
79124 | 397 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
398 |
||
399 |
fun abstract_rule_proof thy T U x t u prf = |
|
400 |
let |
|
401 |
val A = ztyp_of T; |
|
402 |
val B = ztyp_of U; |
|
403 |
val f = global_zterm_of thy t; |
|
404 |
val g = global_zterm_of thy u; |
|
79126 | 405 |
val ax = |
406 |
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g) |
|
407 |
abstract_rule_axiom; |
|
79124 | 408 |
in ZAppP (ax, forall_intr_proof thy T x prf) end; |
409 |
||
410 |
fun combination_proof thy T U f g t u prf1 prf2 = |
|
411 |
let |
|
412 |
val A = ztyp_of T; |
|
413 |
val B = ztyp_of U; |
|
414 |
val f' = global_zterm_of thy f; |
|
415 |
val g' = global_zterm_of thy g; |
|
416 |
val x = global_zterm_of thy t; |
|
417 |
val y = global_zterm_of thy u; |
|
418 |
val ax = |
|
79126 | 419 |
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y) |
79124 | 420 |
combination_axiom; |
421 |
in ZAppP (ZAppP (ax, prf1), prf2) end; |
|
422 |
||
79098
d8940e5bbb25
tight representation of types / terms / proof terms (presently unused);
wenzelm
parents:
diff
changeset
|
423 |
end; |
79124 | 424 |
|
425 |
end; |