# HG changeset patch # User haftmann # Date 1280243427 -7200 # Node ID 0c15b8a655cd73eb592cb2a36acddc21c2563d2e # Parent cd67805a36b902e4f6d1874064567f32f88af9f0# Parent 3ca193a6ae5ad97ab3974b0a892720bb51c95dd0 merged diff -r cd67805a36b9 -r 0c15b8a655cd src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Tue Jul 27 14:12:35 2010 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Tue Jul 27 17:10:27 2010 +0200 @@ -125,7 +125,7 @@ fun BasicSimpTac var_names tac = simp_tac - (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc]) + (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc]) THEN_MAYBE' MaxSimpTac var_names tac; diff -r cd67805a36b9 -r 0c15b8a655cd src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Tue Jul 27 14:12:35 2010 +0200 +++ b/src/HOL/Statespace/state_fun.ML Tue Jul 27 17:10:27 2010 +0200 @@ -272,7 +272,7 @@ val ss' = (Simplifier.context ctxt ex_lookup_ss); fun prove prop = Goal.prove_global thy [] [] prop - (fn _ => record_split_simp_tac [] (K ~1) 1 THEN + (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN simp_tac ss' 1); fun mkeq (swap,Teq,lT,lo,d,n,x,s) i = diff -r cd67805a36b9 -r 0c15b8a655cd src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Jul 27 14:12:35 2010 +0200 +++ b/src/HOL/Tools/record.ML Tue Jul 27 17:10:27 2010 +0200 @@ -7,9 +7,13 @@ Extensible records with structural subtyping. *) -signature BASIC_RECORD = +signature RECORD = sig - type record_info = + val print_type_abbr: bool Unsynchronized.ref + val print_type_as_fields: bool Unsynchronized.ref + val timing: bool Unsynchronized.ref + + type info = {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, @@ -19,30 +23,11 @@ fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list, surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm, cases: thm, simps: thm list, iffs: thm list} - val get_record: theory -> string -> record_info option - val the_record: theory -> string -> record_info - val record_simproc: simproc - val record_eq_simproc: simproc - val record_upd_simproc: simproc - val record_split_simproc: (term -> int) -> simproc - val record_ex_sel_eq_simproc: simproc - val record_split_tac: int -> tactic - val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic - val record_split_name: string - val record_split_wrapper: string * wrapper - val print_record_type_abbr: bool Unsynchronized.ref - val print_record_type_as_fields: bool Unsynchronized.ref -end; - -signature RECORD = -sig - include BASIC_RECORD - val timing: bool Unsynchronized.ref - val updateN: string - val ext_typeN: string - val extN: string - val makeN: string - val moreN: string + val get_info: theory -> string -> info option + val the_info: theory -> string -> info + val add_record: bool -> (string * sort) list * binding -> (typ list * string) option -> + (binding * typ * mixfix) list -> theory -> theory + val last_extT: typ -> (string * typ list) option val dest_recTs: typ -> (string * typ list) list val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ) @@ -51,13 +36,20 @@ val get_extension: theory -> string -> (string * typ list) option val get_extinjects: theory -> thm list val get_simpset: theory -> simpset - val print_records: theory -> unit + val simproc: simproc + val eq_simproc: simproc + val upd_simproc: simproc + val split_simproc: (term -> int) -> simproc + val ex_sel_eq_simproc: simproc + val split_tac: int -> tactic + val split_simp_tac: thm list -> (term -> int) -> int -> tactic + val split_wrapper: string * wrapper + + val updateN: string + val ext_typeN: string + val extN: string val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list - val add_record: bool -> (string * sort) list * binding -> (typ list * string) option -> - (binding * typ * mixfix) list -> theory -> theory - val add_record_cmd: bool -> (string * string option) list * binding -> string option -> - (binding * string * mixfix) list -> theory -> theory val setup: theory -> theory end; @@ -339,9 +331,9 @@ (** record info **) -(* type record_info and parent_info *) - -type record_info = +(* type info and parent_info *) + +type info = {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, @@ -372,11 +364,11 @@ simps: thm list, iffs: thm list}; -fun make_record_info args parent fields extension +fun make_info args parent fields extension ext_induct ext_inject ext_surjective ext_split ext_def select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs surjective equality induct_scheme induct cases_scheme cases - simps iffs : record_info = + simps iffs : info = {args = args, parent = parent, fields = fields, extension = extension, ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective, ext_split = ext_split, ext_def = ext_def, select_convs = select_convs, @@ -399,8 +391,8 @@ (* theory data *) -type record_data = - {records: record_info Symtab.table, +type data = + {records: info Symtab.table, sel_upd: {selectors: (int * bool) Symtab.table, updates: string Symtab.table, @@ -415,17 +407,17 @@ extfields: (string * typ) list Symtab.table, (*maps extension to its fields*) fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*) -fun make_record_data +fun make_data records sel_upd equalities extinjects extsplit splits extfields fieldext = {records = records, sel_upd = sel_upd, equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, - extfields = extfields, fieldext = fieldext }: record_data; + extfields = extfields, fieldext = fieldext }: data; structure Records_Data = Theory_Data ( - type T = record_data; + type T = data; val empty = - make_record_data Symtab.empty + make_data Symtab.empty {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss, defset = HOL_basic_ss, foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss} @@ -454,7 +446,7 @@ splits = splits2, extfields = extfields2, fieldext = fieldext2}) = - make_record_data + make_data (Symtab.merge (K true) (recs1, recs2)) {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), @@ -472,32 +464,13 @@ (Symtab.merge (K true) (fieldext1, fieldext2)); ); -fun print_records thy = - let - val {records = recs, ...} = Records_Data.get thy; - val prt_typ = Syntax.pretty_typ_global thy; - - fun pretty_parent NONE = [] - | pretty_parent (SOME (Ts, name)) = - [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]]; - - fun pretty_field (c, T) = Pretty.block - [Pretty.str (Sign.extern_const thy c), Pretty.str " ::", - Pretty.brk 1, Pretty.quote (prt_typ T)]; - - fun pretty_record (name, {args, parent, fields, ...}: record_info) = - Pretty.block (Pretty.fbreaks (Pretty.block - [prt_typ (Type (name, map TFree args)), Pretty.str " = "] :: - pretty_parent parent @ map pretty_field fields)); - in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end; - (* access 'records' *) -val get_record = Symtab.lookup o #records o Records_Data.get; - -fun the_record thy name = - (case get_record thy name of +val get_info = Symtab.lookup o #records o Records_Data.get; + +fun the_info thy name = + (case get_info thy name of SOME info => info | NONE => error ("Unknown record type " ^ quote name)); @@ -505,7 +478,7 @@ let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; - val data = make_record_data (Symtab.update (name, info) records) + val data = make_data (Symtab.update (name, info) records) sel_upd equalities extinjects extsplit splits extfields fieldext; in Records_Data.put data thy end; @@ -538,7 +511,7 @@ val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong}, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; - val data = make_record_data records + val data = make_data records {selectors = fold Symtab.update_new sels selectors, updates = fold Symtab.update_new upds updates, simpset = Simplifier.addsimps (simpset, simps), @@ -551,11 +524,11 @@ (* access 'equalities' *) -fun add_record_equalities name thm thy = +fun add_equalities name thm thy = let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; - val data = make_record_data records sel_upd + val data = make_data records sel_upd (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext; in Records_Data.put data thy end; @@ -569,7 +542,7 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; val data = - make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) + make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit splits extfields fieldext; in Records_Data.put data thy end; @@ -583,19 +556,19 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; val data = - make_record_data records sel_upd equalities extinjects + make_data records sel_upd equalities extinjects (Symtab.update_new (name, thm) extsplit) splits extfields fieldext; in Records_Data.put data thy end; (* access 'splits' *) -fun add_record_splits name thmP thy = +fun add_splits name thmP thy = let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; val data = - make_record_data records sel_upd equalities extinjects extsplit + make_data records sel_upd equalities extinjects extsplit (Symtab.update_new (name, thmP) splits) extfields fieldext; in Records_Data.put data thy end; @@ -615,7 +588,7 @@ val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; val data = - make_record_data records sel_upd equalities extinjects extsplit splits + make_data records sel_upd equalities extinjects extsplit splits (Symtab.update_new (name, fields) extfields) fieldext; in Records_Data.put data thy end; @@ -655,7 +628,7 @@ val fieldext' = fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; val data = - make_record_data records sel_upd equalities extinjects + make_data records sel_upd equalities extinjects extsplit splits extfields fieldext'; in Records_Data.put data thy end; @@ -670,7 +643,7 @@ fun err msg = error (msg ^ " parent record " ^ quote name); val {args, parent, fields, extension, induct_scheme, ext_def, ...} = - (case get_record thy name of SOME info => info | NONE => err "Unknown"); + (case get_info thy name of SOME info => info | NONE => err "Unknown"); val _ = if length types <> length args then err "Bad number of arguments for" else (); fun bad_inst ((x, S), T) = @@ -837,8 +810,8 @@ (* print translations *) -val print_record_type_abbr = Unsynchronized.ref true; -val print_record_type_as_fields = Unsynchronized.ref true; +val print_type_abbr = Unsynchronized.ref true; +val print_type_as_fields = Unsynchronized.ref true; local @@ -886,7 +859,7 @@ val _ = null fields andalso raise Match; val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields); in - if not (! print_record_type_as_fields) orelse null fields then raise Match + if not (! print_type_as_fields) orelse null fields then raise Match else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT end; @@ -906,7 +879,7 @@ fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty; in - if ! print_record_type_abbr then + if ! print_type_abbr then (case last_extT T of SOME (name, _) => if name = last_ext then @@ -1175,7 +1148,7 @@ in -(* record_simproc *) +(* simproc *) (* Simplify selections of an record update: @@ -1191,7 +1164,7 @@ - If X is a more-selector we have to make sure that S is not in the updated subrecord. *) -val record_simproc = +val simproc = Simplifier.simproc @{theory HOL} "record_simp" ["x"] (fn thy => fn _ => fn t => (case t of @@ -1255,7 +1228,7 @@ end; -(* record_upd_simproc *) +(* upd_simproc *) (*Simplify multiple updates: (1) "N_update y (M_update g (N_update x (M_update f r))) = @@ -1265,7 +1238,7 @@ In both cases "more" updates complicate matters: for this reason we omit considering further updates if doing so would introduce both a more update and an update to a field within it.*) -val record_upd_simproc = +val upd_simproc = Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"] (fn thy => fn _ => fn t => let @@ -1363,7 +1336,7 @@ in if simp then SOME - (prove_unfold_defs thy noops' [record_simproc] + (prove_unfold_defs thy noops' [simproc] (list_all (vars, Logic.mk_equals (lhs, rhs)))) else NONE end); @@ -1371,7 +1344,7 @@ end; -(* record_eq_simproc *) +(* eq_simproc *) (*Look up the most specific record-equality. @@ -1379,13 +1352,13 @@ Testing equality of records boils down to the test of equality of all components. Therefore the complexity is: #components * complexity for single component. Especially if a record has a lot of components it may be better to split up - the record first and do simplification on that (record_split_simp_tac). + the record first and do simplification on that (split_simp_tac). e.g. r(|lots of updates|) = x - record_eq_simproc record_split_simp_tac + eq_simproc split_simp_tac Complexity: #components * #updates #updates *) -val record_eq_simproc = +val eq_simproc = Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"] (fn thy => fn _ => fn t => (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ => @@ -1398,14 +1371,14 @@ | _ => NONE)); -(* record_split_simproc *) +(* split_simproc *) (*Split quantified occurrences of records, for which P holds. P can peek on the subterm starting at the quantified occurrence of the record (including the quantifier): P t = 0: do not split P t = ~1: completely split P t > 0: split up to given bound of record extensions.*) -fun record_split_simproc P = +fun split_simproc P = Simplifier.simproc @{theory HOL} "record_split_simp" ["x"] (fn thy => fn _ => fn t => (case t of @@ -1427,20 +1400,20 @@ @{const_name all} => all_thm | @{const_name All} => All_thm RS eq_reflection | @{const_name Ex} => Ex_thm RS eq_reflection - | _ => error "record_split_simproc")) + | _ => error "split_simproc")) else NONE end) else NONE | _ => NONE)); -val record_ex_sel_eq_simproc = - Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"] +val ex_sel_eq_simproc = + Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"] (fn thy => fn ss => fn t => let fun prove prop = prove_global true thy [] prop (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) - addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1); + addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1); fun mkeq (lr, Teq, (sel, Tsel), x) i = if is_selector thy sel then @@ -1474,7 +1447,7 @@ end); -(* record_split_simp_tac *) +(* split_simp_tac *) (*Split (and simplify) all records in the goal for which P holds. For quantified occurrences of a record @@ -1483,7 +1456,7 @@ P t = 0: do not split P t = ~1: completely split P t > 0: split up to given bound of record extensions.*) -fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) => +fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) => let val thy = Thm.theory_of_cterm cgoal; @@ -1525,7 +1498,7 @@ else NONE end)); - val simprocs = if has_rec goal then [record_split_simproc P] else []; + val simprocs = if has_rec goal then [split_simproc P] else []; val thms' = K_comp_convs @ thms; in EVERY split_frees_tacs THEN @@ -1533,10 +1506,10 @@ end); -(* record_split_tac *) +(* split_tac *) (*Split all records in the goal, which are quantified by !! or ALL.*) -val record_split_tac = CSUBGOAL (fn (cgoal, i) => +val split_tac = CSUBGOAL (fn (cgoal, i) => let val goal = term_of cgoal; @@ -1550,15 +1523,15 @@ | is_all _ = 0; in if has_rec goal then - Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i + Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i else no_tac end); (* wrapper *) -val record_split_name = "record_split_tac"; -val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac); +val split_name = "record_split_tac"; +val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac); @@ -1842,9 +1815,9 @@ in Thm.implies_elim thm' thm end; -(* record_definition *) - -fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy = +(* definition *) + +fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy = let val prefix = Binding.name_of binding; val name = Sign.full_name thy binding; @@ -2342,7 +2315,7 @@ ((Binding.name "iffs", iffs), [iff_add])]; val info = - make_record_info alphas parent fields extension + make_info alphas parent fields extension ext_induct ext_inject ext_surjective ext_split ext_def sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs' surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs'; @@ -2351,10 +2324,10 @@ thms_thy' |> put_record name info |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs') - |> add_record_equalities extension_id equality' + |> add_equalities extension_id equality' |> add_extinjects ext_inject |> add_extsplit extension_name ext_split - |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme') + |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme') |> add_extfields extension_name (fields @ [(full_moreN, moreT)]) |> add_fieldext (extension_name, snd extension) (names @ [full_moreN]) |> Sign.restore_naming thy; @@ -2408,7 +2381,7 @@ val name = Sign.full_name thy binding; val err_dup_record = - if is_none (get_record thy name) then [] + if is_none (get_info thy name) then [] else ["Duplicate definition of record " ^ quote name]; val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) []; @@ -2433,7 +2406,7 @@ err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields; val _ = if null errs then () else error (cat_lines errs); in - thy |> record_definition (params, binding) parent parents bfields + thy |> definition (params, binding) parent parents bfields end handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding)); @@ -2456,7 +2429,7 @@ Sign.add_trfuns ([], parse_translation, [], []) #> Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #> Simplifier.map_simpset (fn ss => - ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); + ss addsimprocs [simproc, upd_simproc, eq_simproc]); (* outer syntax *) @@ -2469,6 +2442,3 @@ >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z))); end; - -structure Basic_Record: BASIC_RECORD = Record; -open Basic_Record; diff -r cd67805a36b9 -r 0c15b8a655cd src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Tue Jul 27 14:12:35 2010 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Jul 27 17:10:27 2010 +0200 @@ -331,7 +331,7 @@ (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) ML {* fun record_auto_tac (cs, ss) = - auto_tac (cs addIs [ext] addSWrapper record_split_wrapper, + auto_tac (cs addIs [ext] addSWrapper Record.split_wrapper, ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def}, @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def}, @{thm o_apply}, @{thm Let_def}]) diff -r cd67805a36b9 -r 0c15b8a655cd src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Tue Jul 27 14:12:35 2010 +0200 +++ b/src/HOL/ex/Records.thy Tue Jul 27 17:10:27 2010 +0200 @@ -249,8 +249,8 @@ text {* In some cases its convenient to automatically split (quantified) records. For this purpose there is the simproc @{ML [source] -"Record.record_split_simproc"} and the tactic @{ML [source] -"Record.record_split_simp_tac"}. The simplification procedure +"Record.split_simproc"} and the tactic @{ML [source] +"Record.split_simp_tac"}. The simplification procedure only splits the records, whereas the tactic also simplifies the resulting goal with the standard record simplification rules. A (generalized) predicate on the record is passed as parameter that @@ -259,51 +259,51 @@ the quantifier). The value @{ML "0"} indicates no split, a value greater @{ML "0"} splits up to the given bound of record extension and finally the value @{ML "~1"} completely splits the record. -@{ML [source] "Record.record_split_simp_tac"} additionally takes a list of +@{ML [source] "Record.split_simp_tac"} additionally takes a list of equations for simplification and can also split fixed record variables. *} lemma "(\r. P (xpos r)) \ (\x. P x)" apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) + (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) apply simp done lemma "(\r. P (xpos r)) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) apply simp done lemma "(\r. P (xpos r)) \ (\x. P x)" apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) + (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) apply simp done lemma "(\r. P (xpos r)) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) apply simp done lemma "\r. P (xpos r) \ (\x. P x)" apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) + (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) apply auto done lemma "\r. P (xpos r) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) apply auto done lemma "P (xpos r) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) apply auto done lemma fixes r shows "P (xpos r) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) apply auto done @@ -316,7 +316,7 @@ have "\x. P x" using pre apply - - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) apply auto done } @@ -324,13 +324,13 @@ qed text {* The effect of simproc @{ML [source] -"Record.record_ex_sel_eq_simproc"} is illustrated by the +"Record.ex_sel_eq_simproc"} is illustrated by the following lemma. *} lemma "\r. xpos r = x" apply (tactic {*simp_tac - (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*}) + (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*}) done