1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Local_Method_Tests
8imports
9  Lib.Eisbach_Methods
10begin
11
12text \<open>
13  @{command supply_local_method} allows adding named aliases for methods to the local
14  proof context, for when duplicating methods would be too difficult to maintain or debug
15  but refactoring the proof would take too long.
16
17  Usage:
18    supply_local_method my_name = <method text>
19
20    supply_local_method my_name_1 = <method text 1>
21                        my_name_2 = <method text 2>
22                        ...
23
24  Where <method text> uses the same syntax as the input to @{command apply}.
25\<close>
26
27text \<open>
28  @{method local_method} allows using a previously supplied local method to the current proof
29  state.
30
31  Usage:
32    apply (local_method name)
33\<close>
34
35experiment
36begin
37  section \<open>Basic Examples\<close>
38
39  lemma "A \<Longrightarrow> B \<Longrightarrow> A \<or> B"
40    supply_local_method my_simp = simp
41    apply (local_method my_simp)
42    done
43
44  text \<open>Uses standard @{command apply} parser, allowing all the normal combinators\<close>
45  lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
46    supply_local_method my_slightly_complicated_method = (rule conjI, assumption+)
47    apply (local_method my_slightly_complicated_method)
48    done
49
50  text \<open>Can supply multiple methods\<close>
51  lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
52    supply_local_method my_rule = (rule conjI)
53                        my_asm = assumption+
54    apply (local_method my_rule)
55    apply (local_method my_asm)
56    done
57
58  section \<open>Failure Modes\<close>
59
60  text \<open>Fails on non-existent arguments\<close>
61  lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
62    supply_local_method foo = simp
63    apply (fails \<open>local_method bar\<close>)
64    oops
65
66  text \<open>Doesn't persist between subgoals\<close>
67  lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
68    apply (rule conjI)
69     subgoal
70     supply_local_method my_simp = simp
71     apply (local_method my_simp)
72     done
73    apply (fails \<open>local_method my_simp\<close>)
74    oops
75
76  text \<open>Does see top-level method definitions\<close>
77  method foo = simp
78  lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
79    supply_local_method magic = foo
80    apply (local_method magic)
81    done
82
83end
84
85end