wneuper/isa: comparison src/HOL/Tools/record

equal deleted inserted replaced

-:6e6d9e80ebb4
+:e5b55d7be9bb
 => (let
 val flds' = but_last flds;
 val types = map snd flds';
 val (args,rest) = splitargs (map fst flds') fargs;
 val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
 val midx =  fold (fn T => fn i => Int.max (maxidx_of_typ T, i))
 argtypes 0;
 val varifyT = varifyT midx;
 val vartypes = map varifyT types;
 val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes)
 (Syntax.term_of_typ false (HOLogic.unitT));
 val adv_record_type_scheme_tr =
 gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
 val parse_translation =
 [("_record_update", record_update_tr),
 ("_update_name", update_name_tr)];
 val adv_parse_translation =
 [("_record",adv_record_tr),
 ("_record_scheme",adv_record_scheme_tr),
 ("_record_type",adv_record_type_tr),
 ("_record_type_scheme",adv_record_type_scheme_tr)];
 fun mk_type_abbr subst name alphas =
 let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas);
 in Syntax.term_of_typ (! Syntax.show_sorts)
 (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end;
 fun match rT T = (Sign.typ_match thy (varifyT rT,T)
 Vartab.empty);
 in if !print_record_type_abbr
 then (case last_extT T of
 SOME (name,_)
 val T = domain_type fT;
 val (x,T') = hd (Term.variant_frees t' [("x",T)]);
 val f_x = Free (f',fT)$(Free (x,T'));
 fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
 | is_constr _ = false;
 fun subst (t as u$w) = if Free (f',fT)=u
 then if is_constr w then f_x
 else raise TERM ("abstract_over_fun_app",[t])
 else subst u$subst w
 | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
 | subst t = t
 val t'' = abstract_over (f_x,subst t');
 val vars = strip_qnt_vars "all" t'';
 val bdy = strip_qnt_body "all" t'';
 in list_abs ((x,T')::vars,bdy) end
 | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
 (* Generates a theorem of the kind:
 * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
 *)
 fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
 let
 val rT = domain_type fT;
 val vars = Term.strip_qnt_vars "all" t;
 val Ts = map snd vars;
 val n = length vars;
 fun app_bounds 0 t = t$Bound 0
 | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
 val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
 val prop = Logic.mk_equals
 (list_all ((f,fT)::vars,
 app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
 list_all ((fst r,rT)::vars,
 app_bounds (n - 1) ((Free P)$Bound n)));
 val prove_standard = quick_and_dirty_prove true thy;
 val thm = prove_standard [] prop (fn prems =>
 	 EVERY [rtac equal_intr_rule 1,
 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
 in thm end
 | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
 (fn thy => fn _ => fn t =>
 (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
 (trm as Abs _) =>
 (case rec_id (~1) T of
 "" => NONE
 | n => if T=T'
 then (let
 val P=cterm_of thy (abstract_over_fun_app trm);
 val thm = mk_fun_apply_eq trm thy;
 val PV = cterm_of thy (hd (term_vars (prop_of thm)));
 val thm' = cterm_instantiate [(PV,P)] thm;
 in SOME  thm' end handle TERM _ => NONE)
 else NONE)
 | _ => NONE))
 end
 fun prove_split_simp thy ss T prop =
 let
 SOME (all_thm,_,_,_) =>
 all_thm::(case extsplits of [thm] => [] | _ => extsplits)
 (* [thm] is the same as all_thm *)
 | NONE => extsplits)
 val thms'=K_comp_convs@thms;
 val ss' = (Simplifier.inherit_context ss simpset
 addsimps thms'
 addsimprocs [record_split_f_more_simproc]);
 in
 quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1)
 end;
 fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) =
 (case Symtab.lookup updates u of
 NONE => NONE
 | SOME u_name
 => if u_name = s
 then (case mk_eq_terms r of
 NONE =>
 let
 val rv = ("r",rT)
 val rb = Bound 0
 val kv = ("k",kT)
 val kb = Bound 1
 then let val kv = ("k", kT);
 val kb = Bound (length vars);
 in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
 else ((sprout,skeleton),vars);
 fun is_upd_same (sprout,skeleton) u
 ((K_rec as Const ("Record.K_record",_))$
 ((sel as Const (s,_))$r)) =
 if (unsuffix updateN u) = s andalso (seed s sprout) = r
 then SOME (K_rec,sel,seed s skeleton)
 else NONE
 | is_upd_same _ _ _ = NONE
 fun init_seed r = ((r,Bound 0), [("r", rT)]);
 fun add (n:string) f fmaps =
 (case AList.lookup (op =) fmaps n of
 NONE => AList.update (op =) (n,[f]) fmaps
 | SOME fs => AList.update (op =) (n,f::fs) fmaps)
 fun comps (n:string) T fmaps =
 (case AList.lookup (op =) fmaps n of
 SOME fs =>
 foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
 | NONE => error ("record_upd_simproc.comps"))
 (* mk_updterm returns either
 *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
 *     where vars are the bound variables in the skeleton
 *  - Inter (orig-term-skeleton,simplified-term-skeleton,
 *           vars, (term-sprout, skeleton-sprout))
 let
 val n = sel_name u;
 val kv = (n, kT);
 val kb = Bound (length vars);
 val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
 end)
 else
 (case rest (u::already) r of
 Init ((sprout,skel),vars) =>
 (case is_upd_same (sprout,skel) u k of
 val n = sel_name u
 val T = domain_type kT
 val kv = (n, kT)
 val kb = Bound (length vars)
 val (sprout',vars') = grow u uT k kT (kv::vars) sprout
 val fmaps' = add n kb fmaps
 in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
 ,vars',fmaps',sprout') end))
 end
 else Init (init_seed t)
 | mk_updterm _ _ t = Init (init_seed t);
 in (case mk_updterm updates [] t of
 Inter (trm,trm',vars,_,_)
 => SOME (prove_split_simp thy ss rT
 (list_all(vars,(equals rT$trm$trm'))))
 | _ => NONE)
 end
 | _ => NONE))
 end
 (* record_eq_simproc *)
 (* looks up the most specific record-equality.
 fun mkrefl (c,T) = Thm.reflexive
 (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T)));
 val refls = map mkrefl fields_more;
 val dest_convs' = map mk_meta_eq dest_convs;
 val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
 val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
 fun mkthm (udef,(fld_refl,thms)) =
 let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms);
 (* (|N=N (|N=N,M=M,K=K,more=more|)
 rtac (prop_subst OF [surjective]) 1,
 REPEAT (etac meta_allE 1), atac 1]);
 val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
 val (([inject',induct',cases',surjective',split_meta'],
 [dest_convs',upd_convs']),
 thm_thy) =
 defs_thy
 |> (PureThy.add_thms o map Thm.no_attributes)
 [("ext_inject", inject),
 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
 |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
 ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
 ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
 [make_spec, fields_spec, extend_spec, truncate_spec])
 |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
 fold Code.add_default_func sel_defs
 #> fold Code.add_default_func upd_defs
 #> fold Code.add_default_func derived_defs
 #> pair defs)
 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
 val record_decl =
 P.type_args -- P.name --
 (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
-val recordP =
+val _ =
 OuterSyntax.command "record" "define extensible record" K.thy_decl
 (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
-val _ = OuterSyntax.add_parsers [recordP];
 end;
 end;

changeset 24867	e5b55d7be9bb
parent 24830	a7b3ab44d993
child 25070	e2a39b6526b0