# HG changeset patch # User haftmann # Date 1232177394 -3600 # Node ID 0b32c8b84d3e312fec05e0fa682ba175558fccc7 # Parent ad7991d7b5bbc3a956e86030e6e60a5e7a75300e code cleanup diff -r ad7991d7b5bb -r 0b32c8b84d3e src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Jan 17 08:29:40 2009 +0100 +++ b/src/Pure/Isar/class.ML Sat Jan 17 08:29:54 2009 +0100 @@ -45,7 +45,7 @@ |> SOME end; -fun raw_morphism thy class sups param_map some_axiom = +fun calculate_morphism thy class sups param_map some_axiom = let val ctxt = ProofContext.init thy; val (([props], [(_, morph1)], export_morph), _) = ctxt @@ -58,9 +58,8 @@ $> Element.satisfy_morphism [(Element.prove_witness ctxt prop (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))] | [] => morph2; - (*FIXME generic amend operation for classes*) - val morph4 = morph3 $> eq_morph thy (these_defs thy sups); - in (morph4, export_morph) end; + val morph4 = morph3 $> Element.eq_morphism thy (these_defs thy sups); + in (morph3, morph4, export_morph) end; fun calculate_rules thy morph sups base_sort param_map axiom class = let @@ -96,13 +95,6 @@ |> Thm.close_derivation; in (assm_intro, of_class) end; -fun note_assm_intro class assm_intro thy = - thy - |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN) - |> PureThy.store_thm (AxClass.introN, assm_intro) - |> snd - |> Sign.restore_naming thy; - (** define classes **) @@ -110,6 +102,7 @@ fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems = let + (*FIXME 2009 simplify*) val supclasses = map (prep_class thy) raw_supclasses; val supsort = Sign.minimize_sort thy supclasses; val sups = filter (is_class thy) supsort; @@ -127,7 +120,7 @@ sups, []); val constrain = Element.Constrains ((map o apsnd o map_atyps) (K (TFree (Name.aT, base_sort))) supparams); - (*FIXME perhaps better: control type variable by explicit + (*FIXME 2009 perhaps better: control type variable by explicit parameter instantiation of import expression*) val begin_ctxt = begin sups base_sort #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps) @@ -148,6 +141,7 @@ fun add_consts bname class base_sort sups supparams global_syntax thy = let + (*FIXME 2009 simplify*) val supconsts = supparams |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups)) |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); @@ -177,6 +171,7 @@ fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy = let + (*FIXME 2009 simplify*) fun globalize param_map = map_aterms (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) | t => t); @@ -191,12 +186,12 @@ |> add_consts bname class base_sort sups supparams global_syntax |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) (map (fst o snd) params) - [(((*Binding.name (bname ^ "_" ^ AxClass.axiomsN*) Binding.empty, []), + [((Binding.empty, []), Option.map (globalize param_map) raw_pred |> the_list)] #> snd #> `get_axiom #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params - #> pair (map (Const o snd) param_map, param_map, params, assm_axiom))) + #> pair (param_map, params, assm_axiom))) end; fun gen_class prep_spec bname raw_supclasses raw_elems thy = @@ -204,32 +199,20 @@ val class = Sign.full_bname thy bname; val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) = prep_spec thy raw_supclasses raw_elems; - (*val export_morph = (*FIXME how canonical is this?*) - Morphism.morphism { binding = I, var = I, - typ = Logic.varifyT, - term = (*map_types Logic.varifyT*) I, - fact = map Thm.varifyT - } $> Morphism.morphism { binding = I, var = I, - typ = Logic.type_map TermSubst.zero_var_indexes, - term = TermSubst.zero_var_indexes, - fact = Drule.zero_var_indexes_list o map Thm.strip_shyps - };*) in thy |> Expression.add_locale bname "" supexpr elems |> snd |> LocalTheory.exit_global |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax - |-> (fn (inst, param_map, params, assm_axiom) => + |-> (fn (param_map, params, assm_axiom) => `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class) #-> (fn axiom => - `(fn thy => raw_morphism thy class sups param_map axiom) - #-> (fn (morph, export_morph) => Locale.add_registration (class, (morph, export_morph)) + `(fn thy => calculate_morphism thy class sups param_map axiom) + #-> (fn (raw_morph, morph, export_morph) => Locale.add_registration (class, (morph, export_morph)) #> Locale.activate_global_facts (class, morph $> export_morph) #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class) #-> (fn (assm_intro, of_class) => - register class sups params base_sort inst - morph axiom assm_intro of_class - (*#> fold (note_assm_intro class) (the_list assm_intro*))))) + register class sups params base_sort raw_morph axiom assm_intro of_class)))) |> TheoryTarget.init (SOME class) |> pair class end; @@ -246,12 +229,6 @@ local -fun prove_sublocale tac (sub, expr) = - Expression.sublocale sub expr - #> Proof.global_terminal_proof - (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) - #> ProofContext.theory_of; - fun gen_subclass prep_class do_proof raw_sup lthy = let val thy = ProofContext.theory_of lthy; @@ -259,6 +236,7 @@ val sub = case TheoryTarget.peek lthy of {is_class = false, ...} => error "Not a class context" | {target, ...} => target; + val _ = if Sign.subsort thy ([sup], [sub]) then error ("Class " ^ Syntax.string_of_sort lthy [sup] ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub]) @@ -273,15 +251,21 @@ val expr = ([(sup, (("", false), Expression.Positional []))], []); val (([props], _, _), goal_ctxt) = Expression.cert_goal_expression expr lthy; - val some_prop = try the_single props; (*FIXME*) + val some_prop = try the_single props; + + fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm)); + fun prove_sublocale some_thm = + Expression.sublocale sub expr + #> Proof.global_terminal_proof + (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE) + #> ProofContext.theory_of; fun after_qed some_thm = LocalTheory.theory (register_subclass (sub, sup) some_thm) - #> is_some some_thm ? LocalTheory.theory - (prove_sublocale (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) (sub, expr)) - #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); - in - do_proof after_qed some_prop lthy - end; + #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm) + (*FIXME should also go to register_subclass*) + #> ProofContext.theory_of + #> TheoryTarget.init (SOME sub); + in do_proof after_qed some_prop lthy end; fun user_proof after_qed NONE = Proof.theorem_i NONE (K (after_qed NONE)) [[]] diff -r ad7991d7b5bb -r 0b32c8b84d3e src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Sat Jan 17 08:29:40 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Sat Jan 17 08:29:54 2009 +0100 @@ -8,31 +8,27 @@ sig (*classes*) val register: class -> class list -> ((string * typ) * (string * typ)) list - -> sort -> term list -> morphism - -> thm option -> thm option -> thm -> theory -> theory + -> sort -> morphism -> thm option -> thm option -> thm + -> theory -> theory val register_subclass: class * class -> thm option -> theory -> theory + val is_class: theory -> class -> bool + val base_sort: theory -> class -> sort + val rules: theory -> class -> thm option * thm + val these_params: theory -> sort -> (string * (class * (string * typ))) list + val these_defs: theory -> sort -> thm list + val print_classes: theory -> unit + val begin: class list -> sort -> Proof.context -> Proof.context val init: class -> theory -> Proof.context val declare: class -> Properties.T -> (string * mixfix) * term -> theory -> theory val abbrev: class -> Syntax.mode -> Properties.T -> (string * mixfix) * term -> theory -> theory + val class_prefix: string -> string val refresh_syntax: class -> Proof.context -> Proof.context - val intro_classes_tac: thm list -> tactic - val default_intro_tac: Proof.context -> thm list -> tactic - - val class_prefix: string -> string - val is_class: theory -> class -> bool - val these_params: theory -> sort -> (string * (class * (string * typ))) list - val these_defs: theory -> sort -> thm list - val eq_morph: theory -> thm list -> morphism - val base_sort: theory -> class -> sort - val rules: theory -> class -> thm option * thm - val print_classes: theory -> unit - (*instances*) val init_instantiation: string list * (string * sort) list * sort -> theory -> local_theory @@ -50,6 +46,9 @@ val pretty_instantiation: local_theory -> Pretty.T val type_name: string -> string + val intro_classes_tac: thm list -> tactic + val default_intro_tac: Proof.context -> thm list -> tactic + (*old axclass layer*) val axclass_cmd: bstring * xstring list -> (Attrib.binding * string list) list @@ -116,8 +115,6 @@ consts: (string * string) list (*locale parameter ~> constant name*), base_sort: sort, - inst: term list - (*canonical interpretation*), base_morph: Morphism.morphism (*static part of canonical morphism*), assm_intro: thm option, @@ -130,22 +127,22 @@ }; -fun rep_class_data (ClassData d) = d; -fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom), +fun rep_class_data (ClassData data) = data; +fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom), (defs, operations)) = - ClassData { consts = consts, base_sort = base_sort, inst = inst, + ClassData { consts = consts, base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom, defs = defs, operations = operations }; -fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro, +fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro, of_class, axiom, defs, operations }) = - mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom), + mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom), (defs, operations))); fun merge_class_data _ (ClassData { consts = consts, - base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro, + base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, - ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _, + ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _, of_class = _, axiom = _, defs = defs2, operations = operations2 }) = - mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom), + mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom), (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2))); @@ -170,11 +167,8 @@ val is_class = is_some oo lookup_class_data; val ancestry = Graph.all_succs o ClassData.get; - val heritage = Graph.all_preds o ClassData.get; -fun the_inst thy = #inst o the_class_data thy; - fun these_params thy = let fun params class = @@ -187,34 +181,22 @@ end; in maps params o ancestry thy end; -fun these_assm_intros thy = +val base_sort = #base_sort oo the_class_data; + +fun rules thy class = + let val { axiom, of_class, ... } = the_class_data thy class + in (axiom, of_class) end; + +fun all_assm_intros thy = Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm) ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) []; -fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy; - -fun these_operations thy = - maps (#operations o the_class_data thy) o ancestry thy; - -val base_sort = #base_sort oo the_class_data; - -fun rules thy class = let - val { axiom, of_class, ... } = the_class_data thy class - in (axiom, of_class) end; +fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; +fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; -val class_prefix = Logic.const_of_class o Sign.base_name; - -fun class_binding_morph class = - Binding.map_prefix (K (Binding.add_prefix false (class_prefix class))); - -fun eq_morph thy thms = (*FIXME how general is this?*) - Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms []) - $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms); - -fun morphism thy class = - let - val { base_morph, defs, ... } = the_class_data thy class; - in base_morph $> eq_morph thy defs end; +val base_morphism = #base_morph oo the_class_data; +fun morphism thy class = base_morphism thy class + $> Element.eq_morphism thy (these_defs thy [class]); fun print_classes thy = let @@ -236,8 +218,6 @@ (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), (SOME o Pretty.block) [Pretty.str "supersort: ", (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], - if is_class thy class then (SOME o Pretty.str) - ("locale: " ^ Locale.extern thy class) else NONE, ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param o these o Option.map #params o try (AxClass.get_info thy)) class, @@ -254,18 +234,26 @@ (* updaters *) -fun register class superclasses params base_sort inst morph +fun register class sups params base_sort morph axiom assm_intro of_class thy = let val operations = map (fn (v_ty as (_, ty), (c, _)) => (c, (class, (ty, Free v_ty)))) params; val add_class = Graph.new_node (class, mk_class_data (((map o pairself) fst params, base_sort, - inst, morph, assm_intro, of_class, axiom), ([], operations))) - #> fold (curry Graph.add_edge class) superclasses; + morph, assm_intro, of_class, axiom), ([], operations))) + #> fold (curry Graph.add_edge class) sups; in ClassData.map add_class thy end; +fun activate_defs class thms thy = + let + val eq_morph = Element.eq_morphism thy thms; + fun amend cls thy = Locale.amend_registration eq_morph + (cls, morphism thy cls) thy; + in fold amend (heritage thy [class]) thy end; + fun register_operation class (c, (t, some_def)) thy = + (*FIXME 2009 does this still also work for abbrevs?*) let val base_sort = base_sort thy class; val prep_typ = map_type_tfree @@ -279,12 +267,11 @@ (fn (defs, operations) => (fold cons (the_list some_def) defs, (c, (class, (ty', t'))) :: operations)) + |> is_some some_def ? activate_defs class (the_list some_def) end; - -(** tactics and methods **) - fun register_subclass (sub, sup) thms thy = + (*FIXME should also add subclass interpretation*) let val of_class = (snd o rules thy) sup; val intro = case thms @@ -293,46 +280,15 @@ ([], [sub])], []) of_class; val classrel = (intro OF (the_list o fst o rules thy) sub) |> Thm.close_derivation; - (*FIXME generic amend operation for classes*) - val amendments = map (fn class => (class, morphism thy class)) - (heritage thy [sub]); val diff_sort = Sign.complete_sort thy [sup] |> subtract (op =) (Sign.complete_sort thy [sub]); - val defs_morph = eq_morph thy (these_defs thy diff_sort); in thy |> AxClass.add_classrel classrel |> ClassData.map (Graph.add_edge (sub, sup)) - |> fold (Locale.amend_registration defs_morph) amendments - end; - -fun intro_classes_tac facts st = - let - val thy = Thm.theory_of_thm st; - val classes = Sign.all_classes thy; - val class_trivs = map (Thm.class_triv thy) classes; - val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; - val assm_intros = these_assm_intros thy; - in - Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st + |> activate_defs sub (these_defs thy diff_sort) end; -fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE - Locale.intro_locales_tac true ctxt [] - | default_intro_tac _ _ = no_tac; - -fun default_tac rules ctxt facts = - HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE - default_intro_tac ctxt facts; - -val _ = Context.>> (Context.map_theory - (Method.add_methods - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), - "back-chain introduction rules of classes"), - ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), - "apply some intro/elim rule")])); - (** classes and class target **) @@ -393,35 +349,33 @@ (* class target *) +val class_prefix = Logic.const_of_class o Sign.base_name; + fun declare class pos ((c, mx), dict) thy = let val prfx = class_prefix class; val thy' = thy |> Sign.add_path prfx; + (*FIXME 2009 use proper name morphism*) val morph = morphism thy' class; - val inst = the_inst thy' class; val params = map (apsnd fst o snd) (these_params thy' [class]); - val amendments = map (fn class => (class, morphism thy' class)) - (heritage thy' [class]); val c' = Sign.full_bname thy' c; val dict' = Morphism.term morph dict; val ty' = Term.fastype_of dict'; val ty'' = Type.strip_sorts ty'; + (*FIXME 2009 the tinkering with theorems here is a mess*) val def_eq = Logic.mk_equals (Const (c', ty'), dict'); - (*FIXME a mess*) - fun amend def def' (class, morph) thy = - Locale.amend_registration (eq_morph thy [Thm.varifyT def]) - (class, morph) thy; fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy); in thy' |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd - |> Thm.add_def false false (c, def_eq) + |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*) + (*FIXME 2009 add_def should accept binding*) |>> Thm.symmetric ||>> get_axiom |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def'))) - #> fold (amend def def') amendments - #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*) + #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*) + (*FIXME 2009 store_thm etc. should accept binding*) #> snd) |> Sign.restore_naming thy |> Sign.add_const_constraint (c', SOME ty') @@ -522,7 +476,7 @@ fun type_name "*" = "prod" | type_name "+" = "sum" - | type_name s = sanatize_name (NameSpace.base s); (*FIXME*) + | type_name s = sanatize_name (NameSpace.base s); fun resort_terms pp algebra consts constraints ts = let @@ -638,5 +592,35 @@ (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) end; + +(** tactics and methods **) + +fun intro_classes_tac facts st = + let + val thy = Thm.theory_of_thm st; + val classes = Sign.all_classes thy; + val class_trivs = map (Thm.class_triv thy) classes; + val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; + val assm_intros = all_assm_intros thy; + in + Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st + end; + +fun default_intro_tac ctxt [] = + intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE + Locale.intro_locales_tac true ctxt [] + | default_intro_tac _ _ = no_tac; + +fun default_tac rules ctxt facts = + HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE + default_intro_tac ctxt facts; + +val _ = Context.>> (Context.map_theory + (Method.add_methods + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), + "back-chain introduction rules of classes"), + ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), + "apply some intro/elim rule")])); + end;