# HG changeset patch # User wenzelm # Date 1003432049 -7200 # Node ID 8fca3665d1ee165e34392d265c6d5ba69be46b64 # Parent d2421e124fa3007d01b7f389aed4464621aa3994 use abstract product type instead of datatype; diff -r d2421e124fa3 -r 8fca3665d1ee src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Oct 18 21:05:35 2001 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Oct 18 21:07:29 2001 +0200 @@ -38,11 +38,24 @@ val setup: (theory -> theory) list end; - structure RecordPackage: RECORD_PACKAGE = struct +(*** theory context references ***) + +val product_typeN = "Record.product_type"; + +val product_typeI = thm "product_typeI"; +val product_type_inject = thm "product_type_inject"; +val product_type_conv1 = thm "product_type_conv1"; +val product_type_conv2 = thm "product_type_conv2"; +val product_type_induct = thm "product_type_induct"; +val product_type_cases = thm "product_type_cases"; +val product_type_split_paired_all = thm "product_type_split_paired_all"; + + + (*** utilities ***) (* messages *) @@ -51,13 +64,19 @@ fun message s = if ! quiet_mode then () else writeln s; -(* definitions and equations *) +(* fundamental syntax *) infix 0 :== ===; val (op :==) = Logic.mk_defpair; val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; +fun lambda v t = + let val (x, T) = Term.dest_Free v + in Abs (x, T, abstract_over (v, t)) end; + +fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname); + (* proof by simplification *) @@ -81,18 +100,17 @@ val recordN = "record"; val moreN = "more"; val schemeN = "_scheme"; +val field_typeN = "_field_type"; val fieldN = "_field"; -val raw_fieldN = "_raw_field"; -val field_typeN = "_field_type"; val fstN = "_val"; val sndN = "_more"; val updateN = "_update"; val makeN = "make"; val make_schemeN = "make_scheme"; -(*see datatype package*) -val caseN = "_case"; - +(*see typedef_package.ML*) +val RepN = "Rep_"; +val AbsN = "Abs_"; (** generic operations **) @@ -103,19 +121,6 @@ | prime t = raise TERM ("prime: no free variable", [t]); -(* product case *) - -fun fst_fn T U = Abs ("x", T, Abs ("y", U, Bound 1)); -fun snd_fn T U = Abs ("x", T, Abs ("y", U, Bound 0)); - -fun mk_prod_case name f p = - let - val fT as Type ("fun", [A, Type ("fun", [B, C])]) = fastype_of f; - val pT = fastype_of p; - in Const (suffix caseN name, fT --> pT --> C) $ f $ p end; - - - (** tuple operations **) (* more type class *) @@ -134,16 +139,24 @@ | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []); +(* morphisms *) + +fun mk_Rep U (c, T) = + Const (suffix field_typeN (prefix_base RepN c), + mk_fieldT ((c, T), U) --> HOLogic.mk_prodT (T, U)); + +fun mk_Abs U (c, T) = + Const (suffix field_typeN (prefix_base AbsN c), + HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U)); + + (* constructors *) fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U)); -fun gen_mk_field sfx ((c, t), u) = +fun mk_field ((c, t), u) = let val T = fastype_of t and U = fastype_of u - in Const (suffix sfx c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end; - -val mk_field = gen_mk_field fieldN; -val mk_raw_field = gen_mk_field raw_fieldN; + in Const (suffix fieldN c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end; (* destructors *) @@ -528,121 +541,87 @@ "split record fields"); - (** internal theory extenders **) -(* field_type_defs *) +(* field_typedefs *) -fun field_type_def ((thy, simps), (name, tname, vs, T, U)) = +fun field_typedefs zeta moreT names theory = let - val full = Sign.full_name (Theory.sign_of thy); - val (thy', {simps = simps', ...}) = - thy - |> setmp DatatypePackage.quiet_mode true - (DatatypePackage.add_datatype_i true [tname] - [(vs, tname, Syntax.NoSyn, [(name, [T, U], Syntax.NoSyn)])]); - val thy'' = - thy' - |> setmp AxClass.quiet_mode true - (AxClass.add_inst_arity_i (full tname, [HOLogic.termS, moreS], moreS) [] [] None); - in (thy'', simps' @ simps) end; + val alpha = "'a"; + val aT = TFree (alpha, HOLogic.termS); + val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT)); -fun field_type_defs args thy = foldl field_type_def ((thy, []), args); + fun type_def (thy, name) = + 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; (* field_definitions *) -fun field_definitions fields names xs zeta moreT more vars named_vars thy = +fun field_definitions fields names xs alphas zeta moreT more vars named_vars thy = let val sign = Theory.sign_of thy; val base = Sign.base_name; val full_path = Sign.full_name_path sign; + val xT = TFree (variant alphas "'x", HOLogic.termS); + (* prepare declarations and definitions *) - (*field types*) - fun mk_fieldT_spec c = - (suffix raw_fieldN c, suffix field_typeN c, - ["'a", zeta], TFree ("'a", HOLogic.termS), moreT); - val fieldT_specs = map (mk_fieldT_spec o base) names; - (*field constructors*) val field_decls = map (mk_fieldC moreT) fields; - fun mk_field_spec (c, v) = - mk_field ((c, v), more) :== mk_raw_field ((c, v), more); - val field_specs = map mk_field_spec named_vars; + fun mk_field_spec ((c, T), v) = + Term.head_of (mk_field ((c, v), more)) :== + lambda v (lambda more (mk_Abs moreT (c, T) $ (HOLogic.mk_prod (v, more)))); + val field_specs = map mk_field_spec (fields ~~ vars); (*field destructors*) val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields; - fun mk_dest_spec dest f (c, T) = + fun mk_dest_spec dest sel (c, T) = let val p = Free ("p", mk_fieldT ((c, T), moreT)); - in dest p :== mk_prod_case (suffix field_typeN c) (f T moreT) p end; - val dest_specs = - map (mk_dest_spec mk_fst fst_fn) fields @ - map (mk_dest_spec mk_snd snd_fn) fields; + in Term.head_of (dest p) :== lambda p (sel (mk_Rep moreT (c, T) $ p)) end; + val dest_specs1 = map (mk_dest_spec mk_fst HOLogic.mk_fst) fields; + val dest_specs2 = map (mk_dest_spec mk_snd HOLogic.mk_snd) fields; - (* prepare theorems *) - - (*constructor injects*) - fun mk_inject_prop (c, v) = - HOLogic.mk_eq (mk_field ((c, v), more), mk_field ((c, prime v), prime more)) === - (HOLogic.conj $ HOLogic.mk_eq (v, prime v) $ HOLogic.mk_eq (more, prime more)); - val inject_props = map mk_inject_prop named_vars; + (* 1st stage: defs_thy *) - (*destructor conversions*) - fun mk_dest_prop dest dest' (c, v) = - dest (mk_field ((c, v), more)) === dest' (v, more); - val dest_props = - map (mk_dest_prop mk_fst fst) named_vars @ - map (mk_dest_prop mk_snd snd) named_vars; + val (defs_thy, (((typedefs, field_defs), dest_defs1), dest_defs2)) = + thy + |> field_typedefs zeta moreT names + |>> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls) + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) field_specs + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1 + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2; - (*surjective pairing*) - fun mk_surj_prop (c, T) = - let val p = Free ("p", mk_fieldT ((c, T), moreT)); - in p === mk_field ((c, mk_fst p), mk_snd p) end; - val surj_props = map mk_surj_prop fields; + val prod_types = map (fn (((a, b), c), d) => product_typeI OF [a, b, c, d]) + (typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2); - (* 1st stage: types_thy *) + (* 2nd stage: thms_thy *) - val (types_thy, datatype_simps) = - thy - |> field_type_defs fieldT_specs; - - - (* 2nd stage: defs_thy *) + fun make th = map (fn prod_type => Drule.standard (th OF [prod_type])) prod_types; - val (defs_thy, (field_defs, dest_defs)) = - types_thy - |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls) - |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) field_specs - |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) dest_specs; - - - (* 3rd stage: thms_thy *) - - val prove = prove_simp (Theory.sign_of defs_thy) HOL_basic_ss; - val prove_std = prove [] (field_defs @ dest_defs @ datatype_simps); - - val field_injects = map prove_std inject_props; - val dest_convs = map prove_std dest_props; - val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1] - (map Thm.symmetric field_defs @ dest_convs)) surj_props; - - fun mk_split (x, th) = SplitPairedAll.rule_params x moreN (th RS eq_reflection); - val field_splits = map2 mk_split (xs, surj_pairs); + val field_injects = make product_type_inject; + val dest_convs = make product_type_conv1 @ make product_type_conv2; + val field_splits = make product_type_split_paired_all; val thms_thy = defs_thy |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes)) [("field_defs", field_defs), - ("dest_defs", dest_defs), + ("dest_defs", dest_defs1 @ dest_defs2), ("dest_convs", dest_convs), - ("surj_pairs", surj_pairs), ("field_splits", field_splits)]; in (thms_thy, dest_convs, field_injects, field_splits) end; @@ -785,7 +764,7 @@ val (fields_thy, field_simps, field_injects, field_splits) = thy |> Theory.add_path bname - |> field_definitions fields names xs zeta moreT more vars named_vars; + |> field_definitions fields names xs alphas zeta moreT more vars named_vars; val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits); @@ -801,8 +780,8 @@ |> Theory.add_trfuns ([], [], field_tr's, []) |> (Theory.add_consts_i o map Syntax.no_syn) (sel_decls @ update_decls @ make_decls) - |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) sel_specs - |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) update_specs + |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs;