# HG changeset patch # User wenzelm # Date 921674954 -3600 # Node ID 45bb139e6ceb5f5156a611402d8e71728ce2db2f # Parent 8b0c9205da75870489c4412f4f06c7de6a197509 actually check non-emptiness theorem; added typedef_proof(_i); 'typedef' outer syntax; diff -r 8b0c9205da75 -r 45bb139e6ceb src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Wed Mar 17 13:47:34 1999 +0100 +++ b/src/HOL/Tools/typedef_package.ML Wed Mar 17 13:49:14 1999 +0100 @@ -3,22 +3,20 @@ Author: Markus Wenzel, TU Muenchen Gordon/HOL-style type definitions. - -TODO: - - typedefP: elim witness; *) signature TYPEDEF_PACKAGE = sig val quiet_mode: bool ref val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory - val prove_nonempty: cterm -> thm list -> tactic option -> thm val add_typedef: string -> bstring * string list * mixfix -> string -> string list -> thm list -> tactic option -> theory -> theory val add_typedef_i: string -> bstring * string list * mixfix -> term -> string list -> thm list -> tactic option -> theory -> theory val add_typedef_i_no_def: string -> bstring * string list * mixfix -> term -> string list -> thm list -> tactic option -> theory -> theory + val typedef_proof: string -> bstring * string list * mixfix -> string -> theory -> ProofHistory.T + val typedef_proof_i: string -> bstring * string list * mixfix -> term -> theory -> ProofHistory.T end; structure TypedefPackage: TYPEDEF_PACKAGE = @@ -49,44 +47,65 @@ fun message s = if ! quiet_mode then () else writeln s; -(* prove non-emptyness of a set *) (*exception ERROR*) - -val is_def = Logic.is_equals o #prop o rep_thm; +(* non-emptiness of set *) (*exception ERROR*) -fun prove_nonempty cset thms usr_tac = +fun check_nonempty cset thm = let - val {T = setT, t = set, maxidx, sign} = rep_cterm cset; + val {t, sign, maxidx, ...} = Thm.rep_cterm cset; + val {prop, ...} = Thm.rep_thm (Thm.transfer_sg sign (Drule.standard thm)); + val matches = Pattern.matches (Sign.tsig_of sign); + in + (case try (HOLogic.dest_mem o HOLogic.dest_Trueprop) prop of + None => raise ERROR + | Some (_, A) => if matches (Logic.incr_indexes ([], maxidx) A, t) then () else raise ERROR) + end handle ERROR => error ("Bad non-emptiness theorem " ^ Display.string_of_thm thm ^ + "\nfor set " ^ quote (Display.string_of_cterm cset)); + +fun goal_nonempty cset = + let + val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset; val T = HOLogic.dest_setT setT; - val goal = cterm_of sign - (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), set))); + in Thm.cterm_of sign (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), A))) end; + +fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) = + let + val is_def = Logic.is_equals o #prop o Thm.rep_thm; + val thms = PureThy.get_thmss thy witn_names @ witn_thms; val tac = TRY (rewrite_goals_tac (filter is_def thms)) THEN TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN - if_none usr_tac (TRY (ALLGOALS (CLASET' blast_tac))); + if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac))); in - prove_goalw_cterm [] goal (K [tac]) - end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset)); + message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); + prove_goalw_cterm [] (goal_nonempty cset) (K [tac]) + end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset)); -(* gen_add_typedef *) +(* prepare_typedef *) + +fun read_term sg used s = + #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar)); -fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set thm_names thms usr_tac thy = +fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg; + +fun err_in_typedef name = + error ("The error(s) above occurred in typedef " ^ quote name); + +fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy = let val _ = Theory.requires thy "Set" "typedefs"; - val sign = sign_of thy; + val sign = Theory.sign_of thy; val full_name = Sign.full_name sign; (*rhs*) - val cset = prep_term sign raw_set; - val {T = setT, t = set, ...} = rep_cterm cset; + val cset = prep_term sign vs raw_set; + val {T = setT, t = set, ...} = Thm.rep_cterm cset; val rhs_tfrees = term_tfrees set; val oldT = HOLogic.dest_setT setT handle TYPE _ => error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT)); (*lhs*) - val lhs_tfrees = - map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; - + val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; val tname = Syntax.type_name t mx; val newT = Type (full_name tname, map TFree lhs_tfrees); @@ -105,6 +124,23 @@ val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, set')), HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old))); + (*theory extender*) + fun do_typedef theory = + theory + |> Theory.assert_super thy + |> add_typedecls [(t, vs, mx)] + |> Theory.add_consts_i + ((if no_def then [] else [(name, setT, NoSyn)]) @ + [(Rep_name, newT --> oldT, NoSyn), + (Abs_name, oldT --> newT, NoSyn)]) + |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes) + [Logic.mk_defpair (setC, set)]) + |> (PureThy.add_axioms_i o map Thm.no_attributes) + [(Rep_name, rep_type), + (Rep_name ^ "_inverse", rep_type_inv), + (Abs_name ^ "_inverse", abs_type_inv)] + handle ERROR => err_in_typedef name; + (* errors *) @@ -128,65 +164,66 @@ val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; in - if null errs then () - else error (cat_lines errs); - - message ("Proving nonemptiness of " ^ quote name ^ " ..."); - prove_nonempty cset (PureThy.get_thmss thy thm_names @ thms) usr_tac; - - thy - |> PureThy.add_typedecls [(t, vs, mx)] - |> Theory.add_arities_i - [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)] - |> Theory.add_consts_i - ((if no_def then [] else [(name, setT, NoSyn)]) @ - [(Rep_name, newT --> oldT, NoSyn), - (Abs_name, oldT --> newT, NoSyn)]) - |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes) - [(name ^ "_def", Logic.mk_equals (setC, set))]) - |> (PureThy.add_axioms_i o map Thm.no_attributes) - [(Rep_name, rep_type), - (Rep_name ^ "_inverse", rep_type_inv), - (Abs_name ^ "_inverse", abs_type_inv)] - end handle ERROR => error ("The error(s) above occurred in typedef " ^ quote name); + if null errs then () else error (cat_lines errs); + (cset, do_typedef) + end handle ERROR => err_in_typedef name; -(* external interfaces *) +(* add_typedef interfaces *) -fun read_term sg str = - read_cterm sg (str, HOLogic.termTVar); - -fun cert_term sg tm = - cterm_of sg tm handle TERM (msg, _) => error msg; +fun gen_add_typedef prep_term no_def name typ set names thms tac thy = + let + val (cset, do_typedef) = prepare_typedef prep_term no_def name typ set thy; + val result = prove_nonempty thy cset (names, thms, tac); + in check_nonempty cset result; thy |> do_typedef end; val add_typedef = gen_add_typedef read_term false; val add_typedef_i = gen_add_typedef cert_term false; val add_typedef_i_no_def = gen_add_typedef cert_term true; -(* outer syntax *) +(* typedef_proof interface *) + +fun typedef_attribute cset do_typedef (thy, thm) = + (check_nonempty cset thm; (thy |> do_typedef, thm)); -open OuterParse; +fun gen_typedef_proof prep_term name typ set thy = + let + val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy; + val goal = Thm.term_of (goal_nonempty cset); + in + thy + |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) + end; + +val typedef_proof = gen_typedef_proof read_term; +val typedef_proof_i = gen_typedef_proof cert_term; + +(** outer syntax **) + +local open OuterParse in + val typedeclP = - OuterSyntax.parser false "typedecl" "HOL type declaration" - ((type_args -- name -- opt_mixfix) >> (fn ((vs, t), mx) => + OuterSyntax.command "typedecl" "HOL type declaration" + (type_args -- name -- opt_mixfix >> (fn ((vs, t), mx) => Toplevel.theory (add_typedecls [(t, vs, mx)]))); -val opt_witness = - Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) []; +val typedef_proof_decl = + Scan.option ($$$ "(" |-- name --| $$$ ")") -- + (type_args -- name) -- opt_infix -- ($$$ "=" |-- term); -val typedef_decl = - Scan.option ($$$ "(" |-- name --| $$$ ")") -- - (type_args -- name) -- opt_infix -- ($$$ "=" |-- term -- opt_witness); +fun mk_typedef_proof (((opt_name, (vs, t)), mx), A) = + typedef_proof (if_none opt_name (Syntax.type_name t mx)) (t, vs, mx) A; val typedefP = - OuterSyntax.parser false "typedef" "HOL type definition" - (typedef_decl >> (fn (((opt_name, (vs, t)), mx), (A, witn)) => - Toplevel.theory (add_typedef (if_none opt_name t) (t, vs, mx) A witn [] None))); - + OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" + (typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof))); val _ = OuterSyntax.add_parsers [typedeclP, typedefP]; end; + + +end;