recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e;
tuned;
1 (* Title: HOL/Tools/record.ML
2 Author: Wolfgang Naraschewski, TU Muenchen
3 Author: Markus Wenzel, TU Muenchen
4 Author: Norbert Schirmer, TU Muenchen
5 Author: Thomas Sewell, NICTA
7 Extensible records with structural subtyping.
12 val print_type_abbr: bool Unsynchronized.ref
13 val print_type_as_fields: bool Unsynchronized.ref
14 val timing: bool Unsynchronized.ref
17 {args: (string * sort) list,
18 parent: (typ list * string) option,
19 fields: (string * typ) list,
20 extension: (string * typ list),
21 ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
22 select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
23 fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
24 surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
25 cases: thm, simps: thm list, iffs: thm list}
26 val get_info: theory -> string -> info option
27 val the_info: theory -> string -> info
28 val get_hierarchy: theory -> (string * typ list) -> (string * (string * typ) list) list
29 val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
30 (binding * typ * mixfix) list -> theory -> theory
32 val last_extT: typ -> (string * typ list) option
33 val dest_recTs: typ -> (string * typ list) list
34 val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
35 val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
36 val get_parent: theory -> string -> (typ list * string) option
37 val get_extension: theory -> string -> (string * typ list) option
38 val get_extinjects: theory -> thm list
39 val get_simpset: theory -> simpset
41 val eq_simproc: simproc
42 val upd_simproc: simproc
43 val split_simproc: (term -> int) -> simproc
44 val ex_sel_eq_simproc: simproc
45 val split_tac: int -> tactic
46 val split_simp_tac: thm list -> (term -> int) -> int -> tactic
47 val split_wrapper: string * wrapper
52 val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
53 val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
54 val setup: theory -> theory
58 signature ISO_TUPLE_SUPPORT =
60 val add_iso_tuple_type: binding * (string * sort) list ->
61 typ * typ -> theory -> (term * term) * theory
62 val mk_cons_tuple: term * term -> term
63 val dest_cons_tuple: term -> term * term
64 val iso_tuple_intros_tac: int -> tactic
65 val named_cterm_instantiate: (string * cterm) list -> thm -> thm
68 structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
71 val isoN = "_Tuple_Iso";
73 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
74 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
76 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
78 fun named_cterm_instantiate values thm = (* FIXME eliminate *)
80 fun match name ((name', _), _) = name = name';
82 (case find_first (match name) (Term.add_vars (prop_of thm) []) of
83 SOME var => cterm_of (theory_of_thm thm) (Var var)
84 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
86 cterm_instantiate (map (apfst getvar) values) thm
89 structure Iso_Tuple_Thms = Theory_Data
91 type T = thm Symtab.table;
92 val empty = Symtab.make [tuple_iso_tuple];
94 fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
97 fun get_typedef_info tyco vs
98 (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
102 |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
103 val proj_constr = Abs_inverse OF [exists_thm];
104 val absT = Type (tyco, map TFree vs);
107 |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
110 fun do_typedef raw_tyco repT raw_vs thy =
112 val ctxt = ProofContext.init_global thy |> Variable.declare_typ repT;
113 val vs = map (ProofContext.check_tfree ctxt) raw_vs;
114 val tac = Tactic.rtac UNIV_witness 1;
117 |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
118 (HOLogic.mk_UNIV repT) NONE tac
119 |-> (fn (tyco, info) => get_typedef_info tyco vs info)
122 fun mk_cons_tuple (left, right) =
124 val (leftT, rightT) = (fastype_of left, fastype_of right);
125 val prodT = HOLogic.mk_prodT (leftT, rightT);
126 val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
128 Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
129 Const (fst tuple_iso_tuple, isomT) $ left $ right
132 fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
133 | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
135 fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
137 val repT = HOLogic.mk_prodT (leftT, rightT);
139 val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
141 |> do_typedef b repT alphas
142 ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
144 (*construct a type and body for the isomorphism constant by
145 instantiating the theorem to which the definition will be applied*)
147 rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
148 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
149 val isomT = fastype_of body;
150 val isom_binding = Binding.suffix_name isoN b;
151 val isom_name = Sign.full_name typ_thy isom_binding;
152 val isom = Const (isom_name, isomT);
154 val ([isom_def], cdef_thy) =
156 |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
157 |> Global_Theory.add_defs false
158 [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
160 val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
161 val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
165 |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
166 |> Sign.restore_naming thy
168 ((isom, cons $ isom), thm_thy)
171 val iso_tuple_intros_tac =
172 resolve_from_net_tac iso_tuple_intros THEN'
173 CSUBGOAL (fn (cgoal, i) =>
175 val thy = Thm.theory_of_cterm cgoal;
176 val goal = Thm.term_of cgoal;
178 val isthms = Iso_Tuple_Thms.get thy;
179 fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
181 val goal' = Envir.beta_eta_contract goal;
184 Const (@{const_name Trueprop}, _) $
185 (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
186 | _ => err "unexpected goal format" goal');
188 (case Symtab.lookup isthms (#1 is) of
190 | NONE => err "no thm found for constant" (Const is));
191 in rtac isthm i end);
196 structure Record: RECORD =
199 val eq_reflection = @{thm eq_reflection};
200 val meta_allE = @{thm Pure.meta_allE};
201 val prop_subst = @{thm prop_subst};
202 val K_record_comp = @{thm K_record_comp};
203 val K_comp_convs = [@{thm o_apply}, K_record_comp];
204 val o_assoc = @{thm o_assoc};
205 val id_apply = @{thm id_apply};
206 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
207 val Not_eq_iff = @{thm Not_eq_iff};
209 val refl_conj_eq = @{thm refl_conj_eq};
211 val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
212 val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};
214 val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
215 val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
216 val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
217 val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};
219 val updacc_foldE = @{thm update_accessor_congruence_foldE};
220 val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
221 val updacc_noopE = @{thm update_accessor_noopE};
222 val updacc_noop_compE = @{thm update_accessor_noop_compE};
223 val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
224 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
225 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
227 val o_eq_dest = @{thm o_eq_dest};
228 val o_eq_id_dest = @{thm o_eq_id_dest};
229 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
233 (** name components **)
238 val schemeN = "_scheme";
239 val ext_typeN = "_ext";
240 val inner_typeN = "_inner";
242 val updateN = "_update";
244 val fields_selN = "fields";
245 val extendN = "extend";
246 val truncateN = "truncate";
253 let fun varify (a, S) = TVar ((a, midx + 1), S);
254 in map_type_tfree varify end;
259 val timing = Unsynchronized.ref false;
260 fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
261 fun timing_msg s = if ! timing then warning s else ();
266 val Trueprop = HOLogic.mk_Trueprop;
267 fun All xs t = Term.list_all_free (xs, t);
272 val op :== = Misc_Legacy.mk_defpair;
273 val op === = Trueprop o HOLogic.mk_eq;
274 val op ==> = Logic.mk_implies;
279 fun mk_ext (name, T) ts =
280 let val Ts = map fastype_of ts
281 in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
286 fun mk_selC sT (c, T) = (c, sT --> T);
288 fun mk_sel s (c, T) =
289 let val sT = fastype_of s
290 in Const (mk_selC sT (c, T)) $ s end;
295 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
297 fun mk_upd' sfx c v sT =
298 let val vT = domain_type (fastype_of v);
299 in Const (mk_updC sfx sT (c, vT)) $ v end;
301 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
306 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
307 (case try (unsuffix ext_typeN) c_ext_type of
308 NONE => raise TYPE ("Record.dest_recT", [typ], [])
309 | SOME c => ((c, Ts), List.last Ts))
310 | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
312 val is_recT = can dest_recT;
315 let val ((c, Ts), U) = dest_recT T
316 in (c, Ts) :: dest_recTs U
317 end handle TYPE _ => [];
320 let val ((c, Ts), U) = dest_recT T in
324 end handle TYPE _ => NONE;
328 val rTs = dest_recTs T;
329 val rTs' = if i < 0 then rTs else take i rTs;
330 in implode (map #1 rTs') end;
334 (*** extend theory by record definition ***)
338 (* type info and parent_info *)
341 {args: (string * sort) list,
342 parent: (typ list * string) option,
343 fields: (string * typ) list,
344 extension: (string * typ list),
352 select_convs: thm list,
353 update_convs: thm list,
354 select_defs: thm list,
355 update_defs: thm list,
356 fold_congs: thm list,
357 unfold_congs: thm list,
371 fun make_info args parent fields extension
372 ext_induct ext_inject ext_surjective ext_split ext_def
373 select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
374 surjective equality induct_scheme induct cases_scheme cases
376 {args = args, parent = parent, fields = fields, extension = extension,
377 ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
378 ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
379 update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
380 fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
381 surjective = surjective, equality = equality, induct_scheme = induct_scheme,
382 induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
386 fields: (string * typ) list,
387 extension: (string * typ list),
391 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
392 {name = name, fields = fields, extension = extension,
393 ext_def = ext_def, induct_scheme = induct_scheme};
399 {records: info Symtab.table,
401 {selectors: (int * bool) Symtab.table,
402 updates: string Symtab.table,
403 simpset: Simplifier.simpset,
404 defset: Simplifier.simpset,
405 foldcong: Simplifier.simpset,
406 unfoldcong: Simplifier.simpset},
407 equalities: thm Symtab.table,
408 extinjects: thm list,
409 extsplit: thm Symtab.table, (*maps extension name to split rule*)
410 splits: (thm * thm * thm * thm) Symtab.table, (*!!, ALL, EX - split-equalities, induct rule*)
411 extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
412 fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
415 records sel_upd equalities extinjects extsplit splits extfields fieldext =
416 {records = records, sel_upd = sel_upd,
417 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
418 extfields = extfields, fieldext = fieldext }: data;
420 structure Data = Theory_Data
424 make_data Symtab.empty
425 {selectors = Symtab.empty, updates = Symtab.empty,
426 simpset = HOL_basic_ss, defset = HOL_basic_ss,
427 foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
428 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
433 {selectors = sels1, updates = upds1,
434 simpset = ss1, defset = ds1,
435 foldcong = fc1, unfoldcong = uc1},
436 equalities = equalities1,
437 extinjects = extinjects1,
438 extsplit = extsplit1,
440 extfields = extfields1,
441 fieldext = fieldext1},
444 {selectors = sels2, updates = upds2,
445 simpset = ss2, defset = ds2,
446 foldcong = fc2, unfoldcong = uc2},
447 equalities = equalities2,
448 extinjects = extinjects2,
449 extsplit = extsplit2,
451 extfields = extfields2,
452 fieldext = fieldext2}) =
454 (Symtab.merge (K true) (recs1, recs2))
455 {selectors = Symtab.merge (K true) (sels1, sels2),
456 updates = Symtab.merge (K true) (upds1, upds2),
457 simpset = Simplifier.merge_ss (ss1, ss2),
458 defset = Simplifier.merge_ss (ds1, ds2),
459 foldcong = Simplifier.merge_ss (fc1, fc2),
460 unfoldcong = Simplifier.merge_ss (uc1, uc2)}
461 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
462 (Thm.merge_thms (extinjects1, extinjects2))
463 (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
464 (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
465 Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
466 Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
467 (Symtab.merge (K true) (extfields1, extfields2))
468 (Symtab.merge (K true) (fieldext1, fieldext2));
472 (* access 'records' *)
474 val get_info = Symtab.lookup o #records o Data.get;
476 fun the_info thy name =
477 (case get_info thy name of
479 | NONE => error ("Unknown record type " ^ quote name));
481 fun put_record name info =
482 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
483 make_data (Symtab.update (name, info) records)
484 sel_upd equalities extinjects extsplit splits extfields fieldext);
487 (* access 'sel_upd' *)
489 val get_sel_upd = #sel_upd o Data.get;
491 val is_selector = Symtab.defined o #selectors o get_sel_upd;
492 val get_updates = Symtab.lookup o #updates o get_sel_upd;
493 fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
495 val get_simpset = get_ss_with_context #simpset;
496 val get_sel_upd_defs = get_ss_with_context #defset;
498 fun get_update_details u thy =
499 let val sel_upd = get_sel_upd thy in
500 (case Symtab.lookup (#updates sel_upd) u of
502 let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
503 in SOME (s, dep, ismore) end
507 fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
509 val all = names @ [more];
510 val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
511 val upds = map (suffix updateN) all ~~ all;
513 val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
514 equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
515 val data = make_data records
516 {selectors = fold Symtab.update_new sels selectors,
517 updates = fold Symtab.update_new upds updates,
518 simpset = Simplifier.addsimps (simpset, simps),
519 defset = Simplifier.addsimps (defset, defs),
520 foldcong = foldcong addcongs folds,
521 unfoldcong = unfoldcong addcongs unfolds}
522 equalities extinjects extsplit splits extfields fieldext;
523 in Data.put data thy end;
526 (* access 'equalities' *)
528 fun add_equalities name thm =
529 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
530 make_data records sel_upd
531 (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
533 val get_equalities = Symtab.lookup o #equalities o Data.get;
536 (* access 'extinjects' *)
538 fun add_extinjects thm =
539 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
540 make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
541 extsplit splits extfields fieldext);
543 val get_extinjects = rev o #extinjects o Data.get;
546 (* access 'extsplit' *)
548 fun add_extsplit name thm =
549 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
550 make_data records sel_upd equalities extinjects
551 (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
554 (* access 'splits' *)
556 fun add_splits name thmP =
557 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
558 make_data records sel_upd equalities extinjects extsplit
559 (Symtab.update_new (name, thmP) splits) extfields fieldext);
561 val get_splits = Symtab.lookup o #splits o Data.get;
564 (* parent/extension of named record *)
566 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
567 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
570 (* access 'extfields' *)
572 fun add_extfields name fields =
573 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
574 make_data records sel_upd equalities extinjects extsplit splits
575 (Symtab.update_new (name, fields) extfields) fieldext);
577 val get_extfields = Symtab.lookup o #extfields o Data.get;
579 fun get_extT_fields thy T =
581 val ((name, Ts), moreT) = dest_recT T;
583 let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *)
584 in Long_Name.implode (rev (nm :: rst)) end;
585 val midx = maxidx_of_typs (moreT :: Ts);
586 val varifyT = varifyT midx;
587 val {records, extfields, ...} = Data.get thy;
588 val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
589 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
591 val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
592 val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
593 in (fields', (more, moreT)) end;
595 fun get_recT_fields thy T =
597 val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
598 val (rest_fields, rest_more) =
599 if is_recT root_moreT then get_recT_fields thy root_moreT
600 else ([], (root_more, root_moreT));
601 in (root_fields @ rest_fields, rest_more) end;
604 (* access 'fieldext' *)
606 fun add_fieldext extname_types fields =
607 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
610 fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
611 in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
613 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
620 fun add_parents _ NONE = I
621 | add_parents thy (SOME (types, name)) =
623 fun err msg = error (msg ^ " parent record " ^ quote name);
625 val {args, parent, ...} =
626 (case get_info thy name of SOME info => info | NONE => err "Unknown");
627 val _ = if length types <> length args then err "Bad number of arguments for" else ();
629 fun bad_inst ((x, S), T) =
630 if Sign.of_sort thy (T, S) then NONE else SOME x
631 val bads = map_filter bad_inst (args ~~ types);
632 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
634 val inst = map fst args ~~ types;
635 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
636 val parent' = Option.map (apfst (map subst)) parent;
637 in cons (name, inst) #> add_parents thy parent' end;
641 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
643 fun get_parent_info thy parent =
644 add_parents thy parent [] |> map (fn (name, inst) =>
646 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
647 val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
648 val fields' = map (apsnd subst) fields;
649 val extension' = apsnd (map subst) extension;
650 in make_parent_info name fields' extension' ext_def induct_scheme end);
656 (** concrete syntax for records **)
660 fun decode_type thy t =
662 fun get_sort env xi =
663 the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
665 Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
669 (* parse translations *)
673 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
675 | field_type_tr t = raise TERM ("field_type_tr", [t]);
677 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
678 field_type_tr t :: field_types_tr u
679 | field_types_tr t = [field_type_tr t];
681 fun record_field_types_tr more ctxt t =
683 val thy = ProofContext.theory_of ctxt;
684 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
686 fun split_args (field :: fields) ((name, arg) :: fargs) =
687 if can (unsuffix name) field then
688 let val (args, rest) = split_args fields fargs
689 in (arg :: args, rest) end
690 else err ("expecting field " ^ field ^ " but got " ^ name)
691 | split_args [] (fargs as (_ :: _)) = ([], fargs)
692 | split_args (_ :: _) [] = err "expecting more fields"
693 | split_args _ _ = ([], []);
695 fun mk_ext (fargs as (name, _) :: _) =
696 (case get_fieldext thy (Sign.intern_const thy name) of
697 SOME (ext, alphas) =>
698 (case get_extfields thy ext of
701 val (fields', _) = split_last fields;
702 val types = map snd fields';
703 val (args, rest) = split_args (map fst fields') fargs;
704 val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
705 val midx = fold Term.maxidx_typ argtypes 0;
706 val varifyT = varifyT midx;
707 val vartypes = map varifyT types;
709 val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
710 handle Type.TYPE_MATCH => err "type is no proper record (extension)";
711 val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
713 map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
715 val more' = mk_ext rest;
718 (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
720 | NONE => err ("no fields defined for " ^ ext))
721 | NONE => err (name ^ " is no proper field"))
724 mk_ext (field_types_tr t)
727 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
728 | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
730 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
731 | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
734 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
735 | field_tr t = raise TERM ("field_tr", [t]);
737 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
738 | fields_tr t = [field_tr t];
740 fun record_fields_tr more ctxt t =
742 val thy = ProofContext.theory_of ctxt;
743 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
745 fun split_args (field :: fields) ((name, arg) :: fargs) =
746 if can (unsuffix name) field
748 let val (args, rest) = split_args fields fargs
749 in (arg :: args, rest) end
750 else err ("expecting field " ^ field ^ " but got " ^ name)
751 | split_args [] (fargs as (_ :: _)) = ([], fargs)
752 | split_args (_ :: _) [] = err "expecting more fields"
753 | split_args _ _ = ([], []);
755 fun mk_ext (fargs as (name, _) :: _) =
756 (case get_fieldext thy (Sign.intern_const thy name) of
758 (case get_extfields thy ext of
761 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
762 val more' = mk_ext rest;
763 in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
764 | NONE => err ("no fields defined for " ^ ext))
765 | NONE => err (name ^ " is no proper field"))
767 in mk_ext (fields_tr t) end;
769 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
770 | record_tr _ ts = raise TERM ("record_tr", ts);
772 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
773 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
776 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
777 Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
778 | field_update_tr t = raise TERM ("field_update_tr", [t]);
780 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
781 field_update_tr t :: field_updates_tr u
782 | field_updates_tr t = [field_update_tr t];
784 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
785 | record_update_tr ts = raise TERM ("record_update_tr", ts);
789 val parse_translation =
790 [(@{syntax_const "_record_update"}, record_update_tr)];
792 val advanced_parse_translation =
793 [(@{syntax_const "_record"}, record_tr),
794 (@{syntax_const "_record_scheme"}, record_scheme_tr),
795 (@{syntax_const "_record_type"}, record_type_tr),
796 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
801 (* print translations *)
803 val print_type_abbr = Unsynchronized.ref true;
804 val print_type_as_fields = Unsynchronized.ref true;
809 (* FIXME early extern (!??) *)
810 (* FIXME Syntax.free (??) *)
811 fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
813 fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
815 fun record_type_tr' ctxt t =
817 val thy = ProofContext.theory_of ctxt;
819 val T = decode_type thy t;
820 val varifyT = varifyT (Term.maxidx_of_typ T);
822 val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
826 Type (ext, args as _ :: _) =>
827 (case try (unsuffix ext_typeN) ext of
829 (case get_extfields thy ext' of
830 SOME (fields as (x, _) :: _) =>
831 (case get_fieldext thy x of
834 val (f :: fs, _) = split_last fields;
836 apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
837 val (args', more) = split_last args;
838 val alphavars = map varifyT (#1 (split_last alphas));
839 val subst = Type.raw_matches (alphavars, args') Vartab.empty;
840 val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
841 in fields'' @ strip_fields more end
842 handle Type.TYPE_MATCH => [("", T)])
848 val (fields, (_, moreT)) = split_last (strip_fields T);
849 val _ = null fields andalso raise Match;
850 val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
852 if not (! print_type_as_fields) orelse null fields then raise Match
853 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
854 else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
857 (*try to reconstruct the record name type abbreviation from
858 the (nested) extension types*)
859 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
861 val thy = ProofContext.theory_of ctxt;
862 val T = decode_type thy tm;
863 val midx = maxidx_of_typ T;
864 val varifyT = varifyT midx;
866 fun mk_type_abbr subst name args =
867 let val abbrT = Type (name, map (varifyT o TFree) args)
868 in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
870 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
872 if ! print_type_abbr then
875 if name = last_ext then
876 let val subst = match schemeT T in
877 if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
878 then mk_type_abbr subst abbr alphas
879 else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
880 end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
881 else raise Match (*give print translation of specialised record a chance*)
883 else record_type_tr' ctxt tm
888 fun record_ext_type_tr' name =
890 val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
892 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
893 in (ext_type_name, tr') end;
895 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
897 val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
899 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
900 (list_comb (Syntax.const ext_type_name, ts));
901 in (ext_type_name, tr') end;
908 (* FIXME Syntax.free (??) *)
909 fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
910 fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
912 fun record_tr' ctxt t =
914 val thy = ProofContext.theory_of ctxt;
915 val extern = Consts.extern (ProofContext.consts_of ctxt);
918 (case strip_comb t of
919 (Const (ext, _), args as (_ :: _)) =>
920 (case try (Syntax.unmark_const o unsuffix extN) ext of
922 (case get_extfields thy ext' of
925 val (f :: fs, _) = split_last (map fst fields);
926 val fields' = extern f :: map Long_Name.base_name fs;
927 val (args', more) = split_last args;
928 in (fields' ~~ args') @ strip_fields more end
929 handle ListPair.UnequalLengths => [("", t)])
934 val (fields, (_, more)) = split_last (strip_fields t);
935 val _ = null fields andalso raise Match;
936 val u = foldr1 fields_tr' (map field_tr' fields);
939 Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
940 | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
945 fun record_ext_tr' name =
947 val ext_name = Syntax.mark_const (name ^ extN);
948 fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
949 in (ext_name, tr') end;
956 fun dest_update ctxt c =
957 (case try Syntax.unmark_const c of
958 SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
961 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
962 (case dest_update ctxt c of
967 Abs (_, _, Abs (_, _, t) $ Bound 0) =>
968 if null (loose_bnos t) then SOME t else NONE
970 if null (loose_bnos t) then SOME t else NONE
975 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
976 (field_updates_tr' ctxt u)
980 | field_updates_tr' _ tm = ([], tm);
982 fun record_update_tr' ctxt tm =
983 (case field_updates_tr' ctxt tm of
984 ([], _) => raise Match
986 Syntax.const @{syntax_const "_record_update"} $ u $
987 foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
991 fun field_update_tr' name =
993 val update_name = Syntax.mark_const (name ^ updateN);
994 fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
995 | tr' _ _ = raise Match;
996 in (update_name, tr') end;
1002 (** record simprocs **)
1004 fun future_forward_prf_standard thy prf prop () =
1006 if ! quick_and_dirty then Skip_Proof.make_thm thy prop
1007 else if Goal.future_enabled () then
1008 Goal.future_result (ProofContext.init_global thy) (Goal.fork prf) prop
1010 in Drule.export_without_context thm end;
1012 fun prove_common immediate stndrd thy asms prop tac =
1015 if ! quick_and_dirty then Skip_Proof.prove
1016 else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
1017 else Goal.prove_future;
1018 val prf = prv (ProofContext.init_global thy) [] asms prop tac;
1019 in if stndrd then Drule.export_without_context prf else prf end;
1021 val prove_future_global = prove_common false;
1022 val prove_global = prove_common true;
1024 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
1025 (case get_updates thy u of
1026 SOME u_name => u_name = s
1027 | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
1030 let val T = range_type (fastype_of f)
1031 in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
1033 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
1034 | get_upd_funs _ = [];
1036 fun get_accupd_simps thy term defset =
1038 val (acc, [body]) = strip_comb term;
1039 val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
1042 (* FIXME fresh "f" (!?) *)
1043 val T = domain_type (fastype_of upd);
1044 val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
1046 if is_sel_upd_pair thy acc upd
1047 then HOLogic.mk_comp (Free ("f", T), acc)
1048 else mk_comp_id acc;
1049 val prop = lhs === rhs;
1051 Goal.prove (ProofContext.init_global thy) [] [] prop
1053 simp_tac defset 1 THEN
1054 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1055 TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
1057 if is_sel_upd_pair thy acc upd
1060 in Drule.export_without_context (othm RS dest) end;
1061 in map get_simp upd_funs end;
1063 fun get_updupd_simp thy defset u u' comp =
1065 (* FIXME fresh "f" (!?) *)
1066 val f = Free ("f", domain_type (fastype_of u));
1067 val f' = Free ("f'", domain_type (fastype_of u'));
1068 val lhs = HOLogic.mk_comp (u $ f, u' $ f');
1071 then u $ HOLogic.mk_comp (f, f')
1072 else HOLogic.mk_comp (u' $ f', u $ f);
1073 val prop = lhs === rhs;
1075 Goal.prove (ProofContext.init_global thy) [] [] prop
1077 simp_tac defset 1 THEN
1078 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1079 TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
1080 val dest = if comp then o_eq_dest_lhs else o_eq_dest;
1081 in Drule.export_without_context (othm RS dest) end;
1083 fun get_updupd_simps thy term defset =
1085 val upd_funs = get_upd_funs term;
1086 val cname = fst o dest_Const;
1087 fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
1088 fun build_swaps_to_eq _ [] swaps = swaps
1089 | build_swaps_to_eq upd (u :: us) swaps =
1091 val key = (cname u, cname upd);
1093 if Symreltab.defined swaps key then swaps
1094 else Symreltab.insert (K true) (key, getswap u upd) swaps;
1096 if cname u = cname upd then newswaps
1097 else build_swaps_to_eq upd us newswaps
1099 fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
1100 | swaps_needed (u :: us) prev seen swaps =
1101 if Symtab.defined seen (cname u)
1102 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
1103 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
1104 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
1106 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
1108 fun prove_unfold_defs thy ex_simps ex_simprs prop =
1110 val defset = get_sel_upd_defs thy;
1111 val prop' = Envir.beta_eta_contract prop;
1112 val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
1113 val (_, args) = strip_comb lhs;
1114 val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
1116 Goal.prove (ProofContext.init_global thy) [] [] prop'
1118 simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
1119 TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
1125 fun eq (s1: string) (s2: string) = (s1 = s2);
1127 fun has_field extfields f T =
1128 exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
1130 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
1131 if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
1132 | K_skeleton n T b _ = ((n, T), b);
1139 Simplify selections of an record update:
1140 (1) S (S_update k r) = k (S r)
1141 (2) S (X_update k r) = S r
1143 The simproc skips multiple updates at once, eg:
1144 S (X_update x (Y_update y (S_update k r))) = k (S r)
1146 But be careful in (2) because of the extensibility of records.
1147 - If S is a more-selector we have to make sure that the update on component
1148 X does not affect the selected subrecord.
1149 - If X is a more-selector we have to make sure that S is not in the updated
1153 Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
1154 (fn thy => fn _ => fn t =>
1156 (sel as Const (s, Type (_, [_, rangeS]))) $
1157 ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
1158 if is_selector thy s andalso is_some (get_updates thy u) then
1160 val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
1162 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
1163 (case Symtab.lookup updates u of
1167 (case mk_eq_terms r of
1172 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1173 in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
1174 | SOME (trm, trm', vars) =>
1176 val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
1177 in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
1178 else if has_field extfields u_name rangeS orelse
1179 has_field extfields s (domain_type kT) then NONE
1181 (case mk_eq_terms r of
1182 SOME (trm, trm', vars) =>
1183 let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
1184 in SOME (upd $ kb $ trm, trm', kv :: vars) end
1189 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1190 in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
1191 | mk_eq_terms _ = NONE;
1193 (case mk_eq_terms (upd $ k $ r) of
1194 SOME (trm, trm', vars) =>
1196 (prove_unfold_defs thy [] []
1197 (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
1203 fun get_upd_acc_cong_thm upd acc thy simpset =
1205 val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
1206 val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
1208 Goal.prove (ProofContext.init_global thy) [] [] prop
1210 simp_tac simpset 1 THEN
1211 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1212 TRY (resolve_tac [updacc_cong_idI] 1))
1218 (*Simplify multiple updates:
1219 (1) "N_update y (M_update g (N_update x (M_update f r))) =
1220 (N_update (y o x) (M_update (g o f) r))"
1221 (2) "r(|M:= M r|) = r"
1223 In both cases "more" updates complicate matters: for this reason
1224 we omit considering further updates if doing so would introduce
1225 both a more update and an update to a field within it.*)
1227 Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
1228 (fn thy => fn _ => fn t =>
1230 (*We can use more-updators with other updators as long
1231 as none of the other updators go deeper than any more
1232 updator. min here is the depth of the deepest other
1233 updator, max the depth of the shallowest more updator.*)
1234 fun include_depth (dep, true) (min, max) =
1236 then SOME (min, if dep <= max orelse max = ~1 then dep else max)
1238 | include_depth (dep, false) (min, max) =
1239 if dep <= max orelse max = ~1
1240 then SOME (if min <= dep then dep else min, max)
1243 fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
1244 (case get_update_details u thy of
1245 SOME (s, dep, ismore) =>
1246 (case include_depth (dep, ismore) (min, max) of
1247 SOME (min', max') =>
1248 let val (us, bs, _) = getupdseq tm min' max'
1249 in ((upd, s, f) :: us, bs, fastype_of term) end
1250 | NONE => ([], term, HOLogic.unitT))
1251 | NONE => ([], term, HOLogic.unitT))
1252 | getupdseq term _ _ = ([], term, HOLogic.unitT);
1254 val (upds, base, baseT) = getupdseq t 0 ~1;
1256 fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
1257 if s = s' andalso null (loose_bnos tm')
1258 andalso subst_bound (HOLogic.unit, tm') = tm
1259 then (true, Abs (n, T, Const (s', T') $ Bound 1))
1260 else (false, HOLogic.unit)
1261 | is_upd_noop _ _ _ = (false, HOLogic.unit);
1263 fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
1265 val ss = get_sel_upd_defs thy;
1266 val uathm = get_upd_acc_cong_thm upd acc thy ss;
1268 [Drule.export_without_context (uathm RS updacc_noopE),
1269 Drule.export_without_context (uathm RS updacc_noop_compE)]
1272 (*If f is constant then (f o g) = f. We know that K_skeleton
1273 only returns constant abstractions thus when we see an
1274 abstraction we can discard inner updates.*)
1275 fun add_upd (f as Abs _) fs = [f]
1276 | add_upd f fs = (f :: fs);
1278 (*mk_updterm returns
1279 (orig-term-skeleton, simplified-skeleton,
1280 variables, duplicate-updates, simp-flag, noop-simps)
1282 where duplicate-updates is a table used to pass upward
1283 the list of update functions which can be composed
1284 into an update above them, simp-flag indicates whether
1285 any simplification was achieved, and noop-simps are
1286 used for eliminating case (2) defined above*)
1287 fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
1289 val (lhs, rhs, vars, dups, simp, noops) =
1290 mk_updterm upds (Symtab.update (u, ()) above) term;
1292 K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
1293 val (isnoop, skelf') = is_upd_noop s f term;
1294 val funT = domain_type T;
1295 fun mk_comp_local (f, f') =
1296 Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
1299 (upd $ skelf' $ lhs, rhs, vars,
1300 Symtab.update (u, []) dups, true,
1301 if Symtab.defined noops u then noops
1302 else Symtab.update (u, get_noop_simps upd skelf') noops)
1303 else if Symtab.defined above u then
1304 (upd $ skelf $ lhs, rhs, fvar :: vars,
1305 Symtab.map_default (u, []) (add_upd skelf) dups,
1308 (case Symtab.lookup dups u of
1311 upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
1312 fvar :: vars, dups, true, noops)
1313 | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
1315 | mk_updterm [] _ _ =
1316 (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
1317 | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
1319 val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
1320 val noops' = maps snd (Symtab.dest noops);
1324 (prove_unfold_defs thy noops' [simproc]
1325 (list_all (vars, Logic.mk_equals (lhs, rhs))))
1334 (*Look up the most specific record-equality.
1337 Testing equality of records boils down to the test of equality of all components.
1338 Therefore the complexity is: #components * complexity for single component.
1339 Especially if a record has a lot of components it may be better to split up
1340 the record first and do simplification on that (split_simp_tac).
1341 e.g. r(|lots of updates|) = x
1343 eq_simproc split_simp_tac
1344 Complexity: #components * #updates #updates
1347 Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
1348 (fn thy => fn _ => fn t =>
1349 (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
1350 (case rec_id ~1 T of
1353 (case get_equalities thy name of
1355 | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
1361 (*Split quantified occurrences of records, for which P holds. P can peek on the
1362 subterm starting at the quantified occurrence of the record (including the quantifier):
1363 P t = 0: do not split
1364 P t = ~1: completely split
1365 P t > 0: split up to given bound of record extensions.*)
1366 fun split_simproc P =
1367 Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
1368 (fn thy => fn _ => fn t =>
1370 Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
1371 if quantifier = @{const_name all} orelse
1372 quantifier = @{const_name All} orelse
1373 quantifier = @{const_name Ex}
1375 (case rec_id ~1 T of
1378 let val split = P t in
1380 (case get_splits thy (rec_id split T) of
1382 | SOME (all_thm, All_thm, Ex_thm, _) =>
1385 @{const_name all} => all_thm
1386 | @{const_name All} => All_thm RS eq_reflection
1387 | @{const_name Ex} => Ex_thm RS eq_reflection
1388 | _ => error "split_simproc"))
1394 val ex_sel_eq_simproc =
1395 Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
1396 (fn thy => fn ss => fn t =>
1399 prove_global true thy [] prop
1400 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1401 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
1403 fun mkeq (lr, Teq, (sel, Tsel), x) i =
1404 if is_selector thy sel then
1407 if not (loose_bvar1 (x, 0))
1408 then Free ("x" ^ string_of_int i, range_type Tsel)
1409 else raise TERM ("", [x]);
1410 val sel' = Const (sel, Tsel) $ Bound 0;
1411 val (l, r) = if lr then (sel', x') else (x', sel');
1412 in Const (@{const_name HOL.eq}, Teq) $ l $ r end
1413 else raise TERM ("", [Const (sel, Tsel)]);
1415 fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
1416 (true, Teq, (sel, Tsel), X)
1417 | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
1418 (false, Teq, (sel, Tsel), X)
1419 | dest_sel_eq _ = raise TERM ("", []);
1422 Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
1424 val eq = mkeq (dest_sel_eq t) 0;
1426 list_all ([("r", T)],
1428 (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
1429 in SOME (prove prop) end
1430 handle TERM _ => NONE)
1435 (* split_simp_tac *)
1437 (*Split (and simplify) all records in the goal for which P holds.
1438 For quantified occurrences of a record
1439 P can peek on the whole subterm (including the quantifier); for free variables P
1440 can only peek on the variable itself.
1441 P t = 0: do not split
1442 P t = ~1: completely split
1443 P t > 0: split up to given bound of record extensions.*)
1444 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
1446 val thy = Thm.theory_of_cterm cgoal;
1448 val goal = term_of cgoal;
1449 val frees = filter (is_recT o #2) (Term.add_frees goal []);
1451 val has_rec = exists_Const
1452 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1453 (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
1457 fun mk_split_free_tac free induct_thm i =
1459 val cfree = cterm_of thy free;
1460 val _$ (_ $ r) = concl_of induct_thm;
1461 val crec = cterm_of thy r;
1462 val thm = cterm_instantiate [(crec, cfree)] induct_thm;
1464 simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
1466 simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
1469 val split_frees_tacs =
1470 frees |> map_filter (fn (x, T) =>
1471 (case rec_id ~1 T of
1475 val free = Free (x, T);
1479 (case get_splits thy (rec_id split T) of
1481 | SOME (_, _, _, induct_thm) =>
1482 SOME (mk_split_free_tac free induct_thm i))
1486 val simprocs = if has_rec goal then [split_simproc P] else [];
1487 val thms' = K_comp_convs @ thms;
1489 EVERY split_frees_tacs THEN
1490 Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
1496 (*Split all records in the goal, which are quantified by !! or ALL.*)
1497 val split_tac = CSUBGOAL (fn (cgoal, i) =>
1499 val goal = term_of cgoal;
1501 val has_rec = exists_Const
1502 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1503 (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
1506 fun is_all (Const (@{const_name all}, _) $ _) = ~1
1507 | is_all (Const (@{const_name All}, _) $ _) = ~1
1510 if has_rec goal then
1511 Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
1518 val split_name = "record_split_tac";
1519 val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
1523 (** theory extender interface **)
1525 (* prepare arguments *)
1527 fun read_typ ctxt raw_T env =
1529 val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
1530 val T = Syntax.read_typ ctxt' raw_T;
1531 val env' = OldTerm.add_typ_tfrees (T, env);
1534 fun cert_typ ctxt raw_T env =
1536 val thy = ProofContext.theory_of ctxt;
1537 val T = Type.no_tvars (Sign.certify_typ thy raw_T)
1538 handle TYPE (msg, _, _) => error msg;
1539 val env' = OldTerm.add_typ_tfrees (T, env);
1545 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
1546 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
1547 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
1552 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
1554 (*Do case analysis / induction according to rule on last parameter of ith subgoal
1555 (or on s if there are no parameters).
1556 Instatiation of record variable (and predicate) in rule is calculated to
1557 avoid problems with higher order unification.*)
1558 fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
1560 val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
1562 val g = Thm.term_of cgoal;
1563 val params = Logic.strip_params g;
1564 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
1565 val rule' = Thm.lift_rule cgoal rule;
1566 val (P, ys) = strip_comb (HOLogic.dest_Trueprop
1567 (Logic.strip_assums_concl (prop_of rule')));
1568 (*ca indicates if rule is a case analysis or induction rule*)
1570 (case rev (drop (length params) ys) of
1571 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
1572 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
1573 | [x] => (head_of x, false));
1576 (map (pairself cert)
1579 (case AList.lookup (op =) (Term.add_frees g []) s of
1580 NONE => error "try_param_tac: no such variable"
1581 | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1583 [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1584 (x, list_abs (params, Bound 0))])) rule';
1585 in compose_tac (false, rule'', nprems_of rule) i end);
1588 fun extension_definition name fields alphas zeta moreT more vars thy =
1590 val base_name = Long_Name.base_name name;
1592 val fieldTs = map snd fields;
1593 val fields_moreTs = fieldTs @ [moreT];
1595 val alphas_zeta = alphas @ [zeta];
1597 val ext_binding = Binding.name (suffix extN base_name);
1598 val ext_name = suffix extN name;
1599 val ext_tyco = suffix ext_typeN name
1600 val extT = Type (ext_tyco, map TFree alphas_zeta);
1601 val ext_type = fields_moreTs ---> extT;
1604 (* the tree of new types that will back the record extension *)
1606 val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
1608 fun mk_iso_tuple (left, right) (thy, i) =
1610 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
1611 val ((_, cons), thy') = thy
1612 |> Iso_Tuple_Support.add_iso_tuple_type
1613 (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
1614 (fastype_of left, fastype_of right);
1616 (cons $ left $ right, (thy', i + 1))
1619 (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
1620 fun mk_even_iso_tuple [arg] = pair arg
1621 | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
1623 fun build_meta_tree_type i thy vars more =
1624 let val len = length vars in
1625 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
1626 else if len > 16 then
1629 | group16 xs = take 16 xs :: group16 (drop 16 xs);
1630 val vars' = group16 vars;
1631 val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
1633 build_meta_tree_type i' thy' composites more
1636 let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
1640 val _ = timing_msg "record extension preparing definitions";
1643 (* 1st stage part 1: introduce the tree of new types *)
1645 fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
1646 val (ext_body, typ_thy) =
1647 timeit_msg "record extension nested type def:" get_meta_tree;
1650 (* prepare declarations and definitions *)
1652 (* 1st stage part 2: define the ext constant *)
1654 fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
1655 val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
1659 |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
1660 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1661 ||> Theory.checkpoint
1662 val ([ext_def], defs_thy) =
1663 timeit_msg "record extension constructor def:" mk_defs;
1666 (* prepare propositions *)
1668 val _ = timing_msg "record extension preparing propositions";
1669 val vars_more = vars @ [more];
1670 val variants = map (fn Free (x, _) => x) vars_more;
1671 val ext = mk_ext vars_more;
1672 val s = Free (rN, extT);
1673 val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
1676 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1677 HOLogic.mk_conj (HOLogic.eq_const extT $
1678 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
1680 foldr1 HOLogic.mk_conj
1681 (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
1685 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
1687 val split_meta_prop =
1688 let val P = Free (Name.variant variants "P", extT --> Term.propT) in
1690 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1693 val prove_standard = prove_future_global true defs_thy;
1697 (prove_standard [] inject_prop
1699 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1701 (rtac refl_conj_eq 1 ORELSE
1702 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1705 val inject = timeit_msg "record extension inject proof:" inject_prf;
1707 (*We need a surjection property r = (| f = f r, g = g r ... |)
1708 to prove other theorems. We haven't given names to the accessors
1709 f, g etc yet however, so we generate an ext structure with
1710 free variables as all arguments and allow the introduction tactic to
1711 operate on it as far as it can. We then use Drule.export_without_context
1712 to convert the free variables into unifiable variables and unify them with
1713 (roughly) the definition of the accessor.*)
1714 fun surject_prf () =
1716 val cterm_ext = cterm_of defs_thy ext;
1717 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
1719 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1720 REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
1721 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
1722 val [halfway] = Seq.list_of (tactic1 start);
1723 val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
1727 val surject = timeit_msg "record extension surjective proof:" surject_prf;
1729 fun split_meta_prf () =
1730 prove_standard [] split_meta_prop
1733 [rtac equal_intr_rule, Goal.norm_hhf_tac,
1734 etac meta_allE, atac,
1735 rtac (prop_subst OF [surject]),
1736 REPEAT o etac meta_allE, atac]);
1737 val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
1740 let val (assm, concl) = induct_prop in
1741 prove_standard [assm] concl
1743 cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
1744 resolve_tac prems 2 THEN
1745 asm_simp_tac HOL_ss 1)
1747 val induct = timeit_msg "record extension induct proof:" induct_prf;
1749 val ([induct', inject', surjective', split_meta'], thm_thy) =
1751 |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
1752 [("ext_induct", induct),
1753 ("ext_inject", inject),
1754 ("ext_surjective", surject),
1755 ("ext_split", split_meta)]);
1758 (((ext_name, ext_type), (ext_tyco, alphas_zeta),
1759 extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
1762 fun chunks [] [] = []
1763 | chunks [] xs = [xs]
1764 | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
1766 fun chop_last [] = error "chop_last: list should not be empty"
1767 | chop_last [x] = ([], x)
1768 | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
1770 fun subst_last _ [] = error "subst_last: list should not be empty"
1771 | subst_last s [_] = [s]
1772 | subst_last s (x :: xs) = x :: subst_last s xs;
1777 (*build up the record type from the current extension tpye extT and a list
1778 of parent extensions, starting with the root of the record hierarchy*)
1779 fun mk_recordT extT =
1780 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
1783 fun obj_to_meta_all thm =
1785 fun E thm = (* FIXME proper name *)
1786 (case SOME (spec OF [thm]) handle THM _ => NONE of
1790 val th2 = Drule.forall_intr_vars th1;
1793 fun meta_to_obj_all thm =
1795 val thy = Thm.theory_of_thm thm;
1796 val prop = Thm.prop_of thm;
1797 val params = Logic.strip_params prop;
1798 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
1799 val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
1800 val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
1801 in Thm.implies_elim thm' thm end;
1804 (* code generation *)
1806 fun instantiate_random_record tyco vs extN Ts thy =
1808 val size = @{term "i::code_numeral"};
1809 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1810 val T = Type (tyco, map TFree vs);
1811 val Tm = termifyT T;
1812 val params = Name.names Name.context "x" Ts;
1813 val lhs = HOLogic.mk_random T size;
1814 val tc = HOLogic.mk_return Tm @{typ Random.seed}
1815 (HOLogic.mk_valtermify_app extN params T);
1819 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1820 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1821 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
1824 |> Class.instantiation ([tyco], vs, @{sort random})
1825 |> `(fn lthy => Syntax.check_term lthy eq)
1826 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1828 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1831 fun ensure_random_record ext_tyco vs extN Ts thy =
1833 val algebra = Sign.classes_of thy;
1834 val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
1836 if has_inst then thy
1838 (case Quickcheck_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
1840 instantiate_random_record ext_tyco (map constrain vs) extN
1841 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
1845 fun add_code ext_tyco vs extT ext simps inject thy =
1848 (HOLogic.mk_Trueprop o HOLogic.mk_eq)
1849 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
1850 Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
1852 Class.intro_classes_tac []
1853 THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
1854 THEN ALLGOALS (rtac @{thm refl});
1855 fun mk_eq thy eq_def = Simplifier.rewrite_rule
1856 [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
1857 fun mk_eq_refl thy =
1860 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1861 |> AxClass.unoverload thy;
1864 |> Code.add_datatype [ext]
1865 |> fold Code.add_default_eqn simps
1866 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
1867 |> `(fn lthy => Syntax.check_term lthy eq)
1868 |-> (fn eq => Specification.definition
1869 (NONE, (Attrib.empty_binding, eq)))
1870 |-> (fn (_, (_, eq_def)) =>
1871 Class.prove_instantiation_exit_result Morphism.thm
1872 (fn _ => fn eq_def => tac eq_def) eq_def)
1873 |-> (fn eq_def => fn thy =>
1874 thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
1875 |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
1876 |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
1882 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1884 val prefix = Binding.name_of binding;
1885 val name = Sign.full_name thy binding;
1886 val full = Sign.full_name_path thy prefix;
1888 val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
1889 val field_syntax = map #3 raw_fields;
1891 val parent_fields = maps #fields parents;
1892 val parent_chunks = map (length o #fields) parents;
1893 val parent_names = map fst parent_fields;
1894 val parent_types = map snd parent_fields;
1895 val parent_fields_len = length parent_fields;
1896 val parent_variants =
1897 Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
1898 val parent_vars = map2 (curry Free) parent_variants parent_types;
1899 val parent_len = length parents;
1901 val fields = map (apfst full) bfields;
1902 val names = map fst fields;
1903 val types = map snd fields;
1904 val alphas_fields = fold Term.add_tfreesT types [];
1905 val alphas_ext = inter (op =) alphas_fields alphas;
1906 val len = length fields;
1908 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
1909 (map (Binding.name_of o fst) bfields);
1910 val vars = map2 (curry Free) variants types;
1911 val named_vars = names ~~ vars;
1912 val idxms = 0 upto len;
1914 val all_fields = parent_fields @ fields;
1915 val all_types = parent_types @ types;
1916 val all_variants = parent_variants @ variants;
1917 val all_vars = parent_vars @ vars;
1918 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
1920 val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
1921 val moreT = TFree zeta;
1922 val more = Free (moreN, moreT);
1923 val full_moreN = full (Binding.name moreN);
1924 val bfields_more = bfields @ [(Binding.name moreN, moreT)];
1925 val fields_more = fields @ [(full_moreN, moreT)];
1926 val named_vars_more = named_vars @ [(full_moreN, more)];
1927 val all_vars_more = all_vars @ [more];
1928 val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
1931 (* 1st stage: ext_thy *)
1933 val extension_name = full binding;
1935 val ((ext, (ext_tyco, vs),
1936 extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1938 |> Sign.qualified_path false binding
1939 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1941 val _ = timing_msg "record preparing definitions";
1942 val Type extension_scheme = extT;
1943 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1944 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1945 val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
1946 val extension_id = implode extension_names;
1948 fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
1949 val rec_schemeT0 = rec_schemeT 0;
1952 let val (c, Ts) = extension in
1953 mk_recordT (map #extension (drop n parents))
1954 (Type (c, subst_last HOLogic.unitT Ts))
1960 val (args', more) = chop_last args;
1961 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
1963 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
1965 if more = HOLogic.unit
1966 then build (map_range recT (parent_len + 1))
1967 else build (map_range rec_schemeT (parent_len + 1))
1970 val r_rec0 = mk_rec all_vars_more 0;
1971 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
1973 fun r n = Free (rN, rec_schemeT n);
1975 fun r_unit n = Free (rN, recT n);
1976 val r_unit0 = r_unit 0;
1977 val w = Free (wN, rec_schemeT 0);
1980 (* print translations *)
1982 val record_ext_type_abbr_tr's =
1984 val trname = hd extension_names;
1985 val last_ext = unsuffix ext_typeN (fst extension);
1986 in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
1988 val record_ext_type_tr's =
1990 (*avoid conflict with record_type_abbr_tr's*)
1991 val trnames = if parent_len > 0 then [extension_name] else [];
1992 in map record_ext_type_tr' trnames end;
1994 val advanced_print_translation =
1995 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
1996 record_ext_type_tr's @ record_ext_type_abbr_tr's;
1999 (* prepare declarations *)
2001 val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
2002 val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
2003 val make_decl = (makeN, all_types ---> recT0);
2004 val fields_decl = (fields_selN, types ---> Type extension);
2005 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
2006 val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
2009 (* prepare definitions *)
2011 val ext_defs = ext_def :: map #ext_def parents;
2013 (*Theorems from the iso_tuple intros.
2014 By unfolding ext_defs from r_rec0 we create a tree of constructor
2015 calls (many of them Pair, but others as well). The introduction
2016 rules for update_accessor_eq_assist can unify two different ways
2017 on these constructors. If we take the complete result sequence of
2018 running a the introduction tactic, we get one theorem for each upd/acc
2019 pair, from which we can derive the bodies of our selector and
2020 updator and their convs.*)
2021 fun get_access_update_thms () =
2025 (*pick variable indices of 1 to avoid possible variable
2026 collisions with existing variables in updacc_eq_triv*)
2027 fun to_Var (Free (c, T)) = Var ((c, 1), T);
2028 in mk_rec (map to_Var all_vars_more) 0 end;
2030 val cterm_rec = cterm_of ext_thy r_rec0;
2031 val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
2032 val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
2033 val init_thm = named_cterm_instantiate insts updacc_eq_triv;
2034 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
2036 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
2037 REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
2038 val updaccs = Seq.list_of (tactic init_thm);
2040 (updaccs RL [updacc_accessor_eqE],
2041 updaccs RL [updacc_updator_eqE],
2042 updaccs RL [updacc_cong_from_eq])
2044 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
2045 timeit_msg "record getting tree access/updates:" get_access_update_thms;
2047 fun lastN xs = drop parent_fields_len xs;
2050 fun mk_sel_spec ((c, T), thm) =
2052 val (acc $ arg, _) =
2053 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2055 if arg aconv r_rec0 then ()
2056 else raise TERM ("mk_sel_spec: different arg", [arg]);
2058 Const (mk_selC rec_schemeT0 (c, T)) :== acc
2060 val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
2063 fun mk_upd_spec ((c, T), thm) =
2065 val (upd $ _ $ arg, _) =
2066 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2068 if arg aconv r_rec0 then ()
2069 else raise TERM ("mk_sel_spec: different arg", [arg]);
2070 in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
2071 val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
2073 (*derived operations*)
2075 list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
2076 mk_rec (all_vars @ [HOLogic.unit]) 0;
2078 list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
2079 mk_rec (all_vars @ [HOLogic.unit]) parent_len;
2081 Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
2082 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
2084 Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
2085 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
2088 (* 2st stage: defs_thy *)
2092 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
2093 |> Sign.restore_naming thy
2094 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
2095 |> Typedecl.abbrev_global
2096 (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
2097 |> Sign.qualified_path false binding
2098 |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
2099 (sel_decls ~~ (field_syntax @ [NoSyn]))
2100 |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
2101 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
2102 |> (Global_Theory.add_defs false o
2103 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
2104 ||>> (Global_Theory.add_defs false o
2105 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
2106 ||>> (Global_Theory.add_defs false o
2107 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
2108 [make_spec, fields_spec, extend_spec, truncate_spec]
2109 ||> Theory.checkpoint
2110 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
2111 timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
2114 (* prepare propositions *)
2115 val _ = timing_msg "record preparing propositions";
2116 val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
2117 val C = Free (Name.variant all_variants "C", HOLogic.boolT);
2118 val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
2121 val sel_conv_props =
2122 map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
2125 fun mk_upd_prop i (c, T) =
2127 val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
2128 val n = parent_fields_len + i;
2129 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
2130 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
2131 val upd_conv_props = map2 mk_upd_prop idxms fields_more;
2134 val induct_scheme_prop =
2135 All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
2137 (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
2138 Trueprop (P_unit $ r_unit0));
2141 val surjective_prop =
2142 let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
2143 in r0 === mk_rec args 0 end;
2146 val cases_scheme_prop =
2147 (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
2151 (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
2155 val split_meta_prop =
2156 let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
2158 (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
2161 val split_object_prop =
2162 let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
2163 in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
2166 let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
2167 in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
2172 val s' = Free (rN ^ "'", rec_schemeT0);
2173 fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
2174 val seleqs = map mk_sel_eq all_named_vars_more;
2175 in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
2178 (* 3rd stage: thms_thy *)
2180 fun prove stndrd = prove_future_global stndrd defs_thy;
2181 val prove_standard = prove_future_global true defs_thy;
2182 val future_forward_prf = future_forward_prf_standard defs_thy;
2184 fun prove_simp stndrd ss simps =
2185 let val tac = simp_all_tac ss simps
2186 in fn prop => prove stndrd [] prop (K tac) end;
2188 val ss = get_simpset defs_thy;
2190 fun sel_convs_prf () =
2191 map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
2192 val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
2193 fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
2194 val sel_convs_standard =
2195 timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
2197 fun upd_convs_prf () =
2198 map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
2199 val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
2200 fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
2201 val upd_convs_standard =
2202 timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
2204 fun get_upd_acc_congs () =
2206 val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
2207 val fold_ss = HOL_basic_ss addsimps symdefs;
2208 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
2209 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
2210 val (fold_congs, unfold_congs) =
2211 timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
2213 val parent_induct = Option.map #induct_scheme (try List.last parents);
2215 fun induct_scheme_prf () =
2216 prove_standard [] induct_scheme_prop
2219 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
2220 try_param_tac rN ext_induct 1,
2221 asm_simp_tac HOL_basic_ss 1]);
2222 val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
2225 let val (assm, concl) = induct_prop in
2226 prove_standard [assm] concl (fn {prems, ...} =>
2227 try_param_tac rN induct_scheme 1
2228 THEN try_param_tac "more" @{thm unit.induct} 1
2229 THEN resolve_tac prems 1)
2231 val induct = timeit_msg "record induct proof:" induct_prf;
2233 fun cases_scheme_prf () =
2235 val _ $ (Pvar $ _) = concl_of induct_scheme;
2238 [(cterm_of defs_thy Pvar, cterm_of defs_thy
2239 (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
2241 in Object_Logic.rulify (mp OF [ind, refl]) end;
2243 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
2244 val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
2247 prove_standard [] cases_prop
2249 try_param_tac rN cases_scheme 1 THEN
2250 simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
2251 val cases = timeit_msg "record cases proof:" cases_prf;
2253 fun surjective_prf () =
2255 val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps));
2256 val init_ss = HOL_basic_ss addsimps ext_defs;
2258 prove_standard [] surjective_prop
2261 [rtac surject_assist_idE 1,
2264 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
2265 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
2267 val surjective = timeit_msg "record surjective proof:" surjective_prf;
2269 fun split_meta_prf () =
2270 prove false [] split_meta_prop
2273 [rtac equal_intr_rule, Goal.norm_hhf_tac,
2274 etac meta_allE, atac,
2275 rtac (prop_subst OF [surjective]),
2276 REPEAT o etac meta_allE, atac]);
2277 val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
2278 fun split_meta_standardise () = Drule.export_without_context split_meta;
2279 val split_meta_standard =
2280 timeit_msg "record split_meta standard:" split_meta_standardise;
2282 fun split_object_prf () =
2284 val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
2285 val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
2286 val cP = cterm_of defs_thy P;
2287 val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
2288 val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
2289 val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
2290 val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
2292 Thm.assume cl (*All r. P r*) (* 1 *)
2293 |> obj_to_meta_all (*!!r. P r*)
2294 |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*)
2295 |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
2296 |> Thm.implies_intr cl (* 1 ==> 2 *)
2298 Thm.assume cr (*All n m more. P (ext n m more)*)
2299 |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
2300 |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
2301 |> meta_to_obj_all (*All r. P r*)
2302 |> Thm.implies_intr cr (* 2 ==> 1 *)
2303 in thr COMP (thl COMP iffI) end;
2306 val split_object_prf = future_forward_prf split_object_prf split_object_prop;
2307 val split_object = timeit_msg "record split_object proof:" split_object_prf;
2310 fun split_ex_prf () =
2312 val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
2313 val P_nm = fst (dest_Free P);
2314 val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
2315 val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
2316 val so'' = simplify ss so';
2318 prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
2320 val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
2322 fun equality_tac thms =
2324 val s' :: s :: eqs = rev thms;
2325 val ss' = ss addsimps (s' :: s :: sel_convs_standard);
2326 val eqs' = map (simplify ss') eqs;
2327 in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
2329 fun equality_prf () =
2330 prove_standard [] equality_prop (fn {context, ...} =>
2332 let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
2333 st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
2334 res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
2335 Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
2336 (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
2338 val equality = timeit_msg "record equality proof:" equality_prf;
2340 val ((([sel_convs', upd_convs', sel_defs', upd_defs',
2341 fold_congs', unfold_congs',
2342 splits' as [split_meta', split_object', split_ex'], derived_defs'],
2343 [surjective', equality']),
2344 [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
2346 |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
2347 [("select_convs", sel_convs_standard),
2348 ("update_convs", upd_convs_standard),
2349 ("select_defs", sel_defs),
2350 ("update_defs", upd_defs),
2351 ("fold_congs", fold_congs),
2352 ("unfold_congs", unfold_congs),
2353 ("splits", [split_meta_standard, split_object, split_ex]),
2354 ("defs", derived_defs)]
2355 ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
2356 [("surjective", surjective),
2357 ("equality", equality)]
2358 ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
2359 [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
2360 (("induct", induct), induct_type_global name),
2361 (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
2362 (("cases", cases), cases_type_global name)];
2364 val sel_upd_simps = sel_convs' @ upd_convs';
2365 val sel_upd_defs = sel_defs' @ upd_defs';
2366 val iffs = [ext_inject]
2367 val depth = parent_len + 1;
2369 val ([simps', iffs'], thms_thy') =
2371 |> Global_Theory.add_thmss
2372 [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
2373 ((Binding.name "iffs", iffs), [iff_add])];
2376 make_info alphas parent fields extension
2377 ext_induct ext_inject ext_surjective ext_split ext_def
2378 sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
2379 surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
2383 |> put_record name info
2384 |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
2385 |> add_equalities extension_id equality'
2386 |> add_extinjects ext_inject
2387 |> add_extsplit extension_name ext_split
2388 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
2389 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
2390 |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
2391 |> add_code ext_tyco vs extT ext simps' ext_inject
2392 |> Sign.restore_naming thy;
2401 fun read_parent NONE ctxt = (NONE, ctxt)
2402 | read_parent (SOME raw_T) ctxt =
2403 (case ProofContext.read_typ_abbrev ctxt raw_T of
2404 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
2405 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
2407 fun prep_field prep (x, T, mx) = (x, prep T, mx)
2409 cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x));
2411 fun read_field raw_field ctxt =
2412 let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
2413 in (field, Variable.declare_typ T ctxt) end;
2417 fun add_record quiet_mode (params, binding) raw_parent raw_fields thy =
2419 val _ = Theory.requires thy "Record" "record definitions";
2421 if quiet_mode then ()
2422 else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
2424 val ctxt = ProofContext.init_global thy;
2425 fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
2426 handle TYPE (msg, _, _) => error msg;
2431 val parent = Option.map (apfst (map cert_typ)) raw_parent
2433 cat_error msg ("The error(s) above occurred in parent record specification");
2434 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
2435 val parents = get_parent_info thy parent;
2437 val bfields = map (prep_field cert_typ) raw_fields;
2441 val name = Sign.full_name thy binding;
2442 val err_dup_record =
2443 if is_none (get_info thy name) then []
2444 else ["Duplicate definition of record " ^ quote name];
2446 val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
2447 val err_extra_frees =
2448 (case subtract (op =) params spec_frees of
2450 | extras => ["Extra free type variable(s) " ^
2451 commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
2453 val err_no_fields = if null bfields then ["No fields present"] else [];
2455 val err_dup_fields =
2456 (case duplicates Binding.eq_name (map #1 bfields) of
2458 | dups => ["Duplicate field(s) " ^ commas_quote (map Binding.str_of dups)]);
2460 val err_bad_fields =
2461 if forall (not_equal moreN o Binding.name_of o #1) bfields then []
2462 else ["Illegal field name " ^ quote moreN];
2465 err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
2466 val _ = if null errs then () else error (cat_lines errs);
2468 thy |> definition (params, binding) parent parents bfields
2470 handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
2472 fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
2474 val ctxt = ProofContext.init_global thy;
2475 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
2476 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
2477 val (parent, ctxt2) = read_parent raw_parent ctxt1;
2478 val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
2479 val params' = map (ProofContext.check_tfree ctxt3) params;
2480 in thy |> add_record quiet_mode (params', binding) parent fields end;
2488 Sign.add_trfuns ([], parse_translation, [], []) #>
2489 Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
2490 Simplifier.map_simpset (fn ss =>
2491 ss addsimprocs [simproc, upd_simproc, eq_simproc]);
2497 Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
2498 (Parse.type_args_constrained -- Parse.binding --
2499 (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
2500 Scan.repeat1 Parse.const_binding)
2501 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));