1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(*Alternate apply command which displays "used" theorems in refinement step*) 8 9theory Apply_Trace_Cmd 10imports Apply_Trace 11keywords "apply_trace" :: prf_script 12begin 13 14ML\<open> 15 16val _ = 17 Outer_Syntax.command @{command_keyword "apply_trace"} "initial refinement step (unstructured)" 18 19 (Args.mode "only_names" -- (Scan.option (Parse.position Parse.cartouche)) -- Method.parse >> 20 (fn ((on,query),text) => Toplevel.proofs (Apply_Trace.apply_results {silent_fail = false} 21 (Pretty.writeln ooo (Apply_Trace.pretty_deps on query)) text))); 22 23\<close> 24 25lemmas [no_trace] = protectI protectD TrueI Eq_TrueI eq_reflection 26 27(* Test. *) 28lemma "(a \<and> b) = (b \<and> a)" 29 apply_trace auto 30 oops 31 32(* Test. *) 33lemma "(a \<and> b) = (b \<and> a)" 34 apply_trace \<open>intro\<close> auto 35 oops 36 37(* Local assumptions might mask real facts (or each other). Probably not an issue in practice.*) 38lemma 39 assumes X: "b = a" 40 assumes Y: "b = a" 41 shows 42 "b = a" 43 apply_trace (rule Y) 44 oops 45 46(* If any locale facts are accessible their local variant is assumed to the one that is used. *) 47 48locale Apply_Trace_foo = fixes b a 49 assumes X: "b = a" 50begin 51 52 lemma shows "b = a" "b = a" 53 apply - 54 apply_trace (rule Apply_Trace_foo.X) 55 prefer 2 56 apply_trace (rule X) 57 oops 58end 59 60experiment begin 61 62text \<open>Example of trace for grouped lemmas\<close> 63definition ex :: "nat set" where 64 "ex = {1,2,3,4}" 65 66lemma v1: "1 \<in> ex" by (simp add: ex_def) 67lemma v2: "2 \<in> ex" by (simp add: ex_def) 68lemma v3: "3 \<in> ex" by (simp add: ex_def) 69 70text \<open>Group several lemmas in a single one\<close> 71lemmas vs = v1 v2 v3 72 73lemma "2 \<in> ex" 74 apply_trace (simp add: vs) 75 oops 76 77end 78end 79