add [relator_mono] and [relator_distr] rules
authorkuncar
Fri Mar 08 13:21:52 2013 +0100 (2013-03-08)
changeset 513777da251a6c16e
parent 51376 8e38ff09864a
child 51378 502f6a53519b
add [relator_mono] and [relator_distr] rules
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Mar 08 13:21:45 2013 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Mar 08 13:21:52 2013 +0100
     1.3 @@ -22,7 +22,12 @@
     1.4      by (induct xs ys rule: list_induct2') simp_all
     1.5  qed
     1.6  
     1.7 -lemma list_all2_OO: "list_all2 (A OO B) = list_all2 A OO list_all2 B"
     1.8 +lemma list_all2_mono[relator_mono]:
     1.9 +  assumes "A \<le> B"
    1.10 +  shows "(list_all2 A) \<le> (list_all2 B)"
    1.11 +using assms by (auto intro: list_all2_mono)
    1.12 +
    1.13 +lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
    1.14  proof (intro ext iffI)
    1.15    fix xs ys
    1.16    assume "list_all2 (A OO B) xs ys"
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Mar 08 13:21:45 2013 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Mar 08 13:21:52 2013 +0100
     2.3 @@ -46,6 +46,15 @@
     2.4  lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
     2.5    by (metis option.exhaust) (* TODO: move to Option.thy *)
     2.6  
     2.7 +lemma option_rel_mono[relator_mono]:
     2.8 +  assumes "A \<le> B"
     2.9 +  shows "(option_rel A) \<le> (option_rel B)"
    2.10 +using assms by (auto simp: option_rel_unfold split: option.splits)
    2.11 +
    2.12 +lemma option_rel_OO[relator_distr]:
    2.13 +  "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
    2.14 +by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
    2.15 +
    2.16  lemma option_reflp[reflexivity_rule]:
    2.17    "reflp R \<Longrightarrow> reflp (option_rel R)"
    2.18    unfolding reflp_def split_option_all by simp
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Mar 08 13:21:45 2013 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Mar 08 13:21:52 2013 +0100
     3.3 @@ -27,6 +27,16 @@
     3.4    shows "prod_rel (op =) (op =) = (op =)"
     3.5    by (simp add: fun_eq_iff)
     3.6  
     3.7 +lemma prod_rel_mono[relator_mono]:
     3.8 +  assumes "A \<le> C"
     3.9 +  assumes "B \<le> D"
    3.10 +  shows "(prod_rel A B) \<le> (prod_rel C D)"
    3.11 +using assms by (auto simp: prod_rel_def)
    3.12 +
    3.13 +lemma prod_rel_OO[relator_distr]:
    3.14 +  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    3.15 +by (rule ext)+ (auto simp: prod_rel_def OO_def)
    3.16 +
    3.17  lemma prod_reflp [reflexivity_rule]:
    3.18    assumes "reflp R1"
    3.19    assumes "reflp R2"
     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 08 13:21:45 2013 +0100
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 08 13:21:52 2013 +0100
     4.3 @@ -22,7 +22,16 @@
     4.4  lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
     4.5    unfolding set_rel_def by auto
     4.6  
     4.7 -lemma set_rel_OO: "set_rel (R OO S) = set_rel R OO set_rel S"
     4.8 +lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
     4.9 +  unfolding set_rel_def fun_eq_iff by auto
    4.10 +
    4.11 +lemma set_rel_mono[relator_mono]:
    4.12 +  assumes "A \<le> B"
    4.13 +  shows "set_rel A \<le> set_rel B"
    4.14 +using assms unfolding set_rel_def by blast
    4.15 +
    4.16 +lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)"
    4.17 +  apply (rule sym)
    4.18    apply (intro ext, rename_tac X Z)
    4.19    apply (rule iffI)
    4.20    apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
    4.21 @@ -31,9 +40,6 @@
    4.22    apply (simp add: set_rel_def, fast)
    4.23    done
    4.24  
    4.25 -lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
    4.26 -  unfolding set_rel_def fun_eq_iff by auto
    4.27 -
    4.28  lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
    4.29    unfolding reflp_def set_rel_def by fast
    4.30  
    4.31 @@ -207,7 +213,7 @@
    4.32    assumes "Quotient R Abs Rep T"
    4.33    shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
    4.34    using assms unfolding Quotient_alt_def4
    4.35 -  apply (simp add: set_rel_OO set_rel_conversep)
    4.36 +  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
    4.37    apply (simp add: set_rel_def, fast)
    4.38    done
    4.39  
     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Mar 08 13:21:45 2013 +0100
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Mar 08 13:21:52 2013 +0100
     5.3 @@ -46,6 +46,16 @@
     5.4  lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
     5.5    by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
     5.6  
     5.7 +lemma sum_rel_mono[relator_mono]:
     5.8 +  assumes "A \<le> C"
     5.9 +  assumes "B \<le> D"
    5.10 +  shows "(sum_rel A B) \<le> (sum_rel C D)"
    5.11 +using assms by (auto simp: sum_rel_unfold split: sum.splits)
    5.12 +
    5.13 +lemma sum_rel_OO[relator_distr]:
    5.14 +  "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    5.15 +by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
    5.16 +
    5.17  lemma sum_reflp[reflexivity_rule]:
    5.18    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    5.19    unfolding reflp_def split_sum_all sum_rel.simps by fast