src/HOL/Tools/typedef_package.ML
changeset 25513 b7de6e23e143
parent 25495 98f3596bec44
child 25535 4975b7529a14
equal deleted inserted replaced
25512:4134f7c782e2 25513:b7de6e23e143
    21     term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
    21     term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
    22   val typedef: (bool * string) * (bstring * string list * mixfix) * string
    22   val typedef: (bool * string) * (bstring * string list * mixfix) * string
    23     * (string * string) option -> theory -> Proof.state
    23     * (string * string) option -> theory -> Proof.state
    24   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    24   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    25     * (string * string) option -> theory -> Proof.state
    25     * (string * string) option -> theory -> Proof.state
       
    26   val interpretation: (string -> theory -> theory) -> theory -> theory
    26 end;
    27 end;
    27 
    28 
    28 structure TypedefPackage: TYPEDEF_PACKAGE =
    29 structure TypedefPackage: TYPEDEF_PACKAGE =
    29 struct
    30 struct
    30 
    31 
   212   handle ERROR msg => err_in_typedef msg name;
   213   handle ERROR msg => err_in_typedef msg name;
   213 
   214 
   214 
   215 
   215 (* add_typedef interfaces *)
   216 (* add_typedef interfaces *)
   216 
   217 
       
   218 structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
       
   219 val interpretation = TypedefInterpretation.interpretation;
       
   220 
   217 local
   221 local
   218 
   222 
   219 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
   223 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
   220   let
   224   let
   221     val string_of_term = Sign.string_of_term thy;
   225     val string_of_term = Sign.string_of_term thy;
   223     val (set, goal, _, typedef_result) =
   227     val (set, goal, _, typedef_result) =
   224       prepare_typedef prep_term def name typ set opt_morphs thy;
   228       prepare_typedef prep_term def name typ set opt_morphs thy;
   225     val _ = message ("Proving non-emptiness of set " ^ quote (string_of_term set) ^ " ...");
   229     val _ = message ("Proving non-emptiness of set " ^ quote (string_of_term set) ^ " ...");
   226     val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
   230     val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
   227       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
   231       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
   228   in typedef_result non_empty thy end;
   232   in
       
   233     thy
       
   234     |> typedef_result non_empty
       
   235     |-> (fn (a, info) => TypedefInterpretation.data a #> pair (a, info))
       
   236   end;
   229 
   237 
   230 in
   238 in
   231 
   239 
   232 val add_typedef = gen_typedef Syntax.read_term;
   240 val add_typedef = gen_typedef Syntax.read_term;
   233 val add_typedef_i = gen_typedef Syntax.check_term;
   241 val add_typedef_i = gen_typedef Syntax.check_term;