tuned
authorhaftmann
Fri Oct 12 14:42:30 2007 +0200 (2007-10-12)
changeset 25002c3d9cb390471
parent 25001 7982fe02a50e
child 25003 0b067b2d1b88
tuned
src/Pure/Isar/class.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/subclass.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 12 14:42:29 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 12 14:42:30 2007 +0200
     1.3 @@ -14,22 +14,23 @@
     1.4      -> theory -> class * theory
     1.5    val classrel_cmd: xstring * xstring -> theory -> Proof.state
     1.6  
     1.7 -  val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     1.8 +  val class: 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 +  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    1.12      -> xstring list -> theory -> string * Proof.context
    1.13    val init: class -> Proof.context -> Proof.context;
    1.14    val add_const_in_class: string -> (string * term) * Syntax.mixfix
    1.15      -> theory -> string * theory
    1.16    val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    1.17      -> theory -> string * theory
    1.18 -  val remove_constraint: sort -> string -> Proof.context -> Proof.context
    1.19 +  val remove_constraint: class -> string -> Proof.context -> Proof.context
    1.20 +  val class_of_locale: theory -> string -> class option
    1.21 +  val locale_of_class: theory -> class -> string
    1.22 +  val these_params: theory -> sort -> (string * (string * typ)) list
    1.23    val intro_classes_tac: thm list -> tactic
    1.24    val default_intro_classes_tac: thm list -> tactic
    1.25 -  val class_of_locale: theory -> string -> class option
    1.26 -  val locale_of_class: theory -> class -> string
    1.27 -  val local_syntax: theory -> class -> bool
    1.28    val print_classes: theory -> unit
    1.29 +  val uncheck: bool ref
    1.30  
    1.31    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    1.32    val instance: arity list -> ((bstring * Attrib.src list) * term) list
    1.33 @@ -47,7 +48,6 @@
    1.34    val unoverload_const: theory -> string * typ -> string
    1.35    val inst_const: theory -> string * string -> string
    1.36    val param_const: theory -> string -> (string * string) option
    1.37 -  val params_of_sort: theory -> sort -> (string * (string * typ)) list
    1.38  end;
    1.39  
    1.40  structure Class : CLASS =
    1.41 @@ -63,8 +63,8 @@
    1.42      val mx_local = if is_loc then mx else NoSyn;
    1.43    in (mx_global, mx_local) end;
    1.44  
    1.45 -fun prove_interpretation tac prfx_atts expr insts =
    1.46 -  Locale.interpretation_i I prfx_atts expr insts
    1.47 +fun prove_interpretation tac prfx_atts expr inst =
    1.48 +  Locale.interpretation_i I prfx_atts expr inst
    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 @@ -323,32 +323,32 @@
    1.53    inst: typ Symtab.table * term Symtab.table
    1.54      (*canonical interpretation*),
    1.55    intro: thm,
    1.56 -  local_syntax: bool,
    1.57    defs: thm list,
    1.58 -  operations: (string * (term * int) option) list,
    1.59 -    (*constant name ~> (locale term, instantiaton index of class typ)*)
    1.60 -  constraints: (string * typ) list
    1.61 +  operations: (string * (term * (typ * int))) list
    1.62 +    (*constant name ~> (locale term, (constant constraint, instantiaton index of class typ))*),
    1.63 +  operations_rev: (string * string) list
    1.64 +    (*locale operation ~> constant name*)
    1.65  };
    1.66  
    1.67  fun rep_class_data (ClassData d) = d;
    1.68 -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.69 -    (defs, (operations, constraints))) =
    1.70 +fun mk_class_data ((locale, consts, local_sort, inst, intro),
    1.71 +    (defs, operations, operations_rev)) =
    1.72    ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.73 -    intro = intro, local_syntax = local_syntax, defs = defs, operations = operations,
    1.74 -    constraints = constraints };
    1.75 +    intro = intro, defs = defs, operations = operations,
    1.76 +    operations_rev = operations_rev };
    1.77  fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro,
    1.78 -    local_syntax, defs, operations, constraints }) =
    1.79 -  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax),
    1.80 -    (defs, (operations, constraints))));
    1.81 +    defs, operations, operations_rev }) =
    1.82 +  mk_class_data (f ((locale, consts, local_sort, inst, intro),
    1.83 +    (defs, operations, operations_rev)));
    1.84  fun merge_class_data _ (ClassData { locale = locale, consts = consts,
    1.85 -    local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax,
    1.86 -    defs = defs1, operations = operations1, constraints = constraints1 },
    1.87 -  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
    1.88 -    defs = defs2, operations = operations2, constraints = constraints2 }) =
    1.89 -  mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.90 +    local_sort = local_sort, inst = inst, intro = intro,
    1.91 +    defs = defs1, operations = operations1, operations_rev = operations_rev1 },
    1.92 +  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _,
    1.93 +    defs = defs2, operations = operations2, operations_rev = operations_rev2 }) =
    1.94 +  mk_class_data ((locale, consts, local_sort, inst, intro),
    1.95      (Thm.merge_thms (defs1, defs2),
    1.96 -      (AList.merge (op =) (K true) (operations1, operations2),
    1.97 -      AList.merge (op =) (K true) (constraints1, constraints2))));
    1.98 +      AList.merge (op =) (K true) (operations1, operations2),
    1.99 +      AList.merge (op =) (K true) (operations_rev1, operations_rev2)));
   1.100  
   1.101  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   1.102  
   1.103 @@ -377,7 +377,7 @@
   1.104  
   1.105  val ancestry = Graph.all_succs o fst o ClassData.get;
   1.106  
   1.107 -fun params_of_sort thy =
   1.108 +fun these_params thy =
   1.109    let
   1.110      fun params class =
   1.111        let
   1.112 @@ -397,10 +397,12 @@
   1.113  fun these_operations thy =
   1.114    maps (#operations o the_class_data thy) o ancestry thy;
   1.115  
   1.116 -fun these_constraints thy =
   1.117 -  maps (#constraints o the_class_data thy) o ancestry thy;
   1.118 +fun these_operations_rev thy =
   1.119 +  maps (#operations_rev o the_class_data thy) o ancestry thy;
   1.120  
   1.121 -fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
   1.122 +fun local_operation thy = AList.lookup (op =) o these_operations thy;
   1.123 +
   1.124 +fun global_operation thy = AList.lookup (op =) o these_operations_rev thy;
   1.125  
   1.126  fun sups_local_sort thy sort =
   1.127    let
   1.128 @@ -411,8 +413,6 @@
   1.129        | [] => sort;
   1.130    in (sups, local_sort) end;
   1.131  
   1.132 -fun local_syntax thy = #local_syntax o the_class_data thy;
   1.133 -
   1.134  fun print_classes thy =
   1.135    let
   1.136      val ctxt = ProofContext.init thy;
   1.137 @@ -450,25 +450,24 @@
   1.138  
   1.139  (* updaters *)
   1.140  
   1.141 -fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   1.142 -  ClassData.map (fn (gr, tab) => (
   1.143 -    gr
   1.144 -    |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts,
   1.145 -        local_sort, inst, intro, local_syntax),
   1.146 -          ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts))))
   1.147 -    |> fold (curry Graph.add_edge class) superclasses,
   1.148 -    tab
   1.149 -    |> Symtab.update (locale, class)
   1.150 -  ));
   1.151 +fun add_class_data ((class, superclasses), (locale, cs, local_sort, inst, intro)) =
   1.152 +  let
   1.153 +    val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs;
   1.154 +    val cs = (map o pairself) fst cs;
   1.155 +    val add_class = Graph.new_node (class, mk_class_data ((locale,
   1.156 +          cs, local_sort, inst, intro),
   1.157 +            ([], operations, [])))
   1.158 +      #> fold (curry Graph.add_edge class) superclasses;
   1.159 +    val add_locale = Symtab.update (locale, class);
   1.160 +  in
   1.161 +    ClassData.map (fn (gr, tab) => (add_class gr, add_locale tab))
   1.162 +  end;
   1.163  
   1.164 -fun register_const class (entry, def) =
   1.165 +fun register_operation class (entry, some_def) =
   1.166    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   1.167 -    (fn (defs, (operations, constraints)) =>
   1.168 -      (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints)));
   1.169 -
   1.170 -fun register_abbrev class (abbrev, ty) =
   1.171 -  (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd)
   1.172 -    (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints));
   1.173 +    (fn (defs, operations, operations_rev) =>
   1.174 +      (case some_def of NONE => defs | SOME def => def :: defs,
   1.175 +        entry :: operations, (*FIXME*)operations_rev));
   1.176  
   1.177  
   1.178  (** rule calculation, tactics and methods **)
   1.179 @@ -559,23 +558,30 @@
   1.180  
   1.181  (** classes and class target **)
   1.182  
   1.183 -(* class context initialization *)
   1.184 +(* class context syntax *)
   1.185  
   1.186 -fun remove_constraint local_sort c ctxt =
   1.187 +fun internal_remove_constraint local_sort (c, (_, (ty, typidx))) ctxt =
   1.188    let
   1.189 -    val ty = ProofContext.the_const_constraint ctxt c;
   1.190 -    val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
   1.191 -      then TFree (v, local_sort) else ty | ty => ty) ty;
   1.192 +    val consts = ProofContext.consts_of ctxt;
   1.193 +    val typargs = Consts.typargs consts (c, ty);
   1.194 +    val typargs' = nth_map typidx (K (TVar ((Name.aT, 0), local_sort))) typargs;
   1.195 +    val ty' = Consts.instance consts (c, typargs');
   1.196 +  in ProofContext.add_const_constraint (c, SOME ty') ctxt end;
   1.197 +
   1.198 +fun remove_constraint class c ctxt =
   1.199 +  let
   1.200 +    val thy = ProofContext.theory_of ctxt;
   1.201 +    val SOME entry = local_operation thy [class] c;
   1.202    in
   1.203 -    ctxt
   1.204 -    |> ProofContext.add_const_constraint (c, SOME ty')
   1.205 +    internal_remove_constraint
   1.206 +      ((#local_sort o the_class_data thy) class) (c, entry) ctxt
   1.207    end;
   1.208  
   1.209  fun sort_term_check sups local_sort ts ctxt =
   1.210    let
   1.211      val thy = ProofContext.theory_of ctxt;
   1.212      val local_operation = local_operation thy sups;
   1.213 -    val constraints = these_constraints thy sups;
   1.214 +    val constraints = these_operations thy sups |> (map o apsnd) (fst o snd);
   1.215      val consts = ProofContext.consts_of ctxt;
   1.216      fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
   1.217       of TFree (v, _) => if v = Name.aT
   1.218 @@ -585,7 +591,7 @@
   1.219              #> apsnd (insert (op =) vi) else I
   1.220        | _ => I;
   1.221      fun add_const (Const (c, ty)) = (case local_operation c
   1.222 -         of SOME (t', idx) => check_typ (c, ty) (t', idx)
   1.223 +         of SOME (t', (_, idx)) => check_typ (c, ty) (t', idx)
   1.224            | NONE => I)
   1.225        | add_const _ = I;
   1.226      val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
   1.227 @@ -596,6 +602,23 @@
   1.228      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   1.229    in (ts', ctxt') end;
   1.230  
   1.231 +val uncheck = ref false;
   1.232 +
   1.233 +fun sort_term_uncheck sups ts ctxt =
   1.234 +  let
   1.235 +    val thy = ProofContext.theory_of ctxt;
   1.236 +    val global_param = AList.lookup (op =) (these_params thy sups) #> Option.map fst;
   1.237 +    val global_operation = global_operation thy sups;
   1.238 +    fun globalize (t as Free (v, ty)) = (case global_param v
   1.239 +         of SOME c => Const (c, ty)
   1.240 +          | NONE => t)
   1.241 +      | globalize (t as Const (c, ty)) = (case global_operation c
   1.242 +         of SOME c => Const (c, ty)
   1.243 +          | NONE => t)
   1.244 +      | globalize t = t;
   1.245 +    val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
   1.246 +  in (ts', ctxt) end;
   1.247 +
   1.248  fun init_class_ctxt sups local_sort ctxt =
   1.249    let
   1.250      val operations = these_operations (ProofContext.theory_of ctxt) sups;
   1.251 @@ -603,9 +626,11 @@
   1.252      ctxt
   1.253      |> Variable.declare_term
   1.254          (Logic.mk_type (TFree (Name.aT, local_sort)))
   1.255 -    |> fold (remove_constraint local_sort o fst) operations
   1.256 +    |> fold (internal_remove_constraint local_sort) operations
   1.257      |> Context.proof_map (Syntax.add_term_check 50 "class"
   1.258 -        (sort_term_check sups local_sort))
   1.259 +        (sort_term_check sups local_sort)
   1.260 +        #> Syntax.add_term_uncheck 50 "class"
   1.261 +          (sort_term_uncheck sups))
   1.262    end;
   1.263  
   1.264  fun init class ctxt =
   1.265 @@ -627,7 +652,7 @@
   1.266        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.267      val supexpr = Locale.Merge suplocales;
   1.268      val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   1.269 -    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
   1.270 +    val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups))
   1.271        (map fst supparams);
   1.272      val mergeexpr = Locale.Merge (suplocales @ includes);
   1.273      val constrain = Element.Constrains ((map o apsnd o map_atyps)
   1.274 @@ -646,7 +671,6 @@
   1.275  val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   1.276  val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   1.277  
   1.278 -
   1.279  fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
   1.280    let
   1.281      val superclasses = map (Sign.certify_class thy) raw_superclasses;
   1.282 @@ -656,9 +680,8 @@
   1.283        raw_dep_axioms thy cs
   1.284        |> (map o apsnd o map) (Sign.cert_prop thy)
   1.285        |> rpair thy;
   1.286 -    fun add_constraint class (c, ty) =
   1.287 -      Sign.add_const_constraint (c, SOME
   1.288 -        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   1.289 +    fun constrain_typs class = (map o apsnd o Term.map_type_tfree)
   1.290 +      (fn (v, _) => TFree (v, [class]))
   1.291    in
   1.292      thy
   1.293      |> Sign.add_path (Logic.const_of_class name)
   1.294 @@ -667,12 +690,13 @@
   1.295      |-> (fn cs => mk_axioms cs
   1.296      #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   1.297             (map fst cs @ other_consts) axioms_prop
   1.298 -    #-> (fn class => `(fn thy => AxClass.get_info thy class)
   1.299 -    #-> (fn {axioms, ...} => fold (add_constraint class) cs
   1.300 -    #> pair (class, (cs, axioms))))))
   1.301 +    #-> (fn class => `(fn _ => constrain_typs class cs)
   1.302 +    #-> (fn cs' => `(fn thy => AxClass.get_info thy class)
   1.303 +    #-> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs'
   1.304 +    #> pair (class, (cs', axioms)))))))
   1.305    end;
   1.306  
   1.307 -fun gen_class prep_spec prep_param local_syntax bname
   1.308 +fun gen_class prep_spec prep_param bname
   1.309      raw_supclasses raw_includes_elems raw_other_consts thy =
   1.310    let
   1.311      val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
   1.312 @@ -729,7 +753,7 @@
   1.313          add_class_data ((name_axclass, sups),
   1.314            (name_locale, map fst params ~~ consts, local_sort,
   1.315              (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   1.316 -              (map snd supconsts @ consts)), class_intro, local_syntax))
   1.317 +              (map snd supconsts @ consts)), class_intro))
   1.318        #> note_intro name_axclass class_intro
   1.319        #> class_interpretation name_axclass axioms []
   1.320        #> pair name_axclass
   1.321 @@ -748,8 +772,8 @@
   1.322  
   1.323  fun export_fixes thy class =
   1.324    let
   1.325 -    val consts = params_of_sort thy [class];
   1.326 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
   1.327 +    val cs = these_params thy [class];
   1.328 +    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
   1.329           of SOME (c, _) => Const (c, ty)
   1.330            | NONE => t)
   1.331        | subst_aterm t = t;
   1.332 @@ -757,10 +781,10 @@
   1.333  
   1.334  fun mk_operation_entry thy (c, rhs) =
   1.335    let
   1.336 -    val ty = fastype_of rhs;
   1.337 +    val ty = Logic.unvarifyT (Sign.the_const_constraint thy c);
   1.338      val typargs = Sign.const_typargs thy (c, ty);
   1.339      val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   1.340 -  in (c, (ty, (rhs, typidx))) end;
   1.341 +  in (c, (rhs, (ty, typidx))) end;
   1.342  
   1.343  fun add_const_in_class class ((c, rhs), syn) thy =
   1.344    let
   1.345 @@ -771,10 +795,9 @@
   1.346          val n2 = NameSpace.qualifier n1;
   1.347          val n3 = NameSpace.base n1;
   1.348        in NameSpace.implode [n2, prfx, n3] end;
   1.349 -    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   1.350      val rhs' = export_fixes thy class rhs;
   1.351      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.352 -      if w = Name.aT then TFree (w, constrain_sort sort) else TFree var);
   1.353 +      if w = Name.aT then TFree (w, [class]) else TFree var);
   1.354      val ty' = Term.fastype_of rhs';
   1.355      val ty'' = subst_typ ty';
   1.356      val c' = mk_name c;
   1.357 @@ -783,12 +806,13 @@
   1.358      fun interpret def thy =
   1.359        let
   1.360          val def' = symmetric def;
   1.361 -        val def_eq = Thm.prop_of def';
   1.362 -        val entry = mk_operation_entry thy (c', rhs);
   1.363 +        val def_eq = (map_types Logic.unvarifyT o Thm.prop_of) def';
   1.364        in
   1.365          thy
   1.366          |> class_interpretation class [def'] [def_eq]
   1.367 -        |> register_const class (entry, def')
   1.368 +        |> Sign.add_const_constraint (c', SOME ty'')
   1.369 +        |> `(fn thy => mk_operation_entry thy (c', rhs))
   1.370 +        |-> (fn entry => register_operation class (entry, SOME def'))
   1.371        end;
   1.372    in
   1.373      thy
   1.374 @@ -798,7 +822,6 @@
   1.375      |> Sign.sticky_prefix prfx
   1.376      |> PureThy.add_defs_i false [(def, [])]
   1.377      |-> (fn [def] => interpret def)
   1.378 -    |> Sign.add_const_constraint (c', SOME ty'')
   1.379      |> Sign.restore_naming thy
   1.380      |> pair c'
   1.381    end;
   1.382 @@ -818,10 +841,11 @@
   1.383      val c' = mk_name c;
   1.384      val rhs' = export_fixes thy class rhs;
   1.385      val ty' = fastype_of rhs';
   1.386 +    val entry = mk_operation_entry thy (c', rhs);
   1.387    in
   1.388      thy
   1.389      |> Sign.notation true prmode [(Const (c', ty'), syn)]
   1.390 -    |> register_abbrev class (c', ty')
   1.391 +    |> register_operation class (entry, NONE)
   1.392      |> pair c'
   1.393    end;
   1.394  
     2.1 --- a/src/Pure/Isar/instance.ML	Fri Oct 12 14:42:29 2007 +0200
     2.2 +++ b/src/Pure/Isar/instance.ML	Fri Oct 12 14:42:30 2007 +0200
     2.3 @@ -38,7 +38,7 @@
     2.4        ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty),
     2.5          Class.unoverload_const thy (c, ty));
     2.6      fun get_params ((tyco, vs), sort) =
     2.7 -      Class.params_of_sort thy sort
     2.8 +      Class.these_params thy sort
     2.9        |> map (get_param tyco (Type (tyco, map TFree vs)));
    2.10      val params = maps get_params arities;
    2.11      val ctxt =
     3.1 --- a/src/Pure/Isar/locale.ML	Fri Oct 12 14:42:29 2007 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Fri Oct 12 14:42:30 2007 +0200
     3.3 @@ -2104,7 +2104,7 @@
     3.4      (* infer types *)
     3.5      val res = Syntax.check_terms ctxt
     3.6        (map Logic.mk_type type_parms @
     3.7 -       map (uncurry TypeInfer.constrain) (given_parm_types ~~ given_insts') @
     3.8 +       map2 TypeInfer.constrain given_parm_types given_insts' @
     3.9         eqns');
    3.10      val ctxt' = ctxt |> fold Variable.auto_fixes res;
    3.11  
     4.1 --- a/src/Pure/Isar/subclass.ML	Fri Oct 12 14:42:29 2007 +0200
     4.2 +++ b/src/Pure/Isar/subclass.ML	Fri Oct 12 14:42:30 2007 +0200
     4.3 @@ -2,14 +2,14 @@
     4.4      ID:         $Id$
     4.5      Author:     Florian Haftmann, TU Muenchen
     4.6  
     4.7 -Prove subclass relations between type classes
     4.8 +Prove subclass relationship between type classes.
     4.9  *)
    4.10  
    4.11  signature SUBCLASS =
    4.12  sig
    4.13    val subclass: class -> local_theory -> Proof.state
    4.14    val subclass_cmd: xstring -> local_theory -> Proof.state
    4.15 -  (*FIXME val prove_subclass: tactic -> class * class -> theory -> theory*)
    4.16 +  val prove_subclass: tactic -> class -> local_theory -> local_theory
    4.17  end;
    4.18  
    4.19  structure Subclass : SUBCLASS =
    4.20 @@ -48,71 +48,82 @@
    4.21  
    4.22  local
    4.23  
    4.24 -fun mk_subclass_rule lthy sup =
    4.25 +fun gen_subclass prep_class do_proof raw_sup lthy =
    4.26    let
    4.27 -    (*FIXME check for proper parameter inclusion (consts_of) (?)*)
    4.28 -    val ctxt = LocalTheory.target_of lthy;
    4.29 -    val thy = ProofContext.theory_of ctxt;
    4.30 -    val locale = Class.locale_of_class thy sup;
    4.31 -  in
    4.32 -    Locale.global_asms_of thy locale
    4.33 -    |> maps snd
    4.34 -    |> map (ObjectLogic.ensure_propT thy)
    4.35 -  end;
    4.36 -
    4.37 -fun gen_subclass prep_class raw_sup lthy =
    4.38 -  let
    4.39 -    (*FIXME cleanup, provide tactical interface*)
    4.40      val ctxt = LocalTheory.target_of lthy;
    4.41      val thy = ProofContext.theory_of ctxt;
    4.42      val ctxt_thy = ProofContext.init thy;
    4.43      val sup = prep_class thy raw_sup;
    4.44 -    val sub = case Option.mapPartial (Class.class_of_locale thy)
    4.45 -       (TheoryTarget.peek lthy)
    4.46 +    val sub = case Option.mapPartial (Class.class_of_locale thy) (TheoryTarget.peek lthy)
    4.47       of NONE => error "not in class context"
    4.48        | SOME sub => sub;
    4.49 -    val export =
    4.50 -      Assumption.export false ctxt ctxt_thy
    4.51 -      #> singleton (Variable.export ctxt ctxt_thy);
    4.52 +    val sub_params = map fst (Class.these_params thy [sub]);
    4.53 +    val sup_params = map fst (Class.these_params thy [sup]);
    4.54 +    val err_params = subtract (op =) sub_params sup_params;
    4.55 +    val _ = if null err_params then [] else
    4.56 +      error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^
    4.57 +          commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]);
    4.58 +    val sublocale_prop =
    4.59 +      Locale.global_asms_of thy (Class.locale_of_class thy sup)
    4.60 +      |> maps snd
    4.61 +      |> map (ObjectLogic.ensure_propT thy);
    4.62 +    val supclasses = Sign.complete_sort thy [sup]
    4.63 +      |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
    4.64 +    val supclasses' = remove (op =) sup supclasses;
    4.65 +    val _ = if null supclasses' then () else
    4.66 +      error ("The following superclasses of " ^ sup
    4.67 +        ^ " are no superclass of " ^ sub ^ ": "
    4.68 +        ^ commas supclasses');
    4.69 +      (*FIXME*)
    4.70 +    val sub_ax = #axioms (AxClass.get_info thy sub);
    4.71 +    val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
    4.72      val loc_name = Class.locale_of_class thy sub;
    4.73      val loc_expr = Locale.Locale (Class.locale_of_class thy sup);
    4.74 -    fun prove_classrel interp thy =
    4.75 +    fun prove_classrel subclass_rule =
    4.76        let
    4.77 -        val classes = Sign.complete_sort thy [sup]
    4.78 -          |> filter_out (fn class' => Sign.subsort thy ([sub], [class']));
    4.79 -        fun instance_subclass (class1, class2) thy  =
    4.80 +        fun add_classrel sup' thy  =
    4.81            let
    4.82 -            val ax = #axioms (AxClass.get_info thy class1);
    4.83 -            val intro = #intro (AxClass.get_info thy class2)
    4.84 -              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
    4.85 -                  (TVar ((Name.aT, 0), [class1])))] [];
    4.86 -            val thm =
    4.87 -              intro
    4.88 -              |> OF_LAST (interp OF ax)
    4.89 -              |> strip_all_ofclass thy (Sign.super_classes thy class2);
    4.90 +            val classrel =
    4.91 +              #intro (AxClass.get_info thy sup')
    4.92 +              |> Drule.instantiate' [SOME sub_inst] []
    4.93 +              |> OF_LAST (subclass_rule OF sub_ax)
    4.94 +              |> strip_all_ofclass thy (Sign.super_classes thy sup');
    4.95            in
    4.96 -            thy |> AxClass.add_classrel thm
    4.97 +            AxClass.add_classrel classrel thy
    4.98            end;
    4.99        in
   4.100 -        thy |> fold_rev (curry instance_subclass sub) classes
   4.101 +        fold_rev add_classrel supclasses
   4.102        end;
   4.103 -    fun after_qed [thms] =
   4.104 +    fun prove_interpretation sublocale_rule =
   4.105 +      prove_interpretation_in (ProofContext.fact_tac [sublocale_rule] 1)
   4.106 +        I (loc_name, loc_expr)
   4.107 +    fun after_qed thms =
   4.108        let
   4.109 -        val thm = Conjunction.intr_balanced thms;
   4.110 -        val interp = export thm;
   4.111 +        val sublocale_rule = Conjunction.intr_balanced thms;
   4.112 +        val subclass_rule = sublocale_rule
   4.113 +          |> Assumption.export false ctxt ctxt_thy
   4.114 +          |> singleton (Variable.export ctxt ctxt_thy);
   4.115        in
   4.116 -        LocalTheory.theory (prove_classrel interp
   4.117 -          #> prove_interpretation_in (ProofContext.fact_tac [thm] 1)
   4.118 -             I (loc_name, loc_expr))
   4.119 +        LocalTheory.theory (prove_classrel subclass_rule
   4.120 +          #> prove_interpretation sublocale_rule)
   4.121          (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*)
   4.122        end;
   4.123 +  in
   4.124 +    do_proof after_qed sublocale_prop lthy
   4.125 +  end;
   4.126  
   4.127 -  in Proof.theorem_i NONE after_qed [map (rpair []) (mk_subclass_rule lthy sup)] lthy end;
   4.128 +fun user_proof after_qed props =
   4.129 +  Proof.theorem_i NONE (after_qed o the_single) [map (rpair []) props];
   4.130 +
   4.131 +fun tactic_proof tac after_qed props lthy =
   4.132 +  after_qed (Goal.prove_multi (LocalTheory.target_of lthy) [] [] props
   4.133 +    (K tac)) lthy;
   4.134  
   4.135  in
   4.136  
   4.137 -val subclass = gen_subclass (K I);
   4.138 -val subclass_cmd = gen_subclass Sign.read_class;
   4.139 +val subclass = gen_subclass (K I) user_proof;
   4.140 +val subclass_cmd = gen_subclass Sign.read_class user_proof;
   4.141 +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
   4.142  
   4.143  end; (*local*)
   4.144  
     5.1 --- a/src/Pure/Isar/theory_target.ML	Fri Oct 12 14:42:29 2007 +0200
     5.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Oct 12 14:42:30 2007 +0200
     5.3 @@ -203,7 +203,7 @@
     5.4        in (((c, mx2), t), thy') end;
     5.5      fun const_class (SOME class) ((c, _), mx) (_, t) =
     5.6            LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx))
     5.7 -          #-> Class.remove_constraint [class]
     5.8 +          #-> Class.remove_constraint class
     5.9        | const_class NONE _ _ = I;
    5.10      fun hide_abbrev (SOME class) abbrs thy =
    5.11            let
    5.12 @@ -274,7 +274,7 @@
    5.13      val mx3 = if is_loc then NoSyn else mx1;
    5.14      fun add_abbrev_in_class (SOME class) abbr =
    5.15            LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr)
    5.16 -          #-> (fn c => Class.remove_constraint [class] c)
    5.17 +          #-> Class.remove_constraint class
    5.18        | add_abbrev_in_class NONE _ = I;
    5.19    in
    5.20      lthy