32 signature THEORY = |
32 signature THEORY = |
33 sig |
33 sig |
34 include BASIC_THEORY |
34 include BASIC_THEORY |
35 (*theory extendsion primitives*) |
35 (*theory extendsion primitives*) |
36 val add_classes : (class * class list) list -> theory -> theory |
36 val add_classes : (class * class list) list -> theory -> theory |
|
37 val add_classes_i : (class * class list) list -> theory -> theory |
37 val add_classrel : (class * class) list -> theory -> theory |
38 val add_classrel : (class * class) list -> theory -> theory |
|
39 val add_classrel_i : (class * class) list -> theory -> theory |
38 val add_defsort : sort -> theory -> theory |
40 val add_defsort : sort -> theory -> theory |
|
41 val add_defsort_i : sort -> theory -> theory |
39 val add_types : (string * int * mixfix) list -> theory -> theory |
42 val add_types : (string * int * mixfix) list -> theory -> theory |
40 val add_tyabbrs : (string * string list * string * mixfix) list |
43 val add_tyabbrs : (string * string list * string * mixfix) list |
41 -> theory -> theory |
44 -> theory -> theory |
42 val add_tyabbrs_i : (string * string list * typ * mixfix) list |
45 val add_tyabbrs_i : (string * string list * typ * mixfix) list |
43 -> theory -> theory |
46 -> theory -> theory |
44 val add_arities : (string * sort list * sort) list -> theory -> theory |
47 val add_arities : (string * sort list * sort) list -> theory -> theory |
|
48 val add_arities_i : (string * sort list * sort) list -> theory -> theory |
45 val add_consts : (string * string * mixfix) list -> theory -> theory |
49 val add_consts : (string * string * mixfix) list -> theory -> theory |
46 val add_consts_i : (string * typ * mixfix) list -> theory -> theory |
50 val add_consts_i : (string * typ * mixfix) list -> theory -> theory |
47 val add_syntax : (string * string * mixfix) list -> theory -> theory |
51 val add_syntax : (string * string * mixfix) list -> theory -> theory |
48 val add_syntax_i : (string * typ * mixfix) list -> theory -> theory |
52 val add_syntax_i : (string * typ * mixfix) list -> theory -> theory |
49 val add_modesyntax : string * bool -> (string * string * mixfix) list -> theory -> theory |
53 val add_modesyntax : string * bool -> (string * string * mixfix) list -> theory -> theory |
61 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
65 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
62 val add_axioms : (string * string) list -> theory -> theory |
66 val add_axioms : (string * string) list -> theory -> theory |
63 val add_axioms_i : (string * term) list -> theory -> theory |
67 val add_axioms_i : (string * term) list -> theory -> theory |
64 val add_defs : (string * string) list -> theory -> theory |
68 val add_defs : (string * string) list -> theory -> theory |
65 val add_defs_i : (string * term) list -> theory -> theory |
69 val add_defs_i : (string * term) list -> theory -> theory |
|
70 val add_path : string -> theory -> theory |
|
71 val add_space : string * string list -> theory -> theory |
66 val add_name : string -> theory -> theory |
72 val add_name : string -> theory -> theory |
67 |
73 |
68 val set_oracle : (Sign.sg * exn -> term) -> theory -> theory |
74 val set_oracle : (Sign.sg * exn -> term) -> theory -> theory |
69 |
75 |
70 val merge_thy_list : bool -> theory list -> theory |
76 val merge_thy_list : bool -> theory list -> theory |
143 |
149 |
144 fun ext_sg extfun decls (thy as Theory {sign, ...}) = |
150 fun ext_sg extfun decls (thy as Theory {sign, ...}) = |
145 ext_thy thy (extfun decls sign) []; |
151 ext_thy thy (extfun decls sign) []; |
146 |
152 |
147 val add_classes = ext_sg Sign.add_classes; |
153 val add_classes = ext_sg Sign.add_classes; |
|
154 val add_classes_i = ext_sg Sign.add_classes_i; |
148 val add_classrel = ext_sg Sign.add_classrel; |
155 val add_classrel = ext_sg Sign.add_classrel; |
|
156 val add_classrel_i = ext_sg Sign.add_classrel_i; |
149 val add_defsort = ext_sg Sign.add_defsort; |
157 val add_defsort = ext_sg Sign.add_defsort; |
|
158 val add_defsort_i = ext_sg Sign.add_defsort_i; |
150 val add_types = ext_sg Sign.add_types; |
159 val add_types = ext_sg Sign.add_types; |
151 val add_tyabbrs = ext_sg Sign.add_tyabbrs; |
160 val add_tyabbrs = ext_sg Sign.add_tyabbrs; |
152 val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; |
161 val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; |
153 val add_arities = ext_sg Sign.add_arities; |
162 val add_arities = ext_sg Sign.add_arities; |
|
163 val add_arities_i = ext_sg Sign.add_arities_i; |
154 val add_consts = ext_sg Sign.add_consts; |
164 val add_consts = ext_sg Sign.add_consts; |
155 val add_consts_i = ext_sg Sign.add_consts_i; |
165 val add_consts_i = ext_sg Sign.add_consts_i; |
156 val add_syntax = ext_sg Sign.add_syntax; |
166 val add_syntax = ext_sg Sign.add_syntax; |
157 val add_syntax_i = ext_sg Sign.add_syntax_i; |
167 val add_syntax_i = ext_sg Sign.add_syntax_i; |
158 val add_modesyntax = curry (ext_sg Sign.add_modesyntax); |
168 val add_modesyntax = curry (ext_sg Sign.add_modesyntax); |
160 val add_trfuns = ext_sg Sign.add_trfuns; |
170 val add_trfuns = ext_sg Sign.add_trfuns; |
161 val add_trfunsT = ext_sg Sign.add_trfunsT; |
171 val add_trfunsT = ext_sg Sign.add_trfunsT; |
162 val add_tokentrfuns = ext_sg Sign.add_tokentrfuns; |
172 val add_tokentrfuns = ext_sg Sign.add_tokentrfuns; |
163 val add_trrules = ext_sg Sign.add_trrules; |
173 val add_trrules = ext_sg Sign.add_trrules; |
164 val add_trrules_i = ext_sg Sign.add_trrules_i; |
174 val add_trrules_i = ext_sg Sign.add_trrules_i; |
|
175 val add_path = ext_sg Sign.add_path; |
|
176 val add_space = ext_sg Sign.add_space; |
165 val add_name = ext_sg Sign.add_name; |
177 val add_name = ext_sg Sign.add_name; |
166 |
178 |
167 |
179 |
168 (* prepare axioms *) |
180 (* prepare axioms *) |
169 |
181 |
259 |
271 |
260 (* dest_defn *) |
272 (* dest_defn *) |
261 |
273 |
262 fun dest_defn tm = |
274 fun dest_defn tm = |
263 let |
275 let |
264 fun err msg = raise_term msg [tm]; |
276 fun err msg = raise TERM (msg, [tm]); |
265 |
277 |
266 val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) |
278 val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) |
267 handle TERM _ => err "Not a meta-equality (==)"; |
279 handle TERM _ => err "Not a meta-equality (==)"; |
268 val (head, args) = strip_comb lhs; |
280 val (head, args) = strip_comb lhs; |
269 val (c, ty) = dest_Const head |
281 val (c, ty) = dest_Const head |