src/Pure/Isar/class.ML
changeset 24914 95cda5dd58d5
parent 24901 d3cbf79769b9
child 24920 2a45e400fdad
--- a/src/Pure/Isar/class.ML	Mon Oct 08 20:20:13 2007 +0200
+++ b/src/Pure/Isar/class.ML	Mon Oct 08 22:03:21 2007 +0200
@@ -13,18 +13,22 @@
     -> ((bstring * Attrib.src list) * string list) list
     -> theory -> class * theory
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
+
   val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     -> string list -> theory -> string * Proof.context
   val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
     -> xstring list -> theory -> string * Proof.context
+  val init: class -> Proof.context -> Proof.context;
   val add_const_in_class: string -> (string * term) * Syntax.mixfix
-    -> theory -> theory
-  val interpretation_in_class: class * class -> theory -> Proof.state
-  val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state
-  val prove_interpretation_in_class: tactic -> class * class -> theory -> theory
+    -> theory -> string * theory
+  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
+    -> theory -> string * theory
+  val remove_constraint: sort -> string -> Proof.context -> Proof.context
   val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
   val class_of_locale: theory -> string -> class option
+  val locale_of_class: theory -> class -> string
+  val local_syntax: theory -> class -> bool
   val print_classes: theory -> unit
 
   val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
@@ -44,11 +48,6 @@
   val inst_const: theory -> string * string -> string
   val param_const: theory -> string -> (string * string) option
   val params_of_sort: theory -> sort -> (string * (string * typ)) list
-
-  val init: class -> Proof.context -> Proof.context;
-  val local_syntax: theory -> class -> bool
-  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
-    -> theory -> theory
 end;
 
 structure Class : CLASS =
@@ -70,13 +69,6 @@
       (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 =
   let
     val n = (length o Logic.strip_imp_prems o prop_of) thm2;
@@ -331,22 +323,30 @@
   intro: thm,
   local_syntax: bool,
   defs: thm list,
-  operations: (string * (term * int) option) list
+  operations: (string * (term * int) option) list,
     (*constant name ~> (locale term, instantiaton index of class typ)*)
+  constraints: (string * typ) list
 };
 
 fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) =
-  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
-    local_syntax = local_syntax, defs = defs, operations = operations };
-fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) =
-  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)))
-fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
-    intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 },
+fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
+    (defs, (operations, constraints))) =
+  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
+    intro = intro, local_syntax = local_syntax, defs = defs, operations = operations,
+    constraints = constraints };
+fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro,
+    local_syntax, defs, operations, constraints }) =
+  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax),
+    (defs, (operations, constraints))));
+fun merge_class_data _ (ClassData { locale = locale, consts = consts,
+    local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax,
+    defs = defs1, operations = operations1, constraints = constraints1 },
   ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
-    defs = defs2, operations = operations2 }) =
+    defs = defs2, operations = operations2, constraints = constraints2 }) =
   mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
-    (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2)));
+    (Thm.merge_thms (defs1, defs2),
+      (AList.merge (op =) (K true) (operations1, operations2),
+      AList.merge (op =) (K true) (constraints1, constraints2))));
 
 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
 
@@ -371,6 +371,8 @@
  of NONE => error ("undeclared class " ^ quote class)
   | SOME data => data;
 
+val locale_of_class = #locale oo the_class_data;
+
 val ancestry = Graph.all_succs o fst o ClassData.get;
 
 fun params_of_sort thy =
@@ -393,6 +395,9 @@
 fun these_operations thy =
   maps (#operations o the_class_data thy) o ancestry thy;
 
+fun these_constraints thy =
+  maps (#constraints o the_class_data thy) o ancestry thy;
+
 fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
 
 fun sups_local_sort thy sort =
@@ -444,8 +449,9 @@
 fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   ClassData.map (fn (gr, tab) => (
     gr
-    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
-         intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts)))
+    |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts,
+        local_sort, inst, intro, local_syntax),
+          ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts))))
     |> fold (curry Graph.add_edge class) superclasses,
     tab
     |> Symtab.update (locale, class)
@@ -453,11 +459,12 @@
 
 fun register_const class (entry, def) =
   (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
-    (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations));
+    (fn (defs, (operations, constraints)) =>
+      (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints)));
 
-fun register_abbrev class abbrev =
+fun register_abbrev class (abbrev, ty) =
   (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd)
-    (cons (abbrev, NONE));
+    (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints));
 
 
 (** rule calculation, tactics and methods **)
@@ -553,28 +560,21 @@
 
 (* class context initialization *)
 
-fun get_remove_constraints sups local_sort ctxt =
+fun remove_constraint local_sort c ctxt =
+  let
+    val ty = ProofContext.the_const_constraint ctxt c;
+    val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
+      then TFree (v, local_sort) else ty | ty => ty) ty;
+  in
+    ctxt
+    |> ProofContext.add_const_constraint (c, SOME ty')
+  end;
+
+fun sort_term_check sups local_sort ts ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val operations = these_operations thy sups;
-    fun get_remove (c, _) ctxt =
-      let
-        val ty = ProofContext.the_const_constraint ctxt c;
-        val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
-          then TFree (v, local_sort) else ty | ty => ty) ty;
-      in
-        ctxt
-        |> ProofContext.add_const_constraint (c, SOME ty')
-        |> pair (c, ty)
-      end;
-  in
-    ctxt
-    |> fold_map get_remove operations
-  end;
-
-fun sort_term_check thy sups local_sort constraints ts ctxt =
-  let
     val local_operation = local_operation thy sups;
+    val constraints = these_constraints thy sups;
     val consts = ProofContext.consts_of ctxt;
     fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
      of TFree (v, _) => if v = Name.aT
@@ -595,20 +595,22 @@
     val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   in (ts', ctxt') end;
 
-fun init_class_ctxt thy sups local_sort ctxt =
-  ctxt
-  |> Variable.declare_term
-      (Logic.mk_type (TFree (Name.aT, local_sort)))
-  |> get_remove_constraints sups local_sort
-  |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
-        (sort_term_check thy sups local_sort constraints)));
+fun init_class_ctxt sups local_sort ctxt =
+  let
+    val operations = these_operations (ProofContext.theory_of ctxt) sups;
+  in
+    ctxt
+    |> Variable.declare_term
+        (Logic.mk_type (TFree (Name.aT, local_sort)))
+    |> fold (remove_constraint local_sort o fst) operations
+    |> Context.proof_map (Syntax.add_term_check 50 "class"
+        (sort_term_check sups local_sort))
+  end;
 
 fun init class ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val local_sort = (#local_sort o the_class_data thy) class;
-  in init_class_ctxt thy [class] local_sort ctxt end;
-  
+  init_class_ctxt [class]
+    ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
+
 
 (* class definition *)
 
@@ -641,7 +643,7 @@
     ProofContext.init thy
     |> Locale.cert_expr supexpr [constrain]
     |> snd
-    |> init_class_ctxt thy sups local_sort
+    |> init_class_ctxt sups local_sort
     |> process_expr Locale.empty raw_elems
     |> fst
     |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
@@ -706,7 +708,7 @@
         `(fn thy => class_intro thy name_locale name_axclass sups)
       #-> (fn class_intro =>
         add_class_data ((name_axclass, sups),
-          (name_locale, map fst params ~~ map fst consts, local_sort,
+          (name_locale, map fst params ~~ consts, local_sort,
             (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
               (map snd supconsts @ consts)), class_intro, local_syntax))
       #> note_intro name_axclass class_intro
@@ -736,9 +738,10 @@
 
 fun mk_operation_entry thy (c, rhs) =
   let
-    val typargs = Sign.const_typargs thy (c, fastype_of rhs);
+    val ty = fastype_of rhs;
+    val typargs = Sign.const_typargs thy (c, ty);
     val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
-  in (c, (rhs, typidx)) end;
+  in (c, (ty, (rhs, typidx))) end;
 
 fun add_const_in_class class ((c, rhs), syn) thy =
   let
@@ -778,6 +781,7 @@
     |-> (fn [def] => interpret def)
     |> Sign.add_const_constraint (c', SOME ty'')
     |> Sign.restore_naming thy
+    |> pair c'
   end;
 
 
@@ -798,55 +802,8 @@
   in
     thy
     |> Sign.add_notation prmode [(Const (c', ty'), syn)]
-    |> register_abbrev class c'
+    |> register_abbrev class (c', ty')
+    |> pair c'
   end;
 
-
-(* interpretation in class target *)
-
-local
-
-fun gen_interpretation_in_class prep_class do_proof (raw_class, raw_superclass) theory =
-  let
-    val class = prep_class theory raw_class;
-    val superclass = prep_class theory raw_superclass;
-    val loc_name = (#locale o the_class_data theory) class;
-    val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
-    fun prove_classrel (class, superclass) thy =
-      let
-        val classes = Sign.complete_sort thy [superclass]
-          |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
-        fun instance_subclass (class1, class2) thy  =
-          let
-            val interp = interpretation_in_rule thy (class1, class2);
-            val ax = #axioms (AxClass.get_definition thy class1);
-            val intro = #intro (AxClass.get_definition thy class2)
-              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
-                  (TVar ((Name.aT, 0), [class1])))] [];
-            val thm =
-              intro
-              |> OF_LAST (interp OF ax)
-              |> strip_all_ofclass thy (Sign.super_classes thy class2);
-          in
-            thy |> AxClass.add_classrel thm
-          end;
-      in
-        thy |> fold_rev (curry instance_subclass class) classes
-      end;
-  in
-    theory
-    |> do_proof (prove_classrel (class, superclass)) (loc_name, loc_expr)
-  end;
-
-in
-
-val interpretation_in_class = gen_interpretation_in_class Sign.certify_class
-  (Locale.interpretation_in_locale o ProofContext.theory);
-val interpretation_in_class_cmd = gen_interpretation_in_class Sign.read_class
-  (Locale.interpretation_in_locale o ProofContext.theory);
-val prove_interpretation_in_class = gen_interpretation_in_class Sign.certify_class
-  o prove_interpretation_in;
-
-end; (*local*)
-
 end;