src/HOL/Lifting.thy
 changeset 47982 7aa35601ff65 parent 47937 70375fa2679d child 48891 c0eafbd55de3
```--- a/src/HOL/Lifting.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Lifting.thy	Thu May 24 14:20:23 2012 +0200
@@ -121,9 +121,6 @@
lemma identity_quotient: "Quotient (op =) id id (op =)"
unfolding Quotient_def by simp

-lemma reflp_equality: "reflp (op =)"
-by (auto intro: reflpI)
-
text {* TODO: Use one of these alternatives as the real definition. *}

lemma Quotient_alt_def:
@@ -380,6 +377,45 @@
shows "T c c'"
using assms by (auto dest: Quotient_cr_rel)

+text {* Proving reflexivity *}
+
+definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
+
+lemma left_totalI:
+  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
+unfolding left_total_def by blast
+
+lemma left_totalE:
+  assumes "left_total R"
+  obtains "(\<And>x. \<exists>y. R x y)"
+using assms unfolding left_total_def by blast
+
+lemma Quotient_to_left_total:
+  assumes q: "Quotient R Abs Rep T"
+  and r_R: "reflp R"
+  shows "left_total T"
+using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
+
+lemma reflp_Quotient_composition:
+  assumes lt_R1: "left_total R1"
+  and r_R2: "reflp R2"
+  shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
+using assms
+proof -
+  {
+    fix x
+    from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
+    moreover then have "R1\<inverse>\<inverse> y x" by simp
+    moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
+    ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
+  }
+  then show ?thesis by (auto intro: reflpI)
+qed
+
+lemma reflp_equality: "reflp (op =)"
+by (auto intro: reflpI)
+
subsection {* ML setup *}

use "Tools/Lifting/lifting_util.ML"
@@ -388,7 +424,7 @@
setup Lifting_Info.setup

declare fun_quotient[quot_map]
-declare reflp_equality[reflp_preserve]
+lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition

use "Tools/Lifting/lifting_term.ML"
```