src/HOL/Tools/typedef_package.ML
changeset 5104 230cca8452c7
parent 4970 8b65444edbb0
child 5180 d82a70766af0
equal deleted inserted replaced
5103:866a281a8c2a 5104:230cca8452c7
     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 add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    10   val prove_nonempty: cterm -> thm list -> tactic option -> thm
    11   val prove_nonempty: cterm -> thm list -> tactic option -> thm
    11   val add_typedef: string -> bstring * string list * mixfix ->
    12   val add_typedef: string -> bstring * string list * mixfix ->
    12     string -> string list -> thm list -> tactic option -> theory -> theory
    13     string -> string list -> thm list -> tactic option -> theory -> theory
    13   val add_typedef_i: string -> bstring * string list * mixfix ->
    14   val add_typedef_i: string -> bstring * string list * mixfix ->
    14     term -> string list -> thm list -> tactic option -> theory -> theory
    15     term -> string list -> thm list -> tactic option -> theory -> theory
    15 end;
    16 end;
    16 
    17 
    17 structure TypedefPackage: TYPEDEF_PACKAGE =
    18 structure TypedefPackage: TYPEDEF_PACKAGE =
    18 struct
    19 struct
    19 
    20 
       
    21 
       
    22 (** type declarations **)
       
    23 
       
    24 fun add_typedecls decls thy =
       
    25   let
       
    26     val full = Sign.full_name (Theory.sign_of thy);
       
    27 
       
    28     fun arity_of (raw_name, args, mx) =
       
    29       (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
       
    30   in
       
    31     thy
       
    32     |> PureThy.add_typedecls decls
       
    33     |> Theory.add_arities_i (map arity_of decls)
       
    34   end;
       
    35 
       
    36 
       
    37 
       
    38 (** type definitions **)
    20 
    39 
    21 (* prove non-emptyness of a set *)   (*exception ERROR*)
    40 (* prove non-emptyness of a set *)   (*exception ERROR*)
    22 
    41 
    23 val is_def = Logic.is_equals o #prop o rep_thm;
    42 val is_def = Logic.is_equals o #prop o rep_thm;
    24 
    43