src/HOL/Tools/typedef_package.ML
changeset 5697 e816c4f1a396
parent 5180 d82a70766af0
child 6092 d9db67970c73
equal deleted inserted replaced
5696:c2c2214f8037 5697:e816c4f1a396
     5 Gordon/HOL style type definitions.
     5 Gordon/HOL style type definitions.
     6 *)
     6 *)
     7 
     7 
     8 signature TYPEDEF_PACKAGE =
     8 signature TYPEDEF_PACKAGE =
     9 sig
     9 sig
       
    10   val quiet_mode: bool ref
    10   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    11   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    11   val prove_nonempty: cterm -> thm list -> tactic option -> thm
    12   val prove_nonempty: cterm -> thm list -> tactic option -> thm
    12   val add_typedef: string -> bstring * string list * mixfix ->
    13   val add_typedef: string -> bstring * string list * mixfix ->
    13     string -> string list -> thm list -> tactic option -> theory -> theory
    14     string -> string list -> thm list -> tactic option -> theory -> theory
    14   val add_typedef_i: string -> bstring * string list * mixfix ->
    15   val add_typedef_i: string -> bstring * string list * mixfix ->
    36   end;
    37   end;
    37 
    38 
    38 
    39 
    39 
    40 
    40 (** type definitions **)
    41 (** type definitions **)
       
    42 
       
    43 (* messages *)
       
    44 
       
    45 val quiet_mode = ref false;
       
    46 fun message s = if ! quiet_mode then () else writeln s;
       
    47 
    41 
    48 
    42 (* prove non-emptyness of a set *)   (*exception ERROR*)
    49 (* prove non-emptyness of a set *)   (*exception ERROR*)
    43 
    50 
    44 val is_def = Logic.is_equals o #prop o rep_thm;
    51 val is_def = Logic.is_equals o #prop o rep_thm;
    45 
    52 
   121     val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   128     val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   122   in
   129   in
   123     if null errs then ()
   130     if null errs then ()
   124     else error (cat_lines errs);
   131     else error (cat_lines errs);
   125 
   132 
   126     writeln("Proving nonemptiness of " ^ quote name ^ " ...");
   133     message ("Proving nonemptiness of " ^ quote name ^ " ...");
   127     prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
   134     prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
   128 
   135 
   129     thy
   136     thy
   130     |> PureThy.add_typedecls [(t, vs, mx)]
   137     |> PureThy.add_typedecls [(t, vs, mx)]
   131     |> Theory.add_arities_i
   138     |> Theory.add_arities_i