author haftmann Fri Mar 02 21:45:45 2012 +0100 (2012-03-02) changeset 46767 807a5d219c23 parent 46766 4269ae06afc5 child 46768 46acd255810d
more fundamental pred-to-set conversions for range and domain by means of inductive_set
 src/HOL/Relation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Relation.thy	Fri Mar 02 22:57:57 2012 +0100
1.2 +++ b/src/HOL/Relation.thy	Fri Mar 02 21:45:45 2012 +0100
1.3 @@ -15,7 +15,7 @@
1.4  (* CANDIDATE declare predicate1D [Pure.dest, dest] *)
1.5  declare predicate2I [Pure.intro!, intro!]
1.6  declare predicate2D [Pure.dest, dest]
1.7 -declare bot1E [elim!]
1.8 +declare bot1E [elim!]
1.9  declare bot2E [elim!]
1.10  declare top1I [intro!]
1.11  declare top2I [intro!]
1.12 @@ -729,98 +729,156 @@
1.13
1.14  subsubsection {* Domain, range and field *}
1.15
1.16 -definition Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set"
1.17 +inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set"
1.18 +  for r :: "('a \<times> 'b) set"
1.19  where
1.20 -  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
1.21 +  DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r"
1.22 +
1.23 +abbreviation (input) "DomainP \<equiv> Domainp"
1.24 +
1.25 +lemmas DomainPI = Domainp.DomainI
1.26 +
1.27 +inductive_cases DomainE [elim!]: "a \<in> Domain r"
1.28 +inductive_cases DomainpE [elim!]: "Domainp r a"
1.29
1.30 -definition Range  :: "('a \<times> 'b) set \<Rightarrow> 'b set"
1.31 +inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set"
1.32 +  for r :: "('a \<times> 'b) set"
1.33  where
1.34 -  "Range r = Domain (r\<inverse>)"
1.35 +  RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r"
1.36 +
1.37 +abbreviation (input) "RangeP \<equiv> Rangep"
1.38 +
1.39 +lemmas RangePI = Rangep.RangeI
1.40 +
1.41 +inductive_cases RangeE [elim!]: "b \<in> Range r"
1.42 +inductive_cases RangepE [elim!]: "Rangep r b"
1.43
1.44  definition Field :: "'a rel \<Rightarrow> 'a set"
1.45  where
1.46    "Field r = Domain r \<union> Range r"
1.47
1.48 -declare Domain_def [no_atp]
1.49 -
1.50 -lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
1.51 -  by (unfold Domain_def) blast
1.52 -
1.53 -lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
1.54 -  by (iprover intro!: iffD2 [OF Domain_iff])
1.55 -
1.56 -lemma DomainE [elim!]:
1.57 -  "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
1.58 -  by (iprover dest!: iffD1 [OF Domain_iff])
1.59 -
1.60 -lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)"
1.61 -  by (simp add: Domain_def Range_def)
1.62 -
1.63 -lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
1.64 -  by (unfold Range_def) (iprover intro!: converseI DomainI)
1.65 -
1.66 -lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
1.67 -  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
1.68 -
1.69 -inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
1.70 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
1.71 -where
1.72 -  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
1.73 -
1.74 -inductive_cases DomainPE [elim!]: "DomainP r a"
1.75 -
1.76 -lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
1.77 -  by (blast intro!: Orderings.order_antisym predicate1I)
1.78 -
1.79 -inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
1.80 -  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
1.81 -where
1.82 -  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
1.83 -
1.84 -inductive_cases RangePE [elim!]: "RangeP r b"
1.85 -
1.86 -lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
1.87 -  by (auto intro!: Orderings.order_antisym predicate1I)
1.88 -
1.89  lemma Domain_fst [code]:
1.90    "Domain r = fst ` r"
1.91 -  by (auto simp add: image_def Bex_def)
1.92 +  by force
1.93 +
1.94 +lemma Range_snd [code]:
1.95 +  "Range r = snd ` r"
1.96 +  by force
1.97 +
1.98 +lemma fst_eq_Domain: "fst ` R = Domain R"
1.99 +  by force
1.100 +
1.101 +lemma snd_eq_Range: "snd ` R = Range R"
1.102 +  by force
1.103
1.104  lemma Domain_empty [simp]: "Domain {} = {}"
1.105 -  by blast
1.106 +  by auto
1.107 +
1.108 +lemma Range_empty [simp]: "Range {} = {}"
1.109 +  by auto
1.110 +
1.111 +lemma Field_empty [simp]: "Field {} = {}"
1.112 +  by (simp add: Field_def)
1.113
1.114  lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}"
1.115    by auto
1.116
1.117 -lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)"
1.118 +lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
1.119 +  by auto
1.120 +
1.121 +lemma Domain_insert (* CANDIDATE [simp] *): "Domain (insert (a, b) r) = insert a (Domain r)"
1.122 +  by blast
1.123 +
1.124 +lemma Range_insert (* CANDIDATE [simp] *): "Range (insert (a, b) r) = insert b (Range r)"
1.125 +  by blast
1.126 +
1.127 +lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
1.128 +  by (auto simp add: Field_def Domain_insert Range_insert)
1.129 +
1.130 +lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)"
1.131 +  by blast
1.132 +
1.133 +lemma Range_iff: "a \<in> Range r \<longleftrightarrow> (\<exists>y. (y, a) \<in> r)"
1.134    by blast
1.135
1.136  lemma Domain_Id [simp]: "Domain Id = UNIV"
1.137    by blast
1.138
1.139 +lemma Range_Id [simp]: "Range Id = UNIV"
1.140 +  by blast
1.141 +
1.142  lemma Domain_Id_on [simp]: "Domain (Id_on A) = A"
1.143    by blast
1.144
1.145 -lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
1.146 +lemma Range_Id_on [simp]: "Range (Id_on A) = A"
1.147 +  by blast
1.148 +
1.149 +lemma Domain_Un_eq: "Domain (A \<union> B) = Domain A \<union> Domain B"
1.150    by blast
1.151
1.152 -lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)"
1.153 +lemma Range_Un_eq: "Range (A \<union> B) = Range A \<union> Range B"
1.154 +  by blast
1.155 +
1.156 +lemma Field_Un [simp]: "Field (r \<union> s) = Field r \<union> Field s"
1.157 +  by (auto simp: Field_def)
1.158 +
1.159 +lemma Domain_Int_subset: "Domain (A \<inter> B) \<subseteq> Domain A \<inter> Domain B"
1.160    by blast
1.161
1.162 -lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)"
1.163 +lemma Range_Int_subset: "Range (A \<inter> B) \<subseteq> Range A \<inter> Range B"
1.164 +  by blast
1.165 +
1.166 +lemma Domain_Diff_subset: "Domain A - Domain B \<subseteq> Domain (A - B)"
1.167 +  by blast
1.168 +
1.169 +lemma Range_Diff_subset: "Range A - Range B \<subseteq> Range (A - B)"
1.170    by blast
1.171
1.172 -lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)"
1.173 +lemma Domain_Union: "Domain (\<Union>S) = (\<Union>A\<in>S. Domain A)"
1.174    by blast
1.175
1.176 +lemma Range_Union: "Range (\<Union>S) = (\<Union>A\<in>S. Range A)"
1.177 +  by blast
1.178 +
1.179 +lemma Field_Union [simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
1.180 +  by (auto simp: Field_def)
1.181 +
1.182  lemma Domain_converse [simp]: "Domain (r\<inverse>) = Range r"
1.183    by auto
1.184
1.185 -lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
1.186 +lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r"
1.187    by blast
1.188
1.189 -lemma fst_eq_Domain: "fst ` R = Domain R"
1.190 -  by force
1.191 +lemma Field_converse [simp]: "Field (r\<inverse>) = Field r"
1.192 +  by (auto simp: Field_def)
1.193 +
1.194 +lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
1.195 +  by auto
1.196 +
1.197 +lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
1.198 +  by auto
1.199 +
1.200 +lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
1.201 +  by (induct set: finite) (auto simp add: Domain_insert)
1.202 +
1.203 +lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
1.204 +  by (induct set: finite) (auto simp add: Range_insert)
1.205 +
1.206 +lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
1.207 +  by (simp add: Field_def finite_Domain finite_Range)
1.208 +
1.209 +lemma Domain_mono: "r \<subseteq> s \<Longrightarrow> Domain r \<subseteq> Domain s"
1.210 +  by blast
1.211 +
1.212 +lemma Range_mono: "r \<subseteq> s \<Longrightarrow> Range r \<subseteq> Range s"
1.213 +  by blast
1.214 +
1.215 +lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
1.216 +  by (auto simp: Field_def Domain_def Range_def)
1.217 +
1.218 +lemma Domain_unfold:
1.219 +  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
1.220 +  by blast
1.221
1.222  lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
1.223    by auto
1.224 @@ -828,83 +886,6 @@
1.225  lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
1.226    by auto
1.227
1.228 -lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
1.229 -  by auto
1.230 -
1.231 -lemma finite_Domain: "finite r ==> finite (Domain r)"
1.232 -  by (induct set: finite) (auto simp add: Domain_insert)
1.233 -
1.234 -lemma Range_snd [code]:
1.235 -  "Range r = snd ` r"
1.236 -  by (auto simp add: image_def Bex_def)
1.237 -
1.238 -lemma Range_empty [simp]: "Range {} = {}"
1.239 -  by blast
1.240 -
1.241 -lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
1.242 -  by auto
1.243 -
1.244 -lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)"
1.245 -  by blast
1.246 -
1.247 -lemma Range_Id [simp]: "Range Id = UNIV"
1.248 -  by blast
1.249 -
1.250 -lemma Range_Id_on [simp]: "Range (Id_on A) = A"
1.251 -  by auto
1.252 -
1.253 -lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
1.254 -  by blast
1.255 -
1.256 -lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)"
1.257 -  by blast
1.258 -
1.259 -lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)"
1.260 -  by blast
1.261 -
1.262 -lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
1.263 -  by blast
1.264 -
1.265 -lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r"
1.266 -  by blast
1.267 -
1.268 -lemma snd_eq_Range: "snd ` R = Range R"
1.269 -  by force
1.270 -
1.271 -lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
1.272 -  by auto
1.273 -
1.274 -lemma finite_Range: "finite r ==> finite (Range r)"
1.275 -  by (induct set: finite) (auto simp add: Range_insert)
1.276 -
1.277 -lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
1.278 -  by (auto simp: Field_def Domain_def Range_def)
1.279 -
1.280 -lemma Field_empty[simp]: "Field {} = {}"
1.281 -  by (auto simp: Field_def)
1.282 -
1.283 -lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
1.284 -  by (auto simp: Field_def)
1.285 -
1.286 -lemma Field_Un [simp]: "Field (r \<union> s) = Field r \<union> Field s"
1.287 -  by (auto simp: Field_def)
1.288 -
1.289 -lemma Field_Union [simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
1.290 -  by (auto simp: Field_def)
1.291 -
1.292 -lemma Field_converse [simp]: "Field(r^-1) = Field r"
1.293 -  by (auto simp: Field_def)
1.294 -
1.295 -lemma finite_Field: "finite r ==> finite (Field r)"
1.296 -  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
1.297 -  apply (induct set: finite)
1.298 -   apply (auto simp add: Field_def Domain_insert Range_insert)
1.299 -  done
1.300 -
1.301 -lemma Domain_unfold:
1.302 -  "Domain r = {x. \<exists>y. (x, y) \<in> r}"
1.303 -  by (fact Domain_def)
1.304 -
1.305
1.306  subsubsection {* Image of a set under a relation *}
1.307
1.308 @@ -947,8 +928,8 @@
1.309    by blast
1.310
1.311  lemma Image_Int_eq:
1.312 -     "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
1.313 -     by (simp add: single_valued_def, blast)
1.314 +  "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
1.315 +  by (simp add: single_valued_def, blast)
1.316
1.317  lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
1.318    by blast
```