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.37 +lemma refl_Id: "refl Id"
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.48 +lemma Id_on_empty [simp]: "Id_on {} = {}"
1.50
1.51 -lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
1.53 +lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
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.128 +lemma refl_on_empty[simp]: "refl_on {} {}"
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
```