added proper subclass concept; improved class target
authorhaftmann
Mon Oct 08 22:03:21 2007 +0200 (2007-10-08)
changeset 2491495cda5dd58d5
parent 24913 eb6fd8f78d56
child 24915 fc90277c0dd7
added proper subclass concept; improved class target
src/HOL/Dense_Linear_Order.thy
src/HOL/ex/Classpackage.thy
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/class.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/subclass.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Mon Oct 08 20:20:13 2007 +0200
     1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Mon Oct 08 22:03:21 2007 +0200
     1.3 @@ -404,18 +404,12 @@
     1.4    fixes between
     1.5    assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y"
     1.6       and  between_same: "between x x = x"
     1.7 +begin
     1.8  
     1.9 -instance advanced constr_dense_linear_order < dense_linear_order
    1.10 +subclass dense_linear_order
    1.11    apply unfold_locales
    1.12    using gt_ex lt_ex between_less
    1.13      by (auto, rule_tac x="between x y" in exI, simp)
    1.14 -(*FIXME*)
    1.15 -lemmas gt_ex = dense_linear_order_class.less_eq_less.gt_ex
    1.16 -lemmas lt_ex = dense_linear_order_class.less_eq_less.lt_ex
    1.17 -lemmas dense = dense_linear_order_class.less_eq_less.dense
    1.18 -
    1.19 -context constr_dense_linear_order
    1.20 -begin
    1.21  
    1.22  lemma rinf_U:
    1.23    assumes fU: "finite U"
     2.1 --- a/src/HOL/ex/Classpackage.thy	Mon Oct 08 20:20:13 2007 +0200
     2.2 +++ b/src/HOL/ex/Classpackage.thy	Mon Oct 08 22:03:21 2007 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Test and examples for Isar class package *}
     2.5  
     2.6  theory Classpackage
     2.7 -imports Main
     2.8 +imports List
     2.9  begin
    2.10  
    2.11  class semigroup = type +
    2.12 @@ -192,14 +192,18 @@
    2.13    thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
    2.14  qed
    2.15  
    2.16 -lemma neutr:
    2.17 -  "x \<^loc>\<otimes> \<^loc>\<one> = x"
    2.18 -proof -
    2.19 +subclass monoid
    2.20 +proof unfold_locales
    2.21 +  fix x
    2.22    from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
    2.23    with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
    2.24 -  with cancel show ?thesis by simp
    2.25 +  with cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
    2.26  qed
    2.27  
    2.28 +end context group begin
    2.29 +
    2.30 +find_theorems name: neut
    2.31 +
    2.32  lemma invr:
    2.33    "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
    2.34  proof -
    2.35 @@ -209,27 +213,6 @@
    2.36    with cancel show ?thesis ..
    2.37  qed
    2.38  
    2.39 -end
    2.40 -
    2.41 -instance advanced group < monoid
    2.42 -proof unfold_locales
    2.43 -  fix x
    2.44 -  from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
    2.45 -qed
    2.46 -
    2.47 -hide const npow (*FIXME*)
    2.48 -lemmas neutr = monoid_class.mult_one.neutr
    2.49 -lemmas inv_obtain = monoid_class.inv_obtain
    2.50 -lemmas inv_unique = monoid_class.inv_unique
    2.51 -lemmas nat_pow_mult = monoid_class.nat_pow_mult
    2.52 -lemmas nat_pow_one = monoid_class.nat_pow_one
    2.53 -lemmas nat_pow_pow = monoid_class.nat_pow_pow
    2.54 -lemmas units_def = monoid_class.units_def
    2.55 -lemmas mult_one_def = monoid_class.units_inv_comm
    2.56 -
    2.57 -context group
    2.58 -begin
    2.59 -
    2.60  lemma all_inv [intro]:
    2.61    "(x\<Colon>'a) \<in> units"
    2.62    unfolding units_def
    2.63 @@ -290,15 +273,6 @@
    2.64    "pow k x = (if k < 0 then \<^loc>\<div> (npow (nat (-k)) x)
    2.65      else (npow (nat k) x))"
    2.66  
    2.67 -end
    2.68 -
    2.69 -(*FIXME*)
    2.70 -thm (no_abbrevs) pow_def
    2.71 -thm (no_abbrevs) pow_def [folded monoid_class.npow]
    2.72 -lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
    2.73 -
    2.74 -context group begin
    2.75 -
    2.76  abbreviation
    2.77    pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>\<up>" 75)
    2.78  where
    2.79 @@ -340,7 +314,7 @@
    2.80  definition "x2 = X (1::int) 2 3"
    2.81  definition "y2 = Y (1::int) 2 3"
    2.82  
    2.83 -export_code mult x1 x2 y2 in SML module_name Classpackage
    2.84 +export_code x1 x2 y2 pow in SML module_name Classpackage
    2.85    in OCaml file -
    2.86    in Haskell file -
    2.87  
     3.1 --- a/src/Pure/IsaMakefile	Mon Oct 08 20:20:13 2007 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Mon Oct 08 22:03:21 2007 +0200
     3.3 @@ -43,7 +43,7 @@
     3.4    Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML			\
     3.5    Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML			\
     3.6    Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML				\
     3.7 -  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML			\
     3.8 +  Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML Isar/toplevel.ML	\
     3.9    ML-Systems/alice.ML ML-Systems/exn.ML						\
    3.10    ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML		\
    3.11    ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML			\
     4.1 --- a/src/Pure/Isar/ROOT.ML	Mon Oct 08 20:20:13 2007 +0200
     4.2 +++ b/src/Pure/Isar/ROOT.ML	Mon Oct 08 22:03:21 2007 +0200
     4.3 @@ -58,6 +58,7 @@
     4.4  use "instance.ML";
     4.5  use "spec_parse.ML";
     4.6  use "specification.ML";
     4.7 +use "subclass.ML"; (*FIXME improve structure*)
     4.8  use "constdefs.ML";
     4.9  
    4.10  (*toplevel environment*)
     5.1 --- a/src/Pure/Isar/class.ML	Mon Oct 08 20:20:13 2007 +0200
     5.2 +++ b/src/Pure/Isar/class.ML	Mon Oct 08 22:03:21 2007 +0200
     5.3 @@ -13,18 +13,22 @@
     5.4      -> ((bstring * Attrib.src list) * string list) list
     5.5      -> theory -> class * theory
     5.6    val classrel_cmd: xstring * xstring -> theory -> Proof.state
     5.7 +
     5.8    val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     5.9      -> string list -> theory -> string * Proof.context
    5.10    val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
    5.11      -> xstring list -> theory -> string * Proof.context
    5.12 +  val init: class -> Proof.context -> Proof.context;
    5.13    val add_const_in_class: string -> (string * term) * Syntax.mixfix
    5.14 -    -> theory -> theory
    5.15 -  val interpretation_in_class: class * class -> theory -> Proof.state
    5.16 -  val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state
    5.17 -  val prove_interpretation_in_class: tactic -> class * class -> theory -> theory
    5.18 +    -> theory -> string * theory
    5.19 +  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    5.20 +    -> theory -> string * theory
    5.21 +  val remove_constraint: sort -> string -> Proof.context -> Proof.context
    5.22    val intro_classes_tac: thm list -> tactic
    5.23    val default_intro_classes_tac: thm list -> tactic
    5.24    val class_of_locale: theory -> string -> class option
    5.25 +  val locale_of_class: theory -> class -> string
    5.26 +  val local_syntax: theory -> class -> bool
    5.27    val print_classes: theory -> unit
    5.28  
    5.29    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    5.30 @@ -44,11 +48,6 @@
    5.31    val inst_const: theory -> string * string -> string
    5.32    val param_const: theory -> string -> (string * string) option
    5.33    val params_of_sort: theory -> sort -> (string * (string * typ)) list
    5.34 -
    5.35 -  val init: class -> Proof.context -> Proof.context;
    5.36 -  val local_syntax: theory -> class -> bool
    5.37 -  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    5.38 -    -> theory -> theory
    5.39  end;
    5.40  
    5.41  structure Class : CLASS =
    5.42 @@ -70,13 +69,6 @@
    5.43        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    5.44    #> ProofContext.theory_of;
    5.45  
    5.46 -fun prove_interpretation_in tac after_qed (name, expr) =
    5.47 -  Locale.interpretation_in_locale
    5.48 -      (ProofContext.theory after_qed) (name, expr)
    5.49 -  #> Proof.global_terminal_proof
    5.50 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    5.51 -  #> ProofContext.theory_of;
    5.52 -
    5.53  fun OF_LAST thm1 thm2 =
    5.54    let
    5.55      val n = (length o Logic.strip_imp_prems o prop_of) thm2;
    5.56 @@ -331,22 +323,30 @@
    5.57    intro: thm,
    5.58    local_syntax: bool,
    5.59    defs: thm list,
    5.60 -  operations: (string * (term * int) option) list
    5.61 +  operations: (string * (term * int) option) list,
    5.62      (*constant name ~> (locale term, instantiaton index of class typ)*)
    5.63 +  constraints: (string * typ) list
    5.64  };
    5.65  
    5.66  fun rep_class_data (ClassData d) = d;
    5.67 -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) =
    5.68 -  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
    5.69 -    local_syntax = local_syntax, defs = defs, operations = operations };
    5.70 -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) =
    5.71 -  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)))
    5.72 -fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    5.73 -    intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 },
    5.74 +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    5.75 +    (defs, (operations, constraints))) =
    5.76 +  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    5.77 +    intro = intro, local_syntax = local_syntax, defs = defs, operations = operations,
    5.78 +    constraints = constraints };
    5.79 +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro,
    5.80 +    local_syntax, defs, operations, constraints }) =
    5.81 +  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax),
    5.82 +    (defs, (operations, constraints))));
    5.83 +fun merge_class_data _ (ClassData { locale = locale, consts = consts,
    5.84 +    local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax,
    5.85 +    defs = defs1, operations = operations1, constraints = constraints1 },
    5.86    ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
    5.87 -    defs = defs2, operations = operations2 }) =
    5.88 +    defs = defs2, operations = operations2, constraints = constraints2 }) =
    5.89    mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    5.90 -    (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2)));
    5.91 +    (Thm.merge_thms (defs1, defs2),
    5.92 +      (AList.merge (op =) (K true) (operations1, operations2),
    5.93 +      AList.merge (op =) (K true) (constraints1, constraints2))));
    5.94  
    5.95  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
    5.96  
    5.97 @@ -371,6 +371,8 @@
    5.98   of NONE => error ("undeclared class " ^ quote class)
    5.99    | SOME data => data;
   5.100  
   5.101 +val locale_of_class = #locale oo the_class_data;
   5.102 +
   5.103  val ancestry = Graph.all_succs o fst o ClassData.get;
   5.104  
   5.105  fun params_of_sort thy =
   5.106 @@ -393,6 +395,9 @@
   5.107  fun these_operations thy =
   5.108    maps (#operations o the_class_data thy) o ancestry thy;
   5.109  
   5.110 +fun these_constraints thy =
   5.111 +  maps (#constraints o the_class_data thy) o ancestry thy;
   5.112 +
   5.113  fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
   5.114  
   5.115  fun sups_local_sort thy sort =
   5.116 @@ -444,8 +449,9 @@
   5.117  fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   5.118    ClassData.map (fn (gr, tab) => (
   5.119      gr
   5.120 -    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
   5.121 -         intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts)))
   5.122 +    |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts,
   5.123 +        local_sort, inst, intro, local_syntax),
   5.124 +          ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts))))
   5.125      |> fold (curry Graph.add_edge class) superclasses,
   5.126      tab
   5.127      |> Symtab.update (locale, class)
   5.128 @@ -453,11 +459,12 @@
   5.129  
   5.130  fun register_const class (entry, def) =
   5.131    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   5.132 -    (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations));
   5.133 +    (fn (defs, (operations, constraints)) =>
   5.134 +      (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints)));
   5.135  
   5.136 -fun register_abbrev class abbrev =
   5.137 +fun register_abbrev class (abbrev, ty) =
   5.138    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd)
   5.139 -    (cons (abbrev, NONE));
   5.140 +    (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints));
   5.141  
   5.142  
   5.143  (** rule calculation, tactics and methods **)
   5.144 @@ -553,28 +560,21 @@
   5.145  
   5.146  (* class context initialization *)
   5.147  
   5.148 -fun get_remove_constraints sups local_sort ctxt =
   5.149 +fun remove_constraint local_sort c ctxt =
   5.150 +  let
   5.151 +    val ty = ProofContext.the_const_constraint ctxt c;
   5.152 +    val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
   5.153 +      then TFree (v, local_sort) else ty | ty => ty) ty;
   5.154 +  in
   5.155 +    ctxt
   5.156 +    |> ProofContext.add_const_constraint (c, SOME ty')
   5.157 +  end;
   5.158 +
   5.159 +fun sort_term_check sups local_sort ts ctxt =
   5.160    let
   5.161      val thy = ProofContext.theory_of ctxt;
   5.162 -    val operations = these_operations thy sups;
   5.163 -    fun get_remove (c, _) ctxt =
   5.164 -      let
   5.165 -        val ty = ProofContext.the_const_constraint ctxt c;
   5.166 -        val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
   5.167 -          then TFree (v, local_sort) else ty | ty => ty) ty;
   5.168 -      in
   5.169 -        ctxt
   5.170 -        |> ProofContext.add_const_constraint (c, SOME ty')
   5.171 -        |> pair (c, ty)
   5.172 -      end;
   5.173 -  in
   5.174 -    ctxt
   5.175 -    |> fold_map get_remove operations
   5.176 -  end;
   5.177 -
   5.178 -fun sort_term_check thy sups local_sort constraints ts ctxt =
   5.179 -  let
   5.180      val local_operation = local_operation thy sups;
   5.181 +    val constraints = these_constraints thy sups;
   5.182      val consts = ProofContext.consts_of ctxt;
   5.183      fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
   5.184       of TFree (v, _) => if v = Name.aT
   5.185 @@ -595,20 +595,22 @@
   5.186      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   5.187    in (ts', ctxt') end;
   5.188  
   5.189 -fun init_class_ctxt thy sups local_sort ctxt =
   5.190 -  ctxt
   5.191 -  |> Variable.declare_term
   5.192 -      (Logic.mk_type (TFree (Name.aT, local_sort)))
   5.193 -  |> get_remove_constraints sups local_sort
   5.194 -  |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
   5.195 -        (sort_term_check thy sups local_sort constraints)));
   5.196 +fun init_class_ctxt sups local_sort ctxt =
   5.197 +  let
   5.198 +    val operations = these_operations (ProofContext.theory_of ctxt) sups;
   5.199 +  in
   5.200 +    ctxt
   5.201 +    |> Variable.declare_term
   5.202 +        (Logic.mk_type (TFree (Name.aT, local_sort)))
   5.203 +    |> fold (remove_constraint local_sort o fst) operations
   5.204 +    |> Context.proof_map (Syntax.add_term_check 50 "class"
   5.205 +        (sort_term_check sups local_sort))
   5.206 +  end;
   5.207  
   5.208  fun init class ctxt =
   5.209 -  let
   5.210 -    val thy = ProofContext.theory_of ctxt;
   5.211 -    val local_sort = (#local_sort o the_class_data thy) class;
   5.212 -  in init_class_ctxt thy [class] local_sort ctxt end;
   5.213 -  
   5.214 +  init_class_ctxt [class]
   5.215 +    ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
   5.216 +
   5.217  
   5.218  (* class definition *)
   5.219  
   5.220 @@ -641,7 +643,7 @@
   5.221      ProofContext.init thy
   5.222      |> Locale.cert_expr supexpr [constrain]
   5.223      |> snd
   5.224 -    |> init_class_ctxt thy sups local_sort
   5.225 +    |> init_class_ctxt sups local_sort
   5.226      |> process_expr Locale.empty raw_elems
   5.227      |> fst
   5.228      |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
   5.229 @@ -706,7 +708,7 @@
   5.230          `(fn thy => class_intro thy name_locale name_axclass sups)
   5.231        #-> (fn class_intro =>
   5.232          add_class_data ((name_axclass, sups),
   5.233 -          (name_locale, map fst params ~~ map fst consts, local_sort,
   5.234 +          (name_locale, map fst params ~~ consts, local_sort,
   5.235              (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   5.236                (map snd supconsts @ consts)), class_intro, local_syntax))
   5.237        #> note_intro name_axclass class_intro
   5.238 @@ -736,9 +738,10 @@
   5.239  
   5.240  fun mk_operation_entry thy (c, rhs) =
   5.241    let
   5.242 -    val typargs = Sign.const_typargs thy (c, fastype_of rhs);
   5.243 +    val ty = fastype_of rhs;
   5.244 +    val typargs = Sign.const_typargs thy (c, ty);
   5.245      val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   5.246 -  in (c, (rhs, typidx)) end;
   5.247 +  in (c, (ty, (rhs, typidx))) end;
   5.248  
   5.249  fun add_const_in_class class ((c, rhs), syn) thy =
   5.250    let
   5.251 @@ -778,6 +781,7 @@
   5.252      |-> (fn [def] => interpret def)
   5.253      |> Sign.add_const_constraint (c', SOME ty'')
   5.254      |> Sign.restore_naming thy
   5.255 +    |> pair c'
   5.256    end;
   5.257  
   5.258  
   5.259 @@ -798,55 +802,8 @@
   5.260    in
   5.261      thy
   5.262      |> Sign.add_notation prmode [(Const (c', ty'), syn)]
   5.263 -    |> register_abbrev class c'
   5.264 +    |> register_abbrev class (c', ty')
   5.265 +    |> pair c'
   5.266    end;
   5.267  
   5.268 -
   5.269 -(* interpretation in class target *)
   5.270 -
   5.271 -local
   5.272 -
   5.273 -fun gen_interpretation_in_class prep_class do_proof (raw_class, raw_superclass) theory =
   5.274 -  let
   5.275 -    val class = prep_class theory raw_class;
   5.276 -    val superclass = prep_class theory raw_superclass;
   5.277 -    val loc_name = (#locale o the_class_data theory) class;
   5.278 -    val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
   5.279 -    fun prove_classrel (class, superclass) thy =
   5.280 -      let
   5.281 -        val classes = Sign.complete_sort thy [superclass]
   5.282 -          |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
   5.283 -        fun instance_subclass (class1, class2) thy  =
   5.284 -          let
   5.285 -            val interp = interpretation_in_rule thy (class1, class2);
   5.286 -            val ax = #axioms (AxClass.get_definition thy class1);
   5.287 -            val intro = #intro (AxClass.get_definition thy class2)
   5.288 -              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   5.289 -                  (TVar ((Name.aT, 0), [class1])))] [];
   5.290 -            val thm =
   5.291 -              intro
   5.292 -              |> OF_LAST (interp OF ax)
   5.293 -              |> strip_all_ofclass thy (Sign.super_classes thy class2);
   5.294 -          in
   5.295 -            thy |> AxClass.add_classrel thm
   5.296 -          end;
   5.297 -      in
   5.298 -        thy |> fold_rev (curry instance_subclass class) classes
   5.299 -      end;
   5.300 -  in
   5.301 -    theory
   5.302 -    |> do_proof (prove_classrel (class, superclass)) (loc_name, loc_expr)
   5.303 -  end;
   5.304 -
   5.305 -in
   5.306 -
   5.307 -val interpretation_in_class = gen_interpretation_in_class Sign.certify_class
   5.308 -  (Locale.interpretation_in_locale o ProofContext.theory);
   5.309 -val interpretation_in_class_cmd = gen_interpretation_in_class Sign.read_class
   5.310 -  (Locale.interpretation_in_locale o ProofContext.theory);
   5.311 -val prove_interpretation_in_class = gen_interpretation_in_class Sign.certify_class
   5.312 -  o prove_interpretation_in;
   5.313 -
   5.314 -end; (*local*)
   5.315 -
   5.316  end;
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Oct 08 20:20:13 2007 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Oct 08 22:03:21 2007 +0200
     6.3 @@ -435,10 +435,13 @@
     6.4            (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin)));
     6.5  
     6.6  val _ =
     6.7 +  OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal
     6.8 +    (P.opt_target -- P.xname >> (fn (loc, class) =>
     6.9 +      Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
    6.10 +
    6.11 +val _ =
    6.12    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    6.13    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    6.14 -    P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    6.15 -      >> Class.interpretation_in_class_cmd  || (* FIXME ?? *)
    6.16      P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    6.17        >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *))))
    6.18      >> (Toplevel.print oo Toplevel.theory_to_proof));
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Isar/subclass.ML	Mon Oct 08 22:03:21 2007 +0200
     7.3 @@ -0,0 +1,122 @@
     7.4 +(*  Title:      Pure/Isar/subclass.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Florian Haftmann, TU Muenchen
     7.7 +
     7.8 +Prove subclass relations between type classes
     7.9 +*)
    7.10 +
    7.11 +signature SUBCLASS =
    7.12 +sig
    7.13 +  val subclass: class -> local_theory -> Proof.state
    7.14 +  val subclass_cmd: xstring -> local_theory -> Proof.state
    7.15 +  (*FIXME val prove_subclass: tactic -> class * class -> theory -> theory*)
    7.16 +end;
    7.17 +
    7.18 +structure Subclass : SUBCLASS =
    7.19 +struct
    7.20 +
    7.21 +(** auxiliary **)
    7.22 +
    7.23 +fun prove_interpretation_in tac after_qed (name, expr) =
    7.24 +  Locale.interpretation_in_locale
    7.25 +      (ProofContext.theory after_qed) (name, expr)
    7.26 +  #> Proof.global_terminal_proof
    7.27 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    7.28 +  #> ProofContext.theory_of;
    7.29 +
    7.30 +fun OF_LAST thm1 thm2 =
    7.31 +  let
    7.32 +    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
    7.33 +  in (thm1 RSN (n, thm2)) end;
    7.34 +
    7.35 +fun strip_all_ofclass thy sort =
    7.36 +  let
    7.37 +    val typ = TVar ((Name.aT, 0), sort);
    7.38 +    fun prem_inclass t =
    7.39 +      case Logic.strip_imp_prems t
    7.40 +       of ofcls :: _ => try Logic.dest_inclass ofcls
    7.41 +        | [] => NONE;
    7.42 +    fun strip_ofclass class thm =
    7.43 +      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
    7.44 +    fun strip thm = case (prem_inclass o Thm.prop_of) thm
    7.45 +     of SOME (_, class) => thm |> strip_ofclass class |> strip
    7.46 +      | NONE => thm;
    7.47 +  in strip end;
    7.48 +
    7.49 +
    7.50 +(** subclassing **)
    7.51 +
    7.52 +local
    7.53 +
    7.54 +fun mk_subclass_rule lthy sup =
    7.55 +  let
    7.56 +    (*FIXME check for proper parameter inclusion (consts_of) (?)*)
    7.57 +    val ctxt = LocalTheory.target_of lthy;
    7.58 +    val thy = ProofContext.theory_of ctxt;
    7.59 +    val locale = Class.locale_of_class thy sup;
    7.60 +  in
    7.61 +    Locale.global_asms_of thy locale
    7.62 +    |> maps snd
    7.63 +    |> map (ObjectLogic.ensure_propT thy)
    7.64 +  end;
    7.65 +
    7.66 +fun gen_subclass prep_class raw_sup lthy =
    7.67 +  let
    7.68 +    (*FIXME cleanup, provide tactical interface*)
    7.69 +    val ctxt = LocalTheory.target_of lthy;
    7.70 +    val thy = ProofContext.theory_of ctxt;
    7.71 +    val ctxt_thy = ProofContext.init thy;
    7.72 +    val sup = prep_class thy raw_sup;
    7.73 +    val sub = case Option.mapPartial (Class.class_of_locale thy)
    7.74 +       (TheoryTarget.peek lthy)
    7.75 +     of NONE => error "not in class context"
    7.76 +      | SOME sub => sub;
    7.77 +    val export =
    7.78 +      Assumption.export false ctxt ctxt_thy
    7.79 +      #> singleton (Variable.export ctxt ctxt_thy);
    7.80 +    val loc_name = Class.locale_of_class thy sub;
    7.81 +    val loc_expr = Locale.Locale (Class.locale_of_class thy sup);
    7.82 +    fun prove_classrel interp thy =
    7.83 +      let
    7.84 +        val classes = Sign.complete_sort thy [sup]
    7.85 +          |> filter_out (fn class' => Sign.subsort thy ([sub], [class']));
    7.86 +        fun instance_subclass (class1, class2) thy  =
    7.87 +          let
    7.88 +            val ax = #axioms (AxClass.get_definition thy class1);
    7.89 +            val intro = #intro (AxClass.get_definition thy class2)
    7.90 +              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
    7.91 +                  (TVar ((Name.aT, 0), [class1])))] [];
    7.92 +            val thm =
    7.93 +              intro
    7.94 +              |> OF_LAST (interp OF ax)
    7.95 +              |> strip_all_ofclass thy (Sign.super_classes thy class2);
    7.96 +          in
    7.97 +            thy |> AxClass.add_classrel thm
    7.98 +          end;
    7.99 +      in
   7.100 +        thy |> fold_rev (curry instance_subclass sub) classes
   7.101 +      end;
   7.102 +    fun after_qed thmss =
   7.103 +      let
   7.104 +        val thm = Conjunction.intr_balanced (the_single thmss);;
   7.105 +        val interp = export thm;
   7.106 +      in
   7.107 +        LocalTheory.theory (prove_classrel interp
   7.108 +          #> prove_interpretation_in (ProofContext.fact_tac [thm] 1)
   7.109 +             I (loc_name, loc_expr))
   7.110 +        (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*)
   7.111 +      end;
   7.112 +    val goal = Element.Shows
   7.113 +      [(("", []), map (rpair []) (mk_subclass_rule lthy sup))];
   7.114 +  in 
   7.115 +    Specification.theorem_i Thm.internalK NONE after_qed ("", []) [] goal true lthy
   7.116 +  end;
   7.117 +
   7.118 +in
   7.119 +
   7.120 +val subclass = gen_subclass (K I);
   7.121 +val subclass_cmd = gen_subclass Sign.read_class;
   7.122 +
   7.123 +end; (*local*)
   7.124 +
   7.125 +end;
     8.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 08 20:20:13 2007 +0200
     8.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 08 22:03:21 2007 +0200
     8.3 @@ -118,9 +118,10 @@
     8.4          val mx3 = if is_loc then NoSyn else mx1;
     8.5          val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy;
     8.6        in (((c, mx2), t), thy') end;
     8.7 -
     8.8      fun const_class (SOME class) ((c, _), mx) (_, t) =
     8.9 -          Class.add_const_in_class class ((c, t), mx)
    8.10 +          LocalTheory.raw_theory_result
    8.11 +            (Class.add_const_in_class class ((c, t), mx))
    8.12 +          #-> (fn c => Class.remove_constraint [class] c)
    8.13        | const_class NONE _ _ = I;
    8.14      fun hide_abbrev (SOME class) abbrs thy =
    8.15            let
    8.16 @@ -137,13 +138,14 @@
    8.17              Sign.hide_consts_i true cs thy
    8.18            end
    8.19        | hide_abbrev NONE _ thy = thy;
    8.20 +
    8.21      val (abbrs, lthy') = lthy
    8.22        |> LocalTheory.theory_result (fold_map const decls)
    8.23      val defs = map (apsnd (pair ("", []))) abbrs;
    8.24  
    8.25    in
    8.26      lthy'
    8.27 -    |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
    8.28 +    |> fold2 (const_class some_class) decls abbrs
    8.29      |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs
    8.30      |> LocalTheory.raw_theory (hide_abbrev some_class abbrs)
    8.31          (*FIXME abbreviations should never occur*)
    8.32 @@ -184,17 +186,17 @@
    8.33      val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u;
    8.34      val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
    8.35      val mx3 = if is_loc then NoSyn else mx1;
    8.36 -    fun add_abbrev_in_class NONE = K I
    8.37 -      | add_abbrev_in_class (SOME class) =
    8.38 -          Class.add_abbrev_in_class class prmode;
    8.39 +    fun add_abbrev_in_class (SOME class) abbr =
    8.40 +          LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr)
    8.41 +          #-> (fn c => Class.remove_constraint [class] c)
    8.42 +      | add_abbrev_in_class NONE _ = I;
    8.43    in
    8.44      lthy
    8.45      |> LocalTheory.theory_result
    8.46          (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
    8.47      |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)])
    8.48      #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    8.49 -    #> LocalTheory.raw_theory
    8.50 -         (add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1))
    8.51 +    #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
    8.52      #> local_abbrev (c, rhs))
    8.53    end;
    8.54