1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 10:53:28 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 10:52:49 2012 +0200
     1.3 @@ -328,18 +328,37 @@
     1.4  
     1.5  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
     1.6  
     1.7 -lemma typedef_bi_unique:
     1.8 +context
     1.9 +  fixes Rep Abs A T
    1.10    assumes type: "type_definition Rep Abs A"
    1.11 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.12 -  shows "bi_unique T"
    1.13 +  assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
    1.14 +begin
    1.15 +
    1.16 +lemma typedef_bi_unique: "bi_unique T"
    1.17    unfolding bi_unique_def T_def
    1.18    by (simp add: type_definition.Rep_inject [OF type])
    1.19  
    1.20 -lemma typedef_right_total:
    1.21 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.22 -  shows "right_total T"
    1.23 +lemma typedef_right_total: "right_total T"
    1.24    unfolding right_total_def T_def by simp
    1.25  
    1.26 +lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
    1.27 +  unfolding T_def fun_rel_def
    1.28 +  by (metis type_definition.Rep [OF type]
    1.29 +    type_definition.Abs_inverse [OF type])
    1.30 +
    1.31 +lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
    1.32 +  unfolding T_def fun_rel_def
    1.33 +  by (metis type_definition.Rep [OF type]
    1.34 +    type_definition.Abs_inverse [OF type])
    1.35 +
    1.36 +lemma typedef_transfer_bforall:
    1.37 +  "((T ===> op =) ===> op =)
    1.38 +    (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
    1.39 +  unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
    1.40 +  by (rule typedef_transfer_All [OF assms])
    1.41 +
    1.42 +end
    1.43 +
    1.44  lemma copy_type_bi_total:
    1.45    assumes type: "type_definition Rep Abs UNIV"
    1.46    assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.47 @@ -347,30 +366,6 @@
    1.48    unfolding bi_total_def T_def
    1.49    by (metis type_definition.Abs_inverse [OF type] UNIV_I)
    1.50  
    1.51 -lemma typedef_transfer_All:
    1.52 -  assumes type: "type_definition Rep Abs A"
    1.53 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.54 -  shows "((T ===> op =) ===> op =) (Ball A) All"
    1.55 -  unfolding T_def fun_rel_def
    1.56 -  by (metis type_definition.Rep [OF type]
    1.57 -    type_definition.Abs_inverse [OF type])
    1.58 -
    1.59 -lemma typedef_transfer_Ex:
    1.60 -  assumes type: "type_definition Rep Abs A"
    1.61 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.62 -  shows "((T ===> op =) ===> op =) (Bex A) Ex"
    1.63 -  unfolding T_def fun_rel_def
    1.64 -  by (metis type_definition.Rep [OF type]
    1.65 -    type_definition.Abs_inverse [OF type])
    1.66 -
    1.67 -lemma typedef_transfer_bforall:
    1.68 -  assumes type: "type_definition Rep Abs A"
    1.69 -  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.70 -  shows "((T ===> op =) ===> op =)
    1.71 -    (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
    1.72 -  unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
    1.73 -  by (rule typedef_transfer_All [OF assms])
    1.74 -
    1.75  text {* Generating the correspondence rule for a constant defined with
    1.76    @{text "lift_definition"}. *}
    1.77  

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:53:28 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 18 10:52:49 2012 +0200
     2.3 @@ -136,7 +136,7 @@
     2.4        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
     2.5          [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
     2.6        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
     2.7 -        [T_def RS @{thm typedef_right_total}])
     2.8 +        [[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
     2.9        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]), 
    2.10          [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
    2.11        |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),