src/HOL/Lifting.thy
changeset 47651 8e4f50afd21a
parent 47575 b90cd7016d4f
child 47652 1b722b100301
     1.1 --- a/src/HOL/Lifting.thy	Sat Apr 21 11:21:23 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Sat Apr 21 13:06:22 2012 +0200
     1.3 @@ -270,23 +270,12 @@
     1.4    assumes "type_definition Rep Abs {x. P x}"
     1.5    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
     1.6    shows "Quotient (invariant P) Abs Rep T"
     1.7 -proof -
     1.8 -  interpret type_definition Rep Abs "{x. P x}" by fact
     1.9 -  from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
    1.10 -    by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
    1.11 -qed
    1.12 +  using typedef_to_Quotient [OF assms] by simp
    1.13  
    1.14  lemma open_typedef_to_part_equivp:
    1.15    assumes "type_definition Rep Abs {x. P x}"
    1.16    shows "part_equivp (invariant P)"
    1.17 -proof (intro part_equivpI)
    1.18 -  interpret type_definition Rep Abs "{x. P x}" by fact
    1.19 -  show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
    1.20 -next
    1.21 -  show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
    1.22 -next
    1.23 -  show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
    1.24 -qed
    1.25 +  using typedef_to_part_equivp [OF assms] by simp
    1.26  
    1.27  text {* Generating transfer rules for quotients. *}
    1.28