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