src/HOL/Tools/typedef_package.ML
changeset 11827 16ef206e6648
parent 11822 122834177ec1
child 11968 859a141085d0
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Oct 18 21:01:18 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Oct 18 21:01:59 2001 +0200
     1.3 @@ -12,12 +12,12 @@
     1.4    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     1.5    val add_typedef_x: string -> bstring * string list * mixfix ->
     1.6      string -> string list -> thm list -> tactic option -> theory -> theory
     1.7 -  val add_typedef: bool -> string -> bstring * string list * mixfix ->
     1.8 +  val add_typedef: bool -> string option -> bstring * string list * mixfix ->
     1.9      string -> (bstring * bstring) option -> tactic -> theory -> theory *
    1.10      {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    1.11        Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    1.12        Rep_induct: thm, Abs_induct: thm}
    1.13 -  val add_typedef_i: bool -> string -> bstring * string list * mixfix ->
    1.14 +  val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
    1.15      term -> (bstring * bstring) option -> tactic -> theory -> theory *
    1.16      {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    1.17        Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    1.18 @@ -79,15 +79,15 @@
    1.19  
    1.20  (* prove_nonempty -- tactical version *)        (*exception ERROR*)
    1.21  
    1.22 -fun prove_nonempty thy cset goal (witn_names, witn_thms, witn_tac) =
    1.23 +fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
    1.24    let
    1.25      val is_def = Logic.is_equals o #prop o Thm.rep_thm;
    1.26      val thms = PureThy.get_thmss thy witn_names @ witn_thms;
    1.27      val tac =
    1.28 -      rtac exI 1 THEN
    1.29 +      witn1_tac THEN
    1.30        TRY (rewrite_goals_tac (filter is_def thms)) THEN
    1.31        TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    1.32 -      if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.33 +      if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.34    in
    1.35      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.36      prove_goalw_cterm [] (cterm_of (sign_of thy) goal) (K [tac])
    1.37 @@ -217,19 +217,20 @@
    1.38  
    1.39  (* add_typedef interfaces *)
    1.40  
    1.41 -fun gen_typedef prep_term def name typ set opt_morphs names thms tac thy =
    1.42 +fun gen_typedef prep_term def name typ set opt_morphs tac1 names thms tac2 thy =
    1.43    let
    1.44      val (cset, goal, _, typedef_result) =
    1.45        prepare_typedef prep_term def name typ set opt_morphs thy;
    1.46 -    val non_empty = prove_nonempty thy cset goal (names, thms, tac);
    1.47 +    val non_empty = prove_nonempty thy cset goal (tac1, names, thms, tac2);
    1.48      val ((thy', _), result) = (thy, non_empty) |> typedef_result;
    1.49    in (thy', result) end;
    1.50  
    1.51 -fun sane_typedef prep_term def name typ set opt_morphs tac =
    1.52 -  gen_typedef prep_term def name typ set opt_morphs [] [] (Some tac);
    1.53 +fun sane_typedef prep_term def opt_name typ set opt_morphs tac =
    1.54 +  gen_typedef prep_term def
    1.55 +    (if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (Some tac);
    1.56  
    1.57  fun add_typedef_x name typ set names thms tac =
    1.58 -  #1 o gen_typedef read_term true name typ set None names thms tac;
    1.59 +  #1 o gen_typedef read_term true name typ set None (Tactic.rtac exI 1) names thms tac;
    1.60  
    1.61  val add_typedef = sane_typedef read_term;
    1.62  val add_typedef_i = sane_typedef cert_term;