src/Pure/Isar/class.ML
changeset 29439 83601bdadae8
parent 29378 2821c2c5270d
child 29509 1ff0f3f08a7b
     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;