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