--- a/src/Pure/Isar/subclass.ML Fri Oct 12 14:42:29 2007 +0200
+++ b/src/Pure/Isar/subclass.ML Fri Oct 12 14:42:30 2007 +0200
@@ -2,14 +2,14 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Prove subclass relations between type classes
+Prove subclass relationship between type classes.
*)
signature SUBCLASS =
sig
val subclass: class -> local_theory -> Proof.state
val subclass_cmd: xstring -> local_theory -> Proof.state
- (*FIXME val prove_subclass: tactic -> class * class -> theory -> theory*)
+ val prove_subclass: tactic -> class -> local_theory -> local_theory
end;
structure Subclass : SUBCLASS =
@@ -48,71 +48,82 @@
local
-fun mk_subclass_rule lthy sup =
+fun gen_subclass prep_class do_proof raw_sup lthy =
let
- (*FIXME check for proper parameter inclusion (consts_of) (?)*)
- val ctxt = LocalTheory.target_of lthy;
- val thy = ProofContext.theory_of ctxt;
- val locale = Class.locale_of_class thy sup;
- in
- Locale.global_asms_of thy locale
- |> maps snd
- |> map (ObjectLogic.ensure_propT thy)
- end;
-
-fun gen_subclass prep_class raw_sup lthy =
- let
- (*FIXME cleanup, provide tactical interface*)
val ctxt = LocalTheory.target_of lthy;
val thy = ProofContext.theory_of ctxt;
val ctxt_thy = ProofContext.init thy;
val sup = prep_class thy raw_sup;
- val sub = case Option.mapPartial (Class.class_of_locale thy)
- (TheoryTarget.peek lthy)
+ val sub = case Option.mapPartial (Class.class_of_locale thy) (TheoryTarget.peek lthy)
of NONE => error "not in class context"
| SOME sub => sub;
- val export =
- Assumption.export false ctxt ctxt_thy
- #> singleton (Variable.export ctxt ctxt_thy);
+ val sub_params = map fst (Class.these_params thy [sub]);
+ val sup_params = map fst (Class.these_params thy [sup]);
+ val err_params = subtract (op =) sub_params sup_params;
+ val _ = if null err_params then [] else
+ error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^
+ commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]);
+ val sublocale_prop =
+ Locale.global_asms_of thy (Class.locale_of_class thy sup)
+ |> maps snd
+ |> map (ObjectLogic.ensure_propT thy);
+ val supclasses = Sign.complete_sort thy [sup]
+ |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
+ val supclasses' = remove (op =) sup supclasses;
+ val _ = if null supclasses' then () else
+ error ("The following superclasses of " ^ sup
+ ^ " are no superclass of " ^ sub ^ ": "
+ ^ commas supclasses');
+ (*FIXME*)
+ val sub_ax = #axioms (AxClass.get_info thy sub);
+ val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
val loc_name = Class.locale_of_class thy sub;
val loc_expr = Locale.Locale (Class.locale_of_class thy sup);
- fun prove_classrel interp thy =
+ fun prove_classrel subclass_rule =
let
- val classes = Sign.complete_sort thy [sup]
- |> filter_out (fn class' => Sign.subsort thy ([sub], [class']));
- fun instance_subclass (class1, class2) thy =
+ fun add_classrel sup' thy =
let
- val ax = #axioms (AxClass.get_info thy class1);
- val intro = #intro (AxClass.get_info thy class2)
- |> Drule.instantiate' [SOME (Thm.ctyp_of thy
- (TVar ((Name.aT, 0), [class1])))] [];
- val thm =
- intro
- |> OF_LAST (interp OF ax)
- |> strip_all_ofclass thy (Sign.super_classes thy class2);
+ val classrel =
+ #intro (AxClass.get_info thy sup')
+ |> Drule.instantiate' [SOME sub_inst] []
+ |> OF_LAST (subclass_rule OF sub_ax)
+ |> strip_all_ofclass thy (Sign.super_classes thy sup');
in
- thy |> AxClass.add_classrel thm
+ AxClass.add_classrel classrel thy
end;
in
- thy |> fold_rev (curry instance_subclass sub) classes
+ fold_rev add_classrel supclasses
end;
- fun after_qed [thms] =
+ fun prove_interpretation sublocale_rule =
+ prove_interpretation_in (ProofContext.fact_tac [sublocale_rule] 1)
+ I (loc_name, loc_expr)
+ fun after_qed thms =
let
- val thm = Conjunction.intr_balanced thms;
- val interp = export thm;
+ val sublocale_rule = Conjunction.intr_balanced thms;
+ val subclass_rule = sublocale_rule
+ |> Assumption.export false ctxt ctxt_thy
+ |> singleton (Variable.export ctxt ctxt_thy);
in
- LocalTheory.theory (prove_classrel interp
- #> prove_interpretation_in (ProofContext.fact_tac [thm] 1)
- I (loc_name, loc_expr))
+ LocalTheory.theory (prove_classrel subclass_rule
+ #> prove_interpretation sublocale_rule)
(*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*)
end;
+ in
+ do_proof after_qed sublocale_prop lthy
+ end;
- in Proof.theorem_i NONE after_qed [map (rpair []) (mk_subclass_rule lthy sup)] lthy end;
+fun user_proof after_qed props =
+ Proof.theorem_i NONE (after_qed o the_single) [map (rpair []) props];
+
+fun tactic_proof tac after_qed props lthy =
+ after_qed (Goal.prove_multi (LocalTheory.target_of lthy) [] [] props
+ (K tac)) lthy;
in
-val subclass = gen_subclass (K I);
-val subclass_cmd = gen_subclass Sign.read_class;
+val subclass = gen_subclass (K I) user_proof;
+val subclass_cmd = gen_subclass Sign.read_class user_proof;
+fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
end; (*local*)