# HG changeset patch # User haftmann # Date 1191873801 -7200 # Node ID 95cda5dd58d5928c11b347630a54c32f4caa2374 # Parent eb6fd8f78d56a62b9494a21d61370560cef33fc7 added proper subclass concept; improved class target diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Mon Oct 08 20:20:13 2007 +0200 +++ b/src/HOL/Dense_Linear_Order.thy Mon Oct 08 22:03:21 2007 +0200 @@ -404,18 +404,12 @@ fixes between assumes between_less: "x \<^loc>< y \ x \<^loc>< between x y \ between x y \<^loc>< y" and between_same: "between x x = x" +begin -instance advanced constr_dense_linear_order < dense_linear_order +subclass dense_linear_order apply unfold_locales using gt_ex lt_ex between_less by (auto, rule_tac x="between x y" in exI, simp) -(*FIXME*) -lemmas gt_ex = dense_linear_order_class.less_eq_less.gt_ex -lemmas lt_ex = dense_linear_order_class.less_eq_less.lt_ex -lemmas dense = dense_linear_order_class.less_eq_less.dense - -context constr_dense_linear_order -begin lemma rinf_U: assumes fU: "finite U" diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Mon Oct 08 20:20:13 2007 +0200 +++ b/src/HOL/ex/Classpackage.thy Mon Oct 08 22:03:21 2007 +0200 @@ -5,7 +5,7 @@ header {* Test and examples for Isar class package *} theory Classpackage -imports Main +imports List begin class semigroup = type + @@ -192,14 +192,18 @@ thus "x \<^loc>\ y = x \<^loc>\ z" by simp qed -lemma neutr: - "x \<^loc>\ \<^loc>\ = x" -proof - +subclass monoid +proof unfold_locales + fix x from invl have "\<^loc>\
x \<^loc>\ x = \<^loc>\" by simp with assoc [symmetric] neutl invl have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\) = \<^loc>\
x \<^loc>\ x" by simp - with cancel show ?thesis by simp + with cancel show "x \<^loc>\ \<^loc>\ = x" by simp qed +end context group begin + +find_theorems name: neut + lemma invr: "x \<^loc>\ \<^loc>\
x = \<^loc>\" proof - @@ -209,27 +213,6 @@ with cancel show ?thesis .. qed -end - -instance advanced group < monoid -proof unfold_locales - fix x - from neutr show "x \<^loc>\ \<^loc>\ = x" . -qed - -hide const npow (*FIXME*) -lemmas neutr = monoid_class.mult_one.neutr -lemmas inv_obtain = monoid_class.inv_obtain -lemmas inv_unique = monoid_class.inv_unique -lemmas nat_pow_mult = monoid_class.nat_pow_mult -lemmas nat_pow_one = monoid_class.nat_pow_one -lemmas nat_pow_pow = monoid_class.nat_pow_pow -lemmas units_def = monoid_class.units_def -lemmas mult_one_def = monoid_class.units_inv_comm - -context group -begin - lemma all_inv [intro]: "(x\'a) \ units" unfolding units_def @@ -290,15 +273,6 @@ "pow k x = (if k < 0 then \<^loc>\
(npow (nat (-k)) x) else (npow (nat k) x))" -end - -(*FIXME*) -thm (no_abbrevs) pow_def -thm (no_abbrevs) pow_def [folded monoid_class.npow] -lemmas pow_def [code func] = pow_def [folded monoid_class.npow] - -context group begin - abbreviation pow_syn :: "'a \ int \ 'a" (infix "\<^loc>\\" 75) where @@ -340,7 +314,7 @@ definition "x2 = X (1::int) 2 3" definition "y2 = Y (1::int) 2 3" -export_code mult x1 x2 y2 in SML module_name Classpackage +export_code x1 x2 y2 pow in SML module_name Classpackage in OCaml file - in Haskell file - diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Oct 08 20:20:13 2007 +0200 +++ b/src/Pure/IsaMakefile Mon Oct 08 22:03:21 2007 +0200 @@ -43,7 +43,7 @@ Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML \ Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML \ Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML \ - Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \ + Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML Isar/toplevel.ML \ ML-Systems/alice.ML ML-Systems/exn.ML \ ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \ diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Mon Oct 08 20:20:13 2007 +0200 +++ b/src/Pure/Isar/ROOT.ML Mon Oct 08 22:03:21 2007 +0200 @@ -58,6 +58,7 @@ use "instance.ML"; use "spec_parse.ML"; use "specification.ML"; +use "subclass.ML"; (*FIXME improve structure*) use "constdefs.ML"; (*toplevel environment*) diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Oct 08 20:20:13 2007 +0200 +++ b/src/Pure/Isar/class.ML Mon Oct 08 22:03:21 2007 +0200 @@ -13,18 +13,22 @@ -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory val classrel_cmd: xstring * xstring -> theory -> Proof.state + val class: bool -> bstring -> class list -> Element.context_i Locale.element list -> string list -> theory -> string * Proof.context val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list -> xstring list -> theory -> string * Proof.context + val init: class -> Proof.context -> Proof.context; val add_const_in_class: string -> (string * term) * Syntax.mixfix - -> theory -> theory - val interpretation_in_class: class * class -> theory -> Proof.state - val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state - val prove_interpretation_in_class: tactic -> class * class -> theory -> theory + -> theory -> string * theory + val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix + -> theory -> string * theory + val remove_constraint: sort -> string -> Proof.context -> Proof.context val intro_classes_tac: thm list -> tactic val default_intro_classes_tac: thm list -> tactic val class_of_locale: theory -> string -> class option + val locale_of_class: theory -> class -> string + val local_syntax: theory -> class -> bool val print_classes: theory -> unit val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state @@ -44,11 +48,6 @@ val inst_const: theory -> string * string -> string val param_const: theory -> string -> (string * string) option val params_of_sort: theory -> sort -> (string * (string * typ)) list - - val init: class -> Proof.context -> Proof.context; - val local_syntax: theory -> class -> bool - val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix - -> theory -> theory end; structure Class : CLASS = @@ -70,13 +69,6 @@ (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) #> ProofContext.theory_of; -fun prove_interpretation_in tac after_qed (name, expr) = - Locale.interpretation_in_locale - (ProofContext.theory after_qed) (name, expr) - #> Proof.global_terminal_proof - (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) - #> ProofContext.theory_of; - fun OF_LAST thm1 thm2 = let val n = (length o Logic.strip_imp_prems o prop_of) thm2; @@ -331,22 +323,30 @@ intro: thm, local_syntax: bool, defs: thm list, - operations: (string * (term * int) option) list + operations: (string * (term * int) option) list, (*constant name ~> (locale term, instantiaton index of class typ)*) + constraints: (string * typ) list }; fun rep_class_data (ClassData d) = d; -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) = - ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro, - local_syntax = local_syntax, defs = defs, operations = operations }; -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) = - mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations))) -fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, - intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 }, +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), + (defs, (operations, constraints))) = + ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, + intro = intro, local_syntax = local_syntax, defs = defs, operations = operations, + constraints = constraints }; +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, + local_syntax, defs, operations, constraints }) = + mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), + (defs, (operations, constraints)))); +fun merge_class_data _ (ClassData { locale = locale, consts = consts, + local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax, + defs = defs1, operations = operations1, constraints = constraints1 }, ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _, - defs = defs2, operations = operations2 }) = + defs = defs2, operations = operations2, constraints = constraints2 }) = mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), - (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2))); + (Thm.merge_thms (defs1, defs2), + (AList.merge (op =) (K true) (operations1, operations2), + AList.merge (op =) (K true) (constraints1, constraints2)))); fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); @@ -371,6 +371,8 @@ of NONE => error ("undeclared class " ^ quote class) | SOME data => data; +val locale_of_class = #locale oo the_class_data; + val ancestry = Graph.all_succs o fst o ClassData.get; fun params_of_sort thy = @@ -393,6 +395,9 @@ fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; +fun these_constraints thy = + maps (#constraints o the_class_data thy) o ancestry thy; + fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy; fun sups_local_sort thy sort = @@ -444,8 +449,9 @@ fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) = ClassData.map (fn (gr, tab) => ( gr - |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst, - intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts))) + |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts, + local_sort, inst, intro, local_syntax), + ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts)))) |> fold (curry Graph.add_edge class) superclasses, tab |> Symtab.update (locale, class) @@ -453,11 +459,12 @@ fun register_const class (entry, def) = (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd) - (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations)); + (fn (defs, (operations, constraints)) => + (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints))); -fun register_abbrev class abbrev = +fun register_abbrev class (abbrev, ty) = (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd) - (cons (abbrev, NONE)); + (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints)); (** rule calculation, tactics and methods **) @@ -553,28 +560,21 @@ (* class context initialization *) -fun get_remove_constraints sups local_sort ctxt = +fun remove_constraint local_sort c ctxt = + let + val ty = ProofContext.the_const_constraint ctxt c; + val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT + then TFree (v, local_sort) else ty | ty => ty) ty; + in + ctxt + |> ProofContext.add_const_constraint (c, SOME ty') + end; + +fun sort_term_check sups local_sort ts ctxt = let val thy = ProofContext.theory_of ctxt; - val operations = these_operations thy sups; - fun get_remove (c, _) ctxt = - let - val ty = ProofContext.the_const_constraint ctxt c; - val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT - then TFree (v, local_sort) else ty | ty => ty) ty; - in - ctxt - |> ProofContext.add_const_constraint (c, SOME ty') - |> pair (c, ty) - end; - in - ctxt - |> fold_map get_remove operations - end; - -fun sort_term_check thy sups local_sort constraints ts ctxt = - let val local_operation = local_operation thy sups; + val constraints = these_constraints thy sups; val consts = ProofContext.consts_of ctxt; fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx of TFree (v, _) => if v = Name.aT @@ -595,20 +595,22 @@ val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt; in (ts', ctxt') end; -fun init_class_ctxt thy sups local_sort ctxt = - ctxt - |> Variable.declare_term - (Logic.mk_type (TFree (Name.aT, local_sort))) - |> get_remove_constraints sups local_sort - |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class" - (sort_term_check thy sups local_sort constraints))); +fun init_class_ctxt sups local_sort ctxt = + let + val operations = these_operations (ProofContext.theory_of ctxt) sups; + in + ctxt + |> Variable.declare_term + (Logic.mk_type (TFree (Name.aT, local_sort))) + |> fold (remove_constraint local_sort o fst) operations + |> Context.proof_map (Syntax.add_term_check 50 "class" + (sort_term_check sups local_sort)) + end; fun init class ctxt = - let - val thy = ProofContext.theory_of ctxt; - val local_sort = (#local_sort o the_class_data thy) class; - in init_class_ctxt thy [class] local_sort ctxt end; - + init_class_ctxt [class] + ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt; + (* class definition *) @@ -641,7 +643,7 @@ ProofContext.init thy |> Locale.cert_expr supexpr [constrain] |> snd - |> init_class_ctxt thy sups local_sort + |> init_class_ctxt sups local_sort |> process_expr Locale.empty raw_elems |> fst |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)), @@ -706,7 +708,7 @@ `(fn thy => class_intro thy name_locale name_axclass sups) #-> (fn class_intro => add_class_data ((name_axclass, sups), - (name_locale, map fst params ~~ map fst consts, local_sort, + (name_locale, map fst params ~~ consts, local_sort, (mk_instT name_axclass, mk_inst name_axclass (map fst globals) (map snd supconsts @ consts)), class_intro, local_syntax)) #> note_intro name_axclass class_intro @@ -736,9 +738,10 @@ fun mk_operation_entry thy (c, rhs) = let - val typargs = Sign.const_typargs thy (c, fastype_of rhs); + val ty = fastype_of rhs; + val typargs = Sign.const_typargs thy (c, ty); val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs; - in (c, (rhs, typidx)) end; + in (c, (ty, (rhs, typidx))) end; fun add_const_in_class class ((c, rhs), syn) thy = let @@ -778,6 +781,7 @@ |-> (fn [def] => interpret def) |> Sign.add_const_constraint (c', SOME ty'') |> Sign.restore_naming thy + |> pair c' end; @@ -798,55 +802,8 @@ in thy |> Sign.add_notation prmode [(Const (c', ty'), syn)] - |> register_abbrev class c' + |> register_abbrev class (c', ty') + |> pair c' end; - -(* interpretation in class target *) - -local - -fun gen_interpretation_in_class prep_class do_proof (raw_class, raw_superclass) theory = - let - val class = prep_class theory raw_class; - val superclass = prep_class theory raw_superclass; - val loc_name = (#locale o the_class_data theory) class; - val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass; - fun prove_classrel (class, superclass) thy = - let - val classes = Sign.complete_sort thy [superclass] - |> filter_out (fn class' => Sign.subsort thy ([class], [class'])); - fun instance_subclass (class1, class2) thy = - let - val interp = interpretation_in_rule thy (class1, class2); - val ax = #axioms (AxClass.get_definition thy class1); - val intro = #intro (AxClass.get_definition thy class2) - |> Drule.instantiate' [SOME (Thm.ctyp_of thy - (TVar ((Name.aT, 0), [class1])))] []; - val thm = - intro - |> OF_LAST (interp OF ax) - |> strip_all_ofclass thy (Sign.super_classes thy class2); - in - thy |> AxClass.add_classrel thm - end; - in - thy |> fold_rev (curry instance_subclass class) classes - end; - in - theory - |> do_proof (prove_classrel (class, superclass)) (loc_name, loc_expr) - end; - -in - -val interpretation_in_class = gen_interpretation_in_class Sign.certify_class - (Locale.interpretation_in_locale o ProofContext.theory); -val interpretation_in_class_cmd = gen_interpretation_in_class Sign.read_class - (Locale.interpretation_in_locale o ProofContext.theory); -val prove_interpretation_in_class = gen_interpretation_in_class Sign.certify_class - o prove_interpretation_in; - -end; (*local*) - end; diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Oct 08 20:20:13 2007 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon Oct 08 22:03:21 2007 +0200 @@ -435,10 +435,13 @@ (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin))); val _ = + OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal + (P.opt_target -- P.xname >> (fn (loc, class) => + Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class))); + +val _ = OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd || - P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) - >> Class.interpretation_in_class_cmd || (* FIXME ?? *) P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *)))) >> (Toplevel.print oo Toplevel.theory_to_proof)); diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/Pure/Isar/subclass.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/subclass.ML Mon Oct 08 22:03:21 2007 +0200 @@ -0,0 +1,122 @@ +(* Title: Pure/Isar/subclass.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Prove subclass relations between type classes +*) + +signature SUBCLASS = +sig + val subclass: class -> local_theory -> Proof.state + val subclass_cmd: xstring -> local_theory -> Proof.state + (*FIXME val prove_subclass: tactic -> class * class -> theory -> theory*) +end; + +structure Subclass : SUBCLASS = +struct + +(** auxiliary **) + +fun prove_interpretation_in tac after_qed (name, expr) = + Locale.interpretation_in_locale + (ProofContext.theory after_qed) (name, expr) + #> Proof.global_terminal_proof + (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) + #> ProofContext.theory_of; + +fun OF_LAST thm1 thm2 = + let + val n = (length o Logic.strip_imp_prems o prop_of) thm2; + in (thm1 RSN (n, thm2)) end; + +fun strip_all_ofclass thy sort = + let + val typ = TVar ((Name.aT, 0), sort); + fun prem_inclass t = + case Logic.strip_imp_prems t + of ofcls :: _ => try Logic.dest_inclass ofcls + | [] => NONE; + fun strip_ofclass class thm = + thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache; + fun strip thm = case (prem_inclass o Thm.prop_of) thm + of SOME (_, class) => thm |> strip_ofclass class |> strip + | NONE => thm; + in strip end; + + +(** subclassing **) + +local + +fun mk_subclass_rule lthy sup = + let + (*FIXME check for proper parameter inclusion (consts_of) (?)*) + val ctxt = LocalTheory.target_of lthy; + val thy = ProofContext.theory_of ctxt; + val locale = Class.locale_of_class thy sup; + in + Locale.global_asms_of thy locale + |> maps snd + |> map (ObjectLogic.ensure_propT thy) + end; + +fun gen_subclass prep_class raw_sup lthy = + let + (*FIXME cleanup, provide tactical interface*) + val ctxt = LocalTheory.target_of lthy; + val thy = ProofContext.theory_of ctxt; + val ctxt_thy = ProofContext.init thy; + val sup = prep_class thy raw_sup; + val sub = case Option.mapPartial (Class.class_of_locale thy) + (TheoryTarget.peek lthy) + of NONE => error "not in class context" + | SOME sub => sub; + val export = + Assumption.export false ctxt ctxt_thy + #> singleton (Variable.export ctxt ctxt_thy); + val loc_name = Class.locale_of_class thy sub; + val loc_expr = Locale.Locale (Class.locale_of_class thy sup); + fun prove_classrel interp thy = + let + val classes = Sign.complete_sort thy [sup] + |> filter_out (fn class' => Sign.subsort thy ([sub], [class'])); + fun instance_subclass (class1, class2) thy = + let + val ax = #axioms (AxClass.get_definition thy class1); + val intro = #intro (AxClass.get_definition thy class2) + |> Drule.instantiate' [SOME (Thm.ctyp_of thy + (TVar ((Name.aT, 0), [class1])))] []; + val thm = + intro + |> OF_LAST (interp OF ax) + |> strip_all_ofclass thy (Sign.super_classes thy class2); + in + thy |> AxClass.add_classrel thm + end; + in + thy |> fold_rev (curry instance_subclass sub) classes + end; + fun after_qed thmss = + let + val thm = Conjunction.intr_balanced (the_single thmss);; + val interp = export thm; + in + LocalTheory.theory (prove_classrel interp + #> prove_interpretation_in (ProofContext.fact_tac [thm] 1) + I (loc_name, loc_expr)) + (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*) + end; + val goal = Element.Shows + [(("", []), map (rpair []) (mk_subclass_rule lthy sup))]; + in + Specification.theorem_i Thm.internalK NONE after_qed ("", []) [] goal true lthy + end; + +in + +val subclass = gen_subclass (K I); +val subclass_cmd = gen_subclass Sign.read_class; + +end; (*local*) + +end; diff -r eb6fd8f78d56 -r 95cda5dd58d5 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Mon Oct 08 20:20:13 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Mon Oct 08 22:03:21 2007 +0200 @@ -118,9 +118,10 @@ val mx3 = if is_loc then NoSyn else mx1; val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy; in (((c, mx2), t), thy') end; - fun const_class (SOME class) ((c, _), mx) (_, t) = - Class.add_const_in_class class ((c, t), mx) + LocalTheory.raw_theory_result + (Class.add_const_in_class class ((c, t), mx)) + #-> (fn c => Class.remove_constraint [class] c) | const_class NONE _ _ = I; fun hide_abbrev (SOME class) abbrs thy = let @@ -137,13 +138,14 @@ Sign.hide_consts_i true cs thy end | hide_abbrev NONE _ thy = thy; + val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls) val defs = map (apsnd (pair ("", []))) abbrs; in lthy' - |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs) + |> fold2 (const_class some_class) decls abbrs |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs |> LocalTheory.raw_theory (hide_abbrev some_class abbrs) (*FIXME abbreviations should never occur*) @@ -184,17 +186,17 @@ val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u; val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; val mx3 = if is_loc then NoSyn else mx1; - fun add_abbrev_in_class NONE = K I - | add_abbrev_in_class (SOME class) = - Class.add_abbrev_in_class class prmode; + fun add_abbrev_in_class (SOME class) abbr = + LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr) + #-> (fn c => Class.remove_constraint [class] c) + | add_abbrev_in_class NONE _ = I; in lthy |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u')) |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)]) #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) - #> LocalTheory.raw_theory - (add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)) + #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) #> local_abbrev (c, rhs)) end;