1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Crunch_Test_NonDet 8imports 9 Lib.Crunch_Instances_NonDet 10 Crunch_Test_Qualified_NonDet 11 Lib.GenericLib 12 Lib.Defs 13begin 14 15text \<open>Test cases for crunch\<close> 16 17definition 18 "crunch_foo1 (x :: nat) \<equiv> do 19 modify ((+) x); 20 modify ((+) x) 21 od" 22 23definition 24 "crunch_foo2 \<equiv> do 25 crunch_foo1 12; 26 crunch_foo1 13 27 od" 28 29crunch (empty_fail) empty_fail: crunch_foo2 30 (ignore: modify bind) 31 32crunch_ignore (add: crunch_foo1) 33 34crunch gt: crunch_foo2 "\<lambda>x. x > y" 35 (ignore: modify bind ignore_del: crunch_foo1) 36 37crunch_ignore (del: crunch_foo1) 38 39definition 40 "crunch_always_true (x :: nat) \<equiv> \<lambda>y :: nat. True" 41 42lemma crunch_foo1_at_2: 43 "True \<Longrightarrow> \<lbrace>crunch_always_true 3 and crunch_always_true 2\<rbrace> 44 crunch_foo1 x \<lbrace>\<lambda>rv. crunch_always_true 2 and K True\<rbrace>" 45 by (simp add: crunch_always_true_def, wp) 46 47lemma crunch_foo1_at_3[wp]: 48 "\<lbrace>crunch_always_true 3\<rbrace> crunch_foo1 x \<lbrace>\<lambda>rv. crunch_always_true 3\<rbrace>" 49 by (simp add: crunch_always_true_def, wp) 50 51lemma crunch_foo1_no_fail: 52 "True \<Longrightarrow> no_fail (crunch_always_true 2 and crunch_always_true 3) (crunch_foo1 x)" 53 apply (simp add:crunch_always_true_def crunch_foo1_def) 54 apply (rule no_fail_pre) 55 apply (wp, simp) 56 done 57 58crunch (no_fail) no_fail: crunch_foo2 59 (ignore: modify bind wp: crunch_foo1_at_2[simplified]) 60 61crunch (valid) at_2: crunch_foo2 "crunch_always_true 2" 62 (ignore: modify bind wp: crunch_foo1_at_2[simplified]) 63 64fun crunch_foo3 :: "nat => nat => 'a => (nat,unit) nondet_monad" where 65 "crunch_foo3 0 x _ = crunch_foo1 x" 66| "crunch_foo3 (Suc n) x y = crunch_foo3 n x y" 67 68crunch gt2: crunch_foo3 "\<lambda>x. x > y" 69 (ignore: modify bind) 70 71crunch (empty_fail) empty_fail2: crunch_foo3 72 (ignore: modify bind) 73 74(* check that simp rules can be used to solve a goal without crunching *) 75crunch (empty_fail) empty_fail: crunch_foo3 76 (ignore: modify bind ignore: crunch_foo1 simp: crunch_foo3_empty_fail2) 77 78class foo_class = 79 fixes stuff :: 'a 80begin 81 82fun crunch_foo4 :: "nat => nat => 'a => (nat,unit) nondet_monad" where 83 "crunch_foo4 0 x _ s = crunch_foo1 x s" 84| "crunch_foo4 (Suc n) x y s = crunch_foo4 n x y s" 85 86definition 87 "crunch_foo5 x (y::'a) \<equiv> crunch_foo1 x" 88 89end 90 91lemma crunch_foo4_alt: 92 "crunch_foo4 n x y \<equiv> crunch_foo1 x" 93 apply (induct n) 94 apply (simp add: fun_eq_iff)+ 95 done 96 97(* prove rules about crunch_foo4 with and without the alternative definition *) 98crunch gt3: crunch_foo4 "\<lambda>x. x > y" 99 (ignore: modify bind) 100 101crunch (no_fail) no_fail2: crunch_foo4 102 (rule: crunch_foo4_alt ignore: modify bind) 103 104crunch gt3': crunch_foo4 "\<lambda>x. x > y" 105 (rule: crunch_foo4_alt ignore: modify bind) 106 107crunch gt4: crunch_foo5 "\<lambda>x. x > y" 108 (ignore: modify bind) 109 110(* Test cases for crunch in locales *) 111 112definition 113 "crunch_foo6 \<equiv> return () >>= (\<lambda>_. return ())" 114 115locale test_locale = 116fixes fixed_return_unit :: "(unit, unit) nondet_monad" 117 118begin 119 120definition 121 "crunch_foo7 \<equiv> return () >>= (\<lambda>_. return ())" 122 123(* crunch works on a global constant within a locale *) 124crunch test[wp]: crunch_foo6 P 125(ignore: bind) 126 127(* crunch works on a locale constant *) 128crunch test[wp]: crunch_foo7 P 129(ignore: bind) 130 131definition 132 "crunch_foo8 \<equiv> fixed_return_unit >>= (\<lambda>_. fixed_return_unit)" 133 134definition 135 "crunch_foo9 (x :: nat) \<equiv> do 136 modify ((+) x); 137 modify ((+) x) 138 od" 139 140crunch test: crunch_foo9 "\<lambda>x. x > y" (ignore: bind) 141 142definition 143 "crunch_foo10 (x :: nat) \<equiv> do 144 modify ((+) x); 145 modify ((+) x) 146 od" 147 148(*crunch_def attribute overrides definition lookup *) 149 150lemma crunch_foo10_def2[crunch_def]: 151 "crunch_foo10 = crunch_foo9" 152 unfolding crunch_foo10_def[abs_def] crunch_foo9_def[abs_def] 153 by simp 154 155crunch test[wp]: crunch_foo10 "\<lambda>x. x > y" 156 157(* crunch_ignore works within a locale *) 158crunch_ignore (add: bind) 159 160crunch test': crunch_foo9 "\<lambda>x. x > y" 161 162end 163 164interpretation test_locale "return ()" . 165 166(* interpretation promotes the wp attribute from the locale *) 167lemma "\<lbrace>Q\<rbrace> crunch_foo7 \<lbrace>\<lambda>_. Q\<rbrace>" by wp 168 169(* crunch still works on an interpreted locale constant *) 170crunch test2: crunch_foo7 P 171 (wp_del: crunch_foo7_test) 172 173locale test_sublocale 174 175sublocale test_sublocale < test_locale "return ()" . 176 177context test_sublocale begin 178 179(* crunch works on a locale constant with a fixed locale parameter *) 180crunch test[wp]: crunch_foo8 P 181 182end 183 184(* check that qualified names are handled properly. *) 185 186consts foo_const :: "(unit, unit) nondet_monad" 187defs foo_const_def: "foo_const \<equiv> Crunch_Test_Qualified_NonDet.foo_const" 188 189crunch test: foo_const P 190 191(* check that the grid-style crunch is working *) 192 193crunches crunch_foo3, crunch_foo4, crunch_foo5 194 for silly: "\<lambda>s. True \<noteq> False" and (no_fail)nf and (empty_fail)ef 195 (ignore: modify bind rule: crunch_foo4_alt wp_del: hoare_vcg_prop) 196 197(* check that crunch can use wps to lift sub-predicates 198 (and also that top-level constants can be ignored) *) 199consts f :: "(nat, unit) nondet_monad" 200consts Q :: "bool \<Rightarrow> nat \<Rightarrow> bool" 201consts R :: "nat \<Rightarrow> bool" 202axiomatization 203 where test1: "\<lbrace>Q x\<rbrace> f \<lbrace>\<lambda>_. Q x\<rbrace>" 204 and test2: "\<lbrace>\<lambda>s. P (R s)\<rbrace> f \<lbrace>\<lambda>_ s. P (R s)\<rbrace>" 205 206crunch test3: f "\<lambda>s. Q (R s) s" 207 (wp: test1 wps: test2 ignore: f) 208 209end 210