src/Pure/axclass.ML
changeset 36417 54bc1a44967d
parent 36346 5518de23101d
child 36418 752ee03427c2
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 27 10:42:41 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 27 14:19:47 2010 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Type classes defined as predicates, associated with a record of
     1.7 -parameters.
     1.8 +parameters.  Proven class relations and type arities.
     1.9  *)
    1.10  
    1.11  signature AX_CLASS =
    1.12 @@ -104,7 +104,7 @@
    1.13        val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
    1.14        val params' =
    1.15          if null params1 then params2
    1.16 -        else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
    1.17 +        else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1;
    1.18  
    1.19        (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
    1.20        val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
    1.21 @@ -232,8 +232,8 @@
    1.22      val classrels = proven_classrels_of thy;
    1.23      val diff_merge_classrels = diff_merge_classrels_of thy;
    1.24      val (needed, thy') = (false, thy) |>
    1.25 -      fold (fn c12 => fn (needed, thy) =>
    1.26 -          put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
    1.27 +      fold (fn rel => fn (needed, thy) =>
    1.28 +          put_trancl_classrel (rel, Symreltab.lookup classrels rel |> the |> #1) thy
    1.29            |>> (fn b => needed orelse b))
    1.30          diff_merge_classrels;
    1.31    in
    1.32 @@ -253,21 +253,25 @@
    1.33  
    1.34  fun thynames_of_arity thy (c, a) =
    1.35    Symtab.lookup_list (proven_arities_of thy) a
    1.36 -  |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
    1.37 +  |> map_filter (fn ((c', _), ((_, name), _)) => if c = c' then SOME name else NONE)
    1.38    |> rev;
    1.39  
    1.40  fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities =
    1.41    let
    1.42      val algebra = Sign.classes_of thy;
    1.43 +    val ars = Symtab.lookup_list arities t;
    1.44      val super_class_completions =
    1.45        Sign.super_classes thy c
    1.46 -      |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
    1.47 -          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
    1.48 -    val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss);
    1.49 +      |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
    1.50 +            c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
    1.51 +
    1.52 +    val names = Name.invents Name.context Name.aT (length Ss);
    1.53 +    val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
    1.54 +
    1.55      val completions = super_class_completions |> map (fn c1 =>
    1.56        let
    1.57          val th1 = (th RS the_classrel_thm thy (c, c1))
    1.58 -          |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) []
    1.59 +          |> Drule.instantiate' std_vars []
    1.60            |> Thm.close_derivation;
    1.61          val prf1 = Thm.proof_of th1;
    1.62        in (((th1, thy_name), prf1), c1) end);
    1.63 @@ -277,12 +281,11 @@
    1.64  
    1.65  fun put_arity ((t, Ss, c), th) thy =
    1.66    let
    1.67 -    val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
    1.68 +    val arity = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
    1.69    in
    1.70      thy
    1.71      |> map_proven_arities
    1.72 -      (Symtab.insert_list (eq_fst op =) arity' #>
    1.73 -        insert_arity_completions thy arity' #> snd)
    1.74 +      (Symtab.insert_list (eq_fst op =) arity #> insert_arity_completions thy arity #> #2)
    1.75    end;
    1.76  
    1.77  fun complete_arities thy =
    1.78 @@ -309,15 +312,15 @@
    1.79  
    1.80  fun add_inst_param (c, tyco) inst =
    1.81    (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    1.82 -  #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    1.83 +  #> (map_inst_params o apsnd) (Symtab.update_new (#1 inst, (c, tyco)));
    1.84  
    1.85  val inst_of_param = Symtab.lookup o #2 o inst_params_of;
    1.86 -val param_of_inst = fst oo get_inst_param;
    1.87 +val param_of_inst = #1 oo get_inst_param;
    1.88  
    1.89  fun inst_thms thy =
    1.90    Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
    1.91  
    1.92 -fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
    1.93 +fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
    1.94  
    1.95  fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    1.96  fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    1.97 @@ -376,7 +379,7 @@
    1.98        | NONE => error ("Not a class parameter: " ^ quote c));
    1.99      val tyco = inst_tyco_of thy (c, T);
   1.100      val name_inst = instance_name (tyco, class) ^ "_inst";
   1.101 -    val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
   1.102 +    val c' = instance_name (tyco, c);
   1.103      val T' = Type.strip_sorts T;
   1.104    in
   1.105      thy
   1.106 @@ -388,7 +391,7 @@
   1.107        #>> apsnd Thm.varifyT_global
   1.108        #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
   1.109          #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
   1.110 -        #> snd
   1.111 +        #> #2
   1.112          #> pair (Const (c, T))))
   1.113      ||> Sign.restore_naming thy
   1.114    end;
   1.115 @@ -399,8 +402,7 @@
   1.116      val tyco = inst_tyco_of thy (c, T);
   1.117      val (c', eq) = get_inst_param thy (c, tyco);
   1.118      val prop = Logic.mk_equals (Const (c', T), t);
   1.119 -    val b' = Thm.def_binding_optional
   1.120 -      (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b;
   1.121 +    val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
   1.122    in
   1.123      thy
   1.124      |> Thm.add_def false false (b', prop)
   1.125 @@ -426,7 +428,7 @@
   1.126    in
   1.127      thy
   1.128      |> Sign.primitive_classrel (c1, c2)
   1.129 -    |> (snd oo put_trancl_classrel) ((c1, c2), th')
   1.130 +    |> (#2 oo put_trancl_classrel) ((c1, c2), th')
   1.131      |> perhaps complete_arities
   1.132    end;
   1.133  
   1.134 @@ -436,20 +438,23 @@
   1.135      val prop = Thm.plain_prop_of th;
   1.136      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   1.137      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   1.138 -    val names = Name.names Name.context Name.aT Ss;
   1.139 -    val T = Type (t, map TFree names);
   1.140 +
   1.141 +    val args = Name.names Name.context Name.aT Ss;
   1.142 +    val T = Type (t, map TFree args);
   1.143 +    val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), S)))) args;
   1.144 +
   1.145      val missing_params = Sign.complete_sort thy [c]
   1.146        |> maps (these o Option.map #params o try (get_info thy))
   1.147        |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
   1.148        |> (map o apsnd o map_atyps) (K T);
   1.149      val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
   1.150      val th' = th
   1.151 -      |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
   1.152 +      |> Drule.instantiate' std_vars []
   1.153        |> Thm.unconstrain_allTs;
   1.154      val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   1.155    in
   1.156      thy
   1.157 -    |> fold (snd oo declare_overloaded) missing_params
   1.158 +    |> fold (#2 oo declare_overloaded) missing_params
   1.159      |> Sign.primitive_arity (t, Ss, [c])
   1.160      |> put_arity ((t, Ss, c), th')
   1.161    end;
   1.162 @@ -585,9 +590,9 @@
   1.163      val axclass = make_axclass (def, intro, axioms, params);
   1.164      val result_thy =
   1.165        facts_thy
   1.166 -      |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
   1.167 +      |> fold (#2 oo put_trancl_classrel) (map (pair class) super ~~ classrel)
   1.168        |> Sign.qualified_path false bconst
   1.169 -      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
   1.170 +      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
   1.171        |> Sign.restore_naming facts_thy
   1.172        |> map_axclasses (Symtab.update (class, axclass))
   1.173        |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
   1.174 @@ -600,8 +605,7 @@
   1.175  
   1.176  local
   1.177  
   1.178 -(* old-style axioms *)
   1.179 -
   1.180 +(*old-style axioms*)
   1.181  fun add_axiom (b, prop) =
   1.182    Thm.add_axiom (b, prop) #->
   1.183    (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));