1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory WP_Pre 8imports 9 Main 10 Trace_Schematic_Insts 11 "HOL-Eisbach.Eisbach_Tools" 12begin 13 14named_theorems wp_pre 15 16ML \<open> 17structure WP_Pre = struct 18 19val wp_trace = Attrib.setup_config_bool @{binding wp_trace} (K false); 20val wp_trace_instantiation = 21 Attrib.setup_config_bool @{binding wp_trace_instantiation} (K false); 22 23fun append_used_rule ctxt used_thms_ref tag used_thm insts = 24 let 25 val name = Thm.get_name_hint used_thm 26 val inst_term = 27 if Config.get ctxt wp_trace_instantiation 28 then Trace_Schematic_Insts.instantiate_thm ctxt used_thm insts 29 else Thm.prop_of used_thm 30 in used_thms_ref := !used_thms_ref @ [(name, tag, inst_term)] end 31 32fun trace_rule' trace ctxt callback tac rule = 33 if trace 34 then Trace_Schematic_Insts.trace_schematic_insts_tac ctxt callback tac rule 35 else tac rule; 36 37fun trace_rule trace ctxt used_thms_ref tag tac rule = 38 trace_rule' trace ctxt 39 (fn rule_insts => fn _ => append_used_rule ctxt used_thms_ref tag rule rule_insts) 40 tac rule; 41 42fun rtac ctxt rule = resolve_tac ctxt [rule] 43 44fun pre_tac trace ctxt pre_rules used_thms_ref i t = let 45 fun apply_rule t = trace_rule trace ctxt used_thms_ref "wp_pre" (rtac ctxt) t i 46 val t2 = FIRST (map apply_rule pre_rules) t |> Seq.hd 47 val etac = TRY o eresolve_tac ctxt [@{thm FalseE}] 48 fun dummy_t2 _ _ = Seq.single t2 49 val t3 = (dummy_t2 THEN_ALL_NEW etac) i t |> Seq.hd 50 in if Thm.nprems_of t3 <> Thm.nprems_of t2 51 then Seq.empty else Seq.single t2 end 52 handle Option => Seq.empty 53 54fun tac trace used_thms_ref ctxt = let 55 val pres = Named_Theorems.get ctxt @{named_theorems wp_pre} 56 in pre_tac trace ctxt pres used_thms_ref end 57 58val method = 59 let 60 val used_thms_ref = Unsynchronized.ref [] : (string * string * term) list Unsynchronized.ref 61 in 62 Args.context >> (fn _ => fn ctxt => 63 Method.SIMPLE_METHOD' (tac (Config.get ctxt wp_trace) used_thms_ref ctxt)) 64 end 65end 66\<close> 67 68method_setup wp_pre0 = \<open>WP_Pre.method\<close> 69method wp_pre = wp_pre0? 70 71definition 72 test_wp_pre :: "bool \<Rightarrow> bool \<Rightarrow> bool" 73where 74 "test_wp_pre P Q = (P \<longrightarrow> Q)" 75 76lemma test_wp_pre_pre[wp_pre]: 77 "test_wp_pre P' Q \<Longrightarrow> (P \<Longrightarrow> P') 78 \<Longrightarrow> test_wp_pre P Q" 79 by (simp add: test_wp_pre_def) 80 81lemma demo: 82 "test_wp_pre P P" 83 (* note that wp_pre0 applies, but only once *) 84 apply wp_pre0+ 85 apply (simp add: test_wp_pre_def, rule imp_refl) 86 apply simp 87 done 88 89end 90