1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory WPBang
8imports
9  WP
10  ProvePart
11  NonDetMonadVCG
12begin
13
14lemma conj_meta_forward:
15  "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> P') \<Longrightarrow> (Q \<Longrightarrow> Q') \<Longrightarrow> P' \<and> Q'"
16  by simp
17
18text \<open>Applying safe WP rules.\<close>
19ML \<open>
20structure WP_Safe = struct
21
22fun check_has_frees_tac Ps (_ : int) thm = let
23    val fs = Term.add_frees (Thm.prop_of thm) [] |> filter (member (=) Ps)
24  in if null fs then Seq.empty else Seq.single thm end
25
26fun wp_bang wp_safe_rules ctxt = let
27    val wp_safe_rules_conj = ((wp_safe_rules RL @{thms hoare_vcg_conj_lift hoare_vcg_R_conj})
28        RL @{thms hoare_strengthen_post hoare_post_imp_R})
29      |> map (rotate_prems 1)
30  in
31    resolve_tac ctxt wp_safe_rules_conj
32    THEN' Split_To_Conj.get_split_tac "P" ctxt
33      (fn Ps => fn i => eresolve0_tac [@{thm conj_meta_forward}] i
34        THEN (REPEAT_ALL_NEW ((CHANGED o asm_full_simp_tac ctxt)
35              ORELSE' Classical.safe_steps_tac ctxt)
36          THEN_ALL_NEW Partial_Prove.cleanup_tac ctxt Ps) i
37        THEN (Partial_Prove.finish_tac ctxt Ps THEN' (assume_tac ctxt)) i
38      )
39  end
40
41val wpe_args =
42  Attrib.thms >> curry (fn (rules, ctxt) =>
43    Method.SIMPLE_METHOD (
44      wp_bang rules ctxt 1
45    )
46  );
47
48end
49\<close>
50
51method_setup wpe = \<open>WP_Safe.wpe_args\<close>
52  "applies 'safe' wp rules to eliminate postcondition components"
53
54text \<open>Testing.\<close>
55
56lemma
57  assumes x: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. Q \<rbrace>"
58       and y: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. R \<rbrace>"
59  shows
60  "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. \<forall>x y. (fst rv = Some x \<longrightarrow> Q s)
61    \<and> (snd rv = Some y \<longrightarrow> Q s )
62    \<and> R s \<rbrace>"
63  apply (rule hoare_pre)
64   apply (simp add: all_conj_distrib)
65   apply (rule hoare_vcg_conj_lift)
66    apply (wpe x)
67    apply wp
68   apply (wpe x)
69   apply (wp y)
70  apply simp
71  done
72
73end
74