author kuncar Mon, 16 Apr 2012 20:50:43 +0200 changeset 47501 0b9294e093db parent 47500 5024b37c489c child 47502 4c949049cd78
leave Lifting prefix
 src/HOL/Lifting.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Lifting.thy	Mon Apr 16 23:23:08 2012 +0200
+++ b/src/HOL/Lifting.thy	Mon Apr 16 20:50:43 2012 +0200
@@ -256,7 +256,7 @@
lemma typedef_to_Quotient:
assumes "type_definition Rep Abs S"
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
+  shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
proof -
interpret type_definition Rep Abs S by fact
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
@@ -265,14 +265,14 @@

lemma typedef_to_part_equivp:
assumes "type_definition Rep Abs S"
-  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
+  shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
proof (intro part_equivpI)
interpret type_definition Rep Abs S by fact
-  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
+  show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
next
-  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
+  show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
next
-  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
+  show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
qed

lemma open_typedef_to_Quotient:```