more fundamental pred-to-set conversions for range and domain by means of inductive_set
authorhaftmann
Fri Mar 02 21:45:45 2012 +0100 (2012-03-02)
changeset 46767807a5d219c23
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
     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