--- a/src/Pure/Isar/class.ML Mon Jan 19 08:16:42 2009 +0100
+++ b/src/Pure/Isar/class.ML Mon Jan 19 08:16:42 2009 +0100
@@ -89,7 +89,7 @@
in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
-fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
+fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
let
(*FIXME 2009 simplify*)
val supclasses = map (prep_class thy) raw_supclasses;
@@ -125,8 +125,8 @@
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
-val cert_class_spec = gen_class_spec (K I) Expression.cert_declaration;
-val read_class_spec = gen_class_spec Sign.intern_class Expression.cert_read_declaration;
+val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
+val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
@@ -218,51 +218,36 @@
fun gen_subclass prep_class do_proof raw_sup lthy =
let
val thy = ProofContext.theory_of lthy;
- val sup = prep_class thy raw_sup;
- val sub = case TheoryTarget.peek lthy
- of {is_class = false, ...} => error "Not a class context"
+ val proto_sup = prep_class thy raw_sup;
+ val proto_sub = case TheoryTarget.peek lthy
+ of {is_class = false, ...} => error "Not in a class context"
| {target, ...} => target;
-
- val _ = if Sign.subsort thy ([sup], [sub])
- then error ("Class " ^ Syntax.string_of_sort lthy [sup]
- ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
- else ();
- val sub_params = map fst (these_params thy [sub]);
- val sup_params = map fst (these_params thy [sup]);
- val err_params = subtract (op =) sub_params sup_params;
- val _ = if null err_params then [] else
- error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
- commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
+ val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
val expr = ([(sup, (("", false), Expression.Positional []))], []);
- val (([props], _, _), goal_ctxt) =
+ val (([props], deps, export), goal_ctxt) =
Expression.cert_goal_expression expr lthy;
val some_prop = try the_single props;
-
- fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm));
- fun prove_sublocale some_thm =
- Expression.sublocale sub expr
- #> Proof.global_terminal_proof
- (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE)
- #> ProofContext.theory_of;
- fun after_qed some_thm =
- LocalTheory.theory (register_subclass (sub, sup) some_thm)
- #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm)
- (*FIXME should also go to register_subclass*)
- #> ProofContext.theory_of
- #> TheoryTarget.init (SOME sub);
- in do_proof after_qed some_prop lthy end;
+ val some_dep_morph = try the_single (map snd deps);
+ fun after_qed some_wit =
+ ProofContext.theory (register_subclass (sub, sup)
+ some_dep_morph some_wit export)
+ #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
+ in do_proof after_qed some_prop goal_ctxt end;
fun user_proof after_qed NONE =
Proof.theorem_i NONE (K (after_qed NONE)) [[]]
+ #> Element.refine_witness #> Seq.hd
| user_proof after_qed (SOME prop) =
- Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
+ Proof.theorem_i NONE (after_qed o SOME o Element.make_witness prop
+ o Thm.close_derivation o the_single o the_single)
+ [[(Element.mark_witness prop, [])]]
+ #> Element.refine_witness #> Seq.hd;
-fun tactic_proof tac after_qed NONE lthy =
- after_qed NONE lthy
- | tactic_proof tac after_qed (SOME prop) lthy =
- after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
- (K tac))) lthy;
+fun tactic_proof tac after_qed NONE ctxt =
+ after_qed NONE ctxt
+ | tactic_proof tac after_qed (SOME prop) ctxt =
+ after_qed (SOME (Element.prove_witness ctxt prop tac)) ctxt;
in
--- a/src/Pure/Isar/class_target.ML Mon Jan 19 08:16:42 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Mon Jan 19 08:16:42 2009 +0100
@@ -10,8 +10,8 @@
val register: class -> class list -> ((string * typ) * (string * typ)) list
-> sort -> morphism -> thm option -> thm option -> thm
-> theory -> theory
- val register_subclass: class * class -> thm option
- -> theory -> theory
+ val register_subclass: class * class -> morphism option -> Element.witness option
+ -> morphism -> theory -> theory
val is_class: theory -> class -> bool
val base_sort: theory -> class -> sort
@@ -270,16 +270,14 @@
|> is_some some_def ? activate_defs class (the_list some_def)
end;
-fun register_subclass (sub, sup) thms thy =
- (*FIXME should also add subclass interpretation*)
+fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
let
- val of_class = (snd o rules thy) sup;
- val intro = case thms
- of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
- | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
- ([], [sub])], []) of_class;
- val classrel = (intro OF (the_list o fst o rules thy) sub)
- |> Thm.close_derivation;
+ val intros = (snd o rules thy) sup :: map_filter I
+ [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
+ (fst o rules thy) sub];
+ val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
+ val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+ (K tac);
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub]);
in
@@ -287,6 +285,11 @@
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
+ |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
+ dep_morph $> Element.satisfy_morphism [wit] $> export))
+ (the_list some_dep_morph) (the_list some_wit)
+ |> (fn thy => fold_rev Locale.activate_global_facts
+ (Locale.get_registrations thy) thy)
end;