src/HOL/Lifting.thy
changeset 47545 a2850a16e30f
parent 47544 e455cdaac479
child 47575 b90cd7016d4f
     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 15:48:32 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 17:04:03 2012 +0200
     1.3 @@ -353,39 +353,27 @@
     1.4    unfolding bi_unique_def T_def
     1.5    by (simp add: type_definition.Rep_inject [OF type])
     1.6  
     1.7 -lemma typedef_right_total: "right_total T"
     1.8 -  unfolding right_total_def T_def by simp
     1.9 -
    1.10  lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
    1.11    unfolding fun_rel_def T_def by simp
    1.12  
    1.13 -lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
    1.14 -  unfolding T_def fun_rel_def
    1.15 -  by (metis type_definition.Rep [OF type]
    1.16 -    type_definition.Abs_inverse [OF type])
    1.17 -
    1.18 -lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
    1.19 +lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All"
    1.20    unfolding T_def fun_rel_def
    1.21    by (metis type_definition.Rep [OF type]
    1.22      type_definition.Abs_inverse [OF type])
    1.23  
    1.24 -lemma typedef_transfer_bforall:
    1.25 +lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex"
    1.26 +  unfolding T_def fun_rel_def
    1.27 +  by (metis type_definition.Rep [OF type]
    1.28 +    type_definition.Abs_inverse [OF type])
    1.29 +
    1.30 +lemma typedef_forall_transfer:
    1.31    "((T ===> op =) ===> op =)
    1.32      (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
    1.33    unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
    1.34 -  by (rule typedef_transfer_All)
    1.35 +  by (rule typedef_All_transfer)
    1.36  
    1.37  end
    1.38  
    1.39 -text {* Generating transfer rules for a type copy. *}
    1.40 -
    1.41 -lemma copy_type_bi_total:
    1.42 -  assumes type: "type_definition Rep Abs UNIV"
    1.43 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.44 -  shows "bi_total T"
    1.45 -  unfolding bi_total_def T_def
    1.46 -  by (metis type_definition.Abs_inverse [OF type] UNIV_I)
    1.47 -
    1.48  text {* Generating the correspondence rule for a constant defined with
    1.49    @{text "lift_definition"}. *}
    1.50