src/Pure/Isar/class_target.ML
changeset 29439 83601bdadae8
parent 29362 f9ded2d789b9
child 29509 1ff0f3f08a7b
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Jan 09 08:22:44 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Jan 11 14:18:16 2009 +0100
     1.3 @@ -7,9 +7,8 @@
     1.4  signature CLASS_TARGET =
     1.5  sig
     1.6    (*classes*)
     1.7 -  type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
     1.8    val register: class -> class list -> ((string * typ) * (string * typ)) list
     1.9 -    -> sort -> term list -> raw_morphism
    1.10 +    -> sort -> term list -> morphism
    1.11      -> thm option -> thm option -> thm -> theory -> theory
    1.12  
    1.13    val begin: class list -> sort -> Proof.context -> Proof.context
    1.14 @@ -22,10 +21,8 @@
    1.15  
    1.16    val intro_classes_tac: thm list -> tactic
    1.17    val default_intro_tac: Proof.context -> thm list -> tactic
    1.18 -  val activate_class_morphism: theory -> class -> term list
    1.19 -    -> raw_morphism -> morphism
    1.20    val prove_class_interpretation: class -> term list -> (class * string) list
    1.21 -    -> thm list -> thm list -> theory -> raw_morphism * theory
    1.22 +    -> thm list -> thm list -> theory -> theory
    1.23    val prove_subclass_relation: class * class -> thm option -> theory -> theory
    1.24  
    1.25    val class_prefix: string -> string
    1.26 @@ -97,19 +94,6 @@
    1.27  end;
    1.28  
    1.29  
    1.30 -(** auxiliary **)
    1.31 -
    1.32 -val class_prefix = Logic.const_of_class o Sign.base_name;
    1.33 -
    1.34 -fun class_name_morphism class =
    1.35 -  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
    1.36 -
    1.37 -type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
    1.38 -
    1.39 -fun activate_class_morphism thy class inst morphism =
    1.40 -  Locale_Layer.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
    1.41 -
    1.42 -
    1.43  (** primitive axclass and instance commands **)
    1.44  
    1.45  fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    1.46 @@ -164,8 +148,8 @@
    1.47    base_sort: sort,
    1.48    inst: term list
    1.49      (*canonical interpretation*),
    1.50 -  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
    1.51 -    (*morphism cookie of canonical interpretation*),
    1.52 +  base_morph: Morphism.morphism
    1.53 +    (*static part of canonical morphism*),
    1.54    assm_intro: thm option,
    1.55    of_class: thm,
    1.56    axiom: thm option,
    1.57 @@ -177,21 +161,21 @@
    1.58  };
    1.59  
    1.60  fun rep_class_data (ClassData d) = d;
    1.61 -fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.62 +fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    1.63      (defs, operations)) =
    1.64    ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.65 -    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.66 +    base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.67      defs = defs, operations = operations };
    1.68 -fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
    1.69 +fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
    1.70      of_class, axiom, defs, operations }) =
    1.71 -  mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.72 +  mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    1.73      (defs, operations)));
    1.74  fun merge_class_data _ (ClassData { consts = consts,
    1.75 -    base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
    1.76 +    base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
    1.77      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    1.78 -  ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
    1.79 +  ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
    1.80      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    1.81 -  mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    1.82 +  mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    1.83      (Thm.merge_thms (defs1, defs2),
    1.84        AList.merge (op =) (K true) (operations1, operations2)));
    1.85  
    1.86 @@ -246,10 +230,19 @@
    1.87      val { axiom, of_class, ... } = the_class_data thy class
    1.88    in (axiom, of_class) end;
    1.89  
    1.90 +val class_prefix = Logic.const_of_class o Sign.base_name;
    1.91 +
    1.92 +fun class_binding_morph class =
    1.93 +  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
    1.94 +
    1.95  fun morphism thy class =
    1.96    let
    1.97 -    val { inst, morphism, ... } = the_class_data thy class;
    1.98 -  in activate_class_morphism thy class inst morphism end;
    1.99 +    val { base_morph, defs, ... } = the_class_data thy class;
   1.100 +  in
   1.101 +    base_morph 
   1.102 +    $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy defs [])
   1.103 +    $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule defs)
   1.104 +  end;
   1.105  
   1.106  fun print_classes thy =
   1.107    let
   1.108 @@ -289,23 +282,23 @@
   1.109  
   1.110  (* updaters *)
   1.111  
   1.112 -fun register class superclasses params base_sort inst phi
   1.113 +fun register class superclasses params base_sort inst morph
   1.114      axiom assm_intro of_class thy =
   1.115    let
   1.116      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   1.117        (c, (class, (ty, Free v_ty)))) params;
   1.118      val add_class = Graph.new_node (class,
   1.119          mk_class_data (((map o pairself) fst params, base_sort,
   1.120 -          inst, phi, assm_intro, of_class, axiom), ([], operations)))
   1.121 +          inst, morph, assm_intro, of_class, axiom), ([], operations)))
   1.122        #> fold (curry Graph.add_edge class) superclasses;
   1.123    in ClassData.map add_class thy end;
   1.124  
   1.125  fun register_operation class (c, (t, some_def)) thy =
   1.126    let
   1.127      val base_sort = base_sort thy class;
   1.128 -    val prep_typ = map_type_tvar
   1.129 -      (fn (vi as (v, _), sort) => if Name.aT = v
   1.130 -        then TFree (v, base_sort) else TVar (vi, sort));
   1.131 +    val prep_typ = map_type_tfree
   1.132 +      (fn (v, sort) => if Name.aT = v
   1.133 +        then TFree (v, base_sort) else TVar ((v, 0), sort));
   1.134      val t' = map_types prep_typ t;
   1.135      val ty' = Term.fastype_of t';
   1.136    in
   1.137 @@ -331,9 +324,10 @@
   1.138    in
   1.139      thy
   1.140      |> fold2 add_constraint (map snd consts) no_constraints
   1.141 -    |> Locale_Layer.prove_interpretation tac (class_name_morphism class) (Locale_Layer.Locale class)
   1.142 +    |> Locale_Layer.prove_interpretation tac (class_binding_morph class) (Locale_Layer.Locale class)
   1.143            (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
   1.144 -    ||> fold2 add_constraint (map snd consts) constraints
   1.145 +    |> snd
   1.146 +    |> fold2 add_constraint (map snd consts) constraints
   1.147    end;
   1.148  
   1.149  fun prove_subclass_relation (sub, sup) some_thm thy =
   1.150 @@ -444,16 +438,15 @@
   1.151    let
   1.152      val prfx = class_prefix class;
   1.153      val thy' = thy |> Sign.add_path prfx;
   1.154 -    val phi = morphism thy' class;
   1.155 +    val morph = morphism thy' class;
   1.156      val inst = the_inst thy' class;
   1.157      val params = map (apsnd fst o snd) (these_params thy' [class]);
   1.158  
   1.159      val c' = Sign.full_bname thy' c;
   1.160 -    val dict' = Morphism.term phi dict;
   1.161 -    val dict_def = map_types Logic.unvarifyT dict';
   1.162 -    val ty' = Term.fastype_of dict_def;
   1.163 +    val dict' = Morphism.term morph dict;
   1.164 +    val ty' = Term.fastype_of dict';
   1.165      val ty'' = Type.strip_sorts ty';
   1.166 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   1.167 +    val def_eq = Logic.mk_equals (Const (c', ty'), dict');
   1.168      fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   1.169    in
   1.170      thy'
   1.171 @@ -462,9 +455,6 @@
   1.172      |>> Thm.symmetric
   1.173      ||>> get_axiom
   1.174      |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
   1.175 -      #> snd
   1.176 -        (*assumption: interpretation cookie does not change
   1.177 -          by adding equations to interpretation*)
   1.178        #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   1.179        #> PureThy.store_thm (c ^ "_raw", def')
   1.180        #> snd)
   1.181 @@ -649,9 +639,9 @@
   1.182  
   1.183  fun prove_instantiation_exit_result f tac x lthy =
   1.184    let
   1.185 -    val phi = ProofContext.export_morphism lthy
   1.186 +    val morph = ProofContext.export_morphism lthy
   1.187        (ProofContext.init (ProofContext.theory_of lthy));
   1.188 -    val y = f phi x;
   1.189 +    val y = f morph x;
   1.190    in
   1.191      lthy
   1.192      |> prove_instantiation_exit (fn ctxt => tac ctxt y)