src/Pure/Isar/class_target.ML
changeset 29558 9846af6c6d6a
parent 29545 4be5e49c74b1
child 29577 08f783c5fcf0
     1.1 --- a/src/Pure/Isar/class_target.ML	Mon Jan 19 08:16:42 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon Jan 19 08:16:42 2009 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4    val register: class -> class list -> ((string * typ) * (string * typ)) list
     1.5      -> sort -> morphism -> thm option -> thm option -> thm
     1.6      -> theory -> theory
     1.7 -  val register_subclass: class * class -> thm option
     1.8 -    -> theory -> theory
     1.9 +  val register_subclass: class * class -> morphism option -> Element.witness option
    1.10 +    -> morphism -> theory -> theory
    1.11  
    1.12    val is_class: theory -> class -> bool
    1.13    val base_sort: theory -> class -> sort
    1.14 @@ -270,16 +270,14 @@
    1.15      |> is_some some_def ? activate_defs class (the_list some_def)
    1.16    end;
    1.17  
    1.18 -fun register_subclass (sub, sup) thms thy =
    1.19 -  (*FIXME should also add subclass interpretation*)
    1.20 +fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
    1.21    let
    1.22 -    val of_class = (snd o rules thy) sup;
    1.23 -    val intro = case thms
    1.24 -     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
    1.25 -      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.26 -          ([], [sub])], []) of_class;
    1.27 -    val classrel = (intro OF (the_list o fst o rules thy) sub)
    1.28 -      |> Thm.close_derivation;
    1.29 +    val intros = (snd o rules thy) sup :: map_filter I
    1.30 +      [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
    1.31 +        (fst o rules thy) sub];
    1.32 +    val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
    1.33 +    val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.34 +      (K tac);
    1.35      val diff_sort = Sign.complete_sort thy [sup]
    1.36        |> subtract (op =) (Sign.complete_sort thy [sub]);
    1.37    in
    1.38 @@ -287,6 +285,11 @@
    1.39      |> AxClass.add_classrel classrel
    1.40      |> ClassData.map (Graph.add_edge (sub, sup))
    1.41      |> activate_defs sub (these_defs thy diff_sort)
    1.42 +    |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
    1.43 +        dep_morph $> Element.satisfy_morphism [wit] $> export))
    1.44 +          (the_list some_dep_morph) (the_list some_wit)
    1.45 +    |> (fn thy => fold_rev Locale.activate_global_facts
    1.46 +      (Locale.get_registrations thy) thy)
    1.47    end;
    1.48  
    1.49