# HG changeset patch
# User kuncar
# Date 1362745312 -3600
# Node ID 7da251a6c16e57703f7d09528f4d4358c816ccd1
# Parent  8e38ff09864a13697170db44405d56cc54008bd7
add [relator_mono] and [relator_distr] rules

diff -r 8e38ff09864a -r 7da251a6c16e src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Mar 08 13:21:45 2013 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Fri Mar 08 13:21:52 2013 +0100
@@ -22,7 +22,12 @@
     by (induct xs ys rule: list_induct2') simp_all
 qed
 
-lemma list_all2_OO: "list_all2 (A OO B) = list_all2 A OO list_all2 B"
+lemma list_all2_mono[relator_mono]:
+  assumes "A \<le> B"
+  shows "(list_all2 A) \<le> (list_all2 B)"
+using assms by (auto intro: list_all2_mono)
+
+lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
 proof (intro ext iffI)
   fix xs ys
   assume "list_all2 (A OO B) xs ys"
diff -r 8e38ff09864a -r 7da251a6c16e src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Mar 08 13:21:45 2013 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Mar 08 13:21:52 2013 +0100
@@ -46,6 +46,15 @@
 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_rel_mono[relator_mono]:
+  assumes "A \<le> B"
+  shows "(option_rel A) \<le> (option_rel B)"
+using assms by (auto simp: option_rel_unfold split: option.splits)
+
+lemma option_rel_OO[relator_distr]:
+  "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
+by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
+
 lemma option_reflp[reflexivity_rule]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
diff -r 8e38ff09864a -r 7da251a6c16e src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Fri Mar 08 13:21:45 2013 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Fri Mar 08 13:21:52 2013 +0100
@@ -27,6 +27,16 @@
   shows "prod_rel (op =) (op =) = (op =)"
   by (simp add: fun_eq_iff)
 
+lemma prod_rel_mono[relator_mono]:
+  assumes "A \<le> C"
+  assumes "B \<le> D"
+  shows "(prod_rel A B) \<le> (prod_rel C D)"
+using assms by (auto simp: prod_rel_def)
+
+lemma prod_rel_OO[relator_distr]:
+  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
+by (rule ext)+ (auto simp: prod_rel_def OO_def)
+
 lemma prod_reflp [reflexivity_rule]:
   assumes "reflp R1"
   assumes "reflp R2"
diff -r 8e38ff09864a -r 7da251a6c16e src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 08 13:21:45 2013 +0100
+++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 08 13:21:52 2013 +0100
@@ -22,7 +22,16 @@
 lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
   unfolding set_rel_def by auto
 
-lemma set_rel_OO: "set_rel (R OO S) = set_rel R OO set_rel S"
+lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
+  unfolding set_rel_def fun_eq_iff by auto
+
+lemma set_rel_mono[relator_mono]:
+  assumes "A \<le> B"
+  shows "set_rel A \<le> set_rel B"
+using assms unfolding set_rel_def by blast
+
+lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)"
+  apply (rule sym)
   apply (intro ext, rename_tac X Z)
   apply (rule iffI)
   apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
@@ -31,9 +40,6 @@
   apply (simp add: set_rel_def, fast)
   done
 
-lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
-  unfolding set_rel_def fun_eq_iff by auto
-
 lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
   unfolding reflp_def set_rel_def by fast
 
@@ -207,7 +213,7 @@
   assumes "Quotient R Abs Rep T"
   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
   using assms unfolding Quotient_alt_def4
-  apply (simp add: set_rel_OO set_rel_conversep)
+  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
   apply (simp add: set_rel_def, fast)
   done
 
diff -r 8e38ff09864a -r 7da251a6c16e src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Mar 08 13:21:45 2013 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Mar 08 13:21:52 2013 +0100
@@ -46,6 +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_rel_mono[relator_mono]:
+  assumes "A \<le> C"
+  assumes "B \<le> D"
+  shows "(sum_rel A B) \<le> (sum_rel C D)"
+using assms by (auto simp: sum_rel_unfold split: sum.splits)
+
+lemma sum_rel_OO[relator_distr]:
+  "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
+by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
+
 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