src/HOL/Relation.thy
changeset 19228 30fce6da8cbe
parent 17589 58eeffd73be1
child 19323 ec5cd5b1804c
     1.1 --- a/src/HOL/Relation.thy	Thu Mar 09 06:05:01 2006 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Mar 10 00:53:28 2006 +0100
     1.3 @@ -82,6 +82,9 @@
     1.4    -- {* A strange result, since @{text Id} is also symmetric. *}
     1.5    by (simp add: antisym_def)
     1.6  
     1.7 +lemma sym_Id: "sym Id"
     1.8 +  by (simp add: sym_def)
     1.9 +
    1.10  lemma trans_Id: "trans Id"
    1.11    by (simp add: trans_def)
    1.12  
    1.13 @@ -151,6 +154,29 @@
    1.14  lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
    1.15    by (unfold refl_def) blast
    1.16  
    1.17 +lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
    1.18 +  by (unfold refl_def) blast
    1.19 +
    1.20 +lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
    1.21 +  by (unfold refl_def) blast
    1.22 +
    1.23 +lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
    1.24 +  by (unfold refl_def) blast
    1.25 +
    1.26 +lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
    1.27 +  by (unfold refl_def) blast
    1.28 +
    1.29 +lemma refl_INTER:
    1.30 +  "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
    1.31 +  by (unfold refl_def) fast
    1.32 +
    1.33 +lemma refl_UNION:
    1.34 +  "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
    1.35 +  by (unfold refl_def) blast
    1.36 +
    1.37 +lemma refl_diag: "refl A (diag A)"
    1.38 +  by (rule reflI [OF diag_subset_Times diagI])
    1.39 +
    1.40  
    1.41  subsection {* Antisymmetry *}
    1.42  
    1.43 @@ -161,12 +187,42 @@
    1.44  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
    1.45    by (unfold antisym_def) iprover
    1.46  
    1.47 +lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
    1.48 +  by (unfold antisym_def) blast
    1.49  
    1.50 -subsection {* Symmetry and Transitivity *}
    1.51 +lemma antisym_empty [simp]: "antisym {}"
    1.52 +  by (unfold antisym_def) blast
    1.53 +
    1.54 +lemma antisym_diag [simp]: "antisym (diag A)"
    1.55 +  by (unfold antisym_def) blast
    1.56 +
    1.57 +
    1.58 +subsection {* Symmetry *}
    1.59 +
    1.60 +lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
    1.61 +  by (unfold sym_def) iprover
    1.62  
    1.63  lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
    1.64    by (unfold sym_def, blast)
    1.65  
    1.66 +lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
    1.67 +  by (fast intro: symI dest: symD)
    1.68 +
    1.69 +lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
    1.70 +  by (fast intro: symI dest: symD)
    1.71 +
    1.72 +lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
    1.73 +  by (fast intro: symI dest: symD)
    1.74 +
    1.75 +lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
    1.76 +  by (fast intro: symI dest: symD)
    1.77 +
    1.78 +lemma sym_diag [simp]: "sym (diag A)"
    1.79 +  by (rule symI) clarify
    1.80 +
    1.81 +
    1.82 +subsection {* Transitivity *}
    1.83 +
    1.84  lemma transI:
    1.85    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
    1.86    by (unfold trans_def) iprover
    1.87 @@ -174,6 +230,15 @@
    1.88  lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
    1.89    by (unfold trans_def) iprover
    1.90  
    1.91 +lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
    1.92 +  by (fast intro: transI elim: transD)
    1.93 +
    1.94 +lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
    1.95 +  by (fast intro: transI elim: transD)
    1.96 +
    1.97 +lemma trans_diag [simp]: "trans (diag A)"
    1.98 +  by (fast intro: transI elim: transD)
    1.99 +
   1.100  
   1.101  subsection {* Converse *}
   1.102  
   1.103 @@ -197,21 +262,45 @@
   1.104  lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   1.105    by blast
   1.106  
   1.107 +lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   1.108 +  by blast
   1.109 +
   1.110 +lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
   1.111 +  by blast
   1.112 +
   1.113 +lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)"
   1.114 +  by fast
   1.115 +
   1.116 +lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
   1.117 +  by blast
   1.118 +
   1.119  lemma converse_Id [simp]: "Id^-1 = Id"
   1.120    by blast
   1.121  
   1.122  lemma converse_diag [simp]: "(diag A)^-1 = diag A"
   1.123    by blast
   1.124  
   1.125 -lemma refl_converse: "refl A r ==> refl A (converse r)"
   1.126 -  by (unfold refl_def) blast
   1.127 +lemma refl_converse [simp]: "refl A (converse r) = refl A r"
   1.128 +  by (unfold refl_def) auto
   1.129  
   1.130 -lemma antisym_converse: "antisym (converse r) = antisym r"
   1.131 +lemma sym_converse [simp]: "sym (converse r) = sym r"
   1.132 +  by (unfold sym_def) blast
   1.133 +
   1.134 +lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   1.135    by (unfold antisym_def) blast
   1.136  
   1.137 -lemma trans_converse: "trans (converse r) = trans r"
   1.138 +lemma trans_converse [simp]: "trans (converse r) = trans r"
   1.139    by (unfold trans_def) blast
   1.140  
   1.141 +lemma sym_conv_converse_eq: "sym r = (r^-1 = r)"
   1.142 +  by (unfold sym_def) fast
   1.143 +
   1.144 +lemma sym_Un_converse: "sym (r \<union> r^-1)"
   1.145 +  by (unfold sym_def) blast
   1.146 +
   1.147 +lemma sym_Int_converse: "sym (r \<inter> r^-1)"
   1.148 +  by (unfold sym_def) blast
   1.149 +
   1.150  
   1.151  subsection {* Domain *}
   1.152  
   1.153 @@ -371,6 +460,20 @@
   1.154    "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   1.155    by (simp add: single_valued_def)
   1.156  
   1.157 +lemma single_valued_rel_comp:
   1.158 +  "single_valued r ==> single_valued s ==> single_valued (r O s)"
   1.159 +  by (unfold single_valued_def) blast
   1.160 +
   1.161 +lemma single_valued_subset:
   1.162 +  "r \<subseteq> s ==> single_valued s ==> single_valued r"
   1.163 +  by (unfold single_valued_def) blast
   1.164 +
   1.165 +lemma single_valued_Id [simp]: "single_valued Id"
   1.166 +  by (unfold single_valued_def) blast
   1.167 +
   1.168 +lemma single_valued_diag [simp]: "single_valued (diag A)"
   1.169 +  by (unfold single_valued_def) blast
   1.170 +
   1.171  
   1.172  subsection {* Graphs given by @{text Collect} *}
   1.173  
   1.174 @@ -386,6 +489,9 @@
   1.175  
   1.176  subsection {* Inverse image *}
   1.177  
   1.178 +lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
   1.179 +  by (unfold sym_def inv_image_def) blast
   1.180 +
   1.181  lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
   1.182    apply (unfold trans_def inv_image_def)
   1.183    apply (simp (no_asm))