src/HOL/Predicate.thy
changeset 30328 ab47f43f7581
parent 26797 a6cb51c314f2
child 30376 e8cc806a3755
     1.1 --- a/src/HOL/Predicate.thy	Fri Mar 06 20:30:17 2009 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Fri Mar 06 20:30:17 2009 +0100
     1.3 @@ -1,15 +1,40 @@
     1.4  (*  Title:      HOL/Predicate.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Stefan Berghofer, TU Muenchen
     1.7 +    Author:     Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen
     1.8  *)
     1.9  
    1.10 -header {* Predicates *}
    1.11 +header {* Predicates as relations and enumerations *}
    1.12  
    1.13  theory Predicate
    1.14  imports Inductive Relation
    1.15  begin
    1.16  
    1.17 -subsection {* Equality and Subsets *}
    1.18 +notation
    1.19 +  inf (infixl "\<sqinter>" 70) and
    1.20 +  sup (infixl "\<squnion>" 65) and
    1.21 +  Inf ("\<Sqinter>_" [900] 900) and
    1.22 +  Sup ("\<Squnion>_" [900] 900) and
    1.23 +  top ("\<top>") and
    1.24 +  bot ("\<bottom>")
    1.25 +
    1.26 +
    1.27 +subsection {* Predicates as (complete) lattices *}
    1.28 +
    1.29 +subsubsection {* @{const sup} on @{typ bool} *}
    1.30 +
    1.31 +lemma sup_boolI1:
    1.32 +  "P \<Longrightarrow> P \<squnion> Q"
    1.33 +  by (simp add: sup_bool_eq)
    1.34 +
    1.35 +lemma sup_boolI2:
    1.36 +  "Q \<Longrightarrow> P \<squnion> Q"
    1.37 +  by (simp add: sup_bool_eq)
    1.38 +
    1.39 +lemma sup_boolE:
    1.40 +  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.41 +  by (auto simp add: sup_bool_eq)
    1.42 +
    1.43 +
    1.44 +subsubsection {* Equality and Subsets *}
    1.45  
    1.46  lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
    1.47    by (simp add: mem_def)
    1.48 @@ -24,7 +49,7 @@
    1.49    by fast
    1.50  
    1.51  
    1.52 -subsection {* Top and bottom elements *}
    1.53 +subsubsection {* Top and bottom elements *}
    1.54  
    1.55  lemma top1I [intro!]: "top x"
    1.56    by (simp add: top_fun_eq top_bool_eq)
    1.57 @@ -39,7 +64,7 @@
    1.58    by (simp add: bot_fun_eq bot_bool_eq)
    1.59  
    1.60  
    1.61 -subsection {* The empty set *}
    1.62 +subsubsection {* The empty set *}
    1.63  
    1.64  lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
    1.65    by (auto simp add: expand_fun_eq)
    1.66 @@ -48,7 +73,7 @@
    1.67    by (auto simp add: expand_fun_eq)
    1.68  
    1.69  
    1.70 -subsection {* Binary union *}
    1.71 +subsubsection {* Binary union *}
    1.72  
    1.73  lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
    1.74    by (simp add: sup_fun_eq sup_bool_eq)
    1.75 @@ -92,7 +117,7 @@
    1.76    by simp iprover
    1.77  
    1.78  
    1.79 -subsection {* Binary intersection *}
    1.80 +subsubsection {* Binary intersection *}
    1.81  
    1.82  lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
    1.83    by (simp add: inf_fun_eq inf_bool_eq)
    1.84 @@ -131,7 +156,7 @@
    1.85    by simp
    1.86  
    1.87  
    1.88 -subsection {* Unions of families *}
    1.89 +subsubsection {* Unions of families *}
    1.90  
    1.91  lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
    1.92    by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
    1.93 @@ -158,7 +183,7 @@
    1.94    by (simp add: expand_fun_eq)
    1.95  
    1.96  
    1.97 -subsection {* Intersections of families *}
    1.98 +subsubsection {* Intersections of families *}
    1.99  
   1.100  lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
   1.101    by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
   1.102 @@ -191,7 +216,9 @@
   1.103    by (simp add: expand_fun_eq)
   1.104  
   1.105  
   1.106 -subsection {* Composition of two relations *}
   1.107 +subsection {* Predicates as relations *}
   1.108 +
   1.109 +subsubsection {* Composition  *}
   1.110  
   1.111  inductive
   1.112    pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
   1.113 @@ -207,7 +234,7 @@
   1.114    by (auto simp add: expand_fun_eq elim: pred_compE)
   1.115  
   1.116  
   1.117 -subsection {* Converse *}
   1.118 +subsubsection {* Converse *}
   1.119  
   1.120  inductive
   1.121    conversep :: "('a => 'b => bool) => 'b => 'a => bool"
   1.122 @@ -253,7 +280,7 @@
   1.123    by (auto simp add: expand_fun_eq)
   1.124  
   1.125  
   1.126 -subsection {* Domain *}
   1.127 +subsubsection {* Domain *}
   1.128  
   1.129  inductive
   1.130    DomainP :: "('a => 'b => bool) => 'a => bool"
   1.131 @@ -267,7 +294,7 @@
   1.132    by (blast intro!: Orderings.order_antisym predicate1I)
   1.133  
   1.134  
   1.135 -subsection {* Range *}
   1.136 +subsubsection {* Range *}
   1.137  
   1.138  inductive
   1.139    RangeP :: "('a => 'b => bool) => 'b => bool"
   1.140 @@ -281,7 +308,7 @@
   1.141    by (blast intro!: Orderings.order_antisym predicate1I)
   1.142  
   1.143  
   1.144 -subsection {* Inverse image *}
   1.145 +subsubsection {* Inverse image *}
   1.146  
   1.147  definition
   1.148    inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
   1.149 @@ -294,7 +321,7 @@
   1.150    by (simp add: inv_imagep_def)
   1.151  
   1.152  
   1.153 -subsection {* The Powerset operator *}
   1.154 +subsubsection {* Powerset *}
   1.155  
   1.156  definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.157    "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
   1.158 @@ -305,7 +332,7 @@
   1.159  lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
   1.160  
   1.161  
   1.162 -subsection {* Properties of relations - predicate versions *}
   1.163 +subsubsection {* Properties of relations *}
   1.164  
   1.165  abbreviation antisymP :: "('a => 'a => bool) => bool" where
   1.166    "antisymP r == antisym {(x, y). r x y}"
   1.167 @@ -316,4 +343,264 @@
   1.168  abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   1.169    "single_valuedP r == single_valued {(x, y). r x y}"
   1.170  
   1.171 +
   1.172 +subsection {* Predicates as enumerations *}
   1.173 +
   1.174 +subsubsection {* The type of predicate enumerations (a monad) *}
   1.175 +
   1.176 +datatype 'a pred = Pred "'a \<Rightarrow> bool"
   1.177 +
   1.178 +primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
   1.179 +  eval_pred: "eval (Pred f) = f"
   1.180 +
   1.181 +lemma Pred_eval [simp]:
   1.182 +  "Pred (eval x) = x"
   1.183 +  by (cases x) simp
   1.184 +
   1.185 +lemma eval_inject: "eval x = eval y \<longleftrightarrow> x = y"
   1.186 +  by (cases x) auto
   1.187 +
   1.188 +definition single :: "'a \<Rightarrow> 'a pred" where
   1.189 +  "single x = Pred ((op =) x)"
   1.190 +
   1.191 +definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   1.192 +  "P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
   1.193 +
   1.194 +instantiation pred :: (type) complete_lattice
   1.195 +begin
   1.196 +
   1.197 +definition
   1.198 +  "P \<le> Q \<longleftrightarrow> eval P \<le> eval Q"
   1.199 +
   1.200 +definition
   1.201 +  "P < Q \<longleftrightarrow> eval P < eval Q"
   1.202 +
   1.203 +definition
   1.204 +  "\<bottom> = Pred \<bottom>"
   1.205 +
   1.206 +definition
   1.207 +  "\<top> = Pred \<top>"
   1.208 +
   1.209 +definition
   1.210 +  "P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)"
   1.211 +
   1.212 +definition
   1.213 +  "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
   1.214 +
   1.215 +definition
   1.216 +  "\<Sqinter>A = Pred (INFI A eval)"
   1.217 +
   1.218 +definition
   1.219 +  "\<Squnion>A = Pred (SUPR A eval)"
   1.220 +
   1.221 +instance by default
   1.222 +  (auto simp add: less_eq_pred_def less_pred_def
   1.223 +    inf_pred_def sup_pred_def bot_pred_def top_pred_def
   1.224 +    Inf_pred_def Sup_pred_def,
   1.225 +    auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
   1.226 +    eval_inject mem_def)
   1.227 +
   1.228  end
   1.229 +
   1.230 +lemma bind_bind:
   1.231 +  "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
   1.232 +  by (auto simp add: bind_def expand_fun_eq)
   1.233 +
   1.234 +lemma bind_single:
   1.235 +  "P \<guillemotright>= single = P"
   1.236 +  by (simp add: bind_def single_def)
   1.237 +
   1.238 +lemma single_bind:
   1.239 +  "single x \<guillemotright>= P = P x"
   1.240 +  by (simp add: bind_def single_def)
   1.241 +
   1.242 +lemma bottom_bind:
   1.243 +  "\<bottom> \<guillemotright>= P = \<bottom>"
   1.244 +  by (auto simp add: bot_pred_def bind_def expand_fun_eq)
   1.245 +
   1.246 +lemma sup_bind:
   1.247 +  "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
   1.248 +  by (auto simp add: bind_def sup_pred_def expand_fun_eq)
   1.249 +
   1.250 +lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   1.251 +  by (auto simp add: bind_def Sup_pred_def expand_fun_eq)
   1.252 +
   1.253 +lemma pred_iffI:
   1.254 +  assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
   1.255 +  and "\<And>x. eval B x \<Longrightarrow> eval A x"
   1.256 +  shows "A = B"
   1.257 +proof -
   1.258 +  from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast
   1.259 +  then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq)
   1.260 +qed
   1.261 +  
   1.262 +lemma singleI: "eval (single x) x"
   1.263 +  unfolding single_def by simp
   1.264 +
   1.265 +lemma singleI_unit: "eval (single ()) x"
   1.266 +  by simp (rule singleI)
   1.267 +
   1.268 +lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P"
   1.269 +  unfolding single_def by simp
   1.270 +
   1.271 +lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   1.272 +  by (erule singleE) simp
   1.273 +
   1.274 +lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
   1.275 +  unfolding bind_def by auto
   1.276 +
   1.277 +lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   1.278 +  unfolding bind_def by auto
   1.279 +
   1.280 +lemma botE: "eval \<bottom> x \<Longrightarrow> P"
   1.281 +  unfolding bot_pred_def by auto
   1.282 +
   1.283 +lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
   1.284 +  unfolding sup_pred_def by simp
   1.285 +
   1.286 +lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
   1.287 +  unfolding sup_pred_def by simp
   1.288 +
   1.289 +lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   1.290 +  unfolding sup_pred_def by auto
   1.291 +
   1.292 +
   1.293 +subsubsection {* Derived operations *}
   1.294 +
   1.295 +definition if_pred :: "bool \<Rightarrow> unit pred" where
   1.296 +  if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
   1.297 +
   1.298 +definition eq_pred :: "'a \<Rightarrow> 'a \<Rightarrow> unit pred" where
   1.299 +  eq_pred_eq: "eq_pred a b = if_pred (a = b)"
   1.300 +
   1.301 +definition not_pred :: "unit pred \<Rightarrow> unit pred" where
   1.302 +  not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
   1.303 +
   1.304 +lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()"
   1.305 +  unfolding if_pred_eq by (auto intro: singleI)
   1.306 +
   1.307 +lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
   1.308 +  unfolding if_pred_eq by (cases b) (auto elim: botE)
   1.309 +
   1.310 +lemma eq_predI: "eval (eq_pred a a) ()"
   1.311 +  unfolding eq_pred_eq if_pred_eq by (auto intro: singleI)
   1.312 +
   1.313 +lemma eq_predE: "eval (eq_pred a b) x \<Longrightarrow> (a = b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
   1.314 +  unfolding eq_pred_eq by (erule if_predE)
   1.315 +
   1.316 +lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()"
   1.317 +  unfolding not_pred_eq eval_pred by (auto intro: singleI)
   1.318 +
   1.319 +lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()"
   1.320 +  unfolding not_pred_eq by (auto intro: singleI)
   1.321 +
   1.322 +lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   1.323 +  unfolding not_pred_eq
   1.324 +  by (auto split: split_if_asm elim: botE)
   1.325 +
   1.326 +lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   1.327 +  unfolding not_pred_eq
   1.328 +  by (auto split: split_if_asm elim: botE)
   1.329 +
   1.330 +
   1.331 +subsubsection {* Implementation *}
   1.332 +
   1.333 +datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
   1.334 +
   1.335 +primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
   1.336 +    "pred_of_seq Empty = \<bottom>"
   1.337 +  | "pred_of_seq (Insert x P) = single x \<squnion> P"
   1.338 +  | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
   1.339 +
   1.340 +definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
   1.341 +  "Seq f = pred_of_seq (f ())"
   1.342 +
   1.343 +code_datatype Seq
   1.344 +
   1.345 +primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool"  where
   1.346 +  "member Empty x \<longleftrightarrow> False"
   1.347 +  | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
   1.348 +  | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
   1.349 +
   1.350 +lemma eval_member:
   1.351 +  "member xq = eval (pred_of_seq xq)"
   1.352 +proof (induct xq)
   1.353 +  case Empty show ?case
   1.354 +  by (auto simp add: expand_fun_eq elim: botE)
   1.355 +next
   1.356 +  case Insert show ?case
   1.357 +  by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI)
   1.358 +next
   1.359 +  case Join then show ?case
   1.360 +  by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2)
   1.361 +qed
   1.362 +
   1.363 +lemma eval_code [code]: "eval (Seq f) = member (f ())"
   1.364 +  unfolding Seq_def by (rule sym, rule eval_member)
   1.365 +
   1.366 +lemma single_code [code]:
   1.367 +  "single x = Seq (\<lambda>u. Insert x \<bottom>)"
   1.368 +  unfolding Seq_def by simp
   1.369 +
   1.370 +primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   1.371 +    "apply f Empty = Empty"
   1.372 +  | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
   1.373 +  | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
   1.374 +
   1.375 +lemma apply_bind:
   1.376 +  "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
   1.377 +proof (induct xq)
   1.378 +  case Empty show ?case
   1.379 +    by (simp add: bottom_bind)
   1.380 +next
   1.381 +  case Insert show ?case
   1.382 +    by (simp add: single_bind sup_bind)
   1.383 +next
   1.384 +  case Join then show ?case
   1.385 +    by (simp add: sup_bind)
   1.386 +qed
   1.387 +  
   1.388 +lemma bind_code [code]:
   1.389 +  "Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))"
   1.390 +  unfolding Seq_def by (rule sym, rule apply_bind)
   1.391 +
   1.392 +lemma bot_set_code [code]:
   1.393 +  "\<bottom> = Seq (\<lambda>u. Empty)"
   1.394 +  unfolding Seq_def by simp
   1.395 +
   1.396 +lemma sup_code [code]:
   1.397 +  "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f ()
   1.398 +    of Empty \<Rightarrow> g ()
   1.399 +     | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
   1.400 +     | Join P xq \<Rightarrow> Join (Seq g) (Join P xq))" (*FIXME order!?*)
   1.401 +proof (cases "f ()")
   1.402 +  case Empty
   1.403 +  thus ?thesis
   1.404 +    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot)
   1.405 +next
   1.406 +  case Insert
   1.407 +  thus ?thesis
   1.408 +    unfolding Seq_def by (simp add: sup_assoc)
   1.409 +next
   1.410 +  case Join
   1.411 +  thus ?thesis
   1.412 +    unfolding Seq_def by (simp add: sup_commute [of "pred_of_seq (g ())"] sup_assoc)
   1.413 +qed
   1.414 +
   1.415 +
   1.416 +declare eq_pred_def [code, code del]
   1.417 +
   1.418 +no_notation
   1.419 +  inf (infixl "\<sqinter>" 70) and
   1.420 +  sup (infixl "\<squnion>" 65) and
   1.421 +  Inf ("\<Sqinter>_" [900] 900) and
   1.422 +  Sup ("\<Squnion>_" [900] 900) and
   1.423 +  top ("\<top>") and
   1.424 +  bot ("\<bottom>") and
   1.425 +  bind (infixl "\<guillemotright>=" 70)
   1.426 +
   1.427 +hide (open) type pred seq
   1.428 +hide (open) const Pred eval single bind if_pred eq_pred not_pred
   1.429 +  Empty Insert Join Seq member "apply"
   1.430 +
   1.431 +end