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