# HG changeset patch # User traytel # Date 1347181091 -7200 # Node ID e43910ccee74e45d388c8e386932fb29e6241cb4 # Parent 2652319c394e7a98b15ed4cb43dfa7d41e46d72a open typedefs everywhere in the package diff -r 2652319c394e -r e43910ccee74 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Sun Sep 09 10:15:58 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Sun Sep 09 10:58:11 2012 +0200 @@ -658,23 +658,15 @@ val params = fold Term.add_tfreesT Ds []; val deads = map TFree params; - val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) = - lthy - |> Typedef.add_typedef true NONE (bdT_bind, params, NoSyn) - (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) - ||> `Local_Theory.restore; - - val phi = Proof_Context.export_morphism lthy lthy'; + val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) = + typedef false NONE (bdT_bind, params, NoSyn) + (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val bnf_bd' = mk_dir_image bnf_bd (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads))) - val set_def = Morphism.thm phi (the (#set_def bdT_loc_info)); - val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info); - val Abs_cases = Morphism.thm phi (#Abs_cases bdT_loc_info); - - val Abs_bdT_inj = mk_Abs_inj_thm set_def Abs_inject; - val Abs_bdT_bij = mk_Abs_bij_thm lthy' set_def Abs_inject Abs_cases; + val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info); + val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info); val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf]; val bd_card_order = diff -r 2652319c394e -r e43910ccee74 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sun Sep 09 10:15:58 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sun Sep 09 10:58:11 2012 +0200 @@ -77,9 +77,6 @@ val mk_set_minimalN: int -> string val mk_set_inductN: int -> string - val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> - (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory - val split_conj_thm: thm -> thm list val split_conj_prems: int -> thm -> thm @@ -126,18 +123,6 @@ then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer)) else (); Timer.startRealTimer ()); -(*TODO: is this really different from Typedef.add_typedef_global?*) -fun typedef def opt_name typ set opt_morphs tac lthy = - let - val ((name, info), (lthy, lthy_old)) = - lthy - |> Typedef.add_typedef def opt_name typ set opt_morphs tac - ||> `Local_Theory.restore; - val phi = Proof_Context.export_morphism lthy_old lthy; - in - ((name, Typedef.transform_info phi info), lthy) - end; - val preN = "pre_" val rawN = "raw_" diff -r 2652319c394e -r e43910ccee74 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Sun Sep 09 10:15:58 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Sun Sep 09 10:58:11 2012 +0200 @@ -1028,7 +1028,7 @@ val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = - typedef true NONE (sbdT_bind, params, NoSyn) + typedef false NONE (sbdT_bind, params, NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, params'); @@ -1052,12 +1052,8 @@ val sbd_def = Morphism.thm phi sbd_def_free; val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT)); - val sbdT_set_def = the (#set_def sbdT_loc_info); - val sbdT_Abs_inject = #Abs_inject sbdT_loc_info; - val sbdT_Abs_cases = #Abs_cases sbdT_loc_info; - - val Abs_sbdT_inj = mk_Abs_inj_thm sbdT_set_def sbdT_Abs_inject; - val Abs_sbdT_bij = mk_Abs_bij_thm lthy sbdT_set_def sbdT_Abs_inject sbdT_Abs_cases; + val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info); + val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info); fun mk_sum_Cinfinite [thm] = thm | mk_sum_Cinfinite (thm :: thms) = diff -r 2652319c394e -r e43910ccee74 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Sun Sep 09 10:15:58 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Sun Sep 09 10:58:11 2012 +0200 @@ -774,14 +774,13 @@ val IIT_bind = Binding.suffix_name ("_" ^ IITN) b; val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) = - typedef true NONE (IIT_bind, params, NoSyn) + typedef false NONE (IIT_bind, params, NoSyn) (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val IIT = Type (IIT_name, params'); val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT); val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT); - val Abs_IIT_inverse_thm = - mk_Abs_inverse_thm (the (#set_def IIT_loc_info)) (#Abs_inverse IIT_loc_info); + val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info; val initT = IIT --> Asuc_bdT; val active_initTs = replicate n initT; diff -r 2652319c394e -r e43910ccee74 src/HOL/Codatatype/Tools/bnf_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Sun Sep 09 10:15:58 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Sun Sep 09 10:58:11 2012 +0200 @@ -20,12 +20,8 @@ val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> int -> tactic - val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm -> thm - val mk_Abs_inj_thm: thm -> thm -> thm - val mk_Abs_inverse_thm: thm -> thm -> thm - val mk_T_I: thm -> thm - val mk_T_subset1: thm -> thm - val mk_T_subset2: thm -> thm + val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm + val mk_Abs_inj_thm: thm -> thm val mk_Card_order_tac: thm -> tactic val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic @@ -81,17 +77,11 @@ -(* Theorems for typedefs with UNIV as representing set *) +(* Theorems for open typedefs with UNIV as representing set *) -(*equivalent to UNIV_I for the representing set of the particular type T*) -fun mk_T_subset1 def = set_mp OF [def RS meta_eq_to_obj_eq RS equalityD2]; -fun mk_T_subset2 def = set_mp OF [def RS meta_eq_to_obj_eq RS equalityD1]; -fun mk_T_I def = UNIV_I RS mk_T_subset1 def; - -fun mk_Abs_inverse_thm def inv = mk_T_I def RS inv; -fun mk_Abs_inj_thm def inj = inj OF (replicate 2 (mk_T_I def)); -fun mk_Abs_bij_thm ctxt def inj surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1) - (mk_Abs_inj_thm def inj RS @{thm bijI}); +fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I); +fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1) + (Abs_inj_thm RS @{thm bijI}); diff -r 2652319c394e -r e43910ccee74 src/HOL/Codatatype/Tools/bnf_util.ML --- a/src/HOL/Codatatype/Tools/bnf_util.ML Sun Sep 09 10:15:58 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML Sun Sep 09 10:58:11 2012 +0200 @@ -124,6 +124,9 @@ val certifyT: Proof.context -> typ -> ctyp val certify: Proof.context -> term -> cterm + val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> + (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory + val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int -> tactic @@ -243,6 +246,18 @@ fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); +(*TODO: is this really different from Typedef.add_typedef_global?*) +fun typedef def opt_name typ set opt_morphs tac lthy = + let + val ((name, info), (lthy, lthy_old)) = + lthy + |> Typedef.add_typedef def opt_name typ set opt_morphs tac + ||> `Local_Theory.restore; + val phi = Proof_Context.export_morphism lthy_old lthy; + in + ((name, Typedef.transform_info phi info), lthy) + end; + (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*) fun WRAP gen_before gen_after xs core_tac = fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;