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