1(* Title: HOL/Quickcheck_Random.thy 2 Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen 3*) 4 5section \<open>A simple counterexample generator performing random testing\<close> 6 7theory Quickcheck_Random 8imports Random Code_Evaluation Enum 9begin 10 11notation fcomp (infixl "\<circ>>" 60) 12notation scomp (infixl "\<circ>\<rightarrow>" 60) 13 14setup \<open>Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)])\<close> 15 16subsection \<open>Catching Match exceptions\<close> 17 18axiomatization catch_match :: "'a => 'a => 'a" 19 20code_printing 21 constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)" 22 23code_reserved Quickcheck Match 24 25subsection \<open>The \<open>random\<close> class\<close> 26 27class random = typerep + 28 fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 29 30 31subsection \<open>Fundamental and numeric types\<close> 32 33instantiation bool :: random 34begin 35 36definition 37 "random i = Random.range 2 \<circ>\<rightarrow> 38 (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" 39 40instance .. 41 42end 43 44instantiation itself :: (typerep) random 45begin 46 47definition 48 random_itself :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 49where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" 50 51instance .. 52 53end 54 55instantiation char :: random 56begin 57 58definition 59 "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))" 60 61instance .. 62 63end 64 65instantiation String.literal :: random 66begin 67 68definition 69 "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))" 70 71instance .. 72 73end 74 75instantiation nat :: random 76begin 77 78definition random_nat :: "natural \<Rightarrow> Random.seed 79 \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" 80where 81 "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( 82 let n = nat_of_natural k 83 in (n, \<lambda>_. Code_Evaluation.term_of n)))" 84 85instance .. 86 87end 88 89instantiation int :: random 90begin 91 92definition 93 "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( 94 let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k)))) 95 in (j, \<lambda>_. Code_Evaluation.term_of j)))" 96 97instance .. 98 99end 100 101instantiation natural :: random 102begin 103 104definition random_natural :: "natural \<Rightarrow> Random.seed 105 \<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" 106where 107 "random_natural i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>n. Pair (n, \<lambda>_. Code_Evaluation.term_of n))" 108 109instance .. 110 111end 112 113instantiation integer :: random 114begin 115 116definition random_integer :: "natural \<Rightarrow> Random.seed 117 \<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" 118where 119 "random_integer i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( 120 let j = (if k \<ge> i then integer_of_natural (k - i) else - (integer_of_natural (i - k))) 121 in (j, \<lambda>_. Code_Evaluation.term_of j)))" 122 123instance .. 124 125end 126 127 128subsection \<open>Complex generators\<close> 129 130text \<open>Towards @{typ "'a \<Rightarrow> 'b"}\<close> 131 132axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 133 \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 134 \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) 135 \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 136 137definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 138 \<Rightarrow> Random.seed \<Rightarrow> (('a::term_of \<Rightarrow> 'b::typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 139where 140 "random_fun_lift f = 141 random_fun_aux TYPEREP('a) TYPEREP('b) (=) Code_Evaluation.term_of f Random.split_seed" 142 143instantiation "fun" :: ("{equal, term_of}", random) random 144begin 145 146definition 147 random_fun :: "natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 148 where "random i = random_fun_lift (random i)" 149 150instance .. 151 152end 153 154text \<open>Towards type copies and datatypes\<close> 155 156definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" 157 where "collapse f = (f \<circ>\<rightarrow> id)" 158 159definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural" 160 where "beyond k l = (if l > k then l else 0)" 161 162lemma beyond_zero: "beyond k 0 = 0" 163 by (simp add: beyond_def) 164 165 166definition (in term_syntax) [code_unfold]: 167 "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)" 168 169definition (in term_syntax) [code_unfold]: 170 "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" 171 172instantiation set :: (random) random 173begin 174 175fun random_aux_set 176where 177 "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])" 178| "random_aux_set (Code_Numeral.Suc i) j = 179 collapse (Random.select_weight 180 [(1, Pair valterm_emptyset), 181 (Code_Numeral.Suc i, 182 random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" 183 184lemma [code]: 185 "random_aux_set i j = 186 collapse (Random.select_weight [(1, Pair valterm_emptyset), 187 (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" 188proof (induct i rule: natural.induct) 189 case zero 190 show ?case by (subst select_weight_drop_zero [symmetric]) 191 (simp add: random_aux_set.simps [simplified] less_natural_def) 192next 193 case (Suc i) 194 show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_natural_minus_one) 195qed 196 197definition "random_set i = random_aux_set i i" 198 199instance .. 200 201end 202 203lemma random_aux_rec: 204 fixes random_aux :: "natural \<Rightarrow> 'a" 205 assumes "random_aux 0 = rhs 0" 206 and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)" 207 shows "random_aux k = rhs k" 208 using assms by (rule natural.induct) 209 210subsection \<open>Deriving random generators for datatypes\<close> 211 212ML_file "Tools/Quickcheck/quickcheck_common.ML" 213ML_file "Tools/Quickcheck/random_generators.ML" 214 215 216subsection \<open>Code setup\<close> 217 218code_printing 219 constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun" 220 \<comment> \<open>With enough criminal energy this can be abused to derive @{prop False}; 221 for this reason we use a distinguished target \<open>Quickcheck\<close> 222 not spoiling the regular trusted code generation\<close> 223 224code_reserved Quickcheck Random_Generators 225 226no_notation fcomp (infixl "\<circ>>" 60) 227no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 228 229hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift 230 231hide_fact (open) collapse_def beyond_def random_fun_lift_def 232 233end 234