# HG changeset patch # User huffman # Date 1335006382 -7200 # Node ID 8e4f50afd21a89f2b23b44419a3b3890981ed9bb # Parent 33ecf14d5ee9fbe6c07291ea439119c5c5ff83ad tuned proofs diff -r 33ecf14d5ee9 -r 8e4f50afd21a src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Sat Apr 21 11:21:23 2012 +0200 +++ b/src/HOL/Lifting.thy Sat Apr 21 13:06:22 2012 +0200 @@ -270,23 +270,12 @@ assumes "type_definition Rep Abs {x. P x}" and T_def: "T \ (\x y. x = Rep y)" shows "Quotient (invariant P) Abs Rep T" -proof - - interpret type_definition Rep Abs "{x. P x}" by fact - from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis - by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) -qed + using typedef_to_Quotient [OF assms] by simp lemma open_typedef_to_part_equivp: assumes "type_definition Rep Abs {x. P x}" shows "part_equivp (invariant P)" -proof (intro part_equivpI) - interpret type_definition Rep Abs "{x. P x}" by fact - show "\x. invariant P x x" using Rep by (auto simp: invariant_def) -next - show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) -next - show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) -qed + using typedef_to_part_equivp [OF assms] by simp text {* Generating transfer rules for quotients. *}