misc tuning and simplification;
authorwenzelm
Sun Apr 25 21:02:36 2010 +0200 (2010-04-25 ago)
changeset 36327c0415cb24a10
parent 36326 85d026788fce
child 36328 4d9deabf6474
misc tuning and simplification;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Sun Apr 25 19:44:47 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Apr 25 21:02:36 2010 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4    val add_arity: thm -> theory -> theory
     1.5    val prove_classrel: class * class -> tactic -> theory -> theory
     1.6    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
     1.7 -  val get_info: theory -> class ->
     1.8 -    {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
     1.9 +  type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
    1.10 +  val get_info: theory -> class -> info
    1.11    val class_intros: theory -> thm list
    1.12    val class_of_param: theory -> string -> class option
    1.13    val cert_classrel: theory -> class * class -> class * class
    1.14 @@ -60,17 +60,17 @@
    1.15        fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
    1.16  
    1.17  
    1.18 -(* axclasses *)
    1.19 +(* axclass info *)
    1.20  
    1.21 -datatype axclass = AxClass of
    1.22 +type info =
    1.23   {def: thm,
    1.24    intro: thm,
    1.25    axioms: thm list,
    1.26    params: (string * typ) list};
    1.27  
    1.28 -type axclasses = axclass Symtab.table * param list;
    1.29 +type axclasses = info Symtab.table * param list;
    1.30  
    1.31 -fun make_axclass ((def, intro, axioms), params) = AxClass
    1.32 +fun make_axclass ((def, intro, axioms), params): info =
    1.33    {def = def, intro = intro, axioms = axioms, params = params};
    1.34  
    1.35  fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
    1.36 @@ -106,7 +106,7 @@
    1.37  
    1.38  (* setup data *)
    1.39  
    1.40 -structure AxClassData = Theory_Data_PP
    1.41 +structure Data = Theory_Data_PP
    1.42  (
    1.43    type T = axclasses * ((instances * inst_params) * (class * class) list);
    1.44    val empty = ((Symtab.empty, []), (((Symreltab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), []));
    1.45 @@ -114,10 +114,11 @@
    1.46    fun merge pp ((axclasses1, ((instances1, inst_params1), diff_merge_classrels1)),
    1.47      (axclasses2, ((instances2, inst_params2), diff_merge_classrels2))) =
    1.48      let
    1.49 -      val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2)
    1.50 -      val diff_merge_classrels = subtract (op =) classrels1 classrels2
    1.51 -        @ subtract (op =) classrels2 classrels1
    1.52 -        @ diff_merge_classrels1 @ diff_merge_classrels2
    1.53 +      val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2);
    1.54 +      val diff_merge_classrels =
    1.55 +        subtract (op =) classrels1 classrels2 @
    1.56 +        subtract (op =) classrels2 classrels1 @
    1.57 +        diff_merge_classrels1 @ diff_merge_classrels2;
    1.58      in
    1.59        (merge_axclasses pp (axclasses1, axclasses2),
    1.60          ((merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)),
    1.61 @@ -128,29 +129,23 @@
    1.62  
    1.63  (* maintain axclasses *)
    1.64  
    1.65 -val get_axclasses = #1 o AxClassData.get;
    1.66 -val map_axclasses = AxClassData.map o apfst;
    1.67 -
    1.68 -val lookup_def = Symtab.lookup o #1 o get_axclasses;
    1.69 +val get_axclasses = #1 o Data.get;
    1.70 +val map_axclasses = Data.map o apfst;
    1.71  
    1.72  fun get_info thy c =
    1.73 -  (case lookup_def thy c of
    1.74 -    SOME (AxClass info) => info
    1.75 +  (case Symtab.lookup (#1 (get_axclasses thy)) c of
    1.76 +    SOME info => info
    1.77    | NONE => error ("No such axclass: " ^ quote c));
    1.78  
    1.79  fun class_intros thy =
    1.80    let
    1.81 -    fun add_intro c =
    1.82 -      (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
    1.83 +    fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
    1.84      val classes = Sign.all_classes thy;
    1.85    in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
    1.86  
    1.87 -
    1.88 -fun get_params thy pred =
    1.89 +fun all_params_of thy S =
    1.90    let val params = #2 (get_axclasses thy);
    1.91 -  in fold (fn (x, c) => if pred c then cons x else I) params [] end;
    1.92 -
    1.93 -fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
    1.94 +  in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
    1.95  
    1.96  fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
    1.97  
    1.98 @@ -159,11 +154,11 @@
    1.99  
   1.100  fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
   1.101  
   1.102 -val get_instances = #1 o #1 o #2 o AxClassData.get;
   1.103 -val map_instances = AxClassData.map o apsnd o apfst o apfst;
   1.104 +val get_instances = #1 o #1 o #2 o Data.get;
   1.105 +val map_instances = Data.map o apsnd o apfst o apfst;
   1.106  
   1.107 -val get_diff_merge_classrels = #2 o #2 o AxClassData.get;
   1.108 -val clear_diff_merge_classrels = AxClassData.map (apsnd (apsnd (K [])));
   1.109 +val get_diff_merge_classrels = #2 o #2 o Data.get;
   1.110 +val clear_diff_merge_classrels = Data.map (apsnd (apsnd (K [])));
   1.111  
   1.112  
   1.113  fun the_classrel thy (c1, c2) =
   1.114 @@ -177,26 +172,29 @@
   1.115  
   1.116  fun put_trancl_classrel ((c1, c2), th) thy =
   1.117    let
   1.118 -    val classrels = fst (get_instances thy)
   1.119 -    val alg = Sign.classes_of thy
   1.120 -    val {classes, ...} = alg |> Sorts.rep_algebra
   1.121 +    val cert = Thm.cterm_of thy;
   1.122 +    val certT = Thm.ctyp_of thy;
   1.123 +
   1.124 +    val classrels = fst (get_instances thy);
   1.125 +    val classes = #classes (Sorts.rep_algebra (Sign.classes_of thy));
   1.126  
   1.127      fun reflcl_classrel (c1', c2') =
   1.128 -      if c1' = c2' then Thm.trivial (Logic.mk_of_class (TVar(("'a",0),[]), c1') |> cterm_of thy)
   1.129 -      else the_classrel_thm thy (c1', c2')
   1.130 +      if c1' = c2'
   1.131 +      then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1')))
   1.132 +      else the_classrel_thm thy (c1', c2');
   1.133      fun gen_classrel (c1_pred, c2_succ) =
   1.134        let
   1.135          val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
   1.136 -          |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] []
   1.137 -          |> Thm.close_derivation
   1.138 -        val prf' = th' |> Thm.proof_of
   1.139 -      in ((c1_pred, c2_succ), (th',prf')) end
   1.140 +          |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
   1.141 +          |> Thm.close_derivation;
   1.142 +        val prf' = th' |> Thm.proof_of;
   1.143 +      in ((c1_pred, c2_succ), (th', prf')) end;
   1.144  
   1.145 -    val new_classrels = Library.map_product pair
   1.146 -        (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
   1.147 +    val new_classrels =
   1.148 +      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
   1.149        |> filter_out (Symreltab.defined classrels)
   1.150 -      |> map gen_classrel
   1.151 -    val needed = length new_classrels > 0
   1.152 +      |> map gen_classrel;
   1.153 +    val needed = not (null new_classrels);
   1.154    in
   1.155      (needed,
   1.156       if needed then
   1.157 @@ -207,13 +205,13 @@
   1.158  
   1.159  fun complete_classrels thy =
   1.160    let
   1.161 -    val diff_merge_classrels = get_diff_merge_classrels thy
   1.162 -    val classrels = fst (get_instances thy)
   1.163 +    val diff_merge_classrels = get_diff_merge_classrels thy;
   1.164 +    val classrels = fst (get_instances thy);
   1.165      val (needed, thy') = (false, thy) |>
   1.166        fold (fn c12 => fn (needed, thy) =>
   1.167            put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> fst) thy
   1.168            |>> (fn b => needed orelse b))
   1.169 -        diff_merge_classrels
   1.170 +        diff_merge_classrels;
   1.171    in
   1.172      if null diff_merge_classrels then NONE
   1.173      else thy' |> clear_diff_merge_classrels |> SOME
   1.174 @@ -246,9 +244,9 @@
   1.175        let
   1.176          val th1 = (th RS the_classrel_thm thy (c, c1))
   1.177            |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) []
   1.178 -          |> Thm.close_derivation
   1.179 -        val prf1 = Thm.proof_of th1
   1.180 -      in (((th1,thy_name), prf1), c1) end)
   1.181 +          |> Thm.close_derivation;
   1.182 +        val prf1 = Thm.proof_of th1;
   1.183 +      in (((th1, thy_name), prf1), c1) end);
   1.184      val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1)))
   1.185        completions arities;
   1.186    in (null completions, arities') end;
   1.187 @@ -281,24 +279,23 @@
   1.188  
   1.189  (* maintain instance parameters *)
   1.190  
   1.191 -val get_inst_params = #2 o #1 o #2 o AxClassData.get;
   1.192 -val map_inst_params = AxClassData.map o apsnd o apfst o apsnd;
   1.193 +val get_inst_params = #2 o #1 o #2 o Data.get;
   1.194 +val map_inst_params = Data.map o apsnd o apfst o apsnd;
   1.195  
   1.196  fun get_inst_param thy (c, tyco) =
   1.197 -  case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
   1.198 -   of SOME c' => c'
   1.199 -    | NONE => error ("No instance parameter for constant " ^ quote c
   1.200 -        ^ " on type constructor " ^ quote tyco);
   1.201 +  (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (get_inst_params thy)) c)) tyco of
   1.202 +    SOME c' => c'
   1.203 +  | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
   1.204  
   1.205 -fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
   1.206 -      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   1.207 +fun add_inst_param (c, tyco) inst =
   1.208 +  (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   1.209    #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   1.210  
   1.211  val inst_of_param = Symtab.lookup o snd o get_inst_params;
   1.212  val param_of_inst = fst oo get_inst_param;
   1.213  
   1.214 -fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
   1.215 -  (get_inst_params thy) [];
   1.216 +fun inst_thms thy =
   1.217 +  (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) (get_inst_params thy) [];
   1.218  
   1.219  fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
   1.220  
   1.221 @@ -308,18 +305,20 @@
   1.222  fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
   1.223  fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   1.224  
   1.225 -fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
   1.226 - of SOME tyco => AList.lookup (op =) params (c, tyco)
   1.227 -  | NONE => NONE;
   1.228 +fun lookup_inst_param consts params (c, T) =
   1.229 +  (case get_inst_tyco consts (c, T) of
   1.230 +    SOME tyco => AList.lookup (op =) params (c, tyco)
   1.231 +  | NONE => NONE);
   1.232  
   1.233  fun unoverload_const thy (c_ty as (c, _)) =
   1.234 -  if is_some (class_of_param thy c)
   1.235 -  then case get_inst_tyco (Sign.consts_of thy) c_ty
   1.236 -   of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   1.237 -    | NONE => c
   1.238 +  if is_some (class_of_param thy c) then
   1.239 +    (case get_inst_tyco (Sign.consts_of thy) c_ty of
   1.240 +      SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   1.241 +    | NONE => c)
   1.242    else c;
   1.243  
   1.244  
   1.245 +
   1.246  (** instances **)
   1.247  
   1.248  (* class relations *)
   1.249 @@ -340,11 +339,8 @@
   1.250    cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
   1.251      handle TYPE (msg, _, _) => error msg;
   1.252  
   1.253 -fun check_shyps_topped th errmsg =
   1.254 -  let val {shyps, ...} = Thm.rep_thm th
   1.255 -  in
   1.256 -    forall null shyps orelse raise Fail errmsg
   1.257 -  end;
   1.258 +val shyps_topped = forall null o #shyps o Thm.rep_thm;
   1.259 +
   1.260  
   1.261  (* declaration and definition of instances of overloaded constants *)
   1.262  
   1.263 @@ -406,7 +402,7 @@
   1.264      val th' = th
   1.265        |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
   1.266        |> Drule.unconstrainTs;
   1.267 -    val _ = check_shyps_topped th' "add_classrel: nontop shyps after unconstrain"
   1.268 +    val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
   1.269    in
   1.270      thy
   1.271      |> Sign.primitive_classrel (c1, c2)
   1.272 @@ -430,7 +426,7 @@
   1.273      val th' = th
   1.274        |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
   1.275        |> Drule.unconstrainTs;
   1.276 -    val _ = check_shyps_topped th' "add_arity: nontop shyps after unconstrain"
   1.277 +    val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   1.278    in
   1.279      thy
   1.280      |> fold (snd oo declare_overloaded) missing_params