improved tackling of subclasses
authorhaftmann
Mon Jan 19 08:16:42 2009 +0100 (2009-01-19)
changeset 295589846af6c6d6a
parent 29557 5362cc5ee3a8
child 29559 fe9cfe076c23
improved tackling of subclasses
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Jan 19 08:16:42 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jan 19 08:16:42 2009 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  
     1.5    in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
     1.6  
     1.7 -fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
     1.8 +fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
     1.9    let
    1.10      (*FIXME 2009 simplify*)
    1.11      val supclasses = map (prep_class thy) raw_supclasses;
    1.12 @@ -125,8 +125,8 @@
    1.13      val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
    1.14    in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
    1.15  
    1.16 -val cert_class_spec = gen_class_spec (K I) Expression.cert_declaration;
    1.17 -val read_class_spec = gen_class_spec Sign.intern_class Expression.cert_read_declaration;
    1.18 +val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
    1.19 +val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
    1.20  
    1.21  fun add_consts bname class base_sort sups supparams global_syntax thy =
    1.22    let
    1.23 @@ -218,51 +218,36 @@
    1.24  fun gen_subclass prep_class do_proof raw_sup lthy =
    1.25    let
    1.26      val thy = ProofContext.theory_of lthy;
    1.27 -    val sup = prep_class thy raw_sup;
    1.28 -    val sub = case TheoryTarget.peek lthy
    1.29 -     of {is_class = false, ...} => error "Not a class context"
    1.30 +    val proto_sup = prep_class thy raw_sup;
    1.31 +    val proto_sub = case TheoryTarget.peek lthy
    1.32 +     of {is_class = false, ...} => error "Not in a class context"
    1.33        | {target, ...} => target;
    1.34 -
    1.35 -    val _ = if Sign.subsort thy ([sup], [sub])
    1.36 -      then error ("Class " ^ Syntax.string_of_sort lthy [sup]
    1.37 -        ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
    1.38 -      else ();
    1.39 -    val sub_params = map fst (these_params thy [sub]);
    1.40 -    val sup_params = map fst (these_params thy [sup]);
    1.41 -    val err_params = subtract (op =) sub_params sup_params;
    1.42 -    val _ = if null err_params then [] else
    1.43 -      error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
    1.44 -        commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
    1.45 +    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
    1.46  
    1.47      val expr = ([(sup, (("", false), Expression.Positional []))], []);
    1.48 -    val (([props], _, _), goal_ctxt) =
    1.49 +    val (([props], deps, export), goal_ctxt) =
    1.50        Expression.cert_goal_expression expr lthy;
    1.51      val some_prop = try the_single props;
    1.52 -
    1.53 -    fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm));
    1.54 -    fun prove_sublocale some_thm =
    1.55 -      Expression.sublocale sub expr
    1.56 -      #> Proof.global_terminal_proof
    1.57 -          (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE)
    1.58 -      #> ProofContext.theory_of;
    1.59 -    fun after_qed some_thm =
    1.60 -      LocalTheory.theory (register_subclass (sub, sup) some_thm)
    1.61 -      #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm)
    1.62 -          (*FIXME should also go to register_subclass*)
    1.63 -      #> ProofContext.theory_of
    1.64 -      #> TheoryTarget.init (SOME sub);
    1.65 -  in do_proof after_qed some_prop lthy end;
    1.66 +    val some_dep_morph = try the_single (map snd deps);
    1.67 +    fun after_qed some_wit =
    1.68 +      ProofContext.theory (register_subclass (sub, sup)
    1.69 +        some_dep_morph some_wit export)
    1.70 +      #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
    1.71 +  in do_proof after_qed some_prop goal_ctxt end;
    1.72  
    1.73  fun user_proof after_qed NONE =
    1.74        Proof.theorem_i NONE (K (after_qed NONE)) [[]]
    1.75 +      #> Element.refine_witness #> Seq.hd
    1.76    | user_proof after_qed (SOME prop) =
    1.77 -      Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
    1.78 +      Proof.theorem_i NONE (after_qed o SOME o Element.make_witness prop
    1.79 +        o Thm.close_derivation o the_single o the_single)
    1.80 +          [[(Element.mark_witness prop, [])]]
    1.81 +      #> Element.refine_witness #> Seq.hd;
    1.82  
    1.83 -fun tactic_proof tac after_qed NONE lthy =
    1.84 -      after_qed NONE lthy
    1.85 -  | tactic_proof tac after_qed (SOME prop) lthy =
    1.86 -      after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
    1.87 -        (K tac))) lthy;
    1.88 +fun tactic_proof tac after_qed NONE ctxt =
    1.89 +      after_qed NONE ctxt
    1.90 +  | tactic_proof tac after_qed (SOME prop) ctxt =
    1.91 +      after_qed (SOME (Element.prove_witness ctxt prop tac)) ctxt;
    1.92  
    1.93  in
    1.94  
     2.1 --- a/src/Pure/Isar/class_target.ML	Mon Jan 19 08:16:42 2009 +0100
     2.2 +++ b/src/Pure/Isar/class_target.ML	Mon Jan 19 08:16:42 2009 +0100
     2.3 @@ -10,8 +10,8 @@
     2.4    val register: class -> class list -> ((string * typ) * (string * typ)) list
     2.5      -> sort -> morphism -> thm option -> thm option -> thm
     2.6      -> theory -> theory
     2.7 -  val register_subclass: class * class -> thm option
     2.8 -    -> theory -> theory
     2.9 +  val register_subclass: class * class -> morphism option -> Element.witness option
    2.10 +    -> morphism -> theory -> theory
    2.11  
    2.12    val is_class: theory -> class -> bool
    2.13    val base_sort: theory -> class -> sort
    2.14 @@ -270,16 +270,14 @@
    2.15      |> is_some some_def ? activate_defs class (the_list some_def)
    2.16    end;
    2.17  
    2.18 -fun register_subclass (sub, sup) thms thy =
    2.19 -  (*FIXME should also add subclass interpretation*)
    2.20 +fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
    2.21    let
    2.22 -    val of_class = (snd o rules thy) sup;
    2.23 -    val intro = case thms
    2.24 -     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
    2.25 -      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    2.26 -          ([], [sub])], []) of_class;
    2.27 -    val classrel = (intro OF (the_list o fst o rules thy) sub)
    2.28 -      |> Thm.close_derivation;
    2.29 +    val intros = (snd o rules thy) sup :: map_filter I
    2.30 +      [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
    2.31 +        (fst o rules thy) sub];
    2.32 +    val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
    2.33 +    val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    2.34 +      (K tac);
    2.35      val diff_sort = Sign.complete_sort thy [sup]
    2.36        |> subtract (op =) (Sign.complete_sort thy [sub]);
    2.37    in
    2.38 @@ -287,6 +285,11 @@
    2.39      |> AxClass.add_classrel classrel
    2.40      |> ClassData.map (Graph.add_edge (sub, sup))
    2.41      |> activate_defs sub (these_defs thy diff_sort)
    2.42 +    |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
    2.43 +        dep_morph $> Element.satisfy_morphism [wit] $> export))
    2.44 +          (the_list some_dep_morph) (the_list some_wit)
    2.45 +    |> (fn thy => fold_rev Locale.activate_global_facts
    2.46 +      (Locale.get_registrations thy) thy)
    2.47    end;
    2.48  
    2.49