diff --git a/src/Pure/pure_thy.ML b/src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML +++ b/src/Pure/pure_thy.ML @@ -1,254 +1,254 @@ (* Title: Pure/pure_thy.ML Author: Markus Wenzel, TU Muenchen Pure theory syntax and further logical content. *) signature PURE_THY = sig val old_appl_syntax: theory -> bool val old_appl_syntax_setup: theory -> theory val token_markers: string list end; structure Pure_Thy: PURE_THY = struct (* auxiliary *) val typ = Simple_Syntax.read_typ; val prop = Simple_Syntax.read_prop; val tycon = Lexicon.mark_type; val const = Lexicon.mark_const; val qualify = Binding.qualify true Context.PureN; fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); fun add_deps_type c thy = let val n = Sign.arity_number thy c; val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end fun add_deps_const c thy = let val T = Logic.unvarifyT_global (Sign.the_const_type thy c); val typargs = Sign.const_typargs thy (c, T); in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end; (* application syntax variants *) val appl_syntax = [("_appl", typ "('b \ 'a) \ args \ logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), ("_appl", typ "('b \ 'a) \ args \ aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; val applC_syntax = [("", typ "'a \ cargs", Mixfix.mixfix "_"), ("_cargs", typ "'a \ cargs \ cargs", mixfix ("_/ _", [1000, 1000], 1000)), ("_applC", typ "('b \ 'a) \ cargs \ logic", mixfix ("(1_/ _)", [1000, 1000], 999)), ("_applC", typ "('b \ 'a) \ cargs \ aprop", mixfix ("(1_/ _)", [1000, 1000], 999))]; structure Old_Appl_Syntax = Theory_Data ( type T = bool; val empty = false; val extend = I; fun merge (b1, b2) : T = if b1 = b2 then b1 else error "Cannot merge theories with different application syntax"; ); val old_appl_syntax = Old_Appl_Syntax.get; val old_appl_syntax_setup = Old_Appl_Syntax.put true #> Sign.del_syntax Syntax.mode_default applC_syntax #> Sign.add_syntax Syntax.mode_default appl_syntax; (* main content *) val token_markers = ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"]; val _ = Theory.setup - (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #> + (Sign.theory_naming #> Old_Appl_Syntax.put false #> Sign.add_types_global [(Binding.make ("fun", \<^here>), 2, NoSyn), (Binding.make ("prop", \<^here>), 0, NoSyn), (Binding.make ("itself", \<^here>), 1, NoSyn), (Binding.make ("dummy", \<^here>), 0, NoSyn), (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)] #> add_deps_type "fun" #> add_deps_type "prop" #> add_deps_type "itself" #> add_deps_type "dummy" #> add_deps_type "Pure.proof" #> Sign.add_nonterminals_global (map (fn name => Binding.make (name, \<^here>)) (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", "any", "prop'", "num_const", "float_const", "num_position", "float_position", "index", "struct", "tid_position", "tvar_position", "id_position", "longid_position", "var_position", "str_position", "string_position", "cartouche_position", "type_name", "class_name"])) #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) #> Sign.add_syntax Syntax.mode_default [("", typ "prop' \ prop", Mixfix.mixfix "_"), ("", typ "logic \ any", Mixfix.mixfix "_"), ("", typ "prop' \ any", Mixfix.mixfix "_"), ("", typ "logic \ logic", Mixfix.mixfix "'(_')"), ("", typ "prop' \ prop'", Mixfix.mixfix "'(_')"), ("_constrain", typ "logic \ type \ logic", mixfix ("_::_", [4, 0], 3)), ("_constrain", typ "prop' \ type \ prop'", mixfix ("_::_", [4, 0], 3)), ("_ignore_type", typ "'a", NoSyn), ("", typ "tid_position \ type", Mixfix.mixfix "_"), ("", typ "tvar_position \ type", Mixfix.mixfix "_"), ("", typ "type_name \ type", Mixfix.mixfix "_"), ("_type_name", typ "id \ type_name", Mixfix.mixfix "_"), ("_type_name", typ "longid \ type_name", Mixfix.mixfix "_"), ("_ofsort", typ "tid_position \ sort \ type", mixfix ("_::_", [1000, 0], 1000)), ("_ofsort", typ "tvar_position \ sort \ type", mixfix ("_::_", [1000, 0], 1000)), ("_dummy_ofsort", typ "sort \ type", mixfix ("'_()::_", [0], 1000)), ("", typ "class_name \ sort", Mixfix.mixfix "_"), ("_class_name", typ "id \ class_name", Mixfix.mixfix "_"), ("_class_name", typ "longid \ class_name", Mixfix.mixfix "_"), ("_dummy_sort", typ "sort", Mixfix.mixfix "'_"), ("_topsort", typ "sort", Mixfix.mixfix "{}"), ("_sort", typ "classes \ sort", Mixfix.mixfix "{_}"), ("", typ "class_name \ classes", Mixfix.mixfix "_"), ("_classes", typ "class_name \ classes \ classes", Mixfix.mixfix "_,_"), ("_tapp", typ "type \ type_name \ type", mixfix ("_ _", [1000, 0], 1000)), ("_tappl", typ "type \ types \ type_name \ type", Mixfix.mixfix "((1'(_,/ _')) _)"), ("", typ "type \ types", Mixfix.mixfix "_"), ("_types", typ "type \ types \ types", Mixfix.mixfix "_,/ _"), ("\<^type>fun", typ "type \ type \ type", mixfix ("(_/ \ _)", [1, 0], 0)), ("_bracket", typ "types \ type \ type", mixfix ("([_]/ \ _)", [0, 0], 0)), ("", typ "type \ type", Mixfix.mixfix "'(_')"), ("\<^type>dummy", typ "type", Mixfix.mixfix "'_"), ("_type_prop", typ "'a", NoSyn), ("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3\_./ _)", [0, 3], 3)), ("_abs", typ "'a", NoSyn), ("", typ "'a \ args", Mixfix.mixfix "_"), ("_args", typ "'a \ args \ args", Mixfix.mixfix "_,/ _"), ("", typ "id_position \ idt", Mixfix.mixfix "_"), ("_idtdummy", typ "idt", Mixfix.mixfix "'_"), ("_idtyp", typ "id_position \ type \ idt", mixfix ("_::_", [], 0)), ("_idtypdummy", typ "type \ idt", mixfix ("'_()::_", [], 0)), ("", typ "idt \ idt", Mixfix.mixfix "'(_')"), ("", typ "idt \ idts", Mixfix.mixfix "_"), ("_idts", typ "idt \ idts \ idts", mixfix ("_/ _", [1, 0], 0)), ("", typ "idt \ pttrn", Mixfix.mixfix "_"), ("", typ "pttrn \ pttrns", Mixfix.mixfix "_"), ("_pttrns", typ "pttrn \ pttrns \ pttrns", mixfix ("_/ _", [1, 0], 0)), ("", typ "aprop \ aprop", Mixfix.mixfix "'(_')"), ("", typ "id_position \ aprop", Mixfix.mixfix "_"), ("", typ "longid_position \ aprop", Mixfix.mixfix "_"), ("", typ "var_position \ aprop", Mixfix.mixfix "_"), ("_DDDOT", typ "aprop", Mixfix.mixfix "\"), ("_aprop", typ "aprop \ prop", Mixfix.mixfix "PROP _"), ("_asm", typ "prop \ asms", Mixfix.mixfix "_"), ("_asms", typ "prop \ asms \ asms", Mixfix.mixfix "_;/ _"), ("_bigimpl", typ "asms \ prop \ prop", mixfix ("((1\_\)/ \ _)", [0, 1], 1)), ("_ofclass", typ "type \ logic \ prop", Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"), ("_mk_ofclass", typ "dummy", NoSyn), ("_TYPE", typ "type \ logic", Mixfix.mixfix "(1TYPE/(1'(_')))"), ("", typ "id_position \ logic", Mixfix.mixfix "_"), ("", typ "longid_position \ logic", Mixfix.mixfix "_"), ("", typ "var_position \ logic", Mixfix.mixfix "_"), ("_DDDOT", typ "logic", Mixfix.mixfix "\"), ("_strip_positions", typ "'a", NoSyn), ("_position", typ "num_token \ num_position", Mixfix.mixfix "_"), ("_position", typ "float_token \ float_position", Mixfix.mixfix "_"), ("_constify", typ "num_position \ num_const", Mixfix.mixfix "_"), ("_constify", typ "float_position \ float_const", Mixfix.mixfix "_"), ("_index", typ "logic \ index", Mixfix.mixfix "(\unbreakable\\<^bsub>_\<^esub>)"), ("_indexdefault", typ "index", Mixfix.mixfix ""), ("_indexvar", typ "index", Mixfix.mixfix "'\"), ("_struct", typ "index \ logic", NoSyn), ("_update_name", typ "idt", NoSyn), ("_constrainAbs", typ "'a", NoSyn), ("_position_sort", typ "tid \ tid_position", Mixfix.mixfix "_"), ("_position_sort", typ "tvar \ tvar_position", Mixfix.mixfix "_"), ("_position", typ "id \ id_position", Mixfix.mixfix "_"), ("_position", typ "longid \ longid_position", Mixfix.mixfix "_"), ("_position", typ "var \ var_position", Mixfix.mixfix "_"), ("_position", typ "str_token \ str_position", Mixfix.mixfix "_"), ("_position", typ "string_token \ string_position", Mixfix.mixfix "_"), ("_position", typ "cartouche \ cartouche_position", Mixfix.mixfix "_"), ("_type_constraint_", typ "'a", NoSyn), ("_context_const", typ "id_position \ logic", Mixfix.mixfix "CONST _"), ("_context_const", typ "id_position \ aprop", Mixfix.mixfix "CONST _"), ("_context_const", typ "longid_position \ logic", Mixfix.mixfix "CONST _"), ("_context_const", typ "longid_position \ aprop", Mixfix.mixfix "CONST _"), ("_context_xconst", typ "id_position \ logic", Mixfix.mixfix "XCONST _"), ("_context_xconst", typ "id_position \ aprop", Mixfix.mixfix "XCONST _"), ("_context_xconst", typ "longid_position \ logic", Mixfix.mixfix "XCONST _"), ("_context_xconst", typ "longid_position \ aprop", Mixfix.mixfix "XCONST _"), (const "Pure.dummy_pattern", typ "aprop", Mixfix.mixfix "'_"), ("_sort_constraint", typ "type \ prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic \ prop", Mixfix.mixfix "TERM _"), (const "Pure.conjunction", typ "prop \ prop \ prop", infixr_ ("&&&", 2))] #> Sign.add_syntax Syntax.mode_default applC_syntax #> Sign.add_syntax (Print_Mode.ASCII, true) [(tycon "fun", typ "type \ type \ type", mixfix ("(_/ => _)", [1, 0], 0)), ("_bracket", typ "types \ type \ type", mixfix ("([_]/ => _)", [0, 0], 0)), ("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3)), (const "Pure.eq", typ "'a \ 'a \ prop", infix_ ("==", 2)), (const "Pure.all_binder", typ "idts \ prop \ prop", mixfix ("(3!!_./ _)", [0, 0], 0)), (const "Pure.imp", typ "prop \ prop \ prop", infixr_ ("==>", 1)), ("_DDDOT", typ "aprop", Mixfix.mixfix "..."), ("_bigimpl", typ "asms \ prop \ prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), ("_DDDOT", typ "logic", Mixfix.mixfix "...")] #> Sign.add_syntax ("", false) [(const "Pure.prop", typ "prop \ prop", mixfix ("_", [0], 0))] #> Sign.add_consts [(qualify (Binding.make ("eq", \<^here>)), typ "'a \ 'a \ prop", infix_ ("\", 2)), (qualify (Binding.make ("imp", \<^here>)), typ "prop \ prop \ prop", infixr_ ("\", 1)), (qualify (Binding.make ("all", \<^here>)), typ "('a \ prop) \ prop", binder ("\", 0, 0)), (qualify (Binding.make ("prop", \<^here>)), typ "prop \ prop", NoSyn), (qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn), (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_"), (qualify (Binding.make ("Appt", \<^here>)), typ "Pure.proof \ 'a \ Pure.proof", NoSyn), (qualify (Binding.make ("AppP", \<^here>)), typ "Pure.proof \ Pure.proof \ Pure.proof", NoSyn), (qualify (Binding.make ("Abst", \<^here>)), typ "('a \ Pure.proof) \ Pure.proof", NoSyn), (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \ (Pure.proof \ Pure.proof) \ Pure.proof", NoSyn), (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \ Pure.proof", NoSyn), (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \ Pure.proof", NoSyn), (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \ prop) \ Pure.proof", NoSyn), (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)] #> add_deps_const "Pure.eq" #> add_deps_const "Pure.imp" #> add_deps_const "Pure.all" #> add_deps_const "Pure.type" #> add_deps_const "Pure.dummy_pattern" #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation #> Sign.parse_translation Syntax_Trans.pure_parse_translation #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation #> Sign.add_consts [(qualify (Binding.make ("term", \<^here>)), typ "'a \ prop", NoSyn), (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \ prop", NoSyn), (qualify (Binding.make ("conjunction", \<^here>)), typ "prop \ prop \ prop", NoSyn)] #> Sign.local_path #> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.make ("prop_def", \<^here>), prop "(CONST Pure.prop :: prop \ prop) (A::prop) \ A::prop"), (Binding.make ("term_def", \<^here>), prop "(CONST Pure.term :: 'a \ prop) (x::'a) \ (\A::prop. A \ A)"), (Binding.make ("sort_constraint_def", \<^here>), prop "(CONST Pure.sort_constraint :: 'a itself \ prop) (CONST Pure.type :: 'a itself) \\ \ (CONST Pure.term :: 'a itself \ prop) (CONST Pure.type :: 'a itself)"), (Binding.make ("conjunction_def", \<^here>), prop "(A &&& B) \ (\C::prop. (A \ B \ C) \ C)")] #> snd #> fold (fn (a, prop) => snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms); end; diff --git a/src/Pure/sign.ML b/src/Pure/sign.ML --- a/src/Pure/sign.ML +++ b/src/Pure/sign.ML @@ -1,540 +1,543 @@ (* Title: Pure/sign.ML Author: Lawrence C Paulson and Markus Wenzel Logical signature content: naming conventions, concrete syntax, type signature, polymorphic constants. *) signature SIGN = sig val change_begin: theory -> theory val change_end: theory -> theory val change_end_local: Proof.context -> Proof.context val change_check: theory -> theory val syn_of: theory -> Syntax.syntax val tsig_of: theory -> Type.tsig val classes_of: theory -> Sorts.algebra val all_classes: theory -> class list val super_classes: theory -> class -> class list val minimize_sort: theory -> sort -> sort val complete_sort: theory -> sort -> sort val set_defsort: sort -> theory -> theory val defaultS: theory -> sort val subsort: theory -> sort * sort -> bool val of_sort: theory -> typ * sort -> bool val inter_sort: theory -> sort * sort -> sort val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list val logical_types: theory -> string list val typ_instance: theory -> typ * typ -> bool val typ_equiv: theory -> typ * typ -> bool val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int val consts_of: theory -> Consts.T val the_const_constraint: theory -> string -> typ val const_type: theory -> string -> typ option val the_const_type: theory -> string -> typ val declared_tyname: theory -> string -> bool val declared_const: theory -> string -> bool val naming_of: theory -> Name_Space.naming val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory val restore_naming: theory -> theory -> theory val inherit_naming: theory -> Proof.context -> Context.generic val full_name: theory -> binding -> string val full_name_path: theory -> string -> binding -> string val full_bname: theory -> bstring -> string val full_bname_path: theory -> string -> bstring -> string val const_monomorphic: theory -> string -> bool val const_typargs: theory -> string * typ -> typ list val const_instance: theory -> string * typ list -> typ val mk_const: theory -> string * typ list -> term val class_space: theory -> Name_Space.T val type_space: theory -> Name_Space.T val const_space: theory -> Name_Space.T val intern_class: theory -> xstring -> string val intern_type: theory -> xstring -> string val intern_const: theory -> xstring -> string val type_alias: binding -> string -> theory -> theory val const_alias: binding -> string -> theory -> theory val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list val certify_class: theory -> class -> class val certify_sort: theory -> sort -> sort val certify_typ: theory -> typ -> typ val certify_typ_mode: Type.mode -> theory -> typ -> typ val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int val certify_term: theory -> term -> term * typ * int val cert_term: theory -> term -> term val cert_prop: theory -> term -> term val no_frees: Proof.context -> term -> term val no_vars: Proof.context -> term -> term val add_type: Proof.context -> binding * int * mixfix -> theory -> theory val add_types_global: (binding * int * mixfix) list -> theory -> theory val add_nonterminals: Proof.context -> binding list -> theory -> theory val add_nonterminals_global: binding list -> theory -> theory val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory val add_consts: (binding * typ * mixfix) list -> theory -> theory val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory val add_abbrev: string -> binding * term -> theory -> (term * term) * theory val revert_abbrev: string -> string -> theory -> theory val add_const_constraint: string * typ option -> theory -> theory val primitive_class: binding * class list -> theory -> theory val primitive_classrel: class * class -> theory -> theory val primitive_arity: arity -> theory -> theory val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val parse_translation: (string * (Proof.context -> term list -> term)) list -> theory -> theory val print_translation: (string * (Proof.context -> term list -> term)) list -> theory -> theory val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory val get_scope: theory -> Binding.scope option val new_scope: theory -> Binding.scope * theory val new_group: theory -> theory val reset_group: theory -> theory val add_path: string -> theory -> theory val root_path: theory -> theory val parent_path: theory -> theory val mandatory_path: string -> theory -> theory val qualified_path: bool -> binding -> theory -> theory val local_path: theory -> theory + val theory_naming: theory -> theory val private_scope: Binding.scope -> theory -> theory val private: Position.T -> theory -> theory val qualified_scope: Binding.scope -> theory -> theory val qualified: Position.T -> theory -> theory val concealed: theory -> theory val hide_class: bool -> string -> theory -> theory val hide_type: bool -> string -> theory -> theory val hide_const: bool -> string -> theory -> theory end structure Sign: SIGN = struct (** datatype sign **) datatype sign = Sign of {syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*) tsig: Type.tsig, (*order-sorted signature of types*) consts: Consts.T}; (*polymorphic constants*) fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts}; structure Data = Theory_Data' ( type T = sign; fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts); val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty); fun merge old_thys (sign1, sign2) = let val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1; val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2; val syn = Syntax.merge_syntax (syn1, syn2); val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2); val consts = Consts.merge (consts1, consts2); in make_sign (syn, tsig, consts) end; ); fun rep_sg thy = Data.get thy |> (fn Sign args => args); fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts))); fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts)); fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts)); fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts)); (* linear change discipline *) fun change_base begin = map_sign (fn (syn, tsig, consts) => (syn, Type.change_base begin tsig, Consts.change_base begin consts)); val change_begin = change_base true; val change_end = change_base false; fun change_end_local ctxt = Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt; fun change_check thy = if can change_end thy then raise Fail "Unfinished linear change of theory content" else thy; (* syntax *) val syn_of = #syn o rep_sg; (* type signature *) val tsig_of = #tsig o rep_sg; val classes_of = #2 o #classes o Type.rep_tsig o tsig_of; val all_classes = Sorts.all_classes o classes_of; val super_classes = Sorts.super_classes o classes_of; val minimize_sort = Sorts.minimize_sort o classes_of; val complete_sort = Sorts.complete_sort o classes_of; val set_defsort = map_tsig o Type.set_defsort; val defaultS = Type.defaultS o tsig_of; val subsort = Type.subsort o tsig_of; val of_sort = Type.of_sort o tsig_of; val inter_sort = Type.inter_sort o tsig_of; val witness_sorts = Type.witness_sorts o tsig_of; val logical_types = Type.logical_types o tsig_of; val typ_instance = Type.typ_instance o tsig_of; fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T); val typ_match = Type.typ_match o tsig_of; val typ_unify = Type.unify o tsig_of; (* polymorphic constants *) val consts_of = #consts o rep_sg; val the_const_constraint = Consts.the_constraint o consts_of; val the_const_type = #2 oo (Consts.the_const o consts_of); val const_type = try o the_const_type; val const_monomorphic = Consts.is_monomorphic o consts_of; val const_typargs = Consts.typargs o consts_of; val const_instance = Consts.instance o consts_of; fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts)); fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none); val declared_const = can o the_const_constraint; (* naming *) val naming_of = Name_Space.naming_of o Context.Theory; val map_naming = Context.theory_map o Name_Space.map_naming; val restore_naming = map_naming o K o naming_of; fun inherit_naming thy = Name_Space.map_naming (K (naming_of thy)) o Context.Proof; val full_name = Name_Space.full_name o naming_of; fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy)); fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name; fun full_bname_path thy path = full_name_path thy path o Binding.name; (** name spaces **) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; (** certify entities **) (*exception TYPE*) (* certify wrt. type signature *) val arity_number = Type.arity_number o tsig_of; fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy); val certify_class = Type.cert_class o tsig_of; val certify_sort = Type.cert_sort o tsig_of; val certify_typ = Type.cert_typ o tsig_of; fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of; (* certify term/prop *) local fun type_check context tm = let fun err_appl bs t T u U = let val xs = map Free bs; (*we do not rename here*) val t' = subst_bounds (xs, t); val u' = subst_bounds (xs, u); val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U; in raise TYPE (msg, [T, U], [t', u']) end; fun typ_of (_, Const (_, T)) = T | typ_of (_, Free (_, T)) = T | typ_of (_, Var (_, T)) = T | typ_of (bs, Bound i) = snd (nth bs i handle General.Subscript => raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i])) | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body) | typ_of (bs, t $ u) = let val T = typ_of (bs, t) and U = typ_of (bs, u) in (case T of Type ("fun", [T1, T2]) => if T1 = U then T2 else err_appl bs t T u U | _ => err_appl bs t T u U) end; in typ_of ([], tm) end; fun err msg = raise TYPE (msg, [], []); fun check_vars (t $ u) = (check_vars t; check_vars u) | check_vars (Abs (_, _, t)) = check_vars t | check_vars (Free (x, _)) = if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else () | check_vars (Var (xi as (_, i), _)) = if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else () | check_vars _ = (); in fun certify' prop context do_expand consts thy tm = let val _ = check_vars tm; val tm' = Term.map_types (certify_typ thy) tm; val T = type_check context tm'; val _ = if prop andalso T <> propT then err "Term not of type prop" else (); val tm'' = tm' |> Consts.certify context (tsig_of thy) do_expand consts |> Soft_Type_System.global_purge thy; in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end; fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy; fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy; val cert_term = #1 oo certify_term; fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy; end; (* specifications *) fun no_variables kind add addT mk mkT ctxt tm = (case (add tm [], addT tm []) of ([], []) => tm | (frees, tfrees) => error (Pretty.string_of (Pretty.block (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees))))); val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree; val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar; (** signature extension functions **) (*exception ERROR/TYPE*) (* add type constructors *) fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) => let val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx); val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn; val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig; in (syn', tsig', consts) end); fun add_types_global types thy = fold (add_type (Syntax.init_pretty_global thy)) types thy; (* add nonterminals *) fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) => (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts)); fun add_nonterminals_global ns thy = add_nonterminals (Syntax.init_pretty_global thy) ns thy; (* add type abbreviations *) fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) => (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts)); (* modify syntax *) fun gen_syntax change_gram parse_typ mode args thy = let val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy); fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx) handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c); in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end; fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x; val add_syntax = gen_add_syntax (K I); val add_syntax_cmd = gen_add_syntax Syntax.read_typ; val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I); val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ; fun type_notation add mode args = let fun type_syntax (Type (c, args), mx) = SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx) | type_syntax _ = NONE; in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end; fun notation add mode args thy = let fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of SOME T => SOME (Lexicon.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end; (* add constants *) local fun gen_add_consts prep_typ ctxt raw_args thy = let val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt; fun prep (b, raw_T, mx) = let val c = full_name thy b; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ Binding.print b); val T' = Logic.varifyT_global T; in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end; val args = map prep raw_args; in thy |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args) |> add_syntax Syntax.mode_default (map #2 args) |> pair (map #3 args) end; in fun add_consts args thy = #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy); fun add_consts_cmd args thy = #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy); fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx); fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy; end; (* abbreviations *) fun add_abbrev mode (b, raw_t) thy = (* FIXME proper ctxt (?) *) let val ctxt = Syntax.init_pretty_global thy; val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy; val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg) handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); val (res, consts') = consts_of thy |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t); in (res, thy |> map_consts (K consts')) end; fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c); (* add constraints *) fun add_const_constraint (c, opt_T) thy = let fun prepT raw_T = let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T))) in cert_term thy (Const (c, T)); T end handle TYPE (msg, _, _) => error msg; in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end; (* primitive classes and arities *) fun primitive_class (bclass, classes) thy = thy |> map_sign (fn (syn, tsig, consts) => let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig; in (syn, tsig', consts) end) |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)]; fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg); fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.Theory thy) arg); (* add translation functions *) local fun mk trs = map Syntax_Ext.mk_trfun trs; in fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], [])); fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], [])); fun print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), [])); fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, [])); fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's)); end; (* translation rules *) val add_trrules = map_syn o Syntax.update_trrules; val del_trrules = map_syn o Syntax.remove_trrules; (* naming *) val get_scope = Name_Space.get_scope o naming_of; fun new_scope thy = let val (scope, naming') = Name_Space.new_scope (naming_of thy); val thy' = map_naming (K naming') thy; in (scope, thy') end; val new_group = map_naming Name_Space.new_group; val reset_group = map_naming Name_Space.reset_group; val add_path = map_naming o Name_Space.add_path; val root_path = map_naming Name_Space.root_path; val parent_path = map_naming Name_Space.parent_path; val mandatory_path = map_naming o Name_Space.mandatory_path; val qualified_path = map_naming oo Name_Space.qualified_path; fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); +fun theory_naming thy = thy |> map_naming (Name_Space.set_theory_name (Context.theory_name thy)); + val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; val qualified_scope = map_naming o Name_Space.qualified_scope; val qualified = map_naming o Name_Space.qualified; val concealed = map_naming Name_Space.concealed; (* hide names *) val hide_class = map_tsig oo Type.hide_class; val hide_type = map_tsig oo Type.hide_type; val hide_const = map_consts oo Consts.hide; end; diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML --- a/src/Pure/theory.ML +++ b/src/Pure/theory.ML @@ -1,347 +1,347 @@ (* Title: Pure/theory.ML Author: Lawrence C Paulson and Markus Wenzel Logical theory content: axioms, definitions, and begin/end wrappers. *) signature THEORY = sig val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit val local_setup: (Proof.context -> Proof.context) -> unit val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory val get_markup: theory -> Markup.T val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory val at_end: (theory -> theory option) -> theory -> theory val join_theory: theory list -> theory val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end structure Theory: THEORY = struct (** theory context operations **) val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); fun local_setup f = Context.>> (Context.map_proof f); (* implicit theory Pure *) val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; fun install_pure thy = Single_Assignment.assign pure thy; fun get_pure () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => raise Fail "Theory Pure not present"); fun get_pure_bootstrap () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => Context.the_global_context ()); (** datatype thy **) type wrapper = (theory -> theory option) * stamp; fun apply_wrappers (wrappers: wrapper list) = perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); datatype thy = Thy of {pos: Position.T, id: serial, axioms: term Name_Space.table, defs: Defs.T, wrappers: wrapper list * wrapper list}; fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; structure Thy = Theory_Data' ( type T = thy; val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], [])); fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) = make_thy (Position.none, 0, axioms, defs, wrappers); fun merge old_thys (thy1, thy2) = let val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; val axioms' = Name_Space.merge_tables (axioms1, axioms2); val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); val ens' = Library.merge (eq_snd op =) (ens1, ens2); in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end; ); fun rep_theory thy = Thy.get thy |> (fn Thy args => args); fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => make_thy (f (pos, id, axioms, defs, wrappers))); fun map_axioms f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); fun map_defs f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); fun map_wrappers f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); (* entity markup *) fun theory_markup def name id pos = if id = 0 then Markup.empty else Markup.properties (Position.entity_properties_of def id pos) (Markup.entity Markup.theoryN name); fun init_markup (name, pos) thy = let val id = serial (); val _ = Position.report pos (theory_markup true name id pos); in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; fun get_markup thy = let val {pos, id, ...} = rep_theory thy in theory_markup false (Context.theory_name thy) id pos end; fun check long ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val thy' = Context.get_theory long thy name handle ERROR msg => let val completion_report = Completion.make_report (name, pos) (fn completed => map (Context.theory_name' long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy'); in thy' end; (* basic operations *) val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; (* join theory *) fun join_theory [] = raise List.Empty | join_theory [thy] = thy | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys); (* begin/end theory *) val begin_wrappers = rev o #1 o #wrappers o rep_theory; val end_wrappers = rev o #2 o #wrappers o rep_theory; fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); fun begin_theory (name, pos) imports = if name = Context.PureN then (case imports of [thy] => init_markup (name, pos) thy | _ => error "Bad bootstrapping of theory Pure") else let val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy |> init_markup (name, pos) |> Sign.local_path - |> Sign.map_naming (Name_Space.set_theory_name (Long_Name.base_name name)) + |> Sign.theory_naming |> apply_wrappers wrappers |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy = thy |> apply_wrappers (end_wrappers thy) |> Sign.change_check |> Context.finish_thy; (** primitive specifications **) (* raw axioms *) fun cert_axm ctxt (b, raw_tm) = let val thy = Proof_Context.theory_of ctxt; val t = Sign.cert_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; val bad_sorts = rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); val _ = null bad_sorts orelse error ("Illegal sort constraints in primitive specification: " ^ commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); in (b, Sign.no_vars ctxt t) end handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => let val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); val context = ctxt |> Sign.inherit_naming thy |> Context_Position.set_visible_generic false; val (_, axioms') = Name_Space.define context true axm axioms; in axioms' end); (* dependencies *) fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args) | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); val lhs_vars = fold Term.add_tfreesT (snd lhs) []; val rhs_extras = fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs []; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) |> dest_Const |> const_dep thy | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; in thy |> map_defs (dependencies context false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Defs.global_context thy) a x y thy; fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) fun check_overloading ctxt overloaded (c, T) = let val thy = Proof_Context.theory_of ctxt; val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; val T' = Logic.varifyT_global T; fun message sorts txt = [Pretty.block [Pretty.str "Specification of constant ", Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; in if Sign.typ_instance thy (declT, T') then () else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () else error (message false "is strictly less general than the declared type (overloading required)") end; (* definitional axioms *) local fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true, check_free_rhs = K false, check_tfree = K false} tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); val rhs_consts = fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; val rhs_types = (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; end; end;