src/HOL/Random_Pred.thy
author wenzelm
Fri, 05 Apr 2019 17:05:32 +0200
changeset 70067 9b34dbeb1103
parent 67091 1393c2340eec
permissions -rw-r--r--
auxiliary operation for common uses of 'compile_generated_files';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     1
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     2
(* Author: Lukas Bulwahn, TU Muenchen *)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     3
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     4
section \<open>The Random-Predicate Monad\<close>
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     5
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     6
theory Random_Pred
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     7
imports Quickcheck_Random
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     8
begin
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
     9
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    10
fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    11
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    12
  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    13
     let ((x, _), seed') = Quickcheck_Random.random sz seed
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    14
   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    15
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    16
definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    17
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    18
  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    19
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    20
lemma [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    21
  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    22
     let ((x, _), seed') = Quickcheck_Random.random sz seed
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    23
   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    24
   unfolding iter_def iter'.simps [of _ nrandom] ..
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    25
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    26
type_synonym 'a random_pred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    27
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    28
definition empty :: "'a random_pred"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    29
  where "empty = Pair bot"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    30
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    31
definition single :: "'a => 'a random_pred"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    32
  where "single x = Pair (Predicate.single x)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    33
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    34
definition bind :: "'a random_pred \<Rightarrow> ('a \<Rightarrow> 'b random_pred) \<Rightarrow> 'b random_pred"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    35
  where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    36
    "bind R f = (\<lambda>s. let
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    37
       (P, s') = R s;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    38
       (s1, s2) = Random.split_seed s'
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    39
     in (Predicate.bind P (%a. fst (f a s1)), s2))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    40
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    41
definition union :: "'a random_pred \<Rightarrow> 'a random_pred \<Rightarrow> 'a random_pred"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    42
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    43
  "union R1 R2 = (\<lambda>s. let
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    44
     (P1, s') = R1 s; (P2, s'') = R2 s'
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    45
   in (sup_class.sup P1 P2, s''))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    46
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    47
definition if_randompred :: "bool \<Rightarrow> unit random_pred"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    48
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    49
  "if_randompred b = (if b then single () else empty)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    50
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    51
definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    52
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    53
  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    54
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    55
definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    56
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    57
  "not_randompred P = (\<lambda>s. let
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    58
     (P', s') = P s
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    59
   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    60
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    61
definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred"
67091
1393c2340eec more symbols;
wenzelm
parents: 60758
diff changeset
    62
  where "Random g = scomp g (Pair \<circ> (Predicate.single \<circ> fst))"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    63
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    64
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred"
67091
1393c2340eec more symbols;
wenzelm
parents: 60758
diff changeset
    65
  where "map f P = bind P (single \<circ> f)"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    66
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    67
hide_const (open) iter' iter empty single bind union if_randompred
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    68
  iterate_upto not_randompred Random map
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    69
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    70
hide_fact iter'.simps
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    71
  
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    72
hide_fact (open) iter_def empty_def single_def bind_def union_def
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    73
  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    74
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    75
end
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents:
diff changeset
    76