src/HOL/Relation.thy
changeset 30198 922f944f03b2
parent 29859 33bff35f1335
child 31011 506e57123cd1
     1.1 --- a/src/HOL/Relation.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -34,8 +34,8 @@
     1.4    "Id == {p. EX x. p = (x,x)}"
     1.5  
     1.6  definition
     1.7 -  diag  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
     1.8 -  "diag A == \<Union>x\<in>A. {(x,x)}"
     1.9 +  Id_on  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
    1.10 +  "Id_on A == \<Union>x\<in>A. {(x,x)}"
    1.11  
    1.12  definition
    1.13    Domain :: "('a * 'b) set => 'a set" where
    1.14 @@ -50,12 +50,12 @@
    1.15    "Field r == Domain r \<union> Range r"
    1.16  
    1.17  definition
    1.18 -  refl :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
    1.19 -  "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
    1.20 +  refl_on :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
    1.21 +  "refl_on A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
    1.22  
    1.23  abbreviation
    1.24 -  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
    1.25 -  "reflexive == refl UNIV"
    1.26 +  refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
    1.27 +  "refl == refl_on UNIV"
    1.28  
    1.29  definition
    1.30    sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
    1.31 @@ -99,8 +99,8 @@
    1.32  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
    1.33  by (unfold Id_def) blast
    1.34  
    1.35 -lemma reflexive_Id: "reflexive Id"
    1.36 -by (simp add: refl_def)
    1.37 +lemma refl_Id: "refl Id"
    1.38 +by (simp add: refl_on_def)
    1.39  
    1.40  lemma antisym_Id: "antisym Id"
    1.41    -- {* A strange result, since @{text Id} is also symmetric. *}
    1.42 @@ -115,24 +115,24 @@
    1.43  
    1.44  subsection {* Diagonal: identity over a set *}
    1.45  
    1.46 -lemma diag_empty [simp]: "diag {} = {}"
    1.47 -by (simp add: diag_def) 
    1.48 +lemma Id_on_empty [simp]: "Id_on {} = {}"
    1.49 +by (simp add: Id_on_def) 
    1.50  
    1.51 -lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    1.52 -by (simp add: diag_def)
    1.53 +lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
    1.54 +by (simp add: Id_on_def)
    1.55  
    1.56 -lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
    1.57 -by (rule diag_eqI) (rule refl)
    1.58 +lemma Id_onI [intro!,noatp]: "a : A ==> (a, a) : Id_on A"
    1.59 +by (rule Id_on_eqI) (rule refl)
    1.60  
    1.61 -lemma diagE [elim!]:
    1.62 -  "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    1.63 +lemma Id_onE [elim!]:
    1.64 +  "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    1.65    -- {* The general elimination rule. *}
    1.66 -by (unfold diag_def) (iprover elim!: UN_E singletonE)
    1.67 +by (unfold Id_on_def) (iprover elim!: UN_E singletonE)
    1.68  
    1.69 -lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
    1.70 +lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
    1.71  by blast
    1.72  
    1.73 -lemma diag_subset_Times: "diag A \<subseteq> A \<times> A"
    1.74 +lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
    1.75  by blast
    1.76  
    1.77  
    1.78 @@ -184,37 +184,37 @@
    1.79  
    1.80  subsection {* Reflexivity *}
    1.81  
    1.82 -lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
    1.83 -by (unfold refl_def) (iprover intro!: ballI)
    1.84 +lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r"
    1.85 +by (unfold refl_on_def) (iprover intro!: ballI)
    1.86  
    1.87 -lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
    1.88 -by (unfold refl_def) blast
    1.89 +lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r"
    1.90 +by (unfold refl_on_def) blast
    1.91  
    1.92 -lemma reflD1: "refl A r ==> (x, y) : r ==> x : A"
    1.93 -by (unfold refl_def) blast
    1.94 +lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A"
    1.95 +by (unfold refl_on_def) blast
    1.96  
    1.97 -lemma reflD2: "refl A r ==> (x, y) : r ==> y : A"
    1.98 -by (unfold refl_def) blast
    1.99 +lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A"
   1.100 +by (unfold refl_on_def) blast
   1.101  
   1.102 -lemma refl_Int: "refl A r ==> refl B s ==> refl (A \<inter> B) (r \<inter> s)"
   1.103 -by (unfold refl_def) blast
   1.104 +lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
   1.105 +by (unfold refl_on_def) blast
   1.106  
   1.107 -lemma refl_Un: "refl A r ==> refl B s ==> refl (A \<union> B) (r \<union> s)"
   1.108 -by (unfold refl_def) blast
   1.109 +lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)"
   1.110 +by (unfold refl_on_def) blast
   1.111  
   1.112 -lemma refl_INTER:
   1.113 -  "ALL x:S. refl (A x) (r x) ==> refl (INTER S A) (INTER S r)"
   1.114 -by (unfold refl_def) fast
   1.115 +lemma refl_on_INTER:
   1.116 +  "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)"
   1.117 +by (unfold refl_on_def) fast
   1.118  
   1.119 -lemma refl_UNION:
   1.120 -  "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
   1.121 -by (unfold refl_def) blast
   1.122 +lemma refl_on_UNION:
   1.123 +  "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
   1.124 +by (unfold refl_on_def) blast
   1.125  
   1.126 -lemma refl_empty[simp]: "refl {} {}"
   1.127 -by(simp add:refl_def)
   1.128 +lemma refl_on_empty[simp]: "refl_on {} {}"
   1.129 +by(simp add:refl_on_def)
   1.130  
   1.131 -lemma refl_diag: "refl A (diag A)"
   1.132 -by (rule reflI [OF diag_subset_Times diagI])
   1.133 +lemma refl_on_Id_on: "refl_on A (Id_on A)"
   1.134 +by (rule refl_onI [OF Id_on_subset_Times Id_onI])
   1.135  
   1.136  
   1.137  subsection {* Antisymmetry *}
   1.138 @@ -232,7 +232,7 @@
   1.139  lemma antisym_empty [simp]: "antisym {}"
   1.140  by (unfold antisym_def) blast
   1.141  
   1.142 -lemma antisym_diag [simp]: "antisym (diag A)"
   1.143 +lemma antisym_Id_on [simp]: "antisym (Id_on A)"
   1.144  by (unfold antisym_def) blast
   1.145  
   1.146  
   1.147 @@ -256,7 +256,7 @@
   1.148  lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)"
   1.149  by (fast intro: symI dest: symD)
   1.150  
   1.151 -lemma sym_diag [simp]: "sym (diag A)"
   1.152 +lemma sym_Id_on [simp]: "sym (Id_on A)"
   1.153  by (rule symI) clarify
   1.154  
   1.155  
   1.156 @@ -275,7 +275,7 @@
   1.157  lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)"
   1.158  by (fast intro: transI elim: transD)
   1.159  
   1.160 -lemma trans_diag [simp]: "trans (diag A)"
   1.161 +lemma trans_Id_on [simp]: "trans (Id_on A)"
   1.162  by (fast intro: transI elim: transD)
   1.163  
   1.164  lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
   1.165 @@ -331,11 +331,11 @@
   1.166  lemma converse_Id [simp]: "Id^-1 = Id"
   1.167  by blast
   1.168  
   1.169 -lemma converse_diag [simp]: "(diag A)^-1 = diag A"
   1.170 +lemma converse_Id_on [simp]: "(Id_on A)^-1 = Id_on A"
   1.171  by blast
   1.172  
   1.173 -lemma refl_converse [simp]: "refl A (converse r) = refl A r"
   1.174 -by (unfold refl_def) auto
   1.175 +lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
   1.176 +by (unfold refl_on_def) auto
   1.177  
   1.178  lemma sym_converse [simp]: "sym (converse r) = sym r"
   1.179  by (unfold sym_def) blast
   1.180 @@ -382,7 +382,7 @@
   1.181  lemma Domain_Id [simp]: "Domain Id = UNIV"
   1.182  by blast
   1.183  
   1.184 -lemma Domain_diag [simp]: "Domain (diag A) = A"
   1.185 +lemma Domain_Id_on [simp]: "Domain (Id_on A) = A"
   1.186  by blast
   1.187  
   1.188  lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
   1.189 @@ -433,7 +433,7 @@
   1.190  lemma Range_Id [simp]: "Range Id = UNIV"
   1.191  by blast
   1.192  
   1.193 -lemma Range_diag [simp]: "Range (diag A) = A"
   1.194 +lemma Range_Id_on [simp]: "Range (Id_on A) = A"
   1.195  by auto
   1.196  
   1.197  lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
   1.198 @@ -506,7 +506,7 @@
   1.199  lemma Image_Id [simp]: "Id `` A = A"
   1.200  by blast
   1.201  
   1.202 -lemma Image_diag [simp]: "diag A `` B = A \<inter> B"
   1.203 +lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B"
   1.204  by blast
   1.205  
   1.206  lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
   1.207 @@ -571,7 +571,7 @@
   1.208  lemma single_valued_Id [simp]: "single_valued Id"
   1.209  by (unfold single_valued_def) blast
   1.210  
   1.211 -lemma single_valued_diag [simp]: "single_valued (diag A)"
   1.212 +lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
   1.213  by (unfold single_valued_def) blast
   1.214  
   1.215