equal
deleted
inserted
replaced
57 "not_randompred P = (\<lambda>s. let |
57 "not_randompred P = (\<lambda>s. let |
58 (P', s') = P s |
58 (P', s') = P s |
59 in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" |
59 in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" |
60 |
60 |
61 definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred" |
61 definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred" |
62 where "Random g = scomp g (Pair o (Predicate.single o fst))" |
62 where "Random g = scomp g (Pair \<circ> (Predicate.single \<circ> fst))" |
63 |
63 |
64 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred" |
64 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred" |
65 where "map f P = bind P (single o f)" |
65 where "map f P = bind P (single \<circ> f)" |
66 |
66 |
67 hide_const (open) iter' iter empty single bind union if_randompred |
67 hide_const (open) iter' iter empty single bind union if_randompred |
68 iterate_upto not_randompred Random map |
68 iterate_upto not_randompred Random map |
69 |
69 |
70 hide_fact iter'.simps |
70 hide_fact iter'.simps |