1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* WP-specific Eisbach methods *) 8 9theory Eisbach_WP 10imports 11 Eisbach_Methods 12 NonDetMonadVCG 13 Conjuncts 14 Rule_By_Method 15 WPI 16begin 17 18 19text \<open> 20 Methods for manipulating the post conditions of hoare triples as if they 21 were proper subgoals. 22 23 post_asm can be used with the @ attribute to modify existing proofs. Useful 24 for proving large postconditions in one proof and then subsequently decomposing it. 25 26\<close> 27context begin 28 29definition "packed_valid P f si r s \<equiv> P si \<and> (r, s) \<in> fst (f si)" 30 31lemma packed_validE:"(\<And>si r s. packed_valid P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 32 by (clarsimp simp: valid_def packed_valid_def) 33 34lemma packed_validI: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>si r s. packed_valid P f si r s \<longrightarrow> Q r s" 35 apply (clarsimp simp: valid_def packed_valid_def) 36 by auto 37 38definition "packed_validR P f si r s \<equiv> P si \<and> (Inr r, s) \<in> fst (f si)" 39 40 41lemma packed_validRE:"(\<And>si r s. packed_validR P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 42 apply (clarsimp simp: validE_R_def validE_def valid_def packed_validR_def) 43 by (metis sum.case sumE) 44 45lemma packed_validRI: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<forall>si r s. packed_validR P f si r s \<longrightarrow> Q r s" 46 apply (clarsimp simp: valid_def validE_R_def validE_def packed_validR_def) 47 by fastforce 48 49lemma trivial_imp: "\<forall>r s. Q r s \<longrightarrow> Q r s" by simp 50 51lemma uncurry2: "\<forall>r s. Q r s \<and> Q' r s \<longrightarrow> Q'' r s \<Longrightarrow> \<forall>r s. Q r s \<longrightarrow> Q' r s \<longrightarrow> Q'' r s" 52 by simp 53 54named_theorems hoare_post_imps 55 56lemmas [hoare_post_imps] = hoare_post_imp_R hoare_post_imp[rotated] 57 58method post_asm_raw methods m = 59 (drule hoare_post_imps, 60 atomize (full), 61 focus_concl 62 \<open>intro impI allI, 63 m, 64 atomize (full), 65 ((rule uncurry2)+)?\<close>, 66 rule trivial_imp) 67 68method post_asm methods m = 69 (post_asm_raw \<open>(simp only: bipred_conj_def pred_conj_def)?,(elim conjE)?,m\<close>) 70 71 72named_theorems packed_validEs 73 74lemmas [packed_validEs] = packed_validE packed_validRE 75 76named_theorems packed_validIs 77 78lemmas [packed_validIs] = packed_validI packed_validRI 79 80method post_raw methods m = 81 (focus_concl 82 \<open>rule packed_validEs, 83 focus_concl \<open>m,fold_subgoals\<close>, 84 atomize (full), 85 rule packed_validI\<close>) 86 87method post_strong methods m_distinct m_all = 88 (post_raw 89 \<open>(simp only: pred_conj_def bipred_conj_def)?, 90 (intro impI conjI allI)?, 91 distinct_subgoals_strong \<open>m_distinct\<close>, 92 all \<open>m_all\<close>, 93 fold_subgoals\<close>) 94 95method post methods m = post_strong \<open>(assumption | erule mp)+\<close> \<open>m\<close> 96 97end 98 99 100text \<open> 101 Method (meant to be used with @ as an attribute) used for producing multiple facts out of 102 a single hoare triple with a conjunction in its post condition. 103\<close> 104 105context begin 106 107private lemma hoare_decompose: 108 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>" 109 by (fastforce simp add: valid_def pred_conj_def) 110 111private lemma hoare_decomposeE_R: 112 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-" 113 by (fastforce simp add: validE_R_def validE_def valid_def pred_conj_def split: prod.splits sum.splits) 114 115private lemma hoare_decomposeE_E: 116 "\<lbrace>P\<rbrace> f -,\<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>" 117 by (fastforce simp add: validE_E_def validE_def valid_def pred_conj_def split: prod.splits sum.splits) 118 119private lemma hoare_decomposeE: 120 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. E r s \<and> E' r s\<rbrace>,\<lbrace>\<lambda>r s. R r s \<and> R' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>E\<rbrace>,- \<and> \<lbrace>P\<rbrace> f \<lbrace>E'\<rbrace>,- \<and> \<lbrace>P\<rbrace> f -,\<lbrace>R\<rbrace> \<and> \<lbrace>P\<rbrace> f -,\<lbrace>R'\<rbrace>" 121 by (fastforce simp add: validE_R_def validE_E_def validE_def valid_def pred_conj_def split: prod.splits sum.splits) 122 123private lemmas hoare_decomposes' = hoare_decompose hoare_decomposeE_R hoare_decomposeE_E hoare_decomposeE 124 125private method add_pred_conj = (subst pred_conj_def[symmetric]) 126private method add_bipred_conj = (subst bipred_conj_def[symmetric]) 127 128private lemmas hoare_decomposes[THEN conjE] = 129 hoare_decomposes' 130 hoare_decomposes'[# \<open>add_pred_conj\<close>] 131 hoare_decomposes'[# \<open>add_bipred_conj\<close>] 132 hoare_decomposeE[# \<open>add_pred_conj, add_pred_conj\<close>] 133 hoare_decomposeE[# \<open>add_bipred_conj, add_pred_conj\<close>] 134 hoare_decomposeE[# \<open>add_pred_conj, add_bipred_conj\<close>] 135 hoare_decomposeE[# \<open>add_bipred_conj, add_bipred_conj\<close>] 136 137method hoare_decompose = (elim hoare_decomposes) 138 139end 140 141 142notepad begin 143 fix A :: "'a \<Rightarrow> bool" and B C D f 144 assume A: "\<And>s. A s = True" and 145 B: "\<And>s :: 'a. B s = True" and 146 C: "\<And>s :: 'a. C s = True" and 147 D: "\<And>s :: 'a. D s = True" and 148 f: "f = (return () :: ('a,unit) nondet_monad)" 149 150 have f_valid[@ \<open>hoare_decompose\<close>,conjuncts]: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B and C and D\<rbrace>" 151 apply (simp add: f) 152 apply wp 153 by (simp add: B C D) 154 155 note f_valid' = conjuncts 156 157 have f_d: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. D\<rbrace>" by (rule f_valid') 158 159 have f_valid_interm: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B and C and (\<lambda>s. D s \<longrightarrow> B s)\<rbrace>" 160 apply (post_strong \<open>simp\<close> \<open>-\<close>) 161 apply (wp f_valid') 162 by simp 163 164 (* All rotations are attempted when strengthening *) 165 166 have f_valid_interm: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. (\<lambda>s. D s \<longrightarrow> B s) and B and C \<rbrace>" 167 apply (post_strong \<open>simp\<close> \<open>-\<close>, wp f_valid') 168 by simp 169 170end 171 172 173 174 175end 176