1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 10:15:58 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 10:58:11 2012 +0200
     1.3 @@ -658,23 +658,15 @@
     1.4      val params = fold Term.add_tfreesT Ds [];
     1.5      val deads = map TFree params;
     1.6  
     1.7 -    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) =
     1.8 -      lthy
     1.9 -      |> Typedef.add_typedef true NONE (bdT_bind, params, NoSyn)
    1.10 -        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1)
    1.11 -      ||> `Local_Theory.restore;
    1.12 -
    1.13 -    val phi = Proof_Context.export_morphism lthy lthy';
    1.14 +    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
    1.15 +      typedef false NONE (bdT_bind, params, NoSyn)
    1.16 +        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.17  
    1.18      val bnf_bd' = mk_dir_image bnf_bd
    1.19        (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
    1.20  
    1.21 -    val set_def = Morphism.thm phi (the (#set_def bdT_loc_info));
    1.22 -    val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info);
    1.23 -    val Abs_cases = Morphism.thm phi (#Abs_cases bdT_loc_info);
    1.24 -
    1.25 -    val Abs_bdT_inj = mk_Abs_inj_thm set_def Abs_inject;
    1.26 -    val Abs_bdT_bij = mk_Abs_bij_thm lthy' set_def Abs_inject Abs_cases;
    1.27 +    val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
    1.28 +    val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
    1.29  
    1.30      val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
    1.31      val bd_card_order =

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 10:15:58 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 10:58:11 2012 +0200
     2.3 @@ -77,9 +77,6 @@
     2.4    val mk_set_minimalN: int -> string
     2.5    val mk_set_inductN: int -> string
     2.6  
     2.7 -  val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
     2.8 -    (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
     2.9 -
    2.10    val split_conj_thm: thm -> thm list
    2.11    val split_conj_prems: int -> thm -> thm
    2.12  
    2.13 @@ -126,18 +123,6 @@
    2.14    then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
    2.15    else (); Timer.startRealTimer ());
    2.16  
    2.17 -(*TODO: is this really different from Typedef.add_typedef_global?*)
    2.18 -fun typedef def opt_name typ set opt_morphs tac lthy =
    2.19 -  let
    2.20 -    val ((name, info), (lthy, lthy_old)) =
    2.21 -      lthy
    2.22 -      |> Typedef.add_typedef def opt_name typ set opt_morphs tac
    2.23 -      ||> `Local_Theory.restore;
    2.24 -    val phi = Proof_Context.export_morphism lthy_old lthy;
    2.25 -  in
    2.26 -    ((name, Typedef.transform_info phi info), lthy)
    2.27 -  end;
    2.28 -
    2.29  val preN = "pre_"
    2.30  val rawN = "raw_"
    2.31  

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 10:15:58 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 10:58:11 2012 +0200
     3.3 @@ -1028,7 +1028,7 @@
     3.4            val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
     3.5  
     3.6            val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
     3.7 -            typedef true NONE (sbdT_bind, params, NoSyn)
     3.8 +            typedef false NONE (sbdT_bind, params, NoSyn)
     3.9                (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    3.10  
    3.11            val sbdT = Type (sbdT_name, params');
    3.12 @@ -1052,12 +1052,8 @@
    3.13            val sbd_def = Morphism.thm phi sbd_def_free;
    3.14            val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
    3.15  
    3.16 -          val sbdT_set_def = the (#set_def sbdT_loc_info);
    3.17 -          val sbdT_Abs_inject = #Abs_inject sbdT_loc_info;
    3.18 -          val sbdT_Abs_cases = #Abs_cases sbdT_loc_info;
    3.19 -
    3.20 -          val Abs_sbdT_inj = mk_Abs_inj_thm sbdT_set_def sbdT_Abs_inject;
    3.21 -          val Abs_sbdT_bij = mk_Abs_bij_thm lthy sbdT_set_def sbdT_Abs_inject sbdT_Abs_cases;
    3.22 +          val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
    3.23 +          val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
    3.24  
    3.25            fun mk_sum_Cinfinite [thm] = thm
    3.26              | mk_sum_Cinfinite (thm :: thms) =

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sun Sep 09 10:15:58 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sun Sep 09 10:58:11 2012 +0200
     4.3 @@ -774,14 +774,13 @@
     4.4      val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
     4.5  
     4.6      val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
     4.7 -      typedef true NONE (IIT_bind, params, NoSyn)
     4.8 +      typedef false NONE (IIT_bind, params, NoSyn)
     4.9          (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    4.10  
    4.11      val IIT = Type (IIT_name, params');
    4.12      val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
    4.13      val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
    4.14 -    val Abs_IIT_inverse_thm =
    4.15 -      mk_Abs_inverse_thm (the (#set_def IIT_loc_info)) (#Abs_inverse IIT_loc_info);
    4.16 +    val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
    4.17  
    4.18      val initT = IIT --> Asuc_bdT;
    4.19      val active_initTs = replicate n initT;

     5.1 --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sun Sep 09 10:15:58 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sun Sep 09 10:58:11 2012 +0200
     5.3 @@ -20,12 +20,8 @@
     5.4    val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
     5.5      int -> tactic
     5.6  
     5.7 -  val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm -> thm
     5.8 -  val mk_Abs_inj_thm: thm -> thm -> thm
     5.9 -  val mk_Abs_inverse_thm: thm -> thm -> thm
    5.10 -  val mk_T_I: thm -> thm
    5.11 -  val mk_T_subset1: thm -> thm
    5.12 -  val mk_T_subset2: thm -> thm
    5.13 +  val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
    5.14 +  val mk_Abs_inj_thm: thm -> thm
    5.15  
    5.16    val mk_Card_order_tac: thm -> tactic
    5.17    val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
    5.18 @@ -81,17 +77,11 @@
    5.19  
    5.20  
    5.21  
    5.22 -(* Theorems for typedefs with UNIV as representing set *)
    5.23 +(* Theorems for open typedefs with UNIV as representing set *)
    5.24  
    5.25 -(*equivalent to UNIV_I for the representing set of the particular type T*)
    5.26 -fun mk_T_subset1 def = set_mp OF [def RS meta_eq_to_obj_eq RS equalityD2];
    5.27 -fun mk_T_subset2 def = set_mp OF [def RS meta_eq_to_obj_eq RS equalityD1];
    5.28 -fun mk_T_I def = UNIV_I RS mk_T_subset1 def;
    5.29 -
    5.30 -fun mk_Abs_inverse_thm def inv = mk_T_I def RS inv;
    5.31 -fun mk_Abs_inj_thm def inj = inj OF (replicate 2 (mk_T_I def));
    5.32 -fun mk_Abs_bij_thm ctxt def inj surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
    5.33 -  (mk_Abs_inj_thm def inj RS @{thm bijI});
    5.34 +fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
    5.35 +fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
    5.36 +  (Abs_inj_thm RS @{thm bijI});
    5.37  
    5.38  
    5.39  

     6.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Sun Sep 09 10:15:58 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Sun Sep 09 10:58:11 2012 +0200
     6.3 @@ -124,6 +124,9 @@
     6.4    val certifyT: Proof.context -> typ -> ctyp
     6.5    val certify: Proof.context -> term -> cterm
     6.6  
     6.7 +  val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
     6.8 +    (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
     6.9 +
    6.10    val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    6.11    val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
    6.12      tactic
    6.13 @@ -243,6 +246,18 @@
    6.14  fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    6.15  fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    6.16  
    6.17 +(*TODO: is this really different from Typedef.add_typedef_global?*)
    6.18 +fun typedef def opt_name typ set opt_morphs tac lthy =
    6.19 +  let
    6.20 +    val ((name, info), (lthy, lthy_old)) =
    6.21 +      lthy
    6.22 +      |> Typedef.add_typedef def opt_name typ set opt_morphs tac
    6.23 +      ||> `Local_Theory.restore;
    6.24 +    val phi = Proof_Context.export_morphism lthy_old lthy;
    6.25 +  in
    6.26 +    ((name, Typedef.transform_info phi info), lthy)
    6.27 +  end;
    6.28 +
    6.29  (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
    6.30  fun WRAP gen_before gen_after xs core_tac =
    6.31    fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;