src/Pure/Isar/class.ML

   val add_syntactic_const: string -> Syntax.mode -> Markup.property list
     -> (string * mixfix) * term -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
   val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
+  val prove_subclass: class * class -> thm list -> Proof.context
+    -> theory -> theory
   val print_classes: theory -> unit
   val uncheck: bool ref
 
   val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
   val instance: arity list -> ((bstring * Attrib.src list) * term) list

 val classN = "class";
 val introN = "intro";
 
 fun prove_interpretation tac prfx_atts expr inst =
   Locale.interpretation_i I prfx_atts expr inst
+  #> Proof.global_terminal_proof
+      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+  #> ProofContext.theory_of;
+
+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 = thm1 RSN (Thm.nprems_of thm2, thm2);

     (*canonical interpretation*),
   morphism: morphism,
     (*partial morphism of canonical interpretation*)
   intro: thm,
   defs: thm list,
-  operations: (string * ((term * (typ * int)) * (term * typ))) list
-    (*constant name ~> ((locale term,
-        (constant constraint, instantiaton index of class typ)), locale term & typ for uncheck)*)
+  operations: (string * (term * (typ * int))) list,
+    (*constant name ~> (locale term,
+        (constant constraint, instantiaton index of class typ))*)
+  unchecks: (term * term) list
 };
 
 fun rep_class_data (ClassData d) = d;
 fun mk_class_data ((consts, base_sort, inst, morphism, intro),
-    (defs, operations)) =
+    (defs, (operations, unchecks))) =
   ClassData { consts = consts, base_sort = base_sort, inst = inst,
     morphism = morphism, intro = intro, defs = defs,
-    operations = operations };
+    operations = operations, unchecks = unchecks };
 fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
-    defs, operations }) =
+    defs, operations, unchecks }) =
   mk_class_data (f ((consts, base_sort, inst, morphism, intro),
-    (defs, operations)));
+    (defs, (operations, unchecks))));
 fun merge_class_data _ (ClassData { consts = consts,
     base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
-    defs = defs1, operations = operations1 },
+    defs = defs1, operations = operations1, unchecks = unchecks1 },
   ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
-    defs = defs2, operations = operations2 }) =
+    defs = defs2, operations = operations2, unchecks = unchecks2 }) =
   mk_class_data ((consts, base_sort, inst, morphism, intro),
     (Thm.merge_thms (defs1, defs2),
-      AList.merge (op =) (K true) (operations1, operations2)));
+      (AList.merge (op =) (K true) (operations1, operations2),
+        Library.merge (op aconv o pairself snd) (unchecks1, unchecks2))));
 
 structure ClassData = TheoryDataFun
 (
   type T = class_data Graph.T
   val empty = Graph.empty;

     (ClassData.get thy) [];
 
 fun these_operations thy =
   maps (#operations o the_class_data thy) o ancestry thy;
 
-fun local_operation thy = AList.lookup (op =) o these_operations thy;
+fun these_unchecks thy =
+  maps (#unchecks o the_class_data thy) o ancestry thy;
 
 fun sups_base_sort thy sort =
   let
     val sups = filter (is_class thy) sort
       |> Sign.minimize_sort thy;

 
 (* updaters *)
 
 fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
   let
-    val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
-      (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
+    val operations = map (fn (v_ty, (c, ty)) =>
+      (c, ((Free v_ty, (Logic.varifyT ty, 0))))) cs;
+    val unchecks = map (fn ((v, ty'), (c, _)) =>
+      (Free (v, Type.strip_sorts ty'), Const (c, Type.strip_sorts ty'))) cs;
     val cs = (map o pairself) fst cs;
     val add_class = Graph.new_node (class,
-        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
+        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], (operations, unchecks))))
       #> fold (curry Graph.add_edge class) superclasses;
   in
     ClassData.map add_class thy
   end;
 
-fun register_operation class ((c, (t, t_rev)), some_def) thy =
+fun register_operation class (c, ((t, some_t_rev), some_def)) thy =
   let
     val ty = Sign.the_const_constraint thy c;
     val typargs = Sign.const_typargs thy (c, ty);
     val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
-    val t_rev' = (map_types o map_atyps)
-      (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, []) else ty | ty => ty) t_rev;
-    val ty' = Term.fastype_of t_rev';
+    fun mk_uncheck t_rev =
+      let
+        val t_rev' = map_types Type.strip_sorts t_rev;
+        val ty' = Term.fastype_of t_rev';
+      in (t_rev', Const (c, ty')) end;
+    val some_t_rev' = Option.map mk_uncheck some_t_rev;
   in
     thy
     |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
-      (fn (defs, operations) =>
+      (fn (defs, (operations, unchecks)) =>
         (fold cons (the_list some_def) defs,
-          (c, ((t, (ty, typidx)), (t_rev', ty'))) :: operations))
+          ((c, (t, (ty, typidx))) :: operations, fold cons (the_list some_t_rev') unchecks)))
   end;
 
 
 (** rule calculation, tactics and methods **)
 

  [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
     "back-chain introduction rules of classes"),
   ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
     "apply some intro/elim rule")]);
 
+fun subclass_rule thy (sub, sup) =
+  let
+    val ctxt = Locale.init sub thy;
+    val ctxt_thy = ProofContext.init thy;
+    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)
+    |> ClassData.map (Graph.add_edge (sub, 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;
+
 
 (** classes and class target **)
 
 (* class context syntax *)
 
 structure ClassSyntax = ProofDataFun(
   type T = {
     constraints: (string * typ) list,
     base_sort: sort,
     local_operation: string * typ -> (typ * term) option,
-    rews: (term * term) list,
+    unchecks: (term * term) list,
     passed: bool
   } option;
   fun init _ = NONE;
 );
 
 fun synchronize_syntax thy sups base_sort ctxt =
   let
+    (* constraints *)
     val operations = these_operations thy sups;
-
-    (* constraints *)
-    fun local_constraint (c, ((_, (ty, _)),_ )) =
+    fun local_constraint (c, (_, (ty, _))) =
       let
         val ty' = ty
           |> map_atyps (fn ty as TVar ((v, 0), _) =>
                if v = Name.aT then TVar ((v, 0), base_sort) else ty)
           |> SOME;
       in (c, ty') end
-    val constraints = (map o apsnd) (fst o snd o fst) operations;
+    val constraints = (map o apsnd) (fst o snd) operations;
 
     (* check phase *)
     val typargs = Consts.typargs (ProofContext.consts_of ctxt);
-    fun check_const (c, ty) ((t, (_, idx)), _) =
+    fun check_const (c, ty) (t, (_, idx)) =
       ((nth (typargs (c, ty)) idx), t);
     fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
       |> Option.map (check_const c_ty);
 
     (* uncheck phase *)
-    val rews = map (fn (c, (_, (t, ty))) => (t, Const (c, ty))) operations;
+    val basify =
+      map_atyps (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, base_sort)
+        else ty | ty => ty);
+    val unchecks = these_unchecks thy sups
+      |> (map o pairself o map_types) basify;
   in
     ctxt
     |> fold (ProofContext.add_const_constraint o local_constraint) operations
     |> ClassSyntax.map (K (SOME {
         constraints = constraints,
         base_sort = base_sort,
         local_operation = local_operation,
-        rews = rews,
+        unchecks = unchecks,
         passed = false
       }))
   end;
 
 fun refresh_syntax class ctxt =

     val thy = ProofContext.theory_of ctxt;
     val base_sort = (#base_sort o the_class_data thy) class;
   in synchronize_syntax thy [class] base_sort ctxt end;
 
 val mark_passed = (ClassSyntax.map o Option.map)
-  (fn { constraints, base_sort, local_operation, rews, passed } =>
+  (fn { constraints, base_sort, local_operation, unchecks, passed } =>
     { constraints = constraints, base_sort = base_sort,
-      local_operation = local_operation, rews = rews, passed = true });
+      local_operation = local_operation, unchecks = unchecks, passed = true });
 
 fun sort_term_check ts ctxt =
   let
     val { constraints, base_sort, local_operation, passed, ... } =
       the (ClassSyntax.get ctxt);

 
 fun sort_term_uncheck ts ctxt =
   let
     (*FIXME abbreviations*)
     val thy = ProofContext.theory_of ctxt;
-    val rews = (#rews o the o ClassSyntax.get) ctxt;
+    val unchecks = (#unchecks o the o ClassSyntax.get) ctxt;
     val ts' = if ! uncheck
-      then map (Pattern.rewrite_term thy rews []) ts else ts;
+      then map (Pattern.rewrite_term thy unchecks []) ts else ts;
   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
 
 fun init_ctxt thy sups base_sort ctxt =
   ctxt
   |> Variable.declare_term

 fun add_logical_const class pos ((c, mx), dict) thy =
   let
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
     val phi = morphism thy' class;
+    val base_sort = (#base_sort o the_class_data thy) class;
 
     val c' = Sign.full_name thy' c;
     val dict' = (map_types Logic.unvarifyT o Morphism.term phi) dict;
     val ty' = Term.fastype_of dict';
     val ty'' = Type.strip_sorts ty';

     |> Sign.hide_consts_i false [c''] (*FIXME*)
     |> Sign.declare_const pos (c, ty'', mx) |> snd
     |> Thm.add_def false (c, def_eq)
     |>> Thm.symmetric
     |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
-          #> register_operation class ((c', (dict, dict')), SOME (Thm.varifyT def)))
+          #> register_operation class (c', ((dict, SOME dict'), SOME (Thm.varifyT def))))
     |> Sign.restore_naming thy
     |> Sign.add_const_constraint (c', SOME ty')
   end;
 
 

     val phi = morphism thy class;
 
     val c' = Sign.full_name thy' c;
     val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
     val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
-    val rhs'' = map_types Logic.unvarifyT rhs';
-    val ty' = Term.fastype_of rhs'';
+    val ty' = (Logic.unvarifyT o Term.fastype_of) rhs';
 
     val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
     val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
   in
     thy'
     |> Sign.add_const_constraint (c'', SOME ty'') (*FIXME*)
     |> Sign.hide_consts_i false [c''] (*FIXME*)
     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> register_operation class ((c', (rhs, rhs'')), NONE)
+    |> register_operation class (c', ((rhs, NONE), NONE))
     |> Sign.restore_naming thy
   end;
 
 end;