removed obsolete add_typedef_x;
authorwenzelm
Wed Oct 19 21:52:34 2005 +0200 (2005-10-19)
changeset 179220cba8edb269e
parent 17921 fce7b764cbd6
child 17923 18c66ca0c776
removed obsolete add_typedef_x;
tuned;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Oct 19 21:52:33 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 19 21:52:34 2005 +0200
     1.3 @@ -9,8 +9,6 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     1.7 -  val add_typedef_x: string -> bstring * string list * mixfix ->
     1.8 -    string -> string list -> thm list -> tactic option -> theory -> theory
     1.9    val add_typedef: bool -> string option -> bstring * string list * mixfix ->
    1.10      string -> (bstring * bstring) option -> tactic -> theory -> theory *
    1.11      {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    1.12 @@ -48,7 +46,30 @@
    1.13  
    1.14  
    1.15  
    1.16 -(** theory data **)
    1.17 +(** type declarations **)
    1.18 +
    1.19 +fun add_typedecls decls thy =
    1.20 +  let
    1.21 +    fun arity_of (raw_name, args, mx) =
    1.22 +      (Sign.full_name thy (Syntax.type_name raw_name mx),
    1.23 +        replicate (length args) HOLogic.typeS, HOLogic.typeS);
    1.24 +  in
    1.25 +    thy
    1.26 +    |> Theory.add_typedecls decls
    1.27 +    |> can (Theory.assert_super HOL.thy) ? Theory.add_arities_i (map arity_of decls)
    1.28 +  end;
    1.29 +
    1.30 +
    1.31 +
    1.32 +(** type definitions **)
    1.33 +
    1.34 +(* messages *)
    1.35 +
    1.36 +val quiet_mode = ref false;
    1.37 +fun message s = if ! quiet_mode then () else writeln s;
    1.38 +
    1.39 +
    1.40 +(* theory data *)
    1.41  
    1.42  structure TypedefData = TheoryDataFun
    1.43  (struct
    1.44 @@ -65,49 +86,6 @@
    1.45    TypedefData.map (Symtab.update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)));
    1.46  
    1.47  
    1.48 -
    1.49 -(** type declarations **)
    1.50 -
    1.51 -fun add_typedecls decls thy =
    1.52 -  let
    1.53 -    fun arity_of (raw_name, args, mx) =
    1.54 -      (Sign.full_name thy (Syntax.type_name raw_name mx),
    1.55 -        replicate (length args) HOLogic.typeS, HOLogic.typeS);
    1.56 -  in
    1.57 -    if can (Theory.assert_super HOL.thy) thy then
    1.58 -      thy |> Theory.add_typedecls decls
    1.59 -      |> Theory.add_arities_i (map arity_of decls)
    1.60 -    else thy |> Theory.add_typedecls decls
    1.61 -  end;
    1.62 -
    1.63 -
    1.64 -
    1.65 -(** type definitions **)
    1.66 -
    1.67 -(* messages *)
    1.68 -
    1.69 -val quiet_mode = ref false;
    1.70 -fun message s = if ! quiet_mode then () else writeln s;
    1.71 -
    1.72 -
    1.73 -(* prove_nonempty -- tactical version *)        (*exception ERROR*)
    1.74 -
    1.75 -fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
    1.76 -  let
    1.77 -    val is_def = Logic.is_equals o #prop o Thm.rep_thm;
    1.78 -    val thms = PureThy.get_thmss thy (map Name witn_names) @ witn_thms;
    1.79 -    val tac =
    1.80 -      witn1_tac THEN
    1.81 -      TRY (rewrite_goals_tac (List.filter is_def thms)) THEN
    1.82 -      TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    1.83 -      if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.84 -  in
    1.85 -    message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.86 -    Tactic.prove thy [] [] goal (K tac)
    1.87 -  end
    1.88 -  handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.89 -
    1.90 -
    1.91  (* prepare_typedef *)
    1.92  
    1.93  fun read_term thy used s =
    1.94 @@ -242,25 +220,21 @@
    1.95  
    1.96  local
    1.97  
    1.98 -fun gen_typedef prep_term def name typ set opt_morphs tac1 names thms tac2 thy =
    1.99 +fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
   1.100    let
   1.101 +    val name = the_default (#1 typ) opt_name;
   1.102      val (cset, goal, _, typedef_result) =
   1.103        prepare_typedef prep_term def name typ set opt_morphs thy;
   1.104 -    val non_empty = prove_nonempty thy cset goal (tac1, names, thms, tac2);
   1.105 +    val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
   1.106 +    val non_empty = Tactic.prove thy [] [] goal (K tac) handle ERROR =>
   1.107 +      error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
   1.108      val ((thy', _), result) = (thy, non_empty) |> typedef_result;
   1.109    in (thy', result) end;
   1.110  
   1.111 -fun sane_typedef prep_term def opt_name typ set opt_morphs tac =
   1.112 -  gen_typedef prep_term def
   1.113 -    (if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (SOME tac);
   1.114 -
   1.115  in
   1.116  
   1.117 -fun add_typedef_x name typ set names thms tac =
   1.118 -  #1 o gen_typedef read_term true name typ set NONE (Tactic.rtac exI 1) names thms tac;
   1.119 -
   1.120 -val add_typedef = sane_typedef read_term;
   1.121 -val add_typedef_i = sane_typedef cert_term;
   1.122 +val add_typedef = gen_typedef read_term;
   1.123 +val add_typedef_i = gen_typedef cert_term;
   1.124  
   1.125  end;
   1.126