1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory DetWPLib 8imports HaskellLemmaBucket 9begin 10 11definition 12 "det_wp P f \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r}, False))" 13 14lemma det_result: 15 "\<lbrakk> det_wp P f; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. fst (f s) = {(rv, s)}\<rbrace>" 16 by (fastforce simp: det_wp_def valid_def split_def) 17 18lemma det_wp_use: 19 "det_wp P f \<Longrightarrow> P s \<Longrightarrow> (fst (f s) = {s'}) = (s' \<in> fst (f s))" 20 by (fastforce simp: det_wp_def) 21 22lemma det_wp_det: 23 "det f \<Longrightarrow> det_wp \<top> f" 24 by (clarsimp simp: det_def det_wp_def) 25 26lemma det_wp_no_fail: 27 "det_wp P f \<Longrightarrow> no_fail P f" 28 by (fastforce simp: det_wp_def no_fail_def) 29 30lemma det_wp_bind [wp]: 31 "\<lbrakk> det_wp P f; \<And>rv. det_wp (Q rv) (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> det_wp (P and P') (f >>= (\<lambda>rv. g rv))" 32 apply (simp add: det_wp_def valid_def split_def bind_def) 33 apply fastforce 34 done 35 36lemma det_wp_pre: 37 "det_wp P' f \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> det_wp P f" 38 by (simp add: det_wp_def) 39 40lemma det_wp_return [wp]: 41 "det_wp \<top> (return x)" 42 by (simp add: det_wp_def return_def) 43 44lemma det_wp_case_option [wp]: 45 "\<lbrakk> x = None \<Longrightarrow> det_wp P f; 46 \<And>y. x = Some y \<Longrightarrow> det_wp (Q y) (g y) \<rbrakk> \<Longrightarrow> 47 det_wp (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q y s)) (case_option f g x)" 48 by (cases x) auto 49 50lemma det_wp_mapM [wp]: 51 assumes "\<And>x. x \<in> set xs \<Longrightarrow> det_wp (P x) (f x)" 52 assumes "\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>" 53 shows "det_wp (\<lambda>s. \<forall>x \<in> set xs. P x s) (mapM f xs)" using assms 54proof (induct xs) 55 case Nil thus ?case 56 by (simp add: mapM_Nil) (rule det_wp_pre, wp) 57next 58 case (Cons z zs) 59 show ?case 60 apply (simp add: mapM_Cons) 61 apply (rule det_wp_pre) 62 apply (wp Cons.hyps Cons.prems hoare_vcg_const_Ball_lift|simp)+ 63 done 64qed 65 66lemma det_wp_get [wp]: 67 "det_wp \<top> get" 68 by (simp add: get_def det_wp_def) 69 70lemma det_wp_gets [wp]: 71 "det_wp \<top> (gets f)" 72 by (simp add: simpler_gets_def det_wp_def) 73 74lemma det_wp_fail [wp]: 75 "det_wp \<bottom> fail" 76 by (simp add: fail_def det_wp_def) 77 78lemma det_wp_assert [wp]: 79 "det_wp (\<lambda>_. P) (assert P)" 80 by (simp add: assert_def det_wp_fail det_wp_return) 81 82lemma det_wp_stateAssert [wp]: 83 "det_wp P (stateAssert P xs)" 84 apply (simp add: stateAssert_def) 85 apply (rule det_wp_pre, wp) 86 apply simp 87 done 88 89lemma det_wp_select_f: 90 "det_wp (\<lambda>_. P s) f \<Longrightarrow> det_wp (\<lambda>_. P s) (select_f (f s))" 91 apply (clarsimp simp: select_f_def det_wp_def) 92 apply (erule_tac x=s in allE) 93 apply clarsimp 94 done 95 96lemma det_wp_modify [wp]: 97 "det_wp \<top> (modify f)" 98 by (simp add: det_wp_def simpler_modify_def) 99 100(* DetWP.thy:det_wp_liftM line 31 annotation [wp]*) 101lemma det_wp_liftM [wp]: 102 "det_wp P g \<Longrightarrow> det_wp P (liftM f g)" 103 apply (simp add: liftM_def) 104 apply (rule det_wp_pre) 105 apply (wp|simp)+ 106 done 107 108 109(* DetWP.thy:det_wp_when line 37 annotation [wp]*) 110lemma det_wp_when [wp]: 111 "det_wp P f \<Longrightarrow> det_wp (\<lambda>s. Q \<longrightarrow> P s) (when Q f)" 112 by (clarsimp simp: when_def det_wp_return) 113 114(* DetWP.thy:det_wp_unless line 41 annotation [wp]*) 115lemma det_wp_unless [wp]: 116 "det_wp P f \<Longrightarrow> det_wp (\<lambda>s. \<not>Q \<longrightarrow> P s) (unless Q f)" 117 by (simp add: unless_def det_wp_when) 118 119(* DetWP.thy:det_wp_assert_opt line 38 annotation [wp]*) 120lemma det_wp_assert_opt : 121 "det_wp (\<lambda>_. x \<noteq> None) (assert_opt x)" 122 apply (simp add: assert_opt_def) 123 apply (rule det_wp_pre, wp) 124 apply simp 125 done 126 127end 128