# HG changeset patch # User wenzelm # Date 1003968688 -7200 # Node ID 96f267adc0294ab29ad5d547d9ea2079a3a925a7 # Parent e31f781611b39287ddd3ef7933b34aad3b3f038c provodes induct/cases for use with corresponding Isar methods; "record" operation (acts as type cast); internal field_inducts, field_cases; make_defs no longer declared as simps; fixed printing of fixed records; diff -r e31f781611b3 -r 96f267adc029 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Wed Oct 24 19:20:02 2001 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Oct 25 02:11:28 2001 +0200 @@ -50,6 +50,8 @@ 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"; @@ -64,26 +66,33 @@ (* fundamental syntax *) -infix 0 :== ===; - -val (op :==) = Logic.mk_defpair; -val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; - fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname); +val Trueprop = HOLogic.mk_Trueprop; +fun All xs t = Term.list_all_free (xs, t); -(* proof by simplification *) +infix 0 :== === ==>; +val (op :==) = Logic.mk_defpair; +val (op ===) = Trueprop o HOLogic.mk_eq; +val (op ==>) = Logic.mk_implies; + + +(* proof tools *) + +fun prove_goal sign goal tacs = + Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal) tacs + handle ERROR => error ("The error(s) above occurred while trying to prove " ^ + quote (Sign.string_of_term sign goal)); fun prove_simp sign ss tacs simps = let val ss' = Simplifier.addsimps (ss, simps); + fun prove goal = prove_goal sign goal + (K (tacs @ [ALLGOALS (Simplifier.asm_full_simp_tac ss')])); + in prove end; - fun prove goal = - Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal) - (K (tacs @ [ALLGOALS (Simplifier.asm_full_simp_tac ss')])) - handle ERROR => error ("The error(s) above occurred while trying to prove " - ^ quote (Sign.string_of_term sign goal)); - in prove end; +fun try_param_tac x s rule i st = + res_inst_tac [(x, (case Tactic.innermost_params i st of [] => s | (p, _) :: _ => p))] rule i st; @@ -91,7 +100,7 @@ (** name components **) -val recordN = "record"; +val rN = "r"; val moreN = "more"; val schemeN = "_scheme"; val field_typeN = "_field_type"; @@ -101,6 +110,7 @@ val updateN = "_update"; val makeN = "make"; val make_schemeN = "make_scheme"; +val recordN = "record"; (*see typedef_package.ML*) val RepN = "Rep_"; @@ -294,7 +304,8 @@ (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme"; val record_tr' = - gen_record_tr' "_fields" "_field" fieldN HOLogic.is_unit "_record" "_record_scheme"; + gen_record_tr' "_fields" "_field" fieldN + (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme"; fun record_update_tr' tm = let val (ts, u) = gen_fields_tr' "_update" updateN tm in @@ -324,12 +335,21 @@ {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, - simps: thm list}; + simps: thm list, induct: thm, cases: thm}; + +fun make_record_info args parent fields simps induct cases = + {args = args, parent = parent, fields = fields, simps = simps, + induct = induct, cases = cases}: record_info; type parent_info = {name: string, fields: (string * typ) list, - simps: thm list}; + simps: thm list, induct: thm, cases: thm}; + +fun make_parent_info name fields simps induct cases = + {name = name, fields = fields, simps = simps, + induct = induct, cases = cases}: parent_info; + (* data kind 'HOL/records' *) @@ -386,8 +406,9 @@ fun pretty_field (c, T) = Pretty.block [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)]; - fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks - (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] :: + fun pretty_record (name, {args, parent, fields, simps = _, induct = _, cases = _}) = + 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 (Sign.cond_extern_table sg Sign.typeK recs) @@ -452,7 +473,7 @@ val sign = Theory.sign_of thy; fun err msg = error (msg ^ " parent record " ^ quote name); - val {args, parent, fields, simps} = + val {args, parent, fields, simps, induct, cases} = (case get_record thy name of Some info => info | None => err "Unknown"); val _ = if length types <> length args then err "Bad number of arguments for" else (); @@ -465,13 +486,13 @@ in if not (null bads) then err ("Ill-sorted instantiation of " ^ commas bads ^ " in") - else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simps) + else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simps, induct, cases) end; fun add_parents thy (None, parents) = parents | add_parents thy (Some (types, name), parents) = - let val (pparent, pfields, psimps) = inst_record thy (types, name) - in add_parents thy (pparent, {name = name, fields = pfields, simps = psimps} :: parents) end; + let val (parent, fields, simps, induct, cases) = inst_record thy (types, name) + in add_parents thy (parent, make_parent_info name fields simps induct cases :: parents) end; @@ -610,17 +631,21 @@ 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 - |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes)) + |> (PureThy.add_thmss o map Thm.no_attributes) [("field_defs", field_defs), ("dest_defs", dest_defs1 @ dest_defs2), ("dest_convs", dest_convs), - ("field_splits", field_splits)]; + ("field_inducts", field_inducts), + ("field_cases", field_cases), + ("field_splits", field_splits)] |> #1; - in (thms_thy, dest_convs, field_injects, field_splits) end; + in (thms_thy, dest_convs, field_injects, field_splits, field_inducts, field_cases) end; (* record_definition *) @@ -637,11 +662,13 @@ val alphas = map fst args; val name = Sign.full_name sign bname; (*not made part of record name space!*) + val previous = if null parents then None else Some (last_elem parents); + val parent_fields = flat (map #fields parents); val parent_names = map fst parent_fields; val parent_types = map snd parent_fields; val parent_len = length parent_fields; - val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, recordN]); + val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]); val parent_vars = ListPair.map Free (parent_xs, parent_types); val parent_named_vars = parent_names ~~ parent_vars; @@ -649,7 +676,7 @@ val names = map fst fields; val types = map snd fields; val len = length fields; - val xs = variantlist (map fst bfields, moreN :: recordN :: parent_xs); + val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs); val vars = ListPair.map Free (xs, types); val named_vars = names ~~ vars; @@ -667,14 +694,18 @@ val full_moreN = full moreN; fun more_part t = mk_more t full_moreN; fun more_part_update t x = mk_more_update t (full_moreN, x); + val all_types_more = all_types @ [moreT]; + val all_xs_more = all_xs @ [moreN]; val parent_more = funpow parent_len mk_snd; val idxs = 0 upto (len - 1); val rec_schemeT = mk_recordT (all_fields, moreT); val rec_scheme = mk_record (all_named_vars, more); - val r = Free (recordN, rec_schemeT); val recT = mk_recordT (all_fields, HOLogic.unitT); + val rec_ = mk_record (all_named_vars, HOLogic.unit); + val r = Free (rN, rec_schemeT); + val r' = Free (rN, recT); (* prepare print translation functions *) @@ -692,6 +723,7 @@ val make_decls = [(mk_makeC rec_schemeT (make_schemeN, all_types @ [moreT])), (mk_makeC recT (makeN, all_types))]; + val record_decl = (recordN, rec_schemeT --> recT); (* prepare definitions *) @@ -722,7 +754,9 @@ val make = Const (mk_makeC recT (full makeN, all_types)); val make_specs = [list_comb (make_scheme, all_vars) $ more :== rec_scheme, - list_comb (make, all_vars) :== mk_record (all_named_vars, HOLogic.unit)]; + list_comb (make, all_vars) :== rec_]; + val record_spec = + Const (full recordN, rec_schemeT --> recT) $ r :== mk_record (all_sels, HOLogic.unit); (* prepare propositions *) @@ -746,18 +780,30 @@ (*equality*) fun mk_sel_eq (t, T) = let val t' = Term.abstract_over (r, t) - in HOLogic.mk_Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end; + in Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end; val sel_eqs = map2 mk_sel_eq (map (mk_sel r) all_names @ [more_part r], all_types @ [moreT]); val equality_prop = Term.all rec_schemeT $ (Abs ("r", rec_schemeT, Term.all rec_schemeT $ (Abs ("r'", rec_schemeT, Logic.list_implies (sel_eqs, - HOLogic.mk_Trueprop (HOLogic.eq_const rec_schemeT $ Bound 1 $ Bound 0)))))); + Trueprop (HOLogic.eq_const rec_schemeT $ Bound 1 $ Bound 0)))))); + + (*induct*) + val P = Free ("P", rec_schemeT --> HOLogic.boolT); + val P' = Free ("P", recT --> HOLogic.boolT); + val induct_scheme_prop = + All (all_xs_more ~~ all_types_more) (Trueprop (P $ rec_scheme)) ==> Trueprop (P $ r); + val induct_prop = All (all_xs ~~ all_types) (Trueprop (P' $ rec_)) ==> Trueprop (P' $ r'); + + (*cases*) + val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT)); + val cases_scheme_prop = All (all_xs_more ~~ all_types_more) ((r === rec_scheme) ==> C) ==> C; + val cases_prop = All (all_xs ~~ all_types) ((r' === rec_) ==> C) ==> C; (* 1st stage: fields_thy *) - val (fields_thy, field_simps, field_injects, field_splits) = + val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) = thy |> Theory.add_path bname |> field_definitions fields names xs alphas zeta moreT more vars named_vars; @@ -767,7 +813,7 @@ (* 2nd stage: defs_thy *) - val (defs_thy, ((sel_defs, update_defs), make_defs)) = + val (defs_thy, (((sel_defs, update_defs), make_defs), [record_def])) = fields_thy |> add_record_splits named_splits |> Theory.parent_path @@ -775,24 +821,46 @@ |> Theory.add_path bname |> Theory.add_trfuns ([], [], field_tr's, []) |> (Theory.add_consts_i o map Syntax.no_syn) - (sel_decls @ update_decls @ make_decls) + (sel_decls @ update_decls @ make_decls @ [record_decl]) |> (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; + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) [record_spec]; + + val defs_sg = Theory.sign_of defs_thy; (* 3rd stage: thms_thy *) val parent_simps = flat (map #simps parents); - val prove = prove_simp (Theory.sign_of defs_thy) HOL_basic_ss []; - val prove' = prove_simp (Theory.sign_of defs_thy) HOL_ss; + val prove = prove_simp defs_sg HOL_basic_ss []; + val prove' = prove_simp defs_sg HOL_ss; val sel_convs = map (prove (parent_simps @ sel_defs @ field_simps)) sel_props; val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props; val equality = prove' [ALLGOALS record_split_tac] (parent_simps @ sel_convs @ field_injects) equality_prop; - val simps = field_simps @ sel_convs @ update_convs @ make_defs @ [equality]; + val induct_scheme = prove_goal defs_sg induct_scheme_prop (fn prems => + (case previous of Some {induct, ...} => res_inst_tac [(rN, rN)] induct 1 + | None => all_tac) :: map (fn rule => try_param_tac "p" rN rule 1) field_inducts @ + [resolve_tac prems 1]); + + val induct = prove_goal defs_sg induct_prop (fn prems => + [res_inst_tac [(rN, rN)] induct_scheme 1, + try_param_tac "x" "more" unit_induct 1, resolve_tac prems 1]); + + val cases_scheme = prove_goal defs_sg cases_scheme_prop (fn prems => + Method.insert_tac prems 1 :: + (case previous of Some {cases, ...} => try_param_tac rN rN cases 1 + | None => all_tac) :: map (fn rule => try_param_tac "p" rN rule 1) field_cases @ + [Simplifier.asm_full_simp_tac HOL_basic_ss 1]); + + val cases = prove_goal defs_sg cases_prop (fn prems => + [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 iffs = field_injects; val thms_thy = @@ -804,7 +872,13 @@ ("select_convs", sel_convs), ("update_convs", update_convs)] |> (#1 oo PureThy.add_thms) - [(("equality", equality), [Classical.xtra_intro_global])] + [(("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) [(("simps", simps), [Simplifier.simp_add_global]), (("iffs", iffs), [iff_add_global])]; @@ -814,7 +888,7 @@ val final_thy = thms_thy - |> put_record name {args = args, parent = parent, fields = fields, simps = simps} + |> 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;