1.1 --- a/src/Pure/Isar/subclass.ML	Thu Oct 25 19:27:53 2007 +0200
     1.2 +++ b/src/Pure/Isar/subclass.ML	Thu Oct 25 19:27:54 2007 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Prove subclass relationship between type classes.
     1.8 +User interface for proving subclass relationship between type classes.
     1.9  *)
    1.10  
    1.11  signature SUBCLASS =
    1.12 @@ -15,87 +15,6 @@
    1.13  structure Subclass : SUBCLASS =
    1.14  struct
    1.15  
    1.16 -(** auxiliary **)
    1.17 -
    1.18 -fun prove_interpretation_in tac after_qed (name, expr) =
    1.19 -  Locale.interpretation_in_locale
    1.20 -      (ProofContext.theory after_qed) (name, expr)
    1.21 -  #> Proof.global_terminal_proof
    1.22 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.23 -  #> ProofContext.theory_of;
    1.24 -
    1.25 -fun OF_LAST thm1 thm2 =
    1.26 -  let
    1.27 -    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
    1.28 -  in (thm1 RSN (n, thm2)) end;
    1.29 -
    1.30 -fun strip_all_ofclass thy sort =
    1.31 -  let
    1.32 -    val typ = TVar ((Name.aT, 0), sort);
    1.33 -    fun prem_inclass t =
    1.34 -      case Logic.strip_imp_prems t
    1.35 -       of ofcls :: _ => try Logic.dest_inclass ofcls
    1.36 -        | [] => NONE;
    1.37 -    fun strip_ofclass class thm =
    1.38 -      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
    1.39 -    fun strip thm = case (prem_inclass o Thm.prop_of) thm
    1.40 -     of SOME (_, class) => thm |> strip_ofclass class |> strip
    1.41 -      | NONE => thm;
    1.42 -  in strip end;
    1.43 -
    1.44 -fun subclass_rule thy (sub, sup) =
    1.45 -  let
    1.46 -    val ctxt = Locale.init sub thy;
    1.47 -    val ctxt_thy = ProofContext.init thy;
    1.48 -    val params = Class.these_params thy [sup];
    1.49 -    val props =
    1.50 -      Locale.global_asms_of thy sup
    1.51 -      |> maps snd
    1.52 -      |> map (ObjectLogic.ensure_propT thy);
    1.53 -    fun tac { prems, context } =
    1.54 -      Locale.intro_locales_tac true context prems
    1.55 -        ORELSE ALLGOALS assume_tac;
    1.56 -  in
    1.57 -    Goal.prove_multi ctxt [] [] props tac
    1.58 -    |> map (Assumption.export false ctxt ctxt_thy)
    1.59 -    |> Variable.export ctxt ctxt_thy
    1.60 -  end;
    1.61 -
    1.62 -fun prove_single_subclass (sub, sup) thms ctxt thy =
    1.63 -  let
    1.64 -    val ctxt_thy = ProofContext.init thy;
    1.65 -    val subclass_rule = Conjunction.intr_balanced thms
    1.66 -      |> Assumption.export false ctxt ctxt_thy
    1.67 -      |> singleton (Variable.export ctxt ctxt_thy);
    1.68 -    val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
    1.69 -    val sub_ax = #axioms (AxClass.get_info thy sub);
    1.70 -    val classrel =
    1.71 -      #intro (AxClass.get_info thy sup)
    1.72 -      |> Drule.instantiate' [SOME sub_inst] []
    1.73 -      |> OF_LAST (subclass_rule OF sub_ax)
    1.74 -      |> strip_all_ofclass thy (Sign.super_classes thy sup)
    1.75 -      |> Thm.strip_shyps
    1.76 -  in
    1.77 -    thy
    1.78 -    |> AxClass.add_classrel classrel
    1.79 -    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms))
    1.80 -         I (sub, Locale.Locale sup)
    1.81 -  end;
    1.82 -
    1.83 -fun prove_subclass (sub, sup) thms ctxt thy =
    1.84 -  let
    1.85 -    val supclasses = Sign.complete_sort thy [sup]
    1.86 -      |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
    1.87 -    fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
    1.88 -  in
    1.89 -    thy
    1.90 -    |> fold_rev (fn sup' => prove_single_subclass (sub, sup')
    1.91 -         (transform sup') ctxt) supclasses
    1.92 - end;
    1.93 -
    1.94 -
    1.95 -(** subclassing **)
    1.96 -
    1.97  local
    1.98  
    1.99  fun gen_subclass prep_class do_proof raw_sup lthy =
   1.100 @@ -118,7 +37,7 @@
   1.101        |> maps snd
   1.102        |> map (ObjectLogic.ensure_propT thy);
   1.103      fun after_qed thms =
   1.104 -      LocalTheory.theory (prove_subclass (sub, sup) thms ctxt)
   1.105 +      LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt)
   1.106        (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*);
   1.107    in
   1.108      do_proof after_qed sublocale_prop lthy