# HG changeset patch # User haftmann # Date 1224677744 -7200 # Node ID 64ab5bb68d4c7ea5908ae94a3868d3828a971b6b # Parent a287d0e8aa9d446e72a75d6c2a9c3fff823afeb5 tuned typedef interface diff -r a287d0e8aa9d -r 64ab5bb68d4c src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Wed Oct 22 14:15:43 2008 +0200 +++ b/src/HOL/Import/proof_kernel.ML Wed Oct 22 14:15:44 2008 +0200 @@ -2097,7 +2097,7 @@ val tnames = map fst tfrees val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy + val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 @@ -2183,7 +2183,7 @@ val tnames = sort string_ord (map fst tfrees) val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy + val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2 val fulltyname = Sign.intern_type thy' tycname val aty = Type (fulltyname, map mk_vartype tnames) diff -r a287d0e8aa9d -r 64ab5bb68d4c src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Wed Oct 22 14:15:43 2008 +0200 +++ b/src/HOL/Import/replay.ML Wed Oct 22 14:15:44 2008 +0200 @@ -344,7 +344,7 @@ | delta (Hol_theorem (thyname, thmname, th)) thy = add_hol4_theorem thyname thmname ([], th_of thy th) thy | delta (Typedef (thmname, typ, c, repabs, th)) thy = - snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy) + snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy) | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = add_hol4_type_mapping thyname tycname true fulltyname thy | delta (Indexed_theorem (i, th)) thy = diff -r a287d0e8aa9d -r 64ab5bb68d4c src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Oct 22 14:15:43 2008 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Wed Oct 22 14:15:44 2008 +0200 @@ -608,7 +608,7 @@ val (typedefs, thy6) = thy4 |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy => - TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) + TypedefPackage.add_typedef false (SOME name') (name, tvs, mx) (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE (rtac exI 1 THEN rtac CollectI 1 THEN diff -r a287d0e8aa9d -r 64ab5bb68d4c src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Oct 22 14:15:43 2008 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Oct 22 14:15:44 2008 +0200 @@ -194,7 +194,7 @@ val (typedefs, thy3) = thy2 |> parent_path flat_names |> fold_map (fn ((((name, mx), tvs), c), name') => - TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) + TypedefPackage.add_typedef false (SOME name') (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) diff -r a287d0e8aa9d -r 64ab5bb68d4c src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Wed Oct 22 14:15:43 2008 +0200 +++ b/src/HOL/Tools/typedef_package.ML Wed Oct 22 14:15:44 2008 +0200 @@ -15,12 +15,10 @@ Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; val get_info: theory -> string -> info option val add_typedef: bool -> string option -> bstring * string list * mixfix -> - string -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory - val add_typedef_i: bool -> string option -> bstring * string list * mixfix -> term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory - val typedef: (bool * string) * (bstring * string list * mixfix) * string + val typedef: (bool * string) * (bstring * string list * mixfix) * term * (string * string) option -> theory -> Proof.state - val typedef_i: (bool * string) * (bstring * string list * mixfix) * term + val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string * (string * string) option -> theory -> Proof.state val interpretation: (string -> theory -> theory) -> theory -> theory val setup: theory -> theory @@ -33,15 +31,15 @@ val type_definitionN = "Typedef.type_definition"; -val Rep = thm "type_definition.Rep"; -val Rep_inverse = thm "type_definition.Rep_inverse"; -val Abs_inverse = thm "type_definition.Abs_inverse"; -val Rep_inject = thm "type_definition.Rep_inject"; -val Abs_inject = thm "type_definition.Abs_inject"; -val Rep_cases = thm "type_definition.Rep_cases"; -val Abs_cases = thm "type_definition.Abs_cases"; -val Rep_induct = thm "type_definition.Rep_induct"; -val Abs_induct = thm "type_definition.Abs_induct"; +val Rep = @{thm "type_definition.Rep"}; +val Rep_inverse = @{thm "type_definition.Rep_inverse"}; +val Abs_inverse = @{thm "type_definition.Abs_inverse"}; +val Rep_inject = @{thm "type_definition.Rep_inject"}; +val Abs_inject = @{thm "type_definition.Abs_inject"}; +val Rep_cases = @{thm "type_definition.Rep_cases"}; +val Abs_cases = @{thm "type_definition.Abs_cases"}; +val Rep_induct = @{thm "type_definition.Rep_induct"}; +val Abs_induct = @{thm "type_definition.Abs_induct"}; @@ -214,27 +212,18 @@ handle ERROR msg => err_in_typedef msg name; -(* add_typedef interfaces *) +(* add_typedef interface *) -local - -fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy = +fun add_typedef def opt_name typ set opt_morphs tac thy = let val name = the_default (#1 typ) opt_name; val (set, goal, _, typedef_result) = - prepare_typedef prep_term def name typ set opt_morphs thy; + prepare_typedef Syntax.check_term def name typ set opt_morphs thy; val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); in typedef_result non_empty thy end; -in - -val add_typedef = gen_typedef Syntax.read_term; -val add_typedef_i = gen_typedef Syntax.check_term; - -end; - (* Isar typedef interface *) @@ -249,8 +238,8 @@ in -val typedef = gen_typedef Syntax.read_term; -val typedef_i = gen_typedef Syntax.check_term; +val typedef = gen_typedef Syntax.check_term; +val typedef_cmd = gen_typedef Syntax.read_term; end; @@ -270,7 +259,7 @@ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); + typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); val _ = OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal diff -r a287d0e8aa9d -r 64ab5bb68d4c src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Wed Oct 22 14:15:43 2008 +0200 +++ b/src/HOLCF/Tools/pcpodef_package.ML Wed Oct 22 14:15:44 2008 +0200 @@ -89,7 +89,7 @@ fun make_po tac thy1 = let val ((_, {type_definition, set_def, ...}), thy2) = thy1 - |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac; + |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac; val lthy3 = thy2 |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"}); val less_def' = Syntax.check_term lthy3 less_def;