moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
1.1 --- a/src/HOL/Predicate.thy Thu Feb 23 21:25:59 2012 +0100
1.2 +++ b/src/HOL/Predicate.thy Fri Feb 24 07:30:24 2012 +0100
1.3 @@ -1,11 +1,11 @@
1.4 (* Title: HOL/Predicate.thy
1.5 - Author: Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen
1.6 + Author: Lukas Bulwahn and Florian Haftmann, TU Muenchen
1.7 *)
1.8
1.9 -header {* Predicates as relations and enumerations *}
1.10 +header {* Predicates as enumerations *}
1.11
1.12 theory Predicate
1.13 -imports Inductive Relation
1.14 +imports List
1.15 begin
1.16
1.17 notation
1.18 @@ -22,261 +22,7 @@
1.19 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
1.20 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
1.21
1.22 -
1.23 -subsection {* Classical rules for reasoning on predicates *}
1.24 -
1.25 -declare predicate1D [Pure.dest?, dest?]
1.26 -declare predicate2I [Pure.intro!, intro!]
1.27 -declare predicate2D [Pure.dest, dest]
1.28 -declare bot1E [elim!]
1.29 -declare bot2E [elim!]
1.30 -declare top1I [intro!]
1.31 -declare top2I [intro!]
1.32 -declare inf1I [intro!]
1.33 -declare inf2I [intro!]
1.34 -declare inf1E [elim!]
1.35 -declare inf2E [elim!]
1.36 -declare sup1I1 [intro?]
1.37 -declare sup2I1 [intro?]
1.38 -declare sup1I2 [intro?]
1.39 -declare sup2I2 [intro?]
1.40 -declare sup1E [elim!]
1.41 -declare sup2E [elim!]
1.42 -declare sup1CI [intro!]
1.43 -declare sup2CI [intro!]
1.44 -declare INF1_I [intro!]
1.45 -declare INF2_I [intro!]
1.46 -declare INF1_D [elim]
1.47 -declare INF2_D [elim]
1.48 -declare INF1_E [elim]
1.49 -declare INF2_E [elim]
1.50 -declare SUP1_I [intro]
1.51 -declare SUP2_I [intro]
1.52 -declare SUP1_E [elim!]
1.53 -declare SUP2_E [elim!]
1.54 -
1.55 -
1.56 -subsection {* Conversion between set and predicate relations *}
1.57 -
1.58 -subsubsection {* Equality *}
1.59 -
1.60 -lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
1.61 - by (simp add: set_eq_iff fun_eq_iff)
1.62 -
1.63 -lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
1.64 - by (simp add: set_eq_iff fun_eq_iff)
1.65 -
1.66 -
1.67 -subsubsection {* Order relation *}
1.68 -
1.69 -lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
1.70 - by (simp add: subset_iff le_fun_def)
1.71 -
1.72 -lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
1.73 - by (simp add: subset_iff le_fun_def)
1.74 -
1.75 -
1.76 -subsubsection {* Top and bottom elements *}
1.77 -
1.78 -lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
1.79 - by (auto simp add: fun_eq_iff)
1.80 -
1.81 -lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
1.82 - by (auto simp add: fun_eq_iff)
1.83 -
1.84 -
1.85 -subsubsection {* Binary intersection *}
1.86 -
1.87 -lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
1.88 - by (simp add: inf_fun_def)
1.89 -
1.90 -lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
1.91 - by (simp add: inf_fun_def)
1.92 -
1.93 -
1.94 -subsubsection {* Binary union *}
1.95 -
1.96 -lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
1.97 - by (simp add: sup_fun_def)
1.98 -
1.99 -lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
1.100 - by (simp add: sup_fun_def)
1.101 -
1.102 -
1.103 -subsubsection {* Intersections of families *}
1.104 -
1.105 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
1.106 - by (simp add: INF_apply fun_eq_iff)
1.107 -
1.108 -lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
1.109 - by (simp add: INF_apply fun_eq_iff)
1.110 -
1.111 -
1.112 -subsubsection {* Unions of families *}
1.113 -
1.114 -lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
1.115 - by (simp add: SUP_apply fun_eq_iff)
1.116 -
1.117 -lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
1.118 - by (simp add: SUP_apply fun_eq_iff)
1.119 -
1.120 -
1.121 -subsection {* Predicates as relations *}
1.122 -
1.123 -subsubsection {* Composition *}
1.124 -
1.125 -inductive pred_comp :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
1.126 - for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
1.127 - pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
1.128 -
1.129 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
1.130 -
1.131 -lemma pred_comp_rel_comp_eq [pred_set_conv]:
1.132 - "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
1.133 - by (auto simp add: fun_eq_iff)
1.134 -
1.135 -
1.136 -subsubsection {* Converse *}
1.137 -
1.138 -inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
1.139 - for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.140 - conversepI: "r a b \<Longrightarrow> r^--1 b a"
1.141 -
1.142 -notation (xsymbols)
1.143 - conversep ("(_\<inverse>\<inverse>)" [1000] 1000)
1.144 -
1.145 -lemma conversepD:
1.146 - assumes ab: "r^--1 a b"
1.147 - shows "r b a" using ab
1.148 - by cases simp
1.149 -
1.150 -lemma conversep_iff [iff]: "r^--1 a b = r b a"
1.151 - by (iprover intro: conversepI dest: conversepD)
1.152 -
1.153 -lemma conversep_converse_eq [pred_set_conv]:
1.154 - "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
1.155 - by (auto simp add: fun_eq_iff)
1.156 -
1.157 -lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
1.158 - by (iprover intro: order_antisym conversepI dest: conversepD)
1.159 -
1.160 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
1.161 - by (iprover intro: order_antisym conversepI pred_compI
1.162 - elim: pred_compE dest: conversepD)
1.163 -
1.164 -lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
1.165 - by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
1.166 -
1.167 -lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
1.168 - by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
1.169 -
1.170 -lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
1.171 - by (auto simp add: fun_eq_iff)
1.172 -
1.173 -lemma conversep_eq [simp]: "(op =)^--1 = op ="
1.174 - by (auto simp add: fun_eq_iff)
1.175 -
1.176 -
1.177 -subsubsection {* Domain *}
1.178 -
1.179 -inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
1.180 - for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.181 - DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
1.182 -
1.183 -inductive_cases DomainPE [elim!]: "DomainP r a"
1.184 -
1.185 -lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
1.186 - by (blast intro!: Orderings.order_antisym predicate1I)
1.187 -
1.188 -
1.189 -subsubsection {* Range *}
1.190 -
1.191 -inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
1.192 - for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.193 - RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
1.194 -
1.195 -inductive_cases RangePE [elim!]: "RangeP r b"
1.196 -
1.197 -lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
1.198 - by (blast intro!: Orderings.order_antisym predicate1I)
1.199 -
1.200 -
1.201 -subsubsection {* Inverse image *}
1.202 -
1.203 -definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
1.204 - "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
1.205 -
1.206 -lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
1.207 - by (simp add: inv_image_def inv_imagep_def)
1.208 -
1.209 -lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
1.210 - by (simp add: inv_imagep_def)
1.211 -
1.212 -
1.213 -subsubsection {* Powerset *}
1.214 -
1.215 -definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
1.216 - "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
1.217 -
1.218 -lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
1.219 - by (auto simp add: Powp_def fun_eq_iff)
1.220 -
1.221 -lemmas Powp_mono [mono] = Pow_mono [to_pred]
1.222 -
1.223 -
1.224 -subsubsection {* Properties of relations *}
1.225 -
1.226 -abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.227 - "antisymP r \<equiv> antisym {(x, y). r x y}"
1.228 -
1.229 -abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.230 - "transP r \<equiv> trans {(x, y). r x y}"
1.231 -
1.232 -abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
1.233 - "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
1.234 -
1.235 -(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
1.236 -
1.237 -definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.238 - "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
1.239 -
1.240 -definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.241 - "symp r \<longleftrightarrow> sym {(x, y). r x y}"
1.242 -
1.243 -definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.244 - "transp r \<longleftrightarrow> trans {(x, y). r x y}"
1.245 -
1.246 -lemma reflpI:
1.247 - "(\<And>x. r x x) \<Longrightarrow> reflp r"
1.248 - by (auto intro: refl_onI simp add: reflp_def)
1.249 -
1.250 -lemma reflpE:
1.251 - assumes "reflp r"
1.252 - obtains "r x x"
1.253 - using assms by (auto dest: refl_onD simp add: reflp_def)
1.254 -
1.255 -lemma sympI:
1.256 - "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
1.257 - by (auto intro: symI simp add: symp_def)
1.258 -
1.259 -lemma sympE:
1.260 - assumes "symp r" and "r x y"
1.261 - obtains "r y x"
1.262 - using assms by (auto dest: symD simp add: symp_def)
1.263 -
1.264 -lemma transpI:
1.265 - "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
1.266 - by (auto intro: transI simp add: transp_def)
1.267 -
1.268 -lemma transpE:
1.269 - assumes "transp r" and "r x y" and "r y z"
1.270 - obtains "r x z"
1.271 - using assms by (auto dest: transD simp add: transp_def)
1.272 -
1.273 -
1.274 -subsection {* Predicates as enumerations *}
1.275 -
1.276 -subsubsection {* The type of predicate enumerations (a monad) *}
1.277 +subsection {* The type of predicate enumerations (a monad) *}
1.278
1.279 datatype 'a pred = Pred "'a \<Rightarrow> bool"
1.280
1.281 @@ -465,7 +211,7 @@
1.282 using assms by (cases A) (auto simp add: bot_pred_def)
1.283
1.284
1.285 -subsubsection {* Emptiness check and definite choice *}
1.286 +subsection {* Emptiness check and definite choice *}
1.287
1.288 definition is_empty :: "'a pred \<Rightarrow> bool" where
1.289 "is_empty A \<longleftrightarrow> A = \<bottom>"
1.290 @@ -578,7 +324,7 @@
1.291 using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
1.292
1.293
1.294 -subsubsection {* Derived operations *}
1.295 +subsection {* Derived operations *}
1.296
1.297 definition if_pred :: "bool \<Rightarrow> unit pred" where
1.298 if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
1.299 @@ -668,7 +414,7 @@
1.300 by (rule ext, rule pred_eqI, auto)+
1.301
1.302
1.303 -subsubsection {* Implementation *}
1.304 +subsection {* Implementation *}
1.305
1.306 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
1.307
1.308 @@ -762,6 +508,12 @@
1.309 by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
1.310 qed
1.311
1.312 +lemma [code]:
1.313 + "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
1.314 +
1.315 +lemma [code]:
1.316 + "pred_size f P = 0" by (cases P) simp
1.317 +
1.318 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
1.319 "contained Empty Q \<longleftrightarrow> True"
1.320 | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
1.321 @@ -937,6 +689,44 @@
1.322 "set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq"
1.323 by auto
1.324
1.325 +text {* Lazy Evaluation of an indexed function *}
1.326 +
1.327 +function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
1.328 +where
1.329 + "iterate_upto f n m =
1.330 + Predicate.Seq (%u. if n > m then Predicate.Empty
1.331 + else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
1.332 +by pat_completeness auto
1.333 +
1.334 +termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
1.335 +
1.336 +text {* Misc *}
1.337 +
1.338 +declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
1.339 +
1.340 +(* FIXME: better implement conversion by bisection *)
1.341 +
1.342 +lemma pred_of_set_fold_sup:
1.343 + assumes "finite A"
1.344 + shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
1.345 +proof (rule sym)
1.346 + interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
1.347 + by (fact comp_fun_idem_sup)
1.348 + from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
1.349 +qed
1.350 +
1.351 +lemma pred_of_set_set_fold_sup:
1.352 + "pred_of_set (set xs) = fold sup (List.map Predicate.single xs) bot"
1.353 +proof -
1.354 + interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
1.355 + by (fact comp_fun_idem_sup)
1.356 + show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
1.357 +qed
1.358 +
1.359 +lemma pred_of_set_set_foldr_sup [code]:
1.360 + "pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot"
1.361 + by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
1.362 +
1.363 no_notation
1.364 bot ("\<bottom>") and
1.365 top ("\<top>") and
1.366 @@ -955,5 +745,7 @@
1.367 hide_type (open) pred seq
1.368 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
1.369 Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
1.370 + iterate_upto
1.371
1.372 end
1.373 +