prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

--- a/src/HOL/Library/Quotient_List.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Thu May 24 14:20:23 2012 +0200
@@ -37,7 +37,7 @@
     by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
 qed
 
-lemma list_reflp[reflp_preserve]:
+lemma list_reflp[reflexivity_rule]:
   assumes "reflp R"
   shows "reflp (list_all2 R)"
 proof (rule reflpI)
@@ -47,6 +47,17 @@
     by (induct xs) (simp_all add: *)
 qed
 
+lemma list_left_total[reflexivity_rule]:
+  assumes "left_total R"
+  shows "left_total (list_all2 R)"
+proof (rule left_totalI)
+  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
+  fix xs
+  show "\<exists> ys. list_all2 R xs ys"
+    by (induct xs) (simp_all add: * list_all2_Cons1)
+qed
+
+
 lemma list_symp:
   assumes "symp R"
   shows "symp (list_all2 R)"

--- a/src/HOL/Library/Quotient_Option.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Thu May 24 14:20:23 2012 +0200
@@ -46,10 +46,16 @@
 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
   by (metis option.exhaust) (* TODO: move to Option.thy *)
 
-lemma option_reflp[reflp_preserve]:
+lemma option_reflp[reflexivity_rule]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
 
+lemma option_left_total[reflexivity_rule]:
+  "left_total R \<Longrightarrow> left_total (option_rel R)"
+  apply (intro left_totalI)
+  unfolding split_option_ex
+  by (case_tac x) (auto elim: left_totalE)
+
 lemma option_symp:
   "symp R \<Longrightarrow> symp (option_rel R)"
   unfolding symp_def split_option_all option_rel.simps by fast

--- a/src/HOL/Library/Quotient_Product.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Thu May 24 14:20:23 2012 +0200
@@ -27,12 +27,18 @@
   shows "prod_rel (op =) (op =) = (op =)"
   by (simp add: fun_eq_iff)
 
-lemma prod_reflp [reflp_preserve]:
+lemma prod_reflp [reflexivity_rule]:
   assumes "reflp R1"
   assumes "reflp R2"
   shows "reflp (prod_rel R1 R2)"
 using assms by (auto intro!: reflpI elim: reflpE)
 
+lemma prod_left_total [reflexivity_rule]:
+  assumes "left_total R1"
+  assumes "left_total R2"
+  shows "left_total (prod_rel R1 R2)"
+using assms by (auto intro!: left_totalI elim!: left_totalE)
+
 lemma prod_equivp [quot_equiv]:
   assumes "equivp R1"
   assumes "equivp R2"

--- a/src/HOL/Library/Quotient_Set.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Thu May 24 14:20:23 2012 +0200
@@ -34,9 +34,22 @@
 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
   unfolding set_rel_def fun_eq_iff by auto
 
-lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
+lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
   unfolding reflp_def set_rel_def by fast
 
+lemma left_total_set_rel[reflexivity_rule]:
+  assumes lt_R: "left_total R"
+  shows "left_total (set_rel R)"
+proof -
+  {
+    fix A
+    let ?B = "{y. \<exists>x \<in> A. R x y}"
+    have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast
+  }
+  then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast
+  then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
+qed
+
 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
   unfolding symp_def set_rel_def by fast
 

--- a/src/HOL/Library/Quotient_Sum.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Thu May 24 14:20:23 2012 +0200
@@ -46,10 +46,16 @@
 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
   by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
 
-lemma sum_reflp[reflp_preserve]:
+lemma sum_reflp[reflexivity_rule]:
   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
   unfolding reflp_def split_sum_all sum_rel.simps by fast
 
+lemma sum_left_total[reflexivity_rule]:
+  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
+  apply (intro left_totalI)
+  unfolding split_sum_ex 
+  by (case_tac x) (auto elim: left_totalE)
+
 lemma sum_symp:
   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
   unfolding symp_def split_sum_all sum_rel.simps by fast

--- 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"
 

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu May 24 14:20:23 2012 +0200
@@ -182,7 +182,7 @@
         
         val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
         val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
-        val rules = Lifting_Info.get_reflp_preserve_rules ctxt
+        val rules = Lifting_Info.get_reflexivity_rules ctxt
       in
         EVERY' [CSUBGOAL intro_reflp_tac, 
                 CONVERSION conv,

--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 14:20:23 2012 +0200
@@ -21,9 +21,9 @@
 
   val get_invariant_commute_rules: Proof.context -> thm list
   
-  val get_reflp_preserve_rules: Proof.context -> thm list
-  val add_reflp_preserve_rule_attribute: attribute
-  val add_reflp_preserve_rule_attrib: Attrib.src
+  val get_reflexivity_rules: Proof.context -> thm list
+  val add_reflexivity_rule_attribute: attribute
+  val add_reflexivity_rule_attrib: Attrib.src
 
   val setup: theory -> theory
 end;
@@ -183,13 +183,13 @@
 
 structure Reflp_Preserve = Named_Thms
 (
-  val name = @{binding reflp_preserve}
+  val name = @{binding reflexivity_rule}
   val description = "theorems that a relator preserves a reflexivity property"
 )
 
-val get_reflp_preserve_rules = Reflp_Preserve.get
-val add_reflp_preserve_rule_attribute = Reflp_Preserve.add
-val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute)
+val get_reflexivity_rules = Reflp_Preserve.get
+val add_reflexivity_rule_attribute = Reflp_Preserve.add
+val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
 
 (* theory setup *)
 

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu May 24 14:20:23 2012 +0200
@@ -103,8 +103,10 @@
     fun quot_info phi = Lifting_Info.transform_quotients phi quotients
     val lthy' = case maybe_reflp_thm of
       SOME reflp_thm => lthy
-        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
               [reflp_thm])
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
+              [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
         |> define_code_constr gen_code quot_thm
       | NONE => lthy
         |> define_abs_type gen_code quot_thm