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