--- a/src/Pure/Isar/subclass.ML Mon Jan 05 19:37:15 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Title: Pure/Isar/subclass.ML
- Author: Florian Haftmann, TU Muenchen
-
-User interface for proving subclass relationship between type classes.
-*)
-
-signature SUBCLASS =
-sig
- val subclass: class -> local_theory -> Proof.state
- val subclass_cmd: xstring -> local_theory -> Proof.state
- val prove_subclass: tactic -> class -> local_theory -> local_theory
-end;
-
-structure Subclass : SUBCLASS =
-struct
-
-local
-
-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"
- | {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 (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 " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
- commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
- val sublocale_prop =
- Locale.global_asms_of thy sup
- |> maps snd
- |> try the_single
- |> Option.map (ObjectLogic.ensure_propT thy);
- fun after_qed some_thm =
- LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm)
- #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
- in
- do_proof after_qed sublocale_prop lthy
- end;
-
-fun user_proof after_qed NONE =
- Proof.theorem_i NONE (K (after_qed NONE)) [[]]
- | user_proof after_qed (SOME prop) =
- Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
-
-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;
-
-in
-
-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*)
-
-end;