src/HOL/Relation.thy
 changeset 29609 a010aab5bed0 parent 28008 f945f8d9ad4d child 29859 33bff35f1335
```     1.1 --- a/src/HOL/Relation.thy	Wed Jan 21 23:40:23 2009 +0100
1.2 +++ b/src/HOL/Relation.thy	Wed Jan 21 23:40:23 2009 +0100
1.3 @@ -1,5 +1,4 @@
1.4  (*  Title:      HOL/Relation.thy
1.5 -    ID:         \$Id\$
1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7      Copyright   1996  University of Cambridge
1.8  *)
1.9 @@ -7,7 +6,7 @@
1.11
1.12  theory Relation
1.13 -imports Product_Type
1.14 +imports Datatype Finite_Set
1.15  begin
1.16
1.17  subsection {* Definitions *}
1.18 @@ -379,6 +378,12 @@
1.19  lemma fst_eq_Domain: "fst ` R = Domain R";
1.20  by (auto intro!:image_eqI)
1.21
1.22 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
1.23 +by auto
1.24 +
1.25 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
1.26 +by auto
1.27 +
1.28
1.29  subsection {* Range *}
1.30
1.31 @@ -566,6 +571,31 @@
1.32    done
1.33
1.34
1.35 +subsection {* Finiteness *}
1.36 +
1.37 +lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.38 +  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
1.39 +   apply simp
1.40 +   apply (rule iffI)
1.41 +    apply (erule finite_imageD [unfolded inj_on_def])
1.42 +    apply (simp split add: split_split)
1.43 +   apply (erule finite_imageI)
1.44 +  apply (simp add: converse_def image_def, auto)
1.45 +  apply (rule bexI)
1.46 +   prefer 2 apply assumption
1.47 +  apply simp
1.48 +  done
1.49 +
1.50 +text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
1.51 +Ehmety) *}
1.52 +
1.53 +lemma finite_Field: "finite r ==> finite (Field r)"
1.54 +  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
1.55 +  apply (induct set: finite)
1.56 +   apply (auto simp add: Field_def Domain_insert Range_insert)
1.57 +  done
1.58 +
1.59 +
1.60  subsection {* Version of @{text lfp_induct} for binary relations *}
1.61
1.62  lemmas lfp_induct2 =
```