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.10  header {* Relations *}
    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 =