# HG changeset patch
# User haftmann
# Date 1193333274 -7200
# Node ID 0db9a16c0d3c5b8a2b57d88d25a991be4c37a683
# Parent  62638dcafe385e3840b2b93632475704456c1fd7
moved primitive operations to class.ML

diff -r 62638dcafe38 -r 0db9a16c0d3c src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Thu Oct 25 19:27:53 2007 +0200
+++ b/src/Pure/Isar/subclass.ML	Thu Oct 25 19:27:54 2007 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Prove subclass relationship between type classes.
+User interface for proving subclass relationship between type classes.
 *)
 
 signature SUBCLASS =
@@ -15,87 +15,6 @@
 structure Subclass : SUBCLASS =
 struct
 
-(** auxiliary **)
-
-fun prove_interpretation_in tac after_qed (name, expr) =
-  Locale.interpretation_in_locale
-      (ProofContext.theory after_qed) (name, expr)
-  #> Proof.global_terminal_proof
-      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
-  #> ProofContext.theory_of;
-
-fun OF_LAST thm1 thm2 =
-  let
-    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
-  in (thm1 RSN (n, thm2)) end;
-
-fun strip_all_ofclass thy sort =
-  let
-    val typ = TVar ((Name.aT, 0), sort);
-    fun prem_inclass t =
-      case Logic.strip_imp_prems t
-       of ofcls :: _ => try Logic.dest_inclass ofcls
-        | [] => NONE;
-    fun strip_ofclass class thm =
-      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
-    fun strip thm = case (prem_inclass o Thm.prop_of) thm
-     of SOME (_, class) => thm |> strip_ofclass class |> strip
-      | NONE => thm;
-  in strip end;
-
-fun subclass_rule thy (sub, sup) =
-  let
-    val ctxt = Locale.init sub thy;
-    val ctxt_thy = ProofContext.init thy;
-    val params = Class.these_params thy [sup];
-    val props =
-      Locale.global_asms_of thy sup
-      |> maps snd
-      |> map (ObjectLogic.ensure_propT thy);
-    fun tac { prems, context } =
-      Locale.intro_locales_tac true context prems
-        ORELSE ALLGOALS assume_tac;
-  in
-    Goal.prove_multi ctxt [] [] props tac
-    |> map (Assumption.export false ctxt ctxt_thy)
-    |> Variable.export ctxt ctxt_thy
-  end;
-
-fun prove_single_subclass (sub, sup) thms ctxt thy =
-  let
-    val ctxt_thy = ProofContext.init thy;
-    val subclass_rule = Conjunction.intr_balanced thms
-      |> Assumption.export false ctxt ctxt_thy
-      |> singleton (Variable.export ctxt ctxt_thy);
-    val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
-    val sub_ax = #axioms (AxClass.get_info thy sub);
-    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)
-      |> Thm.strip_shyps
-  in
-    thy
-    |> AxClass.add_classrel classrel
-    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms))
-         I (sub, Locale.Locale sup)
-  end;
-
-fun prove_subclass (sub, sup) thms ctxt thy =
-  let
-    val supclasses = Sign.complete_sort thy [sup]
-      |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
-    fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
-  in
-    thy
-    |> fold_rev (fn sup' => prove_single_subclass (sub, sup')
-         (transform sup') ctxt) supclasses
- end;
-
-
-(** subclassing **)
-
 local
 
 fun gen_subclass prep_class do_proof raw_sup lthy =
@@ -118,7 +37,7 @@
       |> maps snd
       |> map (ObjectLogic.ensure_propT thy);
     fun after_qed thms =
-      LocalTheory.theory (prove_subclass (sub, sup) thms ctxt)
+      LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt)
       (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*);
   in
     do_proof after_qed sublocale_prop lthy