1.1 --- a/src/HOL/Tools/record.ML Thu Aug 26 15:48:08 2010 +0200
1.2 +++ b/src/HOL/Tools/record.ML Thu Aug 26 16:25:25 2010 +0200
1.3 @@ -420,7 +420,7 @@
1.4 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
1.5 extfields = extfields, fieldext = fieldext }: data;
1.6
1.7 -structure Records_Data = Theory_Data
1.8 +structure Data = Theory_Data
1.9 (
1.10 type T = data;
1.11 val empty =
1.12 @@ -474,25 +474,22 @@
1.13
1.14 (* access 'records' *)
1.15
1.16 -val get_info = Symtab.lookup o #records o Records_Data.get;
1.17 +val get_info = Symtab.lookup o #records o Data.get;
1.18
1.19 fun the_info thy name =
1.20 (case get_info thy name of
1.21 SOME info => info
1.22 | NONE => error ("Unknown record type " ^ quote name));
1.23
1.24 -fun put_record name info thy =
1.25 - let
1.26 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.27 - Records_Data.get thy;
1.28 - val data = make_data (Symtab.update (name, info) records)
1.29 - sel_upd equalities extinjects extsplit splits extfields fieldext;
1.30 - in Records_Data.put data thy end;
1.31 +fun put_record name info =
1.32 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.33 + make_data (Symtab.update (name, info) records)
1.34 + sel_upd equalities extinjects extsplit splits extfields fieldext);
1.35
1.36
1.37 (* access 'sel_upd' *)
1.38
1.39 -val get_sel_upd = #sel_upd o Records_Data.get;
1.40 +val get_sel_upd = #sel_upd o Data.get;
1.41
1.42 val is_selector = Symtab.defined o #selectors o get_sel_upd;
1.43 val get_updates = Symtab.lookup o #updates o get_sel_upd;
1.44 @@ -517,7 +514,7 @@
1.45 val upds = map (suffix updateN) all ~~ all;
1.46
1.47 val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
1.48 - equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
1.49 + equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
1.50 val data = make_data records
1.51 {selectors = fold Symtab.update_new sels selectors,
1.52 updates = fold Symtab.update_new upds updates,
1.53 @@ -526,80 +523,61 @@
1.54 foldcong = foldcong addcongs folds,
1.55 unfoldcong = unfoldcong addcongs unfolds}
1.56 equalities extinjects extsplit splits extfields fieldext;
1.57 - in Records_Data.put data thy end;
1.58 + in Data.put data thy end;
1.59
1.60
1.61 (* access 'equalities' *)
1.62
1.63 -fun add_equalities name thm thy =
1.64 - let
1.65 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.66 - Records_Data.get thy;
1.67 - val data = make_data records sel_upd
1.68 - (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
1.69 - in Records_Data.put data thy end;
1.70 -
1.71 -val get_equalities = Symtab.lookup o #equalities o Records_Data.get;
1.72 +fun add_equalities name thm =
1.73 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.74 + make_data records sel_upd
1.75 + (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
1.76 +
1.77 +val get_equalities = Symtab.lookup o #equalities o Data.get;
1.78
1.79
1.80 (* access 'extinjects' *)
1.81
1.82 -fun add_extinjects thm thy =
1.83 - let
1.84 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.85 - Records_Data.get thy;
1.86 - val data =
1.87 - make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
1.88 - extsplit splits extfields fieldext;
1.89 - in Records_Data.put data thy end;
1.90 -
1.91 -val get_extinjects = rev o #extinjects o Records_Data.get;
1.92 +fun add_extinjects thm =
1.93 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.94 + make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
1.95 + extsplit splits extfields fieldext);
1.96 +
1.97 +val get_extinjects = rev o #extinjects o Data.get;
1.98
1.99
1.100 (* access 'extsplit' *)
1.101
1.102 -fun add_extsplit name thm thy =
1.103 - let
1.104 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.105 - Records_Data.get thy;
1.106 - val data =
1.107 - make_data records sel_upd equalities extinjects
1.108 - (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
1.109 - in Records_Data.put data thy end;
1.110 +fun add_extsplit name thm =
1.111 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.112 + make_data records sel_upd equalities extinjects
1.113 + (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
1.114
1.115
1.116 (* access 'splits' *)
1.117
1.118 -fun add_splits name thmP thy =
1.119 - let
1.120 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.121 - Records_Data.get thy;
1.122 - val data =
1.123 - make_data records sel_upd equalities extinjects extsplit
1.124 - (Symtab.update_new (name, thmP) splits) extfields fieldext;
1.125 - in Records_Data.put data thy end;
1.126 -
1.127 -val get_splits = Symtab.lookup o #splits o Records_Data.get;
1.128 +fun add_splits name thmP =
1.129 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.130 + make_data records sel_upd equalities extinjects extsplit
1.131 + (Symtab.update_new (name, thmP) splits) extfields fieldext);
1.132 +
1.133 +val get_splits = Symtab.lookup o #splits o Data.get;
1.134
1.135
1.136 (* parent/extension of named record *)
1.137
1.138 -val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Records_Data.get);
1.139 -val get_extension = Option.map #extension oo (Symtab.lookup o #records o Records_Data.get);
1.140 +val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
1.141 +val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
1.142
1.143
1.144 (* access 'extfields' *)
1.145
1.146 -fun add_extfields name fields thy =
1.147 - let
1.148 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.149 - Records_Data.get thy;
1.150 - val data =
1.151 - make_data records sel_upd equalities extinjects extsplit splits
1.152 - (Symtab.update_new (name, fields) extfields) fieldext;
1.153 - in Records_Data.put data thy end;
1.154 -
1.155 -val get_extfields = Symtab.lookup o #extfields o Records_Data.get;
1.156 +fun add_extfields name fields =
1.157 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.158 + make_data records sel_upd equalities extinjects extsplit splits
1.159 + (Symtab.update_new (name, fields) extfields) fieldext);
1.160 +
1.161 +val get_extfields = Symtab.lookup o #extfields o Data.get;
1.162
1.163 fun get_extT_fields thy T =
1.164 let
1.165 @@ -609,7 +587,7 @@
1.166 in Long_Name.implode (rev (nm :: rst)) end;
1.167 val midx = maxidx_of_typs (moreT :: Ts);
1.168 val varifyT = varifyT midx;
1.169 - val {records, extfields, ...} = Records_Data.get thy;
1.170 + val {records, extfields, ...} = Data.get thy;
1.171 val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
1.172 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
1.173
1.174 @@ -628,18 +606,14 @@
1.175
1.176 (* access 'fieldext' *)
1.177
1.178 -fun add_fieldext extname_types fields thy =
1.179 - let
1.180 - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
1.181 - Records_Data.get thy;
1.182 - val fieldext' =
1.183 - fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
1.184 - val data =
1.185 - make_data records sel_upd equalities extinjects
1.186 - extsplit splits extfields fieldext';
1.187 - in Records_Data.put data thy end;
1.188 -
1.189 -val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;
1.190 +fun add_fieldext extname_types fields =
1.191 + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
1.192 + let
1.193 + val fieldext' =
1.194 + fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
1.195 + in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
1.196 +
1.197 +val get_fieldext = Symtab.lookup o #fieldext o Data.get;
1.198
1.199
1.200 (* parent records *)
1.201 @@ -1179,7 +1153,7 @@
1.202 ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
1.203 if is_selector thy s andalso is_some (get_updates thy u) then
1.204 let
1.205 - val {sel_upd = {updates, ...}, extfields, ...} = Records_Data.get thy;
1.206 + val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
1.207
1.208 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
1.209 (case Symtab.lookup updates u of
1.210 @@ -1598,15 +1572,17 @@
1.211 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
1.212 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
1.213 | [x] => (head_of x, false));
1.214 - val rule'' = cterm_instantiate (map (pairself cert)
1.215 - (case rev params of
1.216 - [] =>
1.217 - (case AList.lookup (op =) (Term.add_frees g []) s of
1.218 - NONE => sys_error "try_param_tac: no such variable"
1.219 - | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1.220 - | (_, T) :: _ =>
1.221 - [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1.222 - (x, list_abs (params, Bound 0))])) rule';
1.223 + val rule'' =
1.224 + cterm_instantiate
1.225 + (map (pairself cert)
1.226 + (case rev params of
1.227 + [] =>
1.228 + (case AList.lookup (op =) (Term.add_frees g []) s of
1.229 + NONE => sys_error "try_param_tac: no such variable"
1.230 + | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1.231 + | (_, T) :: _ =>
1.232 + [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1.233 + (x, list_abs (params, Bound 0))])) rule';
1.234 in compose_tac (false, rule'', nprems_of rule) i end);
1.235
1.236
1.237 @@ -1635,7 +1611,8 @@
1.238 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
1.239 val ((_, cons), thy') = thy
1.240 |> Iso_Tuple_Support.add_iso_tuple_type
1.241 - (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right);
1.242 + (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
1.243 + (fastype_of left, fastype_of right);
1.244 in
1.245 (cons $ left $ right, (thy', i + 1))
1.246 end;
1.247 @@ -1778,7 +1755,10 @@
1.248 ("ext_surjective", surject),
1.249 ("ext_split", split_meta)]);
1.250
1.251 - in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
1.252 + in
1.253 + (((ext_name, ext_type), (ext_tyco, alphas_zeta),
1.254 + extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
1.255 + end;
1.256
1.257 fun chunks [] [] = []
1.258 | chunks [] xs = [xs]
1.259 @@ -1795,7 +1775,7 @@
1.260
1.261 (* mk_recordT *)
1.262
1.263 -(*builds up the record type from the current extension tpye extT and a list
1.264 +(*build up the record type from the current extension tpye extT and a list
1.265 of parent extensions, starting with the root of the record hierarchy*)
1.266 fun mk_recordT extT =
1.267 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
1.268 @@ -1834,8 +1814,10 @@
1.269 val lhs = HOLogic.mk_random T size;
1.270 val tc = HOLogic.mk_return Tm @{typ Random.seed}
1.271 (HOLogic.mk_valtermify_app extN params T);
1.272 - val rhs = HOLogic.mk_ST
1.273 - (map (fn (v, T') => ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1.274 + val rhs =
1.275 + HOLogic.mk_ST
1.276 + (map (fn (v, T') =>
1.277 + ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1.278 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1.279 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
1.280 in
1.281 @@ -1860,17 +1842,20 @@
1.282
1.283 fun add_code ext_tyco vs extT ext simps inject thy =
1.284 let
1.285 - val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
1.286 - (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
1.287 - Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
1.288 - fun tac eq_def = Class.intro_classes_tac []
1.289 + val eq =
1.290 + (HOLogic.mk_Trueprop o HOLogic.mk_eq)
1.291 + (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
1.292 + Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
1.293 + fun tac eq_def =
1.294 + Class.intro_classes_tac []
1.295 THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
1.296 THEN ALLGOALS (rtac @{thm refl});
1.297 fun mk_eq thy eq_def = Simplifier.rewrite_rule
1.298 [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
1.299 - fun mk_eq_refl thy = @{thm HOL.eq_refl}
1.300 + fun mk_eq_refl thy =
1.301 + @{thm HOL.eq_refl}
1.302 |> Thm.instantiate
1.303 - ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
1.304 + ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
1.305 |> AxClass.unoverload thy;
1.306 in
1.307 thy
1.308 @@ -1944,7 +1929,8 @@
1.309
1.310 val extension_name = full binding;
1.311
1.312 - val ((ext, (ext_tyco, vs), extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1.313 + val ((ext, (ext_tyco, vs),
1.314 + extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1.315 thy
1.316 |> Sign.qualified_path false binding
1.317 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;