construct explicit class morphism
authorhaftmann
Sun Jan 11 14:18:16 2009 +0100 (2009-01-11)
changeset 2943983601bdadae8
parent 29400 a462459fb5ce
child 29440 0f7031a3e692
construct explicit class morphism
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Jan 09 08:22:44 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Jan 11 14:18:16 2009 +0100
     1.3 @@ -7,8 +7,8 @@
     1.4  signature CLASS =
     1.5  sig
     1.6    include CLASS_TARGET
     1.7 -    (*FIXME the split in class_target.ML, theory_target.ML and
     1.8 -      ML is artificial*)
     1.9 +    (*FIXME the split into class_target.ML, theory_target.ML and
    1.10 +      class.ML is artificial*)
    1.11  
    1.12    val class: bstring -> class list -> Element.context_i list
    1.13      -> theory -> string * local_theory
    1.14 @@ -45,7 +45,25 @@
    1.15          |> SOME
    1.16        end;
    1.17  
    1.18 -fun calculate_rules thy phi sups base_sort param_map axiom class =
    1.19 +fun raw_morphism thy class param_map some_axiom =
    1.20 +  let
    1.21 +    val ctxt = ProofContext.init thy;
    1.22 +    val some_wit = case some_axiom
    1.23 +     of SOME axiom => SOME (Element.prove_witness ctxt
    1.24 +          (Logic.unvarify (Thm.prop_of axiom))
    1.25 +            (ALLGOALS (ProofContext.fact_tac [axiom])))
    1.26 +      | NONE => NONE;
    1.27 +    val instT = Symtab.empty |> Symtab.update ("'a", TFree ("'a", [class]));
    1.28 +    val inst = Symtab.make ((map o apsnd) Const param_map);
    1.29 +  in case some_wit
    1.30 +   of SOME wit => Element.inst_morphism thy (instT, inst)
    1.31 +        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
    1.32 +        $> Element.satisfy_morphism [wit]
    1.33 +    | NONE => Element.inst_morphism thy (instT, inst)
    1.34 +        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
    1.35 +  end;
    1.36 +
    1.37 +fun calculate_rules thy morph sups base_sort param_map axiom class =
    1.38    let
    1.39      fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.40        (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.41 @@ -200,14 +218,13 @@
    1.42      #-> (fn axiom =>
    1.43          prove_class_interpretation class inst
    1.44            (supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
    1.45 -    #-> (fn morphism =>
    1.46 -        `(fn thy => activate_class_morphism thy class inst morphism)
    1.47 -    #-> (fn phi =>
    1.48 -        `(fn thy => calculate_rules thy phi sups base_sort param_map axiom class)
    1.49 +    #> `(fn thy => raw_morphism thy class param_map axiom)
    1.50 +    #-> (fn morph =>
    1.51 +        `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
    1.52      #-> (fn (assm_intro, of_class) =>
    1.53          register class sups params base_sort inst
    1.54 -          morphism axiom assm_intro of_class
    1.55 -    #> fold (note_assm_intro class) (the_list assm_intro))))))
    1.56 +          morph axiom assm_intro of_class
    1.57 +    #> fold (note_assm_intro class) (the_list assm_intro)))))
    1.58      |> TheoryTarget.init (SOME class)
    1.59      |> pair class
    1.60    end;
     2.1 --- a/src/Pure/Isar/class_target.ML	Fri Jan 09 08:22:44 2009 +0100
     2.2 +++ b/src/Pure/Isar/class_target.ML	Sun Jan 11 14:18:16 2009 +0100
     2.3 @@ -7,9 +7,8 @@
     2.4  signature CLASS_TARGET =
     2.5  sig
     2.6    (*classes*)
     2.7 -  type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
     2.8    val register: class -> class list -> ((string * typ) * (string * typ)) list
     2.9 -    -> sort -> term list -> raw_morphism
    2.10 +    -> sort -> term list -> morphism
    2.11      -> thm option -> thm option -> thm -> theory -> theory
    2.12  
    2.13    val begin: class list -> sort -> Proof.context -> Proof.context
    2.14 @@ -22,10 +21,8 @@
    2.15  
    2.16    val intro_classes_tac: thm list -> tactic
    2.17    val default_intro_tac: Proof.context -> thm list -> tactic
    2.18 -  val activate_class_morphism: theory -> class -> term list
    2.19 -    -> raw_morphism -> morphism
    2.20    val prove_class_interpretation: class -> term list -> (class * string) list
    2.21 -    -> thm list -> thm list -> theory -> raw_morphism * theory
    2.22 +    -> thm list -> thm list -> theory -> theory
    2.23    val prove_subclass_relation: class * class -> thm option -> theory -> theory
    2.24  
    2.25    val class_prefix: string -> string
    2.26 @@ -97,19 +94,6 @@
    2.27  end;
    2.28  
    2.29  
    2.30 -(** auxiliary **)
    2.31 -
    2.32 -val class_prefix = Logic.const_of_class o Sign.base_name;
    2.33 -
    2.34 -fun class_name_morphism class =
    2.35 -  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
    2.36 -
    2.37 -type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
    2.38 -
    2.39 -fun activate_class_morphism thy class inst morphism =
    2.40 -  Locale_Layer.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
    2.41 -
    2.42 -
    2.43  (** primitive axclass and instance commands **)
    2.44  
    2.45  fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    2.46 @@ -164,8 +148,8 @@
    2.47    base_sort: sort,
    2.48    inst: term list
    2.49      (*canonical interpretation*),
    2.50 -  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
    2.51 -    (*morphism cookie of canonical interpretation*),
    2.52 +  base_morph: Morphism.morphism
    2.53 +    (*static part of canonical morphism*),
    2.54    assm_intro: thm option,
    2.55    of_class: thm,
    2.56    axiom: thm option,
    2.57 @@ -177,21 +161,21 @@
    2.58  };
    2.59  
    2.60  fun rep_class_data (ClassData d) = d;
    2.61 -fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    2.62 +fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    2.63      (defs, operations)) =
    2.64    ClassData { consts = consts, base_sort = base_sort, inst = inst,
    2.65 -    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    2.66 +    base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    2.67      defs = defs, operations = operations };
    2.68 -fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
    2.69 +fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
    2.70      of_class, axiom, defs, operations }) =
    2.71 -  mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    2.72 +  mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    2.73      (defs, operations)));
    2.74  fun merge_class_data _ (ClassData { consts = consts,
    2.75 -    base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
    2.76 +    base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
    2.77      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    2.78 -  ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
    2.79 +  ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
    2.80      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    2.81 -  mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
    2.82 +  mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    2.83      (Thm.merge_thms (defs1, defs2),
    2.84        AList.merge (op =) (K true) (operations1, operations2)));
    2.85  
    2.86 @@ -246,10 +230,19 @@
    2.87      val { axiom, of_class, ... } = the_class_data thy class
    2.88    in (axiom, of_class) end;
    2.89  
    2.90 +val class_prefix = Logic.const_of_class o Sign.base_name;
    2.91 +
    2.92 +fun class_binding_morph class =
    2.93 +  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
    2.94 +
    2.95  fun morphism thy class =
    2.96    let
    2.97 -    val { inst, morphism, ... } = the_class_data thy class;
    2.98 -  in activate_class_morphism thy class inst morphism end;
    2.99 +    val { base_morph, defs, ... } = the_class_data thy class;
   2.100 +  in
   2.101 +    base_morph 
   2.102 +    $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy defs [])
   2.103 +    $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule defs)
   2.104 +  end;
   2.105  
   2.106  fun print_classes thy =
   2.107    let
   2.108 @@ -289,23 +282,23 @@
   2.109  
   2.110  (* updaters *)
   2.111  
   2.112 -fun register class superclasses params base_sort inst phi
   2.113 +fun register class superclasses params base_sort inst morph
   2.114      axiom assm_intro of_class thy =
   2.115    let
   2.116      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   2.117        (c, (class, (ty, Free v_ty)))) params;
   2.118      val add_class = Graph.new_node (class,
   2.119          mk_class_data (((map o pairself) fst params, base_sort,
   2.120 -          inst, phi, assm_intro, of_class, axiom), ([], operations)))
   2.121 +          inst, morph, assm_intro, of_class, axiom), ([], operations)))
   2.122        #> fold (curry Graph.add_edge class) superclasses;
   2.123    in ClassData.map add_class thy end;
   2.124  
   2.125  fun register_operation class (c, (t, some_def)) thy =
   2.126    let
   2.127      val base_sort = base_sort thy class;
   2.128 -    val prep_typ = map_type_tvar
   2.129 -      (fn (vi as (v, _), sort) => if Name.aT = v
   2.130 -        then TFree (v, base_sort) else TVar (vi, sort));
   2.131 +    val prep_typ = map_type_tfree
   2.132 +      (fn (v, sort) => if Name.aT = v
   2.133 +        then TFree (v, base_sort) else TVar ((v, 0), sort));
   2.134      val t' = map_types prep_typ t;
   2.135      val ty' = Term.fastype_of t';
   2.136    in
   2.137 @@ -331,9 +324,10 @@
   2.138    in
   2.139      thy
   2.140      |> fold2 add_constraint (map snd consts) no_constraints
   2.141 -    |> Locale_Layer.prove_interpretation tac (class_name_morphism class) (Locale_Layer.Locale class)
   2.142 +    |> Locale_Layer.prove_interpretation tac (class_binding_morph class) (Locale_Layer.Locale class)
   2.143            (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
   2.144 -    ||> fold2 add_constraint (map snd consts) constraints
   2.145 +    |> snd
   2.146 +    |> fold2 add_constraint (map snd consts) constraints
   2.147    end;
   2.148  
   2.149  fun prove_subclass_relation (sub, sup) some_thm thy =
   2.150 @@ -444,16 +438,15 @@
   2.151    let
   2.152      val prfx = class_prefix class;
   2.153      val thy' = thy |> Sign.add_path prfx;
   2.154 -    val phi = morphism thy' class;
   2.155 +    val morph = morphism thy' class;
   2.156      val inst = the_inst thy' class;
   2.157      val params = map (apsnd fst o snd) (these_params thy' [class]);
   2.158  
   2.159      val c' = Sign.full_bname thy' c;
   2.160 -    val dict' = Morphism.term phi dict;
   2.161 -    val dict_def = map_types Logic.unvarifyT dict';
   2.162 -    val ty' = Term.fastype_of dict_def;
   2.163 +    val dict' = Morphism.term morph dict;
   2.164 +    val ty' = Term.fastype_of dict';
   2.165      val ty'' = Type.strip_sorts ty';
   2.166 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   2.167 +    val def_eq = Logic.mk_equals (Const (c', ty'), dict');
   2.168      fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   2.169    in
   2.170      thy'
   2.171 @@ -462,9 +455,6 @@
   2.172      |>> Thm.symmetric
   2.173      ||>> get_axiom
   2.174      |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
   2.175 -      #> snd
   2.176 -        (*assumption: interpretation cookie does not change
   2.177 -          by adding equations to interpretation*)
   2.178        #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   2.179        #> PureThy.store_thm (c ^ "_raw", def')
   2.180        #> snd)
   2.181 @@ -649,9 +639,9 @@
   2.182  
   2.183  fun prove_instantiation_exit_result f tac x lthy =
   2.184    let
   2.185 -    val phi = ProofContext.export_morphism lthy
   2.186 +    val morph = ProofContext.export_morphism lthy
   2.187        (ProofContext.init (ProofContext.theory_of lthy));
   2.188 -    val y = f phi x;
   2.189 +    val y = f morph x;
   2.190    in
   2.191      lthy
   2.192      |> prove_instantiation_exit (fn ctxt => tac ctxt y)