equal
deleted
inserted
replaced
381 "is_empty P \<longleftrightarrow> \<not> holds P" |
381 "is_empty P \<longleftrightarrow> \<not> holds P" |
382 unfolding is_empty_def holds_eq |
382 unfolding is_empty_def holds_eq |
383 by (rule unit_pred_cases) (auto elim: botE intro: singleI) |
383 by (rule unit_pred_cases) (auto elim: botE intro: singleI) |
384 |
384 |
385 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where |
385 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where |
386 "map f P = P \<bind> (single o f)" |
386 "map f P = P \<bind> (single \<circ> f)" |
387 |
387 |
388 lemma eval_map [simp]: |
388 lemma eval_map [simp]: |
389 "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))" |
389 "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))" |
390 by (auto simp add: map_def comp_def) |
390 by (auto simp add: map_def comp_def) |
391 |
391 |