src/Pure/Isar/class_target.ML
changeset 29526 0b32c8b84d3e
parent 29509 1ff0f3f08a7b
child 29545 4be5e49c74b1
     1.1 --- a/src/Pure/Isar/class_target.ML	Sat Jan 17 08:29:40 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sat Jan 17 08:29:54 2009 +0100
     1.3 @@ -8,31 +8,27 @@
     1.4  sig
     1.5    (*classes*)
     1.6    val register: class -> class list -> ((string * typ) * (string * typ)) list
     1.7 -    -> sort -> term list -> morphism
     1.8 -    -> thm option -> thm option -> thm -> theory -> theory
     1.9 +    -> sort -> morphism -> thm option -> thm option -> thm
    1.10 +    -> theory -> theory
    1.11    val register_subclass: class * class -> thm option
    1.12      -> theory -> theory
    1.13  
    1.14 +  val is_class: theory -> class -> bool
    1.15 +  val base_sort: theory -> class -> sort
    1.16 +  val rules: theory -> class -> thm option * thm
    1.17 +  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    1.18 +  val these_defs: theory -> sort -> thm list
    1.19 +  val print_classes: theory -> unit
    1.20 +
    1.21    val begin: class list -> sort -> Proof.context -> Proof.context
    1.22    val init: class -> theory -> Proof.context
    1.23    val declare: class -> Properties.T
    1.24      -> (string * mixfix) * term -> theory -> theory
    1.25    val abbrev: class -> Syntax.mode -> Properties.T
    1.26      -> (string * mixfix) * term -> theory -> theory
    1.27 +  val class_prefix: string -> string
    1.28    val refresh_syntax: class -> Proof.context -> Proof.context
    1.29  
    1.30 -  val intro_classes_tac: thm list -> tactic
    1.31 -  val default_intro_tac: Proof.context -> thm list -> tactic
    1.32 -
    1.33 -  val class_prefix: string -> string
    1.34 -  val is_class: theory -> class -> bool
    1.35 -  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    1.36 -  val these_defs: theory -> sort -> thm list
    1.37 -  val eq_morph: theory -> thm list -> morphism
    1.38 -  val base_sort: theory -> class -> sort
    1.39 -  val rules: theory -> class -> thm option * thm
    1.40 -  val print_classes: theory -> unit
    1.41 -
    1.42    (*instances*)
    1.43    val init_instantiation: string list * (string * sort) list * sort
    1.44      -> theory -> local_theory
    1.45 @@ -50,6 +46,9 @@
    1.46    val pretty_instantiation: local_theory -> Pretty.T
    1.47    val type_name: string -> string
    1.48  
    1.49 +  val intro_classes_tac: thm list -> tactic
    1.50 +  val default_intro_tac: Proof.context -> thm list -> tactic
    1.51 +
    1.52    (*old axclass layer*)
    1.53    val axclass_cmd: bstring * xstring list
    1.54      -> (Attrib.binding * string list) list
    1.55 @@ -116,8 +115,6 @@
    1.56    consts: (string * string) list
    1.57      (*locale parameter ~> constant name*),
    1.58    base_sort: sort,
    1.59 -  inst: term list
    1.60 -    (*canonical interpretation*),
    1.61    base_morph: Morphism.morphism
    1.62      (*static part of canonical morphism*),
    1.63    assm_intro: thm option,
    1.64 @@ -130,22 +127,22 @@
    1.65  
    1.66  };
    1.67  
    1.68 -fun rep_class_data (ClassData d) = d;
    1.69 -fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    1.70 +fun rep_class_data (ClassData data) = data;
    1.71 +fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.72      (defs, operations)) =
    1.73 -  ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.74 +  ClassData { consts = consts, base_sort = base_sort,
    1.75      base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.76      defs = defs, operations = operations };
    1.77 -fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
    1.78 +fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
    1.79      of_class, axiom, defs, operations }) =
    1.80 -  mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    1.81 +  mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.82      (defs, operations)));
    1.83  fun merge_class_data _ (ClassData { consts = consts,
    1.84 -    base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
    1.85 +    base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
    1.86      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    1.87 -  ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
    1.88 +  ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
    1.89      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    1.90 -  mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    1.91 +  mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.92      (Thm.merge_thms (defs1, defs2),
    1.93        AList.merge (op =) (K true) (operations1, operations2)));
    1.94  
    1.95 @@ -170,11 +167,8 @@
    1.96  val is_class = is_some oo lookup_class_data;
    1.97  
    1.98  val ancestry = Graph.all_succs o ClassData.get;
    1.99 -
   1.100  val heritage = Graph.all_preds o ClassData.get;
   1.101  
   1.102 -fun the_inst thy = #inst o the_class_data thy;
   1.103 -
   1.104  fun these_params thy =
   1.105    let
   1.106      fun params class =
   1.107 @@ -187,34 +181,22 @@
   1.108        end;
   1.109    in maps params o ancestry thy end;
   1.110  
   1.111 -fun these_assm_intros thy =
   1.112 +val base_sort = #base_sort oo the_class_data;
   1.113 +
   1.114 +fun rules thy class =
   1.115 +  let val { axiom, of_class, ... } = the_class_data thy class
   1.116 +  in (axiom, of_class) end;
   1.117 +
   1.118 +fun all_assm_intros thy =
   1.119    Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   1.120      ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   1.121  
   1.122 -fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   1.123 -
   1.124 -fun these_operations thy =
   1.125 -  maps (#operations o the_class_data thy) o ancestry thy;
   1.126 -
   1.127 -val base_sort = #base_sort oo the_class_data;
   1.128 -
   1.129 -fun rules thy class = let
   1.130 -    val { axiom, of_class, ... } = the_class_data thy class
   1.131 -  in (axiom, of_class) end;
   1.132 +fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
   1.133 +fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
   1.134  
   1.135 -val class_prefix = Logic.const_of_class o Sign.base_name;
   1.136 -
   1.137 -fun class_binding_morph class =
   1.138 -  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
   1.139 -
   1.140 -fun eq_morph thy thms = (*FIXME how general is this?*)
   1.141 -  Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms [])
   1.142 -  $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms);
   1.143 -
   1.144 -fun morphism thy class =
   1.145 -  let
   1.146 -    val { base_morph, defs, ... } = the_class_data thy class;
   1.147 -  in base_morph $> eq_morph thy defs end;
   1.148 +val base_morphism = #base_morph oo the_class_data;
   1.149 +fun morphism thy class = base_morphism thy class
   1.150 +  $> Element.eq_morphism thy (these_defs thy [class]);
   1.151  
   1.152  fun print_classes thy =
   1.153    let
   1.154 @@ -236,8 +218,6 @@
   1.155        (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   1.156        (SOME o Pretty.block) [Pretty.str "supersort: ",
   1.157          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   1.158 -      if is_class thy class then (SOME o Pretty.str)
   1.159 -        ("locale: " ^ Locale.extern thy class) else NONE,
   1.160        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   1.161            (Pretty.str "parameters:" :: ps)) o map mk_param
   1.162          o these o Option.map #params o try (AxClass.get_info thy)) class,
   1.163 @@ -254,18 +234,26 @@
   1.164  
   1.165  (* updaters *)
   1.166  
   1.167 -fun register class superclasses params base_sort inst morph
   1.168 +fun register class sups params base_sort morph
   1.169      axiom assm_intro of_class thy =
   1.170    let
   1.171      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   1.172        (c, (class, (ty, Free v_ty)))) params;
   1.173      val add_class = Graph.new_node (class,
   1.174          mk_class_data (((map o pairself) fst params, base_sort,
   1.175 -          inst, morph, assm_intro, of_class, axiom), ([], operations)))
   1.176 -      #> fold (curry Graph.add_edge class) superclasses;
   1.177 +          morph, assm_intro, of_class, axiom), ([], operations)))
   1.178 +      #> fold (curry Graph.add_edge class) sups;
   1.179    in ClassData.map add_class thy end;
   1.180  
   1.181 +fun activate_defs class thms thy =
   1.182 +  let
   1.183 +    val eq_morph = Element.eq_morphism thy thms;
   1.184 +    fun amend cls thy = Locale.amend_registration eq_morph
   1.185 +      (cls, morphism thy cls) thy;
   1.186 +  in fold amend (heritage thy [class]) thy end;
   1.187 +
   1.188  fun register_operation class (c, (t, some_def)) thy =
   1.189 +  (*FIXME 2009 does this still also work for abbrevs?*)
   1.190    let
   1.191      val base_sort = base_sort thy class;
   1.192      val prep_typ = map_type_tfree
   1.193 @@ -279,12 +267,11 @@
   1.194        (fn (defs, operations) =>
   1.195          (fold cons (the_list some_def) defs,
   1.196            (c, (class, (ty', t'))) :: operations))
   1.197 +    |> is_some some_def ? activate_defs class (the_list some_def)
   1.198    end;
   1.199  
   1.200 -
   1.201 -(** tactics and methods **)
   1.202 -
   1.203  fun register_subclass (sub, sup) thms thy =
   1.204 +  (*FIXME should also add subclass interpretation*)
   1.205    let
   1.206      val of_class = (snd o rules thy) sup;
   1.207      val intro = case thms
   1.208 @@ -293,46 +280,15 @@
   1.209            ([], [sub])], []) of_class;
   1.210      val classrel = (intro OF (the_list o fst o rules thy) sub)
   1.211        |> Thm.close_derivation;
   1.212 -    (*FIXME generic amend operation for classes*)
   1.213 -    val amendments = map (fn class => (class, morphism thy class))
   1.214 -      (heritage thy [sub]);
   1.215      val diff_sort = Sign.complete_sort thy [sup]
   1.216        |> subtract (op =) (Sign.complete_sort thy [sub]);
   1.217 -    val defs_morph = eq_morph thy (these_defs thy diff_sort);
   1.218    in
   1.219      thy
   1.220      |> AxClass.add_classrel classrel
   1.221      |> ClassData.map (Graph.add_edge (sub, sup))
   1.222 -    |> fold (Locale.amend_registration defs_morph) amendments
   1.223 -  end;
   1.224 -
   1.225 -fun intro_classes_tac facts st =
   1.226 -  let
   1.227 -    val thy = Thm.theory_of_thm st;
   1.228 -    val classes = Sign.all_classes thy;
   1.229 -    val class_trivs = map (Thm.class_triv thy) classes;
   1.230 -    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   1.231 -    val assm_intros = these_assm_intros thy;
   1.232 -  in
   1.233 -    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   1.234 +    |> activate_defs sub (these_defs thy diff_sort)
   1.235    end;
   1.236  
   1.237 -fun default_intro_tac ctxt [] =
   1.238 -      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
   1.239 -      Locale.intro_locales_tac true ctxt []
   1.240 -  | default_intro_tac _ _ = no_tac;
   1.241 -
   1.242 -fun default_tac rules ctxt facts =
   1.243 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   1.244 -    default_intro_tac ctxt facts;
   1.245 -
   1.246 -val _ = Context.>> (Context.map_theory
   1.247 -  (Method.add_methods
   1.248 -   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   1.249 -      "back-chain introduction rules of classes"),
   1.250 -    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   1.251 -      "apply some intro/elim rule")]));
   1.252 -
   1.253  
   1.254  (** classes and class target **)
   1.255  
   1.256 @@ -393,35 +349,33 @@
   1.257  
   1.258  (* class target *)
   1.259  
   1.260 +val class_prefix = Logic.const_of_class o Sign.base_name;
   1.261 +
   1.262  fun declare class pos ((c, mx), dict) thy =
   1.263    let
   1.264      val prfx = class_prefix class;
   1.265      val thy' = thy |> Sign.add_path prfx;
   1.266 +      (*FIXME 2009 use proper name morphism*)
   1.267      val morph = morphism thy' class;
   1.268 -    val inst = the_inst thy' class;
   1.269      val params = map (apsnd fst o snd) (these_params thy' [class]);
   1.270 -    val amendments = map (fn class => (class, morphism thy' class))
   1.271 -      (heritage thy' [class]);
   1.272  
   1.273      val c' = Sign.full_bname thy' c;
   1.274      val dict' = Morphism.term morph dict;
   1.275      val ty' = Term.fastype_of dict';
   1.276      val ty'' = Type.strip_sorts ty';
   1.277 +      (*FIXME 2009 the tinkering with theorems here is a mess*)
   1.278      val def_eq = Logic.mk_equals (Const (c', ty'), dict');
   1.279 -    (*FIXME a mess*)
   1.280 -    fun amend def def' (class, morph) thy =
   1.281 -      Locale.amend_registration (eq_morph thy [Thm.varifyT def])
   1.282 -        (class, morph) thy;
   1.283      fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   1.284    in
   1.285      thy'
   1.286      |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
   1.287 -    |> Thm.add_def false false (c, def_eq)
   1.288 +    |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*)
   1.289 +      (*FIXME 2009 add_def should accept binding*)
   1.290      |>> Thm.symmetric
   1.291      ||>> get_axiom
   1.292      |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
   1.293 -      #> fold (amend def def') amendments
   1.294 -      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*)
   1.295 +      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*)
   1.296 +         (*FIXME 2009 store_thm etc. should accept binding*)
   1.297        #> snd)
   1.298      |> Sign.restore_naming thy
   1.299      |> Sign.add_const_constraint (c', SOME ty')
   1.300 @@ -522,7 +476,7 @@
   1.301  
   1.302  fun type_name "*" = "prod"
   1.303    | type_name "+" = "sum"
   1.304 -  | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   1.305 +  | type_name s = sanatize_name (NameSpace.base s);
   1.306  
   1.307  fun resort_terms pp algebra consts constraints ts =
   1.308    let
   1.309 @@ -638,5 +592,35 @@
   1.310        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   1.311    end;
   1.312  
   1.313 +
   1.314 +(** tactics and methods **)
   1.315 +
   1.316 +fun intro_classes_tac facts st =
   1.317 +  let
   1.318 +    val thy = Thm.theory_of_thm st;
   1.319 +    val classes = Sign.all_classes thy;
   1.320 +    val class_trivs = map (Thm.class_triv thy) classes;
   1.321 +    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   1.322 +    val assm_intros = all_assm_intros thy;
   1.323 +  in
   1.324 +    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   1.325 +  end;
   1.326 +
   1.327 +fun default_intro_tac ctxt [] =
   1.328 +      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
   1.329 +      Locale.intro_locales_tac true ctxt []
   1.330 +  | default_intro_tac _ _ = no_tac;
   1.331 +
   1.332 +fun default_tac rules ctxt facts =
   1.333 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   1.334 +    default_intro_tac ctxt facts;
   1.335 +
   1.336 +val _ = Context.>> (Context.map_theory
   1.337 +  (Method.add_methods
   1.338 +   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   1.339 +      "back-chain introduction rules of classes"),
   1.340 +    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   1.341 +      "apply some intro/elim rule")]));
   1.342 +
   1.343  end;
   1.344