# HG changeset patch
# User kuncar
# Date 1337188545 -7200
# Node ID 756f30eac7926b60426af2e8086a5f043cd8c07b
# Parent  631ea563c20a5ac9457f576363a33364d3370e09
infrastructure that makes possible to prove that a relation is reflexive

diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Wed May 16 19:15:45 2012 +0200
@@ -37,7 +37,7 @@
     by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
 qed
 
-lemma list_reflp:
+lemma list_reflp[reflp_preserve]:
   assumes "reflp R"
   shows "reflp (list_all2 R)"
 proof (rule reflpI)
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Wed May 16 19:15:45 2012 +0200
@@ -46,7 +46,7 @@
 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:
+lemma option_reflp[reflp_preserve]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
 
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Wed May 16 19:15:45 2012 +0200
@@ -27,6 +27,12 @@
   shows "prod_rel (op =) (op =) = (op =)"
   by (simp add: fun_eq_iff)
 
+lemma prod_reflp [reflp_preserve]:
+  assumes "reflp R1"
+  assumes "reflp R2"
+  shows "reflp (prod_rel R1 R2)"
+using assms by (auto intro!: reflpI elim: reflpE)
+
 lemma prod_equivp [quot_equiv]:
   assumes "equivp R1"
   assumes "equivp R2"
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Wed May 16 19:15:45 2012 +0200
@@ -34,7 +34,7 @@
 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
   unfolding set_rel_def fun_eq_iff by auto
 
-lemma reflp_set_rel: "reflp R \<Longrightarrow> reflp (set_rel R)"
+lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
   unfolding reflp_def set_rel_def by fast
 
 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Wed May 16 19:15:45 2012 +0200
@@ -46,7 +46,7 @@
 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:
+lemma sum_reflp[reflp_preserve]:
   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
   unfolding reflp_def split_sum_all sum_rel.simps by fast
 
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
@@ -100,6 +100,9 @@
 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:
@@ -364,6 +367,7 @@
 setup Lifting_Info.setup
 
 declare fun_quotient[quot_map]
+declare reflp_equality[reflp_preserve]
 
 use "Tools/Lifting/lifting_term.ML"
 
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed May 16 19:15:45 2012 +0200
@@ -20,6 +20,10 @@
   val print_quotients: Proof.context -> unit
 
   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 setup: theory -> theory
 end;
@@ -157,11 +161,22 @@
 
 fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
 
+structure Reflp_Preserve = Named_Thms
+(
+  val name = @{binding reflp_preserve}
+  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)
+
 (* theory setup *)
 
 val setup =
   quotmaps_attribute_setup
   #> Invariant_Commute.setup
+  #> Reflp_Preserve.setup
 
 (* outer syntax commands *)
 
diff -r 631ea563c20a -r 756f30eac792 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 19:15:45 2012 +0200
@@ -117,6 +117,8 @@
           [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
         |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
           [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+          [reflp_thm])
       | NONE => lthy
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
           [quot_thm RS @{thm Quotient_All_transfer}])
@@ -175,6 +177,8 @@
               [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
             |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
               [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
+            |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+              [reflp_thm])
         end
       | _ => lthy'
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),