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