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