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