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