1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6theory Match_Abbreviation_Test
7
8imports
9  Lib.Match_Abbreviation
10  Lib.NonDetMonad
11begin
12
13experiment
14  fixes a :: "(int, unit) nondet_monad"
15    and b :: "int \<Rightarrow> (int, int) nondet_monad"
16    and c :: "(int, unit) nondet_monad"
17begin
18
19definition
20  "test_foo z = do
21    a; a;
22    x \<leftarrow> b 2;
23    x \<leftarrow> b z;
24    a; a; a; a;
25    x \<leftarrow> c;
26    x \<leftarrow> a; a;
27    return ()
28  od"
29
30match_abbreviation (input) foo_block
31  in concl test_foo_def
32  select "bind (b x) y" (for x y)
33  and rewrite "bind c y" to "c" (for y)
34
35definition
36  "test_foo_bind = do
37    a; a;
38    x \<leftarrow> b 2;
39    y \<leftarrow> b x;
40    a; a; a; a;
41    z \<leftarrow> b (x + y);
42    fin \<leftarrow> b (z + x);
43    x \<leftarrow> a; a;
44    c;
45    a; a;
46    return fin
47  od"
48
49match_abbreviation (input) foo_block_capture
50  in concl test_foo_bind_def[simplified K_bind_def]
51  select "bind (b (x + y)) tail" (for x y tail)
52  and rewrite "bind c y" to "c" (for y)
53  and retype_consts bind
54
55definition
56  "foo_blockc x y = foo_block_capture x y"
57
58reassoc_thm foo_block_capture_reassoc
59  "bind (foo_block_capture x y) f" (for x y f)
60  bind_assoc
61lemmas foo_blockc_fold = foo_block_capture_reassoc[folded foo_blockc_def]
62
63end
64
65end
66