Added lemmas
authornipkow
Fri Mar 14 19:57:12 2008 +0100 (2008-03-14)
changeset 26271e324f8918c98
parent 26270 73ac6430f5e7
child 26272 d63776c3be97
Added lemmas
src/HOL/IsaMakefile
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Mar 14 12:18:56 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Mar 14 19:57:12 2008 +0100
     1.3 @@ -170,7 +170,7 @@
     1.4  HOL-Complex: HOL $(OUT)/HOL-Complex
     1.5  
     1.6  $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
     1.7 -  Library/Zorn.thy							\
     1.8 +  Library/Zorn.thy Library/Order_Relation.thy				\
     1.9    Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy		\
    1.10    Real/Lubs.thy Real/PReal.thy Real/RComplete.thy 			\
    1.11    Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy	\
     2.1 --- a/src/HOL/Relation.thy	Fri Mar 14 12:18:56 2008 +0100
     2.2 +++ b/src/HOL/Relation.thy	Fri Mar 14 19:57:12 2008 +0100
     2.3 @@ -82,245 +82,245 @@
     2.4  subsection {* The identity relation *}
     2.5  
     2.6  lemma IdI [intro]: "(a, a) : Id"
     2.7 -  by (simp add: Id_def)
     2.8 +by (simp add: Id_def)
     2.9  
    2.10  lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
    2.11 -  by (unfold Id_def) (iprover elim: CollectE)
    2.12 +by (unfold Id_def) (iprover elim: CollectE)
    2.13  
    2.14  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
    2.15 -  by (unfold Id_def) blast
    2.16 +by (unfold Id_def) blast
    2.17  
    2.18  lemma reflexive_Id: "reflexive Id"
    2.19 -  by (simp add: refl_def)
    2.20 +by (simp add: refl_def)
    2.21  
    2.22  lemma antisym_Id: "antisym Id"
    2.23    -- {* A strange result, since @{text Id} is also symmetric. *}
    2.24 -  by (simp add: antisym_def)
    2.25 +by (simp add: antisym_def)
    2.26  
    2.27  lemma sym_Id: "sym Id"
    2.28 -  by (simp add: sym_def)
    2.29 +by (simp add: sym_def)
    2.30  
    2.31  lemma trans_Id: "trans Id"
    2.32 -  by (simp add: trans_def)
    2.33 +by (simp add: trans_def)
    2.34  
    2.35  
    2.36  subsection {* Diagonal: identity over a set *}
    2.37  
    2.38  lemma diag_empty [simp]: "diag {} = {}"
    2.39 -  by (simp add: diag_def) 
    2.40 +by (simp add: diag_def) 
    2.41  
    2.42  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    2.43 -  by (simp add: diag_def)
    2.44 +by (simp add: diag_def)
    2.45  
    2.46  lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
    2.47 -  by (rule diag_eqI) (rule refl)
    2.48 +by (rule diag_eqI) (rule refl)
    2.49  
    2.50  lemma diagE [elim!]:
    2.51    "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    2.52    -- {* The general elimination rule. *}
    2.53 -  by (unfold diag_def) (iprover elim!: UN_E singletonE)
    2.54 +by (unfold diag_def) (iprover elim!: UN_E singletonE)
    2.55  
    2.56  lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
    2.57 -  by blast
    2.58 +by blast
    2.59  
    2.60  lemma diag_subset_Times: "diag A \<subseteq> A \<times> A"
    2.61 -  by blast
    2.62 +by blast
    2.63  
    2.64  
    2.65  subsection {* Composition of two relations *}
    2.66  
    2.67  lemma rel_compI [intro]:
    2.68    "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
    2.69 -  by (unfold rel_comp_def) blast
    2.70 +by (unfold rel_comp_def) blast
    2.71  
    2.72  lemma rel_compE [elim!]: "xz : r O s ==>
    2.73    (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
    2.74 -  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    2.75 +by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    2.76  
    2.77  lemma rel_compEpair:
    2.78    "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
    2.79 -  by (iprover elim: rel_compE Pair_inject ssubst)
    2.80 +by (iprover elim: rel_compE Pair_inject ssubst)
    2.81  
    2.82  lemma R_O_Id [simp]: "R O Id = R"
    2.83 -  by fast
    2.84 +by fast
    2.85  
    2.86  lemma Id_O_R [simp]: "Id O R = R"
    2.87 -  by fast
    2.88 +by fast
    2.89  
    2.90  lemma rel_comp_empty1[simp]: "{} O R = {}"
    2.91 -  by blast
    2.92 +by blast
    2.93  
    2.94  lemma rel_comp_empty2[simp]: "R O {} = {}"
    2.95 -  by blast
    2.96 +by blast
    2.97  
    2.98  lemma O_assoc: "(R O S) O T = R O (S O T)"
    2.99 -  by blast
   2.100 +by blast
   2.101  
   2.102  lemma trans_O_subset: "trans r ==> r O r \<subseteq> r"
   2.103 -  by (unfold trans_def) blast
   2.104 +by (unfold trans_def) blast
   2.105  
   2.106  lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)"
   2.107 -  by blast
   2.108 +by blast
   2.109  
   2.110  lemma rel_comp_subset_Sigma:
   2.111      "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
   2.112 -  by blast
   2.113 +by blast
   2.114  
   2.115  
   2.116  subsection {* Reflexivity *}
   2.117  
   2.118  lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
   2.119 -  by (unfold refl_def) (iprover intro!: ballI)
   2.120 +by (unfold refl_def) (iprover intro!: ballI)
   2.121  
   2.122  lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   2.123 -  by (unfold refl_def) blast
   2.124 +by (unfold refl_def) blast
   2.125  
   2.126  lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
   2.127 -  by (unfold refl_def) blast
   2.128 +by (unfold refl_def) blast
   2.129  
   2.130  lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
   2.131 -  by (unfold refl_def) blast
   2.132 +by (unfold refl_def) blast
   2.133  
   2.134  lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
   2.135 -  by (unfold refl_def) blast
   2.136 +by (unfold refl_def) blast
   2.137  
   2.138  lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
   2.139 -  by (unfold refl_def) blast
   2.140 +by (unfold refl_def) blast
   2.141  
   2.142  lemma refl_INTER:
   2.143    "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
   2.144 -  by (unfold refl_def) fast
   2.145 +by (unfold refl_def) fast
   2.146  
   2.147  lemma refl_UNION:
   2.148    "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
   2.149 -  by (unfold refl_def) blast
   2.150 +by (unfold refl_def) blast
   2.151  
   2.152  lemma refl_diag: "refl A (diag A)"
   2.153 -  by (rule reflI [OF diag_subset_Times diagI])
   2.154 +by (rule reflI [OF diag_subset_Times diagI])
   2.155  
   2.156  
   2.157  subsection {* Antisymmetry *}
   2.158  
   2.159  lemma antisymI:
   2.160    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   2.161 -  by (unfold antisym_def) iprover
   2.162 +by (unfold antisym_def) iprover
   2.163  
   2.164  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   2.165 -  by (unfold antisym_def) iprover
   2.166 +by (unfold antisym_def) iprover
   2.167  
   2.168  lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
   2.169 -  by (unfold antisym_def) blast
   2.170 +by (unfold antisym_def) blast
   2.171  
   2.172  lemma antisym_empty [simp]: "antisym {}"
   2.173 -  by (unfold antisym_def) blast
   2.174 +by (unfold antisym_def) blast
   2.175  
   2.176  lemma antisym_diag [simp]: "antisym (diag A)"
   2.177 -  by (unfold antisym_def) blast
   2.178 +by (unfold antisym_def) blast
   2.179  
   2.180  
   2.181  subsection {* Symmetry *}
   2.182  
   2.183  lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
   2.184 -  by (unfold sym_def) iprover
   2.185 +by (unfold sym_def) iprover
   2.186  
   2.187  lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
   2.188 -  by (unfold sym_def, blast)
   2.189 +by (unfold sym_def, blast)
   2.190  
   2.191  lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
   2.192 -  by (fast intro: symI dest: symD)
   2.193 +by (fast intro: symI dest: symD)
   2.194  
   2.195  lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
   2.196 -  by (fast intro: symI dest: symD)
   2.197 +by (fast intro: symI dest: symD)
   2.198  
   2.199  lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
   2.200 -  by (fast intro: symI dest: symD)
   2.201 +by (fast intro: symI dest: symD)
   2.202  
   2.203  lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
   2.204 -  by (fast intro: symI dest: symD)
   2.205 +by (fast intro: symI dest: symD)
   2.206  
   2.207  lemma sym_diag [simp]: "sym (diag A)"
   2.208 -  by (rule symI) clarify
   2.209 +by (rule symI) clarify
   2.210  
   2.211  
   2.212  subsection {* Transitivity *}
   2.213  
   2.214  lemma transI:
   2.215    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
   2.216 -  by (unfold trans_def) iprover
   2.217 +by (unfold trans_def) iprover
   2.218  
   2.219  lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
   2.220 -  by (unfold trans_def) iprover
   2.221 +by (unfold trans_def) iprover
   2.222  
   2.223  lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
   2.224 -  by (fast intro: transI elim: transD)
   2.225 +by (fast intro: transI elim: transD)
   2.226  
   2.227  lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
   2.228 -  by (fast intro: transI elim: transD)
   2.229 +by (fast intro: transI elim: transD)
   2.230  
   2.231  lemma trans_diag [simp]: "trans (diag A)"
   2.232 -  by (fast intro: transI elim: transD)
   2.233 +by (fast intro: transI elim: transD)
   2.234  
   2.235  
   2.236  subsection {* Converse *}
   2.237  
   2.238  lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   2.239 -  by (simp add: converse_def)
   2.240 +by (simp add: converse_def)
   2.241  
   2.242  lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^-1"
   2.243 -  by (simp add: converse_def)
   2.244 +by (simp add: converse_def)
   2.245  
   2.246  lemma converseD[sym]: "(a,b) : r^-1 ==> (b, a) : r"
   2.247 -  by (simp add: converse_def)
   2.248 +by (simp add: converse_def)
   2.249  
   2.250  lemma converseE [elim!]:
   2.251    "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
   2.252      -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   2.253 -  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
   2.254 +by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
   2.255  
   2.256  lemma converse_converse [simp]: "(r^-1)^-1 = r"
   2.257 -  by (unfold converse_def) blast
   2.258 +by (unfold converse_def) blast
   2.259  
   2.260  lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   2.261 -  by blast
   2.262 +by blast
   2.263  
   2.264  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   2.265 -  by blast
   2.266 +by blast
   2.267  
   2.268  lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
   2.269 -  by blast
   2.270 +by blast
   2.271  
   2.272  lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)"
   2.273 -  by fast
   2.274 +by fast
   2.275  
   2.276  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
   2.277 -  by blast
   2.278 +by blast
   2.279  
   2.280  lemma converse_Id [simp]: "Id^-1 = Id"
   2.281 -  by blast
   2.282 +by blast
   2.283  
   2.284  lemma converse_diag [simp]: "(diag A)^-1 = diag A"
   2.285 -  by blast
   2.286 +by blast
   2.287  
   2.288  lemma refl_converse [simp]: "refl A (converse r) = refl A r"
   2.289 -  by (unfold refl_def) auto
   2.290 +by (unfold refl_def) auto
   2.291  
   2.292  lemma sym_converse [simp]: "sym (converse r) = sym r"
   2.293 -  by (unfold sym_def) blast
   2.294 +by (unfold sym_def) blast
   2.295  
   2.296  lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   2.297 -  by (unfold antisym_def) blast
   2.298 +by (unfold antisym_def) blast
   2.299  
   2.300  lemma trans_converse [simp]: "trans (converse r) = trans r"
   2.301 -  by (unfold trans_def) blast
   2.302 +by (unfold trans_def) blast
   2.303  
   2.304  lemma sym_conv_converse_eq: "sym r = (r^-1 = r)"
   2.305 -  by (unfold sym_def) fast
   2.306 +by (unfold sym_def) fast
   2.307  
   2.308  lemma sym_Un_converse: "sym (r \<union> r^-1)"
   2.309 -  by (unfold sym_def) blast
   2.310 +by (unfold sym_def) blast
   2.311  
   2.312  lemma sym_Int_converse: "sym (r \<inter> r^-1)"
   2.313 -  by (unfold sym_def) blast
   2.314 +by (unfold sym_def) blast
   2.315  
   2.316  
   2.317  subsection {* Domain *}
   2.318 @@ -328,87 +328,110 @@
   2.319  declare Domain_def [noatp]
   2.320  
   2.321  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   2.322 -  by (unfold Domain_def) blast
   2.323 +by (unfold Domain_def) blast
   2.324  
   2.325  lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
   2.326 -  by (iprover intro!: iffD2 [OF Domain_iff])
   2.327 +by (iprover intro!: iffD2 [OF Domain_iff])
   2.328  
   2.329  lemma DomainE [elim!]:
   2.330    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
   2.331 -  by (iprover dest!: iffD1 [OF Domain_iff])
   2.332 +by (iprover dest!: iffD1 [OF Domain_iff])
   2.333  
   2.334  lemma Domain_empty [simp]: "Domain {} = {}"
   2.335 -  by blast
   2.336 +by blast
   2.337  
   2.338  lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
   2.339 -  by blast
   2.340 +by blast
   2.341  
   2.342  lemma Domain_Id [simp]: "Domain Id = UNIV"
   2.343 -  by blast
   2.344 +by blast
   2.345  
   2.346  lemma Domain_diag [simp]: "Domain (diag A) = A"
   2.347 -  by blast
   2.348 +by blast
   2.349  
   2.350  lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
   2.351 -  by blast
   2.352 +by blast
   2.353  
   2.354  lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)"
   2.355 -  by blast
   2.356 +by blast
   2.357  
   2.358  lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)"
   2.359 -  by blast
   2.360 +by blast
   2.361  
   2.362  lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)"
   2.363 -  by blast
   2.364 +by blast
   2.365 +
   2.366 +lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
   2.367 +by(auto simp:Range_def)
   2.368  
   2.369  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
   2.370 -  by blast
   2.371 +by blast
   2.372  
   2.373  lemma fst_eq_Domain: "fst ` R = Domain R";
   2.374 -  apply auto
   2.375 -  apply (rule image_eqI, auto) 
   2.376 -  done
   2.377 +by (auto intro!:image_eqI)
   2.378  
   2.379  
   2.380  subsection {* Range *}
   2.381  
   2.382  lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
   2.383 -  by (simp add: Domain_def Range_def)
   2.384 +by (simp add: Domain_def Range_def)
   2.385  
   2.386  lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
   2.387 -  by (unfold Range_def) (iprover intro!: converseI DomainI)
   2.388 +by (unfold Range_def) (iprover intro!: converseI DomainI)
   2.389  
   2.390  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
   2.391 -  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   2.392 +by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
   2.393  
   2.394  lemma Range_empty [simp]: "Range {} = {}"
   2.395 -  by blast
   2.396 +by blast
   2.397  
   2.398  lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
   2.399 -  by blast
   2.400 +by blast
   2.401  
   2.402  lemma Range_Id [simp]: "Range Id = UNIV"
   2.403 -  by blast
   2.404 +by blast
   2.405  
   2.406  lemma Range_diag [simp]: "Range (diag A) = A"
   2.407 -  by auto
   2.408 +by auto
   2.409  
   2.410  lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
   2.411 -  by blast
   2.412 +by blast
   2.413  
   2.414  lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)"
   2.415 -  by blast
   2.416 +by blast
   2.417  
   2.418  lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)"
   2.419 -  by blast
   2.420 +by blast
   2.421  
   2.422  lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
   2.423 -  by blast
   2.424 +by blast
   2.425 +
   2.426 +lemma Range_converse[simp]: "Range(r^-1) = Domain r"
   2.427 +by blast
   2.428  
   2.429  lemma snd_eq_Range: "snd ` R = Range R";
   2.430 -  apply auto
   2.431 -  apply (rule image_eqI, auto) 
   2.432 -  done
   2.433 +by (auto intro!:image_eqI)
   2.434 +
   2.435 +
   2.436 +subsection {* Field *}
   2.437 +
   2.438 +lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   2.439 +by(auto simp:Field_def Domain_def Range_def)
   2.440 +
   2.441 +lemma Field_empty[simp]: "Field {} = {}"
   2.442 +by(auto simp:Field_def)
   2.443 +
   2.444 +lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r"
   2.445 +by(auto simp:Field_def)
   2.446 +
   2.447 +lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s"
   2.448 +by(auto simp:Field_def)
   2.449 +
   2.450 +lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
   2.451 +by(auto simp:Field_def)
   2.452 +
   2.453 +lemma Field_converse[simp]: "Field(r^-1) = Field r"
   2.454 +by(auto simp:Field_def)
   2.455  
   2.456  
   2.457  subsection {* Image of a set under a relation *}
   2.458 @@ -416,62 +439,62 @@
   2.459  declare Image_def [noatp]
   2.460  
   2.461  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   2.462 -  by (simp add: Image_def)
   2.463 +by (simp add: Image_def)
   2.464  
   2.465  lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
   2.466 -  by (simp add: Image_def)
   2.467 +by (simp add: Image_def)
   2.468  
   2.469  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   2.470 -  by (rule Image_iff [THEN trans]) simp
   2.471 +by (rule Image_iff [THEN trans]) simp
   2.472  
   2.473  lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
   2.474 -  by (unfold Image_def) blast
   2.475 +by (unfold Image_def) blast
   2.476  
   2.477  lemma ImageE [elim!]:
   2.478      "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   2.479 -  by (unfold Image_def) (iprover elim!: CollectE bexE)
   2.480 +by (unfold Image_def) (iprover elim!: CollectE bexE)
   2.481  
   2.482  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   2.483    -- {* This version's more effective when we already have the required @{text a} *}
   2.484 -  by blast
   2.485 +by blast
   2.486  
   2.487  lemma Image_empty [simp]: "R``{} = {}"
   2.488 -  by blast
   2.489 +by blast
   2.490  
   2.491  lemma Image_Id [simp]: "Id `` A = A"
   2.492 -  by blast
   2.493 +by blast
   2.494  
   2.495  lemma Image_diag [simp]: "diag A `` B = A \<inter> B"
   2.496 -  by blast
   2.497 +by blast
   2.498  
   2.499  lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
   2.500 -  by blast
   2.501 +by blast
   2.502  
   2.503  lemma Image_Int_eq:
   2.504       "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
   2.505 -  by (simp add: single_valued_def, blast) 
   2.506 +by (simp add: single_valued_def, blast) 
   2.507  
   2.508  lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
   2.509 -  by blast
   2.510 +by blast
   2.511  
   2.512  lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
   2.513 -  by blast
   2.514 +by blast
   2.515  
   2.516  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
   2.517 -  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   2.518 +by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   2.519  
   2.520  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
   2.521    -- {* NOT suitable for rewriting *}
   2.522 -  by blast
   2.523 +by blast
   2.524  
   2.525  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
   2.526 -  by blast
   2.527 +by blast
   2.528  
   2.529  lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
   2.530 -  by blast
   2.531 +by blast
   2.532  
   2.533  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
   2.534 -  by blast
   2.535 +by blast
   2.536  
   2.537  text{*Converse inclusion requires some assumptions*}
   2.538  lemma Image_INT_eq:
   2.539 @@ -482,50 +505,50 @@
   2.540  done
   2.541  
   2.542  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
   2.543 -  by blast
   2.544 +by blast
   2.545  
   2.546  
   2.547  subsection {* Single valued relations *}
   2.548  
   2.549  lemma single_valuedI:
   2.550    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   2.551 -  by (unfold single_valued_def)
   2.552 +by (unfold single_valued_def)
   2.553  
   2.554  lemma single_valuedD:
   2.555    "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   2.556 -  by (simp add: single_valued_def)
   2.557 +by (simp add: single_valued_def)
   2.558  
   2.559  lemma single_valued_rel_comp:
   2.560    "single_valued r ==> single_valued s ==> single_valued (r O s)"
   2.561 -  by (unfold single_valued_def) blast
   2.562 +by (unfold single_valued_def) blast
   2.563  
   2.564  lemma single_valued_subset:
   2.565    "r \<subseteq> s ==> single_valued s ==> single_valued r"
   2.566 -  by (unfold single_valued_def) blast
   2.567 +by (unfold single_valued_def) blast
   2.568  
   2.569  lemma single_valued_Id [simp]: "single_valued Id"
   2.570 -  by (unfold single_valued_def) blast
   2.571 +by (unfold single_valued_def) blast
   2.572  
   2.573  lemma single_valued_diag [simp]: "single_valued (diag A)"
   2.574 -  by (unfold single_valued_def) blast
   2.575 +by (unfold single_valued_def) blast
   2.576  
   2.577  
   2.578  subsection {* Graphs given by @{text Collect} *}
   2.579  
   2.580  lemma Domain_Collect_split [simp]: "Domain{(x,y). P x y} = {x. EX y. P x y}"
   2.581 -  by auto
   2.582 +by auto
   2.583  
   2.584  lemma Range_Collect_split [simp]: "Range{(x,y). P x y} = {y. EX x. P x y}"
   2.585 -  by auto
   2.586 +by auto
   2.587  
   2.588  lemma Image_Collect_split [simp]: "{(x,y). P x y} `` A = {y. EX x:A. P x y}"
   2.589 -  by auto
   2.590 +by auto
   2.591  
   2.592  
   2.593  subsection {* Inverse image *}
   2.594  
   2.595  lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
   2.596 -  by (unfold sym_def inv_image_def) blast
   2.597 +by (unfold sym_def inv_image_def) blast
   2.598  
   2.599  lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
   2.600    apply (unfold trans_def inv_image_def)
     3.1 --- a/src/HOL/Transitive_Closure.thy	Fri Mar 14 12:18:56 2008 +0100
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 14 19:57:12 2008 +0100
     3.3 @@ -63,6 +63,18 @@
     3.4    reflcl  ("(_\<^sup>=)" [1000] 999)
     3.5  
     3.6  
     3.7 +subsection {* Reflexive closure *}
     3.8 +
     3.9 +lemma reflexive_reflcl[simp]: "reflexive(r^=)"
    3.10 +by(simp add:refl_def)
    3.11 +
    3.12 +lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
    3.13 +by(simp add:antisym_def)
    3.14 +
    3.15 +lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
    3.16 +unfolding trans_def by blast
    3.17 +
    3.18 +
    3.19  subsection {* Reflexive-transitive closure *}
    3.20  
    3.21  lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)"
    3.22 @@ -546,7 +558,7 @@
    3.23    by (unfold Domain_def) (blast dest: tranclD)
    3.24  
    3.25  lemma trancl_range [simp]: "Range (r^+) = Range r"
    3.26 -  by (simp add: Range_def trancl_converse [symmetric])
    3.27 +unfolding Range_def by(simp add: trancl_converse [symmetric])
    3.28  
    3.29  lemma Not_Domain_rtrancl:
    3.30      "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"