added many simple lemmas
authorhuffman
Fri Mar 10 00:53:28 2006 +0100 (2006-03-10)
changeset 1922830fce6da8cbe
parent 19227 d15f2baa7ecc
child 19229 7183628d7b29
added many simple lemmas
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
     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))
     2.1 --- a/src/HOL/Transitive_Closure.thy	Thu Mar 09 06:05:01 2006 +0100
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 10 00:53:28 2006 +0100
     2.3 @@ -82,6 +82,9 @@
     2.4    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
     2.5                   consumes 1, case_names refl step]
     2.6  
     2.7 +lemma reflexive_rtrancl: "reflexive (r^*)"
     2.8 +  by (unfold refl_def) fast
     2.9 +
    2.10  lemma trans_rtrancl: "trans(r^*)"
    2.11    -- {* transitivity of transitive closure!! -- by induction *}
    2.12  proof (rule transI)
    2.13 @@ -168,6 +171,9 @@
    2.14  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
    2.15    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
    2.16  
    2.17 +lemma sym_rtrancl: "sym r ==> sym (r^*)"
    2.18 +  by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
    2.19 +
    2.20  theorem converse_rtrancl_induct[consumes 1]:
    2.21    assumes major: "(a, b) : r^*"
    2.22      and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
    2.23 @@ -308,6 +314,9 @@
    2.24    by (fastsimp simp add: split_tupled_all
    2.25      intro!: trancl_converseI trancl_converseD)
    2.26  
    2.27 +lemma sym_trancl: "sym r ==> sym (r^+)"
    2.28 +  by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
    2.29 +
    2.30  lemma converse_trancl_induct:
    2.31    assumes major: "(a,b) : r^+"
    2.32      and cases: "!!y. (y,b) : r ==> P(y)"