1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Trace_Schematic_Insts_Test
8imports
9  Lib.Trace_Schematic_Insts
10begin
11
12text \<open>
13  Trace the schematic variables and types that a method instantiates.
14  This only works for the variables already in the proof goal; new
15  variables introduced by the traced method are not tracked.
16\<close>
17
18experiment begin
19section \<open>Examples\<close>
20
21text \<open>Schematic variables\<close>
22lemma "\<lbrakk> \<forall>x. P x \<rbrakk> \<Longrightarrow> P x"
23  apply (drule spec) \<comment> \<open>introduces schematic var "?x"\<close>
24  apply (trace_schematic_insts \<open>assumption\<close>)
25  done
26
27definition foo :: "'a \<Rightarrow> bool"
28  where "foo x = True"
29
30lemma fooI1:
31  "foo 0 \<Longrightarrow> foo x"
32  by (simp add: foo_def)
33
34lemma fooI2:
35  "foo x \<Longrightarrow> foo 0"
36  by (simp add: foo_def)
37
38lemma fooI2':
39  "foo x \<Longrightarrow> foo (0 :: nat)"
40  by (erule fooI2)
41
42text \<open>Schematic type variables\<close>
43lemma "foo x \<Longrightarrow> foo y"
44  apply (rule fooI1) \<comment> \<open>introduces schematic type "0 :: ?'a"\<close>
45  apply (trace_schematic_insts \<open>erule fooI2'\<close>)
46  done
47
48text \<open>When backtracking, every recursive invocation is traced\<close>
49lemma "\<lbrakk> \<forall>x. Q x \<longrightarrow> R x; \<forall>x. P x \<longrightarrow> Q x; P x; P y \<longrightarrow> R x \<rbrakk> \<Longrightarrow> R x"
50  apply (drule spec)
51  apply (drule spec)
52  text \<open>For more clarity, methods can be named\<close>
53  apply (trace_schematic_insts impE1 \<open>erule impE\<close>,
54         trace_schematic_insts impE2 \<open>erule impE\<close>,
55         (trace_schematic_insts "try assumption" \<open>assumption\<close>)+; fail)
56  done
57
58text \<open>Interactive example\<close>
59ML \<open>
60  fun trace_resolve_tac ctxt =
61      Trace_Schematic_Insts.trace_schematic_insts_tac ctxt
62        (Trace_Schematic_Insts.default_rule_report ctxt "demo title")
63        (fn t => resolve_tac ctxt [t])
64\<close>
65lemma
66  assumes Pf: "\<And>f (x :: nat). Q f \<Longrightarrow> P x \<Longrightarrow> P (f x)"
67  assumes Q: "Q ((*) 2)"
68  assumes P: "P a"
69  shows "\<exists>x. P (x + a + a)"
70  apply (tactic \<open>trace_resolve_tac @{context} @{thm exI} 1\<close>)
71  apply (trace_schematic_insts \<open>subst add_0\<close>)
72
73  \<comment>\<open>
74    This picks *some* instantiation of `f` in @{thm Pf}. The first one is
75    @{term "\<lambda>a. a"}, which isn't what we want.
76  \<close>
77  apply (tactic \<open>trace_resolve_tac @{context} @{thm Pf} 1\<close>)
78   \<comment>\<open>
79     This picks the *next* instantiation of `f`, in this case @{term "\<lambda>a. a + a"}
80     Notice that the reporting callback gets called with the new instantiations!
81   \<close>
82   back
83
84   apply (tactic \<open>
85     Trace_Schematic_Insts.trace_schematic_insts_tac
86       @{context}
87       (Trace_Schematic_Insts.default_rule_report @{context} "demo title")
88       (fn t => EqSubst.eqsubst_tac @{context} [0] [t])
89       @{thm mult_2[symmetric]} 1
90   \<close>)
91   apply (tactic \<open>trace_resolve_tac @{context} @{thm Q} 1\<close>)
92  apply (tactic \<open>trace_resolve_tac @{context} @{thm P} 1\<close>)
93  done
94
95section \<open>Tests\<close>
96
97ML \<open>
98fun trace_schematic_assert ctxt test_name tac expected_vars expected_tvars =
99  let
100    fun skip_dummy_state tac = fn st =>
101        case Thm.prop_of st of
102            Const (@{const_name Pure.prop}, _) $
103              (Const (@{const_name Pure.term}, _) $ Const (@{const_name Pure.dummy_pattern}, _)) =>
104              Seq.succeed st
105          | _ => tac st
106
107    fun check insts =
108      if expected_vars = #terms insts andalso expected_tvars = #typs insts then () else
109        error ("Trace_Schematic_Insts failed test: " ^ test_name)
110
111  in NO_CONTEXT_TACTIC ctxt
112        (Trace_Schematic_Insts.trace_schematic_insts (SIMPLE_METHOD tac) check [])
113     |> skip_dummy_state
114  end
115\<close>
116
117text \<open>Schematic variables\<close>
118lemma "\<lbrakk> \<forall>x. P x \<rbrakk> \<Longrightarrow> P x"
119  apply (drule spec)
120  apply (tactic \<open>let
121      val alpha = TFree ("'a", @{sort type})
122      val expected_vars = [(Var (("x", 0), alpha), Free ("x", alpha))]
123      val expected_tvars = []
124      in trace_schematic_assert @{context}
125            "basic Var test" (assume_tac @{context} 1)
126            expected_vars expected_tvars
127      end\<close>)
128  done
129
130text \<open>Schematic type variables\<close>
131lemma "foo x \<Longrightarrow> foo y"
132  apply (rule fooI1)
133  apply (tactic \<open>let
134      val expected_vars = []
135      val expected_tvars = [(TVar (("'a", 0), @{sort zero}), @{typ nat})]
136      in trace_schematic_assert
137            @{context}
138            "basic TVar test"
139            (eresolve_tac @{context} @{thms fooI2'} 1)
140            expected_vars expected_tvars
141      end\<close>)
142  done
143
144
145ML \<open>
146fun trace_schematic_resolve_tac_assert ctxt test_name thm expected_rule_insts expected_proof_insts =
147  let
148    fun check rule_insts proof_insts =
149        if expected_rule_insts = rule_insts andalso expected_proof_insts = proof_insts
150        then ()
151        else
152          let
153            val _ = tracing (@{make_string} (rule_insts, proof_insts))
154          in error ("Trace_Schematic_Insts failed test: " ^ test_name) end
155    fun tactic thm = resolve_tac ctxt [thm]
156  in HEADGOAL (Trace_Schematic_Insts.trace_schematic_insts_tac ctxt check tactic thm)
157  end
158\<close>
159
160text \<open>Simultaneous rule and goal instantiations\<close>
161lemma "\<exists>a. foo (a :: nat)"
162  apply (rule exI)
163  apply (tactic \<open>
164    let
165      val a' = TVar (("'a", 0), @{sort type})
166      val b' = TVar (("'b", 0), @{sort zero})
167      val a'' = TVar (("'a", 2), @{sort type})
168      val expected_rule_vars = [
169        (Var (("x", 0), a'), Var(("x", 2), a''))
170      ]
171      val expected_rule_tvars = [
172        (a', a''),
173        (b', @{typ nat})
174      ]
175      val expected_goal_vars = [
176        (Var (("a", 0), @{typ nat}), @{term "0 :: nat"})
177      ]
178    in
179      trace_schematic_resolve_tac_assert
180        @{context}
181        "basic rule tracing"
182        @{thm fooI2}
183        {bounds = [], terms = expected_rule_vars, typs = expected_rule_tvars}
184        {bounds = [], terms = expected_goal_vars, typs = []}
185    end
186  \<close>)
187  by (simp add: foo_def)
188
189text \<open>Rule instantiations with bound variables\<close>
190lemma "\<And>X. X \<and> Y \<Longrightarrow> Y \<and> X"
191  apply (tactic \<open>
192    let
193      val expected_rule_bounds = [("X", @{typ bool})]
194      val expected_rule_vars = [
195        (Var (("P", 0), @{typ bool}), @{term "\<lambda>X :: bool. Y :: bool"}),
196        (Var (("Q", 0), @{typ bool}), @{term "\<lambda>X :: bool. X :: bool"})
197      ]
198    in
199      trace_schematic_resolve_tac_assert
200        @{context}
201        "rule tracing with bound variables"
202        @{thm conjI}
203        {bounds = expected_rule_bounds, terms = expected_rule_vars, typs = []}
204        {bounds = [], terms = [], typs = []}
205    end
206  \<close>)
207  by simp+
208
209text \<open>Rule instantiations with function terms\<close>
210lemma "\<exists>f. \<forall>x. f x = x"
211  apply (intro exI allI)
212  apply (rule fun_cong)
213  apply (tactic \<open>
214    let
215      val a' = TVar (("'a", 0), @{sort type})
216      \<comment>\<open>
217        New lambda abstraction gets an anonymous variable name. Usually rendered as
218        @{term "\<lambda>x a. a"}.
219      \<close>
220      val lambda = Abs ("x", @{typ 'a}, Abs ("", @{typ 'a}, Bound 0))
221
222      val expected_rule_bounds = [("x", @{typ 'a})]
223      val expected_rule_vars = [
224        (Var (("t", 0), a'), lambda)
225      ]
226      val expected_rule_typs = [
227        (a', @{typ "'a \<Rightarrow> 'a"})
228      ]
229      val expected_goal_vars = [
230        (Var (("f", 2), @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}), lambda)
231      ]
232    in
233      trace_schematic_resolve_tac_assert
234        @{context}
235        "rule tracing with function term instantiations"
236        @{thm refl}
237        {bounds = expected_rule_bounds, terms = expected_rule_vars, typs = expected_rule_typs}
238        {bounds = [], terms = expected_goal_vars, typs = []}
239    end
240  \<close>)
241  done
242
243end
244
245end