1.1 --- a/src/HOL/Tools/record_package.ML Sat Oct 06 16:41:22 2007 +0200
1.2 +++ b/src/HOL/Tools/record_package.ML Sat Oct 06 16:50:04 2007 +0200
1.3 @@ -607,7 +607,7 @@
1.4 val types = map snd flds';
1.5 val (args,rest) = splitargs (map fst flds') fargs;
1.6 val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
1.7 - val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
1.8 + val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
1.9 argtypes 0;
1.10 val varifyT = varifyT midx;
1.11 val vartypes = map varifyT types;
1.12 @@ -654,12 +654,12 @@
1.13 gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
1.14
1.15
1.16 -val parse_translation =
1.17 +val parse_translation =
1.18 [("_record_update", record_update_tr),
1.19 ("_update_name", update_name_tr)];
1.20
1.21
1.22 -val adv_parse_translation =
1.23 +val adv_parse_translation =
1.24 [("_record",adv_record_tr),
1.25 ("_record_scheme",adv_record_scheme_tr),
1.26 ("_record_type",adv_record_type_tr),
1.27 @@ -762,7 +762,7 @@
1.28 in Syntax.term_of_typ (! Syntax.show_sorts)
1.29 (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
1.30
1.31 - fun match rT T = (Sign.typ_match thy (varifyT rT,T)
1.32 + fun match rT T = (Sign.typ_match thy (varifyT rT,T)
1.33 Vartab.empty);
1.34
1.35 in if !print_record_type_abbr
1.36 @@ -876,8 +876,8 @@
1.37 val f_x = Free (f',fT)$(Free (x,T'));
1.38 fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
1.39 | is_constr _ = false;
1.40 - fun subst (t as u$w) = if Free (f',fT)=u
1.41 - then if is_constr w then f_x
1.42 + fun subst (t as u$w) = if Free (f',fT)=u
1.43 + then if is_constr w then f_x
1.44 else raise TERM ("abstract_over_fun_app",[t])
1.45 else subst u$subst w
1.46 | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
1.47 @@ -885,12 +885,12 @@
1.48 val t'' = abstract_over (f_x,subst t');
1.49 val vars = strip_qnt_vars "all" t'';
1.50 val bdy = strip_qnt_body "all" t'';
1.51 -
1.52 +
1.53 in list_abs ((x,T')::vars,bdy) end
1.54 | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
1.55 (* Generates a theorem of the kind:
1.56 - * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
1.57 - *)
1.58 + * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
1.59 + *)
1.60 fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
1.61 let
1.62 val rT = domain_type fT;
1.63 @@ -900,16 +900,16 @@
1.64 fun app_bounds 0 t = t$Bound 0
1.65 | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
1.66
1.67 -
1.68 +
1.69 val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
1.70 val prop = Logic.mk_equals
1.71 (list_all ((f,fT)::vars,
1.72 app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
1.73 list_all ((fst r,rT)::vars,
1.74 - app_bounds (n - 1) ((Free P)$Bound n)));
1.75 + app_bounds (n - 1) ((Free P)$Bound n)));
1.76 val prove_standard = quick_and_dirty_prove true thy;
1.77 val thm = prove_standard [] prop (fn prems =>
1.78 - EVERY [rtac equal_intr_rule 1,
1.79 + EVERY [rtac equal_intr_rule 1,
1.80 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
1.81 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
1.82 in thm end
1.83 @@ -928,14 +928,14 @@
1.84 (trm as Abs _) =>
1.85 (case rec_id (~1) T of
1.86 "" => NONE
1.87 - | n => if T=T'
1.88 + | n => if T=T'
1.89 then (let
1.90 - val P=cterm_of thy (abstract_over_fun_app trm);
1.91 + val P=cterm_of thy (abstract_over_fun_app trm);
1.92 val thm = mk_fun_apply_eq trm thy;
1.93 val PV = cterm_of thy (hd (term_vars (prop_of thm)));
1.94 val thm' = cterm_instantiate [(PV,P)] thm;
1.95 in SOME thm' end handle TERM _ => NONE)
1.96 - else NONE)
1.97 + else NONE)
1.98 | _ => NONE))
1.99 end
1.100
1.101 @@ -951,7 +951,7 @@
1.102 (* [thm] is the same as all_thm *)
1.103 | NONE => extsplits)
1.104 val thms'=K_comp_convs@thms;
1.105 - val ss' = (Simplifier.inherit_context ss simpset
1.106 + val ss' = (Simplifier.inherit_context ss simpset
1.107 addsimps thms'
1.108 addsimprocs [record_split_f_more_simproc]);
1.109 in
1.110 @@ -992,8 +992,8 @@
1.111 NONE => NONE
1.112 | SOME u_name
1.113 => if u_name = s
1.114 - then (case mk_eq_terms r of
1.115 - NONE =>
1.116 + then (case mk_eq_terms r of
1.117 + NONE =>
1.118 let
1.119 val rv = ("r",rT)
1.120 val rb = Bound 0
1.121 @@ -1064,7 +1064,7 @@
1.122 in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
1.123 else ((sprout,skeleton),vars);
1.124
1.125 - fun is_upd_same (sprout,skeleton) u
1.126 + fun is_upd_same (sprout,skeleton) u
1.127 ((K_rec as Const ("Record.K_record",_))$
1.128 ((sel as Const (s,_))$r)) =
1.129 if (unsuffix updateN u) = s andalso (seed s sprout) = r
1.130 @@ -1074,17 +1074,17 @@
1.131
1.132 fun init_seed r = ((r,Bound 0), [("r", rT)]);
1.133
1.134 - fun add (n:string) f fmaps =
1.135 + fun add (n:string) f fmaps =
1.136 (case AList.lookup (op =) fmaps n of
1.137 NONE => AList.update (op =) (n,[f]) fmaps
1.138 - | SOME fs => AList.update (op =) (n,f::fs) fmaps)
1.139 + | SOME fs => AList.update (op =) (n,f::fs) fmaps)
1.140
1.141 - fun comps (n:string) T fmaps =
1.142 + fun comps (n:string) T fmaps =
1.143 (case AList.lookup (op =) fmaps n of
1.144 - SOME fs =>
1.145 + SOME fs =>
1.146 foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
1.147 | NONE => error ("record_upd_simproc.comps"))
1.148 -
1.149 +
1.150 (* mk_updterm returns either
1.151 * - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
1.152 * where vars are the bound variables in the skeleton
1.153 @@ -1119,7 +1119,7 @@
1.154 val kv = (n, kT);
1.155 val kb = Bound (length vars);
1.156 val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
1.157 - in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
1.158 + in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
1.159 end)
1.160 else
1.161 (case rest (u::already) r of
1.162 @@ -1149,7 +1149,7 @@
1.163 val kv = (n, kT)
1.164 val kb = Bound (length vars)
1.165 val (sprout',vars') = grow u uT k kT (kv::vars) sprout
1.166 - val fmaps' = add n kb fmaps
1.167 + val fmaps' = add n kb fmaps
1.168 in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
1.169 ,vars',fmaps',sprout') end))
1.170 end
1.171 @@ -1161,7 +1161,7 @@
1.172 => SOME (prove_split_simp thy ss rT
1.173 (list_all(vars,(equals rT$trm$trm'))))
1.174 | _ => NONE)
1.175 - end
1.176 + end
1.177 | _ => NONE))
1.178 end
1.179
1.180 @@ -1625,7 +1625,7 @@
1.181 val refls = map mkrefl fields_more;
1.182 val dest_convs' = map mk_meta_eq dest_convs;
1.183 val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
1.184 -
1.185 +
1.186 val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
1.187
1.188 fun mkthm (udef,(fld_refl,thms)) =
1.189 @@ -1664,7 +1664,7 @@
1.190 val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
1.191
1.192
1.193 - val (([inject',induct',cases',surjective',split_meta'],
1.194 + val (([inject',induct',cases',surjective',split_meta'],
1.195 [dest_convs',upd_convs']),
1.196 thm_thy) =
1.197 defs_thy
1.198 @@ -1915,7 +1915,7 @@
1.199 ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
1.200 ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
1.201 [make_spec, fields_spec, extend_spec, truncate_spec])
1.202 - |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
1.203 + |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
1.204 fold Code.add_default_func sel_defs
1.205 #> fold Code.add_default_func upd_defs
1.206 #> fold Code.add_default_func derived_defs
1.207 @@ -2276,12 +2276,10 @@
1.208 P.type_args -- P.name --
1.209 (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
1.210
1.211 -val recordP =
1.212 +val _ =
1.213 OuterSyntax.command "record" "define extensible record" K.thy_decl
1.214 (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
1.215
1.216 -val _ = OuterSyntax.add_parsers [recordP];
1.217 -
1.218 end;
1.219
1.220 end;