src/Pure/Isar/class.ML
changeset 24914 95cda5dd58d5
parent 24901 d3cbf79769b9
child 24920 2a45e400fdad
     1.1 --- a/src/Pure/Isar/class.ML	Mon Oct 08 20:20:13 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Oct 08 22:03:21 2007 +0200
     1.3 @@ -13,18 +13,22 @@
     1.4      -> ((bstring * Attrib.src list) * string list) list
     1.5      -> theory -> class * theory
     1.6    val classrel_cmd: xstring * xstring -> theory -> Proof.state
     1.7 +
     1.8    val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     1.9      -> string list -> theory -> string * Proof.context
    1.10    val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
    1.11      -> xstring list -> theory -> string * Proof.context
    1.12 +  val init: class -> Proof.context -> Proof.context;
    1.13    val add_const_in_class: string -> (string * term) * Syntax.mixfix
    1.14 -    -> theory -> theory
    1.15 -  val interpretation_in_class: class * class -> theory -> Proof.state
    1.16 -  val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state
    1.17 -  val prove_interpretation_in_class: tactic -> class * class -> theory -> theory
    1.18 +    -> theory -> string * theory
    1.19 +  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    1.20 +    -> theory -> string * theory
    1.21 +  val remove_constraint: sort -> string -> Proof.context -> Proof.context
    1.22    val intro_classes_tac: thm list -> tactic
    1.23    val default_intro_classes_tac: thm list -> tactic
    1.24    val class_of_locale: theory -> string -> class option
    1.25 +  val locale_of_class: theory -> class -> string
    1.26 +  val local_syntax: theory -> class -> bool
    1.27    val print_classes: theory -> unit
    1.28  
    1.29    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    1.30 @@ -44,11 +48,6 @@
    1.31    val inst_const: theory -> string * string -> string
    1.32    val param_const: theory -> string -> (string * string) option
    1.33    val params_of_sort: theory -> sort -> (string * (string * typ)) list
    1.34 -
    1.35 -  val init: class -> Proof.context -> Proof.context;
    1.36 -  val local_syntax: theory -> class -> bool
    1.37 -  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    1.38 -    -> theory -> theory
    1.39  end;
    1.40  
    1.41  structure Class : CLASS =
    1.42 @@ -70,13 +69,6 @@
    1.43        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.44    #> ProofContext.theory_of;
    1.45  
    1.46 -fun prove_interpretation_in tac after_qed (name, expr) =
    1.47 -  Locale.interpretation_in_locale
    1.48 -      (ProofContext.theory after_qed) (name, expr)
    1.49 -  #> Proof.global_terminal_proof
    1.50 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.51 -  #> ProofContext.theory_of;
    1.52 -
    1.53  fun OF_LAST thm1 thm2 =
    1.54    let
    1.55      val n = (length o Logic.strip_imp_prems o prop_of) thm2;
    1.56 @@ -331,22 +323,30 @@
    1.57    intro: thm,
    1.58    local_syntax: bool,
    1.59    defs: thm list,
    1.60 -  operations: (string * (term * int) option) list
    1.61 +  operations: (string * (term * int) option) list,
    1.62      (*constant name ~> (locale term, instantiaton index of class typ)*)
    1.63 +  constraints: (string * typ) list
    1.64  };
    1.65  
    1.66  fun rep_class_data (ClassData d) = d;
    1.67 -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) =
    1.68 -  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
    1.69 -    local_syntax = local_syntax, defs = defs, operations = operations };
    1.70 -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) =
    1.71 -  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)))
    1.72 -fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.73 -    intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 },
    1.74 +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.75 +    (defs, (operations, constraints))) =
    1.76 +  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.77 +    intro = intro, local_syntax = local_syntax, defs = defs, operations = operations,
    1.78 +    constraints = constraints };
    1.79 +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro,
    1.80 +    local_syntax, defs, operations, constraints }) =
    1.81 +  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax),
    1.82 +    (defs, (operations, constraints))));
    1.83 +fun merge_class_data _ (ClassData { locale = locale, consts = consts,
    1.84 +    local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax,
    1.85 +    defs = defs1, operations = operations1, constraints = constraints1 },
    1.86    ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
    1.87 -    defs = defs2, operations = operations2 }) =
    1.88 +    defs = defs2, operations = operations2, constraints = constraints2 }) =
    1.89    mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.90 -    (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2)));
    1.91 +    (Thm.merge_thms (defs1, defs2),
    1.92 +      (AList.merge (op =) (K true) (operations1, operations2),
    1.93 +      AList.merge (op =) (K true) (constraints1, constraints2))));
    1.94  
    1.95  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
    1.96  
    1.97 @@ -371,6 +371,8 @@
    1.98   of NONE => error ("undeclared class " ^ quote class)
    1.99    | SOME data => data;
   1.100  
   1.101 +val locale_of_class = #locale oo the_class_data;
   1.102 +
   1.103  val ancestry = Graph.all_succs o fst o ClassData.get;
   1.104  
   1.105  fun params_of_sort thy =
   1.106 @@ -393,6 +395,9 @@
   1.107  fun these_operations thy =
   1.108    maps (#operations o the_class_data thy) o ancestry thy;
   1.109  
   1.110 +fun these_constraints thy =
   1.111 +  maps (#constraints o the_class_data thy) o ancestry thy;
   1.112 +
   1.113  fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
   1.114  
   1.115  fun sups_local_sort thy sort =
   1.116 @@ -444,8 +449,9 @@
   1.117  fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   1.118    ClassData.map (fn (gr, tab) => (
   1.119      gr
   1.120 -    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
   1.121 -         intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts)))
   1.122 +    |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts,
   1.123 +        local_sort, inst, intro, local_syntax),
   1.124 +          ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts))))
   1.125      |> fold (curry Graph.add_edge class) superclasses,
   1.126      tab
   1.127      |> Symtab.update (locale, class)
   1.128 @@ -453,11 +459,12 @@
   1.129  
   1.130  fun register_const class (entry, def) =
   1.131    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   1.132 -    (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations));
   1.133 +    (fn (defs, (operations, constraints)) =>
   1.134 +      (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints)));
   1.135  
   1.136 -fun register_abbrev class abbrev =
   1.137 +fun register_abbrev class (abbrev, ty) =
   1.138    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd)
   1.139 -    (cons (abbrev, NONE));
   1.140 +    (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints));
   1.141  
   1.142  
   1.143  (** rule calculation, tactics and methods **)
   1.144 @@ -553,28 +560,21 @@
   1.145  
   1.146  (* class context initialization *)
   1.147  
   1.148 -fun get_remove_constraints sups local_sort ctxt =
   1.149 +fun remove_constraint local_sort c ctxt =
   1.150 +  let
   1.151 +    val ty = ProofContext.the_const_constraint ctxt c;
   1.152 +    val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
   1.153 +      then TFree (v, local_sort) else ty | ty => ty) ty;
   1.154 +  in
   1.155 +    ctxt
   1.156 +    |> ProofContext.add_const_constraint (c, SOME ty')
   1.157 +  end;
   1.158 +
   1.159 +fun sort_term_check sups local_sort ts ctxt =
   1.160    let
   1.161      val thy = ProofContext.theory_of ctxt;
   1.162 -    val operations = these_operations thy sups;
   1.163 -    fun get_remove (c, _) ctxt =
   1.164 -      let
   1.165 -        val ty = ProofContext.the_const_constraint ctxt c;
   1.166 -        val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
   1.167 -          then TFree (v, local_sort) else ty | ty => ty) ty;
   1.168 -      in
   1.169 -        ctxt
   1.170 -        |> ProofContext.add_const_constraint (c, SOME ty')
   1.171 -        |> pair (c, ty)
   1.172 -      end;
   1.173 -  in
   1.174 -    ctxt
   1.175 -    |> fold_map get_remove operations
   1.176 -  end;
   1.177 -
   1.178 -fun sort_term_check thy sups local_sort constraints ts ctxt =
   1.179 -  let
   1.180      val local_operation = local_operation thy sups;
   1.181 +    val constraints = these_constraints thy sups;
   1.182      val consts = ProofContext.consts_of ctxt;
   1.183      fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
   1.184       of TFree (v, _) => if v = Name.aT
   1.185 @@ -595,20 +595,22 @@
   1.186      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   1.187    in (ts', ctxt') end;
   1.188  
   1.189 -fun init_class_ctxt thy sups local_sort ctxt =
   1.190 -  ctxt
   1.191 -  |> Variable.declare_term
   1.192 -      (Logic.mk_type (TFree (Name.aT, local_sort)))
   1.193 -  |> get_remove_constraints sups local_sort
   1.194 -  |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
   1.195 -        (sort_term_check thy sups local_sort constraints)));
   1.196 +fun init_class_ctxt sups local_sort ctxt =
   1.197 +  let
   1.198 +    val operations = these_operations (ProofContext.theory_of ctxt) sups;
   1.199 +  in
   1.200 +    ctxt
   1.201 +    |> Variable.declare_term
   1.202 +        (Logic.mk_type (TFree (Name.aT, local_sort)))
   1.203 +    |> fold (remove_constraint local_sort o fst) operations
   1.204 +    |> Context.proof_map (Syntax.add_term_check 50 "class"
   1.205 +        (sort_term_check sups local_sort))
   1.206 +  end;
   1.207  
   1.208  fun init class ctxt =
   1.209 -  let
   1.210 -    val thy = ProofContext.theory_of ctxt;
   1.211 -    val local_sort = (#local_sort o the_class_data thy) class;
   1.212 -  in init_class_ctxt thy [class] local_sort ctxt end;
   1.213 -  
   1.214 +  init_class_ctxt [class]
   1.215 +    ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
   1.216 +
   1.217  
   1.218  (* class definition *)
   1.219  
   1.220 @@ -641,7 +643,7 @@
   1.221      ProofContext.init thy
   1.222      |> Locale.cert_expr supexpr [constrain]
   1.223      |> snd
   1.224 -    |> init_class_ctxt thy sups local_sort
   1.225 +    |> init_class_ctxt sups local_sort
   1.226      |> process_expr Locale.empty raw_elems
   1.227      |> fst
   1.228      |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
   1.229 @@ -706,7 +708,7 @@
   1.230          `(fn thy => class_intro thy name_locale name_axclass sups)
   1.231        #-> (fn class_intro =>
   1.232          add_class_data ((name_axclass, sups),
   1.233 -          (name_locale, map fst params ~~ map fst consts, local_sort,
   1.234 +          (name_locale, map fst params ~~ consts, local_sort,
   1.235              (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   1.236                (map snd supconsts @ consts)), class_intro, local_syntax))
   1.237        #> note_intro name_axclass class_intro
   1.238 @@ -736,9 +738,10 @@
   1.239  
   1.240  fun mk_operation_entry thy (c, rhs) =
   1.241    let
   1.242 -    val typargs = Sign.const_typargs thy (c, fastype_of rhs);
   1.243 +    val ty = fastype_of rhs;
   1.244 +    val typargs = Sign.const_typargs thy (c, ty);
   1.245      val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   1.246 -  in (c, (rhs, typidx)) end;
   1.247 +  in (c, (ty, (rhs, typidx))) end;
   1.248  
   1.249  fun add_const_in_class class ((c, rhs), syn) thy =
   1.250    let
   1.251 @@ -778,6 +781,7 @@
   1.252      |-> (fn [def] => interpret def)
   1.253      |> Sign.add_const_constraint (c', SOME ty'')
   1.254      |> Sign.restore_naming thy
   1.255 +    |> pair c'
   1.256    end;
   1.257  
   1.258  
   1.259 @@ -798,55 +802,8 @@
   1.260    in
   1.261      thy
   1.262      |> Sign.add_notation prmode [(Const (c', ty'), syn)]
   1.263 -    |> register_abbrev class c'
   1.264 +    |> register_abbrev class (c', ty')
   1.265 +    |> pair c'
   1.266    end;
   1.267  
   1.268 -
   1.269 -(* interpretation in class target *)
   1.270 -
   1.271 -local
   1.272 -
   1.273 -fun gen_interpretation_in_class prep_class do_proof (raw_class, raw_superclass) theory =
   1.274 -  let
   1.275 -    val class = prep_class theory raw_class;
   1.276 -    val superclass = prep_class theory raw_superclass;
   1.277 -    val loc_name = (#locale o the_class_data theory) class;
   1.278 -    val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
   1.279 -    fun prove_classrel (class, superclass) thy =
   1.280 -      let
   1.281 -        val classes = Sign.complete_sort thy [superclass]
   1.282 -          |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
   1.283 -        fun instance_subclass (class1, class2) thy  =
   1.284 -          let
   1.285 -            val interp = interpretation_in_rule thy (class1, class2);
   1.286 -            val ax = #axioms (AxClass.get_definition thy class1);
   1.287 -            val intro = #intro (AxClass.get_definition thy class2)
   1.288 -              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   1.289 -                  (TVar ((Name.aT, 0), [class1])))] [];
   1.290 -            val thm =
   1.291 -              intro
   1.292 -              |> OF_LAST (interp OF ax)
   1.293 -              |> strip_all_ofclass thy (Sign.super_classes thy class2);
   1.294 -          in
   1.295 -            thy |> AxClass.add_classrel thm
   1.296 -          end;
   1.297 -      in
   1.298 -        thy |> fold_rev (curry instance_subclass class) classes
   1.299 -      end;
   1.300 -  in
   1.301 -    theory
   1.302 -    |> do_proof (prove_classrel (class, superclass)) (loc_name, loc_expr)
   1.303 -  end;
   1.304 -
   1.305 -in
   1.306 -
   1.307 -val interpretation_in_class = gen_interpretation_in_class Sign.certify_class
   1.308 -  (Locale.interpretation_in_locale o ProofContext.theory);
   1.309 -val interpretation_in_class_cmd = gen_interpretation_in_class Sign.read_class
   1.310 -  (Locale.interpretation_in_locale o ProofContext.theory);
   1.311 -val prove_interpretation_in_class = gen_interpretation_in_class Sign.certify_class
   1.312 -  o prove_interpretation_in;
   1.313 -
   1.314 -end; (*local*)
   1.315 -
   1.316  end;