src/HOL/Tools/typedef_package.ML
changeset 5180 d82a70766af0
parent 5104 230cca8452c7
child 5697 e816c4f1a396
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jul 24 12:53:04 1998 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Jul 24 12:55:05 1998 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4      string -> string list -> thm list -> tactic option -> theory -> theory
     1.5    val add_typedef_i: string -> bstring * string list * mixfix ->
     1.6      term -> string list -> thm list -> tactic option -> theory -> theory
     1.7 +  val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
     1.8 +    term -> string list -> thm list -> tactic option -> theory -> theory
     1.9  end;
    1.10  
    1.11  structure TypedefPackage: TYPEDEF_PACKAGE =
    1.12 @@ -60,7 +62,7 @@
    1.13  
    1.14  (* gen_add_typedef *)
    1.15  
    1.16 -fun gen_add_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
    1.17 +fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set axms thms usr_tac thy =
    1.18    let
    1.19      val _ = Theory.requires thy "Set" "typedefs";
    1.20      val sign = sign_of thy;
    1.21 @@ -87,11 +89,12 @@
    1.22      val AbsC = Const (full_name Abs_name, oldT --> newT);
    1.23      val x_new = Free ("x", newT);
    1.24      val y_old = Free ("y", oldT);
    1.25 +    val set' = if no_def then set else setC;
    1.26  
    1.27      (*axioms*)
    1.28 -    val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, setC));
    1.29 +    val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, set'));
    1.30      val rep_type_inv = HOLogic.mk_Trueprop (HOLogic.mk_eq (AbsC $ (RepC $ x_new), x_new));
    1.31 -    val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, setC)),
    1.32 +    val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, set')),
    1.33        HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old)));
    1.34  
    1.35  
    1.36 @@ -128,11 +131,11 @@
    1.37      |> Theory.add_arities_i
    1.38       [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)]
    1.39      |> Theory.add_consts_i
    1.40 -     [(name, setT, NoSyn),
    1.41 -      (Rep_name, newT --> oldT, NoSyn),
    1.42 -      (Abs_name, oldT --> newT, NoSyn)]
    1.43 -    |> (PureThy.add_defs_i o map Attribute.none)
    1.44 -     [(name ^ "_def", Logic.mk_equals (setC, set))]
    1.45 +     ((if no_def then [] else [(name, setT, NoSyn)]) @
    1.46 +      [(Rep_name, newT --> oldT, NoSyn),
    1.47 +       (Abs_name, oldT --> newT, NoSyn)])
    1.48 +    |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none)
    1.49 +     [(name ^ "_def", Logic.mk_equals (setC, set))])
    1.50      |> (PureThy.add_axioms_i o map Attribute.none)
    1.51       [(Rep_name, rep_type),
    1.52        (Rep_name ^ "_inverse", rep_type_inv),
    1.53 @@ -150,8 +153,9 @@
    1.54  fun cert_term sg tm =
    1.55    cterm_of sg tm handle TERM (msg, _) => error msg;
    1.56  
    1.57 -val add_typedef = gen_add_typedef read_term;
    1.58 -val add_typedef_i = gen_add_typedef cert_term;
    1.59 +val add_typedef = gen_add_typedef read_term false;
    1.60 +val add_typedef_i = gen_add_typedef cert_term false;
    1.61 +val add_typedef_i_no_def = gen_add_typedef cert_term true;
    1.62  
    1.63  
    1.64  end;