1.1 --- a/src/HOL/Tools/typedef_package.ML Tue Nov 18 22:25:36 2008 +0100
1.2 +++ b/src/HOL/Tools/typedef_package.ML Wed Nov 19 08:58:57 2008 +0100
1.3 @@ -10,7 +10,7 @@
1.4 sig
1.5 type info =
1.6 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
1.7 - type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
1.8 + inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
1.9 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
1.10 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
1.11 val get_info: theory -> string -> info option
1.12 @@ -49,7 +49,7 @@
1.13
1.14 type info =
1.15 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
1.16 - type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
1.17 + inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
1.18 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
1.19 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
1.20
1.21 @@ -90,10 +90,10 @@
1.22 val rhs_tfreesT = Term.add_tfreesT setT [];
1.23 val oldT = HOLogic.dest_setT setT handle TYPE _ =>
1.24 error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
1.25 - fun mk_nonempty A =
1.26 + fun mk_inhabited A =
1.27 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
1.28 - val goal = mk_nonempty set;
1.29 - val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT));
1.30 + val goal = mk_inhabited set;
1.31 + val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
1.32
1.33 (*lhs*)
1.34 val defS = Sign.defaultS thy;
1.35 @@ -130,7 +130,7 @@
1.36 |-> (fn [th] => pair (SOME th))
1.37 else (NONE, thy);
1.38
1.39 - fun typedef_result nonempty =
1.40 + fun typedef_result inhabited =
1.41 ObjectLogic.typedecl (t, vs, mx)
1.42 #> snd
1.43 #> Sign.add_consts_i
1.44 @@ -139,7 +139,7 @@
1.45 (Abs_name, oldT --> newT, NoSyn)])
1.46 #> add_def (PrimitiveDefs.mk_defpair (setC, set))
1.47 ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
1.48 - [apsnd (fn cond_axm => nonempty RS cond_axm)])]
1.49 + [apsnd (fn cond_axm => inhabited RS cond_axm)])]
1.50 ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
1.51 ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
1.52 #-> (fn (set_def, [type_definition]) => fn thy1 =>
1.53 @@ -168,7 +168,7 @@
1.54 ||> Sign.parent_path;
1.55 val info = {rep_type = oldT, abs_type = newT,
1.56 Rep_name = full Rep_name, Abs_name = full Abs_name,
1.57 - type_definition = type_definition, set_def = set_def,
1.58 + inhabited = inhabited, type_definition = type_definition, set_def = set_def,
1.59 Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
1.60 Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
1.61 Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};