# HG changeset patch
# User huffman
# Date 1141948408 -3600
# Node ID 30fce6da8cbefc9c643657408934e284728e6866
# Parent  d15f2baa7ecc6e3b4a8d7f4e34e52f2efc965cb9
added many simple lemmas

diff -r d15f2baa7ecc -r 30fce6da8cbe src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Mar 09 06:05:01 2006 +0100
+++ b/src/HOL/Relation.thy	Fri Mar 10 00:53:28 2006 +0100
@@ -82,6 +82,9 @@
   -- {* A strange result, since @{text Id} is also symmetric. *}
   by (simp add: antisym_def)
 
+lemma sym_Id: "sym Id"
+  by (simp add: sym_def)
+
 lemma trans_Id: "trans Id"
   by (simp add: trans_def)
 
@@ -151,6 +154,29 @@
 lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   by (unfold refl_def) blast
 
+lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
+  by (unfold refl_def) blast
+
+lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
+  by (unfold refl_def) blast
+
+lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
+  by (unfold refl_def) blast
+
+lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
+  by (unfold refl_def) blast
+
+lemma refl_INTER:
+  "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
+  by (unfold refl_def) fast
+
+lemma refl_UNION:
+  "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
+  by (unfold refl_def) blast
+
+lemma refl_diag: "refl A (diag A)"
+  by (rule reflI [OF diag_subset_Times diagI])
+
 
 subsection {* Antisymmetry *}
 
@@ -161,12 +187,42 @@
 lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   by (unfold antisym_def) iprover
 
+lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r"
+  by (unfold antisym_def) blast
 
-subsection {* Symmetry and Transitivity *}
+lemma antisym_empty [simp]: "antisym {}"
+  by (unfold antisym_def) blast
+
+lemma antisym_diag [simp]: "antisym (diag A)"
+  by (unfold antisym_def) blast
+
+
+subsection {* Symmetry *}
+
+lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r"
+  by (unfold sym_def) iprover
 
 lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r"
   by (unfold sym_def, blast)
 
+lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)"
+  by (fast intro: symI dest: symD)
+
+lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)"
+  by (fast intro: symI dest: symD)
+
+lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)"
+  by (fast intro: symI dest: symD)
+
+lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
+  by (fast intro: symI dest: symD)
+
+lemma sym_diag [simp]: "sym (diag A)"
+  by (rule symI) clarify
+
+
+subsection {* Transitivity *}
+
 lemma transI:
   "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
   by (unfold trans_def) iprover
@@ -174,6 +230,15 @@
 lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
   by (unfold trans_def) iprover
 
+lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)"
+  by (fast intro: transI elim: transD)
+
+lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
+  by (fast intro: transI elim: transD)
+
+lemma trans_diag [simp]: "trans (diag A)"
+  by (fast intro: transI elim: transD)
+
 
 subsection {* Converse *}
 
@@ -197,21 +262,45 @@
 lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   by blast
 
+lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
+  by blast
+
+lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1"
+  by blast
+
+lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)"
+  by fast
+
+lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
+  by blast
+
 lemma converse_Id [simp]: "Id^-1 = Id"
   by blast
 
 lemma converse_diag [simp]: "(diag A)^-1 = diag A"
   by blast
 
-lemma refl_converse: "refl A r ==> refl A (converse r)"
-  by (unfold refl_def) blast
+lemma refl_converse [simp]: "refl A (converse r) = refl A r"
+  by (unfold refl_def) auto
 
-lemma antisym_converse: "antisym (converse r) = antisym r"
+lemma sym_converse [simp]: "sym (converse r) = sym r"
+  by (unfold sym_def) blast
+
+lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   by (unfold antisym_def) blast
 
-lemma trans_converse: "trans (converse r) = trans r"
+lemma trans_converse [simp]: "trans (converse r) = trans r"
   by (unfold trans_def) blast
 
+lemma sym_conv_converse_eq: "sym r = (r^-1 = r)"
+  by (unfold sym_def) fast
+
+lemma sym_Un_converse: "sym (r \<union> r^-1)"
+  by (unfold sym_def) blast
+
+lemma sym_Int_converse: "sym (r \<inter> r^-1)"
+  by (unfold sym_def) blast
+
 
 subsection {* Domain *}
 
@@ -371,6 +460,20 @@
   "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
   by (simp add: single_valued_def)
 
+lemma single_valued_rel_comp:
+  "single_valued r ==> single_valued s ==> single_valued (r O s)"
+  by (unfold single_valued_def) blast
+
+lemma single_valued_subset:
+  "r \<subseteq> s ==> single_valued s ==> single_valued r"
+  by (unfold single_valued_def) blast
+
+lemma single_valued_Id [simp]: "single_valued Id"
+  by (unfold single_valued_def) blast
+
+lemma single_valued_diag [simp]: "single_valued (diag A)"
+  by (unfold single_valued_def) blast
+
 
 subsection {* Graphs given by @{text Collect} *}
 
@@ -386,6 +489,9 @@
 
 subsection {* Inverse image *}
 
+lemma sym_inv_image: "sym r ==> sym (inv_image r f)"
+  by (unfold sym_def inv_image_def) blast
+
 lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
   apply (unfold trans_def inv_image_def)
   apply (simp (no_asm))
diff -r d15f2baa7ecc -r 30fce6da8cbe src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Mar 09 06:05:01 2006 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Mar 10 00:53:28 2006 +0100
@@ -82,6 +82,9 @@
   rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
                  consumes 1, case_names refl step]
 
+lemma reflexive_rtrancl: "reflexive (r^*)"
+  by (unfold refl_def) fast
+
 lemma trans_rtrancl: "trans(r^*)"
   -- {* transitivity of transitive closure!! -- by induction *}
 proof (rule transI)
@@ -168,6 +171,9 @@
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
 
+lemma sym_rtrancl: "sym r ==> sym (r^*)"
+  by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
+
 theorem converse_rtrancl_induct[consumes 1]:
   assumes major: "(a, b) : r^*"
     and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
@@ -308,6 +314,9 @@
   by (fastsimp simp add: split_tupled_all
     intro!: trancl_converseI trancl_converseD)
 
+lemma sym_trancl: "sym r ==> sym (r^+)"
+  by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
+
 lemma converse_trancl_induct:
   assumes major: "(a,b) : r^+"
     and cases: "!!y. (y,b) : r ==> P(y)"