# HG changeset patch # User wenzelm # Date 1192288604 -7200 # Node ID f1344290e4207da490a4ffac70743da823f0c2a5 # Parent 3b2d3b8fc7b6fd9c2dc40d99199184a3903bdaa8 (un)overload: full rewrite; use Attrib.attribute_i for internal args; misc tuning; diff -r 3b2d3b8fc7b6 -r f1344290e420 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Oct 13 17:16:42 2007 +0200 +++ b/src/Pure/Isar/class.ML Sat Oct 13 17:16:44 2007 +0200 @@ -69,10 +69,7 @@ (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 OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2); fun strip_all_ofclass thy sort = let @@ -148,14 +145,14 @@ Symtab.merge (K true) (tabb1, tabb2)); ); -fun inst_thms f thy = (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst) +fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) (InstData.get thy) []; fun add_inst (c, tyco) inst = (InstData.map o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco))); -fun unoverload thy = MetaSimplifier.rewrite false (inst_thms I thy); -fun overload thy = MetaSimplifier.rewrite false (inst_thms symmetric thy); +fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy); +fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); fun inst_const thy (c, tyco) = (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco; @@ -179,7 +176,7 @@ in thy |> Sign.sticky_prefix name_inst - |> Sign.declare_const [] (c_inst_base, ty, Syntax.NoSyn) + |> Sign.declare_const [] (c_inst_base, ty, NoSyn) |-> (fn const as Const (c_inst, _) => PureThy.add_defs_i false [((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])] @@ -205,7 +202,7 @@ |*) add_inst' _ t = add_inst_def (class, tyco) (c, ty); in thy - |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute thy) atts)] + |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)] |-> (fn [def] => add_inst' def (args, rhs) #> pair def) end; @@ -232,11 +229,11 @@ fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory = let val arities = map (prep_arity theory) raw_arities; - val _ = if null arities then error "at least one arity must be given" else (); + val _ = if null arities then error "At least one arity must be given" else (); val _ = case (duplicates (op =) o map #1) arities of [] => () - | dupl_tycos => error ("type constructors occur more than once in arities: " - ^ (commas o map quote) dupl_tycos); + | dupl_tycos => error ("Type constructors occur more than once in arities: " + ^ commas_quote dupl_tycos); fun get_remove_constraint c thy = let val ty = Sign.the_const_constraint thy c; @@ -269,13 +266,13 @@ val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def; val ty = Consts.instance (Sign.consts_of thy_read) (c, inst); val ((class, tyco), ty') = case AList.lookup (op =) cs c - of NONE => error ("illegal definition for constant " ^ quote c) + of NONE => error ("Illegal definition for constant " ^ quote c) | SOME class_ty => class_ty; val name = case name_opt of NONE => Thm.def_name (Logic.name_arity (tyco, [], c)) | SOME name => name; val t' = case mk_typnorm thy_read (ty', ty) - of NONE => error ("illegal definition for constant " ^ + of NONE => error ("Illegal definition for constant " ^ quote (c ^ "::" ^ setmp show_sorts true (Sign.string_of_typ thy_read) ty)) | SOME norm => map_types norm t @@ -370,7 +367,7 @@ fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy); fun the_class_data thy class = case lookup_class_data thy class - of NONE => error ("undeclared class " ^ quote class) + of NONE => error ("Undeclared class " ^ quote class) | SOME data => data; val locale_of_class = #locale oo the_class_data; @@ -475,8 +472,8 @@ fun class_intro thy locale class sups = let fun class_elim class = - case (map Drule.unconstrainTs o #axioms o AxClass.get_info thy) class - of [thm] => SOME thm + case (#axioms o AxClass.get_info thy) class + of [thm] => SOME (Drule.unconstrainTs thm) | [] => NONE; val pred_intro = case Locale.intros thy locale of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME @@ -504,7 +501,7 @@ fun class_interpretation class facts defs thy = let val { locale, inst, ... } = the_class_data thy class; - val tac = (ALLGOALS o ProofContext.fact_tac) facts; + val tac = ALLGOALS (ProofContext.fact_tac facts); val prfx = Logic.const_of_class (NameSpace.base class); in prove_interpretation tac ((false, prfx), []) (Locale.Locale locale) @@ -513,6 +510,7 @@ fun interpretation_in_rule thy (class1, class2) = let + val ctxt = ProofContext.init thy; fun mk_axioms class = let val { locale, inst = (_, insttab), ... } = the_class_data thy class; @@ -526,7 +524,7 @@ val (prems, concls) = pairself mk_axioms (class1, class2); in Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls) - (Locale.intro_locales_tac true (ProofContext.init thy)) + (Locale.intro_locales_tac true ctxt) end; fun intro_classes_tac facts st = @@ -729,7 +727,7 @@ Const ((fst o the o AList.lookup (op =) consts) c, ty) | subst t = t; fun prep_asm ((name, atts), ts) = - ((NameSpace.base name, map (Attrib.attribute thy) atts), + ((NameSpace.base name, map (Attrib.attribute_i thy) atts), (map o map_aterms) subst ts); in Locale.global_asms_of thy name_locale @@ -840,7 +838,7 @@ in NameSpace.implode [n2, prfx, prfx, n3] end; val c' = mk_name c; val rhs' = export_fixes thy class rhs; - val ty' = fastype_of rhs'; + val ty' = Term.fastype_of rhs'; val entry = mk_operation_entry thy (c', rhs); in thy