class morphism stemming from locale interpretation
authorhaftmann
Thu Nov 06 09:09:48 2008 +0100 (2008-11-06)
changeset 28715238f9966c80e
parent 28714 1992553cccfe
child 28716 ee6f9e50f9c8
class morphism stemming from locale interpretation
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Nov 03 14:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Nov 06 09:09:48 2008 +0100
     1.3 @@ -18,10 +18,6 @@
     1.4      -> (string * mixfix) * term -> theory -> theory
     1.5    val abbrev: class -> Syntax.mode -> Properties.T
     1.6      -> (string * mixfix) * term -> theory -> theory
     1.7 -  val note: class -> string
     1.8 -    -> (Attrib.binding * (thm list * Attrib.src list) list) list
     1.9 -    -> theory -> (bstring * thm list) list * theory
    1.10 -  val declaration: class -> declaration -> theory -> theory
    1.11    val refresh_syntax: class -> Proof.context -> Proof.context
    1.12  
    1.13    val intro_classes_tac: thm list -> tactic
    1.14 @@ -67,10 +63,10 @@
    1.15  (** auxiliary **)
    1.16  
    1.17  fun prove_interpretation tac prfx_atts expr inst =
    1.18 -  Locale.interpretation_i I prfx_atts expr inst #> snd
    1.19 -  #> Proof.global_terminal_proof
    1.20 +  Locale.interpretation_i I prfx_atts expr inst
    1.21 +  ##> Proof.global_terminal_proof
    1.22        (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
    1.23 -  #> ProofContext.theory_of;
    1.24 +  ##> ProofContext.theory_of;
    1.25  
    1.26  fun prove_interpretation_in tac after_qed (name, expr) =
    1.27    Locale.interpretation_in_locale
    1.28 @@ -79,6 +75,28 @@
    1.29        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.30    #> ProofContext.theory_of;
    1.31  
    1.32 +val class_prefix = Logic.const_of_class o Sign.base_name;
    1.33 +
    1.34 +fun activate_class_morphism thy class inst morphism =
    1.35 +  Locale.get_interpret_morph thy (class_prefix class) "" morphism class inst;
    1.36 +
    1.37 +fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
    1.38 +  let
    1.39 +    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
    1.40 +      [class]))) (Sign.the_const_type thy c)) consts;
    1.41 +    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
    1.42 +    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
    1.43 +    fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
    1.44 +      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
    1.45 +    val prfx = class_prefix class;
    1.46 +  in
    1.47 +    thy
    1.48 +    |> fold2 add_constraint (map snd consts) no_constraints
    1.49 +    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
    1.50 +          (map SOME inst, map (pair (Attrib.no_binding) o Thm.prop_of) def_facts)
    1.51 +    ||> fold2 add_constraint (map snd consts) constraints
    1.52 +  end;
    1.53 +
    1.54  
    1.55  (** primitive axclass and instance commands **)
    1.56  
    1.57 @@ -127,18 +145,23 @@
    1.58  (** class data **)
    1.59  
    1.60  datatype class_data = ClassData of {
    1.61 +
    1.62 +  (* static part *)
    1.63    consts: (string * string) list
    1.64      (*locale parameter ~> constant name*),
    1.65    base_sort: sort,
    1.66 -  inst: term option list
    1.67 +  inst: term list
    1.68      (*canonical interpretation*),
    1.69 -  morphism: theory -> thm list -> morphism,
    1.70 -    (*partial morphism of canonical interpretation*)
    1.71 +  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
    1.72 +    (*morphism cookie of canonical interpretation*),
    1.73    assm_intro: thm option,
    1.74    of_class: thm,
    1.75    axiom: thm option,
    1.76 +  
    1.77 +  (* dynamic part *)
    1.78    defs: thm list,
    1.79    operations: (string * (class * (typ * term))) list
    1.80 +
    1.81  };
    1.82  
    1.83  fun rep_class_data (ClassData d) = d;
    1.84 @@ -147,8 +170,8 @@
    1.85    ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.86      morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.87      defs = defs, operations = operations };
    1.88 -fun map_class_data f (ClassData { consts, base_sort, inst, morphism,
    1.89 -    assm_intro, of_class, axiom, defs, operations }) =
    1.90 +fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
    1.91 +    of_class, axiom, defs, operations }) =
    1.92    mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.93      (defs, operations)));
    1.94  fun merge_class_data _ (ClassData { consts = consts,
    1.95 @@ -182,6 +205,8 @@
    1.96  
    1.97  val ancestry = Graph.all_succs o ClassData.get;
    1.98  
    1.99 +fun the_inst thy = #inst o the_class_data thy;
   1.100 +
   1.101  fun these_params thy =
   1.102    let
   1.103      fun params class =
   1.104 @@ -194,17 +219,20 @@
   1.105        end;
   1.106    in maps params o ancestry thy end;
   1.107  
   1.108 -fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   1.109 -
   1.110 -fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]);
   1.111 -
   1.112  fun these_assm_intros thy =
   1.113    Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   1.114      ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   1.115  
   1.116 +fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   1.117 +
   1.118  fun these_operations thy =
   1.119    maps (#operations o the_class_data thy) o ancestry thy;
   1.120  
   1.121 +fun morphism thy class =
   1.122 +  let
   1.123 +    val { inst, morphism, ... } = the_class_data thy class;
   1.124 +  in activate_class_morphism thy class inst morphism end;
   1.125 +
   1.126  fun print_classes thy =
   1.127    let
   1.128      val ctxt = ProofContext.init thy;
   1.129 @@ -250,7 +278,7 @@
   1.130        (c, (class, (ty, Free v_ty)))) params;
   1.131      val add_class = Graph.new_node (class,
   1.132          mk_class_data (((map o pairself) fst params, base_sort,
   1.133 -          map (SOME o Const) inst, phi, assm_intro, of_class, axiom), ([], operations)))
   1.134 +          inst, phi, assm_intro, of_class, axiom), ([], operations)))
   1.135        #> fold (curry Graph.add_edge class) superclasses;
   1.136    in ClassData.map add_class thy end;
   1.137  
   1.138 @@ -273,65 +301,38 @@
   1.139  
   1.140  (** rule calculation, tactics and methods **)
   1.141  
   1.142 -val class_prefix = Logic.const_of_class o Sign.base_name;
   1.143 +fun calculate_axiom thy sups base_sort assm_axiom param_map class =
   1.144 +  case Locale.intros thy class
   1.145 +   of (_, []) => assm_axiom
   1.146 +    | (_, [intro]) =>
   1.147 +      let
   1.148 +        fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
   1.149 +          (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
   1.150 +            (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
   1.151 +              Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
   1.152 +        val axiom_premises = map_filter (#axiom o the_class_data thy) sups
   1.153 +          @ the_list assm_axiom;
   1.154 +      in intro
   1.155 +        |> instantiate thy [class]
   1.156 +        |> (fn thm => thm OF axiom_premises)
   1.157 +        |> Drule.standard'
   1.158 +        |> Thm.close_derivation
   1.159 +        |> SOME
   1.160 +      end;
   1.161  
   1.162 -fun calculate sups base_sort assm_axiom param_map class thy =
   1.163 +fun calculate_rules thy phi sups base_sort param_map axiom class =
   1.164    let
   1.165 -    (*static parts of morphism*)
   1.166 -    val subst_typ = map_type_tfree (fn (v, sort) =>
   1.167 -          if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
   1.168 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) param_map v
   1.169 -         of SOME (c, _) => Const (c, ty)
   1.170 -          | NONE => t)
   1.171 -      | subst_aterm t = t;
   1.172      fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
   1.173        (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
   1.174          (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
   1.175            Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
   1.176 -    (*fun inst thy sort thm = (tracing (makestring thm); instantiate thy sort thm);
   1.177 -    val instantiate = inst;*)
   1.178 -    val (proto_assm_intro, locale_intro) = Locale.intros thy class
   1.179 -      |> pairself (try the_single);
   1.180 -    val axiom_premises = map_filter (#axiom o the_class_data thy) sups
   1.181 -      @ the_list assm_axiom;
   1.182 -    val axiom = locale_intro
   1.183 -      |> Option.map (Thm.close_derivation o Drule.standard' o (fn thm => thm OF axiom_premises) o instantiate thy [class])
   1.184 -      |> (fn x as SOME _ => x | NONE => assm_axiom);
   1.185 -    val lift_axiom = case axiom
   1.186 -     of SOME axiom => (fn thm => ((*tracing "-(morphism)-";
   1.187 -          tracing (makestring thm);
   1.188 -          tracing (makestring axiom);*)
   1.189 -          Thm.implies_elim thm axiom))
   1.190 -      | NONE => I;
   1.191 -
   1.192 -    (*dynamic parts of morphism*)
   1.193 -    fun avoid_a thy thm =
   1.194 -      let
   1.195 -        val tvars = Term.add_tvars (Thm.prop_of thm) [];
   1.196 -        val thm' = case AList.lookup (op =) tvars (Name.aT, 0)
   1.197 -         of SOME sort => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o rpair sort o rpair 0)
   1.198 -              (Name.aT, Name.variant (map (fst o fst) tvars) Name.aT)], []) thm
   1.199 -          | NONE => thm;
   1.200 -      in thm' end;
   1.201 -    fun rew_term thy defs = Pattern.rewrite_term thy
   1.202 -      (map (Logic.dest_equals o Thm.prop_of) defs) [];
   1.203 -    fun subst_term thy defs = map_aterms subst_aterm #> rew_term thy defs
   1.204 -      #> map_types subst_typ;
   1.205 -    fun subst_thm thy defs = Drule.zero_var_indexes #> avoid_a thy
   1.206 -      #> Drule.standard' #> instantiate thy [class] #> lift_axiom
   1.207 -      #> MetaSimplifier.rewrite_rule defs;
   1.208 -    fun morphism thy defs =
   1.209 -      Morphism.typ_morphism subst_typ
   1.210 -      $> Morphism.term_morphism (subst_term thy defs)
   1.211 -      $> Morphism.thm_morphism (subst_thm thy defs);
   1.212 -
   1.213 -    (*class rules*)
   1.214      val defs = these_defs thy sups;
   1.215 -    val assm_intro = proto_assm_intro
   1.216 -      |> Option.map (instantiate thy base_sort)
   1.217 -      |> Option.map (MetaSimplifier.rewrite_rule defs)
   1.218 -      |> Option.map Thm.close_derivation;
   1.219 -    val class_intro = (#intro o AxClass.get_info thy) class;
   1.220 +    val assm_intro = Locale.intros thy class
   1.221 +      |> fst
   1.222 +      |> map (instantiate thy base_sort)
   1.223 +      |> map (MetaSimplifier.rewrite_rule defs)
   1.224 +      |> map Thm.close_derivation
   1.225 +      |> try the_single;
   1.226      val fixate = Thm.instantiate
   1.227        (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
   1.228          (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
   1.229 @@ -348,39 +349,11 @@
   1.230          |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort))
   1.231          |> (Thm.assume o Thm.cterm_of thy)
   1.232          |> replicate num_trivs;
   1.233 -    val of_class = (fixate class_intro OF of_class_sups OF locale_dests OF pred_trivs)
   1.234 +    val axclass_intro = (#intro o AxClass.get_info thy) class;
   1.235 +    val of_class = (fixate axclass_intro OF of_class_sups OF locale_dests OF pred_trivs)
   1.236        |> Drule.standard'
   1.237        |> Thm.close_derivation;
   1.238 -    val this_intro = assm_intro |> the_default class_intro;
   1.239 -  in
   1.240 -    thy
   1.241 -    |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
   1.242 -    |> PureThy.store_thm (AxClass.introN, this_intro)
   1.243 -    |> snd
   1.244 -    |> Sign.restore_naming thy
   1.245 -    |> pair (morphism, axiom, assm_intro, of_class)
   1.246 -  end;
   1.247 -
   1.248 -fun class_interpretation class facts defs thy = thy;
   1.249 -
   1.250 -fun class_interpretation class facts defs thy =
   1.251 -  let
   1.252 -    val consts = map (apsnd fst o snd) (these_params thy [class]);
   1.253 -    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
   1.254 -      [class]))) (Sign.the_const_type thy c)) consts;
   1.255 -    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
   1.256 -    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
   1.257 -    val inst = (#inst o the_class_data thy) class;
   1.258 -    fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts
   1.259 -      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
   1.260 -    val prfx = class_prefix class;
   1.261 -  in
   1.262 -    thy
   1.263 -    |> fold2 add_constraint (map snd consts) no_constraints
   1.264 -    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
   1.265 -          (inst, map (fn def => (Attrib.no_binding, def)) defs)
   1.266 -    |> fold2 add_constraint (map snd consts) constraints
   1.267 -  end;
   1.268 +  in (assm_intro, of_class) end;
   1.269  
   1.270  fun prove_subclass (sub, sup) some_thm thy =
   1.271    let
   1.272 @@ -399,6 +372,13 @@
   1.273      |> ClassData.map (Graph.add_edge (sub, sup))
   1.274    end;
   1.275  
   1.276 +fun note_assm_intro class assm_intro thy =
   1.277 +  thy
   1.278 +  |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
   1.279 +  |> PureThy.store_thm (AxClass.introN, assm_intro)
   1.280 +  |> snd
   1.281 +  |> Sign.restore_naming thy;
   1.282 +
   1.283  fun intro_classes_tac facts st =
   1.284    let
   1.285      val thy = Thm.theory_of_thm st;
   1.286 @@ -490,6 +470,8 @@
   1.287      val prfx = class_prefix class;
   1.288      val thy' = thy |> Sign.add_path prfx;
   1.289      val phi = morphism thy' class;
   1.290 +    val inst = the_inst thy' class;
   1.291 +    val params = map (apsnd fst o snd) (these_params thy' [class]);
   1.292  
   1.293      val c' = Sign.full_name thy' c;
   1.294      val dict' = Morphism.term phi dict;
   1.295 @@ -504,7 +486,10 @@
   1.296      |> Thm.add_def false false (c, def_eq)
   1.297      |>> Thm.symmetric
   1.298      ||>> get_axiom
   1.299 -    |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
   1.300 +    |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
   1.301 +      #> snd
   1.302 +        (*assumption: interpretation cookie does not change
   1.303 +          by adding equations to interpretation*)
   1.304        #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   1.305        #> PureThy.store_thm (c ^ "_raw", def')
   1.306        #> snd)
   1.307 @@ -532,22 +517,6 @@
   1.308      |> Sign.restore_naming thy
   1.309    end;
   1.310  
   1.311 -fun note class kind facts thy =
   1.312 -  let
   1.313 -    val phi = morphism thy class;
   1.314 -    val facts' = facts
   1.315 -      |> PureThy.map_facts (Morphism.thm phi) 
   1.316 -      |> Attrib.map_facts (Attrib.attribute_i thy);
   1.317 -  in
   1.318 -    thy
   1.319 -    |> Sign.add_path (class_prefix class)
   1.320 -    |> PureThy.note_thmss kind facts'
   1.321 -    ||> Sign.restore_naming thy
   1.322 -  end;
   1.323 -
   1.324 -fun declaration class decl thy =
   1.325 -  Context.theory_map (decl (morphism thy class)) thy;
   1.326 -
   1.327  
   1.328  (* class definition *)
   1.329  
   1.330 @@ -593,12 +562,13 @@
   1.331  val read_class_spec = gen_class_spec Sign.intern_class Locale.read_expr;
   1.332  val check_class_spec = gen_class_spec (K I) Locale.cert_expr;
   1.333  
   1.334 -fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
   1.335 +fun add_consts bname class base_sort sups supparams global_syntax thy =
   1.336    let
   1.337      val supconsts = map fst supparams
   1.338        |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
   1.339        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
   1.340      val all_params = map fst (Locale.parameters_of thy class);
   1.341 +    val raw_params = (snd o chop (length supparams)) all_params;
   1.342      fun add_const (v, raw_ty) thy =
   1.343        let
   1.344          val c = Sign.full_name thy v;
   1.345 @@ -612,12 +582,16 @@
   1.346          |> snd
   1.347          |> pair ((v, ty), (c, ty'))
   1.348        end;
   1.349 -    fun add_consts raw_params thy =
   1.350 -      thy
   1.351 -      |> Sign.add_path (Logic.const_of_class bname)
   1.352 -      |> fold_map add_const raw_params
   1.353 -      ||> Sign.restore_naming thy
   1.354 -      |-> (fn params => pair (supconsts @ (map o apfst) fst params, params));
   1.355 +  in
   1.356 +    thy
   1.357 +    |> Sign.add_path (Logic.const_of_class bname)
   1.358 +    |> fold_map add_const raw_params
   1.359 +    ||> Sign.restore_naming thy
   1.360 +    |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   1.361 +  end;
   1.362 +
   1.363 +fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
   1.364 +  let
   1.365      fun globalize param_map = map_aterms
   1.366        (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
   1.367          | t => t);
   1.368 @@ -629,14 +603,14 @@
   1.369        | [thm] => SOME thm;
   1.370    in
   1.371      thy
   1.372 -    |> add_consts ((snd o chop (length supparams)) all_params)
   1.373 +    |> add_consts bname class base_sort sups supparams global_syntax
   1.374      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   1.375            (map (fst o snd) params)
   1.376            [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
   1.377      #> snd
   1.378      #> `get_axiom
   1.379      #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   1.380 -    #> pair (param_map, params, assm_axiom)))
   1.381 +    #> pair (map (Const o snd) param_map, param_map, params, assm_axiom)))
   1.382    end;
   1.383  
   1.384  fun gen_class prep_spec bname raw_supclasses raw_elems thy =
   1.385 @@ -644,21 +618,26 @@
   1.386      val class = Sign.full_name thy bname;
   1.387      val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
   1.388        prep_spec thy raw_supclasses raw_elems;
   1.389 +    val supconsts = map (apsnd fst o snd) (these_params thy sups);
   1.390    in
   1.391      thy
   1.392      |> Locale.add_locale_i "" bname mergeexpr elems
   1.393      |> snd
   1.394      |> ProofContext.theory_of
   1.395      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
   1.396 -    |-> (fn (param_map, params, assm_axiom) =>
   1.397 -        calculate sups base_sort assm_axiom param_map class
   1.398 -    #-> (fn (morphism, axiom, assm_intro, of_class) =>
   1.399 -        add_class_data ((class, sups), (params, base_sort,
   1.400 -          map snd param_map, morphism, axiom, assm_intro, of_class))
   1.401 -    (*#> `(fn thy => Locale.facts_of thy class)
   1.402 -    #-> (fn facts => fold_map (note class Thm.assumptionK) facts
   1.403 -    #> snd*)
   1.404 -    #> class_interpretation class (the_list axiom) []))
   1.405 +    |-> (fn (inst, param_map, params, assm_axiom) =>
   1.406 +        `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
   1.407 +    #-> (fn axiom =>
   1.408 +        prove_class_interpretation class inst
   1.409 +          (supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
   1.410 +    #-> (fn morphism =>
   1.411 +        `(fn thy => activate_class_morphism thy class inst morphism)
   1.412 +    #-> (fn phi =>
   1.413 +        `(fn thy => calculate_rules thy phi sups base_sort param_map axiom class)
   1.414 +    #-> (fn (assm_intro, of_class) =>
   1.415 +        add_class_data ((class, sups), (params, base_sort, inst,
   1.416 +          morphism, axiom, assm_intro, of_class))
   1.417 +    #> fold (note_assm_intro class) (the_list assm_intro))))))
   1.418      |> init class
   1.419      |> pair class
   1.420    end;