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