# HG changeset patch # User wenzelm # Date 1004042638 -7200 # Node ID 80365073b8b31ea5d5ec38bda9ee20c287e5e1f1 # Parent c5e69470f03bd8349a9e14431e0f4832328ab0e1 removed "more" sort; refer to properly named theorems internally; diff -r c5e69470f03b -r 80365073b8b3 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Oct 25 22:43:05 2001 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Oct 25 22:43:58 2001 +0200 @@ -19,7 +19,6 @@ include BASIC_RECORD_PACKAGE val quiet_mode: bool ref val updateN: string - val moreS: sort val mk_fieldT: (string * typ) * typ -> typ val dest_fieldT: typ -> (string * typ) * typ val mk_field: (string * term) * term -> term @@ -115,6 +114,7 @@ val makeN = "make"; val extendN = "extend"; val truncateN = "truncate"; +val fieldsN = "fields"; (*see typedef_package.ML*) @@ -125,11 +125,6 @@ (** tuple operations **) -(* more type class *) - -val moreS = ["Record.more"]; - - (* types *) fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]); @@ -570,13 +565,11 @@ val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT)); fun type_def (thy, name) = - let val (thy', {type_definition, set_def = Some def, ...}) = thy - |> setmp TypedefPackage.quiet_mode true + let val (thy', {type_definition, set_def = Some def, ...}) = + thy |> setmp TypedefPackage.quiet_mode true (TypedefPackage.add_typedef_i true None (suffix field_typeN (Sign.base_name name), [alpha, zeta], Syntax.NoSyn) UNIV None (Tactic.rtac UNIV_witness 1)) - |>> setmp AxClass.quiet_mode true (AxClass.add_inst_arity_i - (suffix field_typeN name, [HOLogic.termS, moreS], moreS) all_tac) in (thy', Tactic.rewrite_rule [def] type_definition) end in foldl_map type_def (theory, names) end; @@ -630,23 +623,24 @@ fun make th = map (fn prod_type => Drule.standard (th OF [prod_type])) prod_types; + val dest_convs = make product_type_conv1 @ make product_type_conv2; val field_injects = make product_type_inject; - val dest_convs = make product_type_conv1 @ make product_type_conv2; val field_inducts = make product_type_induct; val field_cases = make product_type_cases; val field_splits = make product_type_split_paired_all; - val thms_thy = - defs_thy + val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects', + field_splits', field_inducts', field_cases']) = defs_thy |> (PureThy.add_thmss o map Thm.no_attributes) - [("field_defs", field_defs), - ("dest_defs", dest_defs1 @ dest_defs2), - ("dest_convs", dest_convs), - ("field_inducts", field_inducts), - ("field_cases", field_cases), - ("field_splits", field_splits)] |> #1; + [("field_defs", field_defs), + ("dest_defs", dest_defs1 @ dest_defs2), + ("dest_convs", dest_convs), + ("field_injects", field_injects), + ("field_splits", field_splits), + ("field_inducts", field_inducts), + ("field_cases", field_cases)]; - in (thms_thy, dest_convs, field_injects, field_splits, field_inducts, field_cases) end; + in (thms_thy, dest_convs', field_injects', field_splits', field_inducts', field_cases') end; (* record_definition *) @@ -690,7 +684,7 @@ val all_named_vars = parent_named_vars @ named_vars; val zeta = variant alphas "'z"; - val moreT = TFree (zeta, moreS); + val moreT = TFree (zeta, HOLogic.termS); val more = Free (moreN, moreT); val full_moreN = full moreN; fun more_part t = mk_more t full_moreN; @@ -864,26 +858,31 @@ [Method.insert_tac prems 1, res_inst_tac [(rN, rN)] cases_scheme 1, Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps [unit_all_eq1]) 1]); - val simps = field_simps @ sel_convs @ update_convs @ [equality]; + val (thms_thy, ([sel_convs', update_convs', sel_defs', update_defs', _], + [equality', induct_scheme', induct', cases_scheme', cases'])) = + defs_thy + |> (PureThy.add_thmss o map Thm.no_attributes) + [("select_convs", sel_convs), + ("update_convs", update_convs), + ("select_defs", sel_defs), + ("update_defs", update_defs), + ("derived_defs", derived_defs)] + |>>> PureThy.add_thms + [(("equality", equality), [Classical.xtra_intro_global]), + (("induct_scheme", induct_scheme), [RuleCases.case_names [fieldsN], + InductAttrib.induct_type_global (suffix schemeN name)]), + (("induct", induct), [RuleCases.case_names [fieldsN], + InductAttrib.induct_type_global name]), + (("cases_scheme", cases_scheme), [RuleCases.case_names [fieldsN], + InductAttrib.cases_type_global (suffix schemeN name)]), + (("cases", cases), [RuleCases.case_names [fieldsN], + InductAttrib.cases_type_global name])]; + + val simps = field_simps @ sel_convs' @ update_convs' @ [equality']; val iffs = field_injects; - val thms_thy = - defs_thy - |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes)) - [("select_defs", sel_defs), - ("update_defs", update_defs), - ("derived_defs", derived_defs), - ("select_convs", sel_convs), - ("update_convs", update_convs)] - |> (#1 oo PureThy.add_thms) - [(("equality", equality), [Classical.xtra_intro_global]), - (("induct_scheme", induct_scheme), - [InductAttrib.induct_type_global (suffix schemeN name)]), - (("induct", induct), [InductAttrib.induct_type_global name]), - (("cases_scheme", cases_scheme), - [InductAttrib.cases_type_global (suffix schemeN name)]), - (("cases", cases), [InductAttrib.cases_type_global name])] - |> (#1 oo PureThy.add_thmss) + val thms_thy' = + thms_thy |> (#1 oo PureThy.add_thmss) [(("simps", simps), [Simplifier.simp_add_global]), (("iffs", iffs), [iff_add_global])]; @@ -891,9 +890,9 @@ (* 4th stage: final_thy *) val final_thy = - thms_thy - |> put_record name (make_record_info args parent fields simps induct_scheme cases_scheme) - |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs @ update_defs) + thms_thy' + |> put_record name (make_record_info args parent fields simps induct_scheme' cases_scheme') + |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs') |> Theory.parent_path; in (final_thy, {simps = simps, iffs = iffs}) end; @@ -1039,7 +1038,6 @@ end; - end; structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;