Quelle Random_Pred.thy Sprache: Isabelle

(* Author: Lukas Bulwahn, TU Muenchen *)

section \<open>The Random-Predicate Monad\<close>

theory Random_Pred
imports Quickcheck_Random
begin

fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
where
  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
     let ((x, _), seed') = Quickcheck_Random.random sz seed
   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"

definition iter :: "natural \ natural \ Random.seed \ ('a::random) Predicate.pred"
where
  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"

lemma [code]:
  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
     let ((x, _), seed') = Quickcheck_Random.random sz seed
   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
   unfolding iter_def iter'.simps [of _ nrandom] ..

type_synonym 'a random_pred = "Random.seed \ ('a Predicate.pred \ Random.seed)"

definition empty :: "'a random_pred"
  where "empty = Pair bot"

definition single :: "'a => 'a random_pred"
  where "single x = Pair (Predicate.single x)"

definition bind :: "'a random_pred \ ('a \ 'b random_pred) \ 'b random_pred"
  where
    "bind R f = (\s. let
       (P, s') = R s;
       (s1, s2) = Random.split_seed s'
     in (Predicate.bind P (%a. fst (f a s1)), s2))"

definition union :: "'a random_pred \ 'a random_pred \ 'a random_pred"
where
  "union R1 R2 = (\s. let
     (P1, s') = R1 s; (P2, s'') = R2 s'
   in (sup_class.sup P1 P2, s''))"

definition if_randompred :: "bool \ unit random_pred"
where
  "if_randompred b = (if b then single () else empty)"

definition iterate_upto :: "(natural \ 'a) => natural \ natural \ 'a random_pred"
where
  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"

definition not_randompred :: "unit random_pred \ unit random_pred"
where
  "not_randompred P = (\s. let
     (P', s') = P s
   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"

definition Random :: "(Random.seed \ ('a \ (unit \ term)) \ Random.seed) \ 'a random_pred"
  where "Random g = scomp g (Pair \ (Predicate.single \ fst))"

definition map :: "('a \ 'b) \ 'a random_pred \ 'b random_pred"
  where "map f P = bind P (single \ f)"

hide_const (open) iter' iter empty single bind union if_randompred
  iterate_upto not_randompred Random map

hide_fact iter'.simps

hide_fact (open) iter_def empty_def single_def bind_def union_def
  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def

end

quality100%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.