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