1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory SpecValid_R
8imports ExtraCorres
9begin
10
11definition
12  spec_valid :: "'s \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
13                 ("_ \<turnstile> /\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>" [60,0,0,0] 100)
14where
15 "spec_valid st P f Q \<equiv> valid (\<lambda>s. s = st \<and> P s) f Q"
16
17definition
18  spec_validE :: "'s \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'r) nondet_monad \<Rightarrow>
19                   ('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('e \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
20                 ("_ \<turnstile> /\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>, /\<lbrace>_\<rbrace>)" [60,0,0,0] 100)
21where
22 "spec_validE st P f Q E \<equiv> validE (\<lambda>s. s = st \<and> P s) f Q E"
23
24lemma use_spec':
25  assumes x: "\<And>s. s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
26  shows      "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
27  apply (clarsimp simp: valid_def)
28  apply (cut_tac s=s in x)
29  apply (clarsimp simp: valid_def spec_valid_def)
30  apply (erule(1) my_BallE, simp)
31  done
32
33lemma use_specE':
34  "\<lbrakk> \<And>s. s \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace>"
35  apply (simp add: validE_def spec_validE_def)
36  apply (fold spec_valid_def)
37  apply (simp add: use_spec')
38  done
39
40lemmas use_spec = use_spec' use_specE'
41
42lemma drop_equalled_validE:
43  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. s = s' \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
44  by (erule hoare_pre, clarsimp)
45
46lemma drop_spec_valid[wp_split]:
47  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
48  apply (simp add: spec_valid_def)
49  apply (erule hoare_vcg_precond_imp)
50  apply clarsimp
51  done
52
53lemma drop_spec_validE[wp_split]:
54  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
55  apply (simp add: spec_validE_def)
56  apply (erule hoare_vcg_precond_impE)
57  apply clarsimp
58  done
59
60lemma split_spec_bindE[wp_split]:
61  assumes x: "\<And>rv s''. (Inr rv, s'') \<in> fst (f s') \<Longrightarrow> s'' \<turnstile> \<lbrace>B rv\<rbrace> g rv \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>"
62  shows "s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>
63   \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>"
64  apply (clarsimp simp: spec_validE_def validE_def valid_def bind_def bindE_def lift_def split_def)
65  apply (case_tac a)
66   apply (clarsimp simp add: throwError_def return_def)
67   apply (erule(1) my_BallE, simp)
68  apply clarsimp
69  apply (erule(1) my_BallE, simp)
70  apply (drule x)
71  apply (clarsimp simp: spec_validE_def validE_def valid_def split_def)
72  apply (erule(1) my_BallE, simp)
73  done
74
75lemma split_spec_bind[wp_split]:
76  assumes x: "\<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> s'' \<turnstile> \<lbrace>B rv\<rbrace> g rv \<lbrace>C\<rbrace>"
77  shows "s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>
78   \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>"
79  apply (clarsimp simp: spec_valid_def valid_def bind_def lift_def split_def)
80  apply (erule(1) my_BallE, simp)
81  apply (drule x)
82  apply (fastforce simp: spec_valid_def valid_def split_def)
83  done
84
85lemma split_spec_if[wp_split]:
86  "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>;
87     \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>
88   \<rbrakk>  \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>"
89  by (cases G, simp+)
90
91lemma split_spec_ifE[wp_split]:
92  "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>;
93     \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>
94   \<rbrakk>  \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
95  by (cases G, simp+)
96
97lemma split_spec_unlessE[wp_split]:
98  "\<lbrakk> \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>  \<Longrightarrow>
99     s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> Q () s) \<and> (\<not> G \<longrightarrow> P s)\<rbrace> unlessE G f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
100  apply (cases G, simp_all add: unlessE_def)
101  apply wp
102  done
103
104lemma spec_fun_applyE [wp_split]:
105  "s \<turnstile> \<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
106  by simp
107
108lemma split_spec_K_bind[wp_split]:
109  "s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>"
110  by simp
111
112lemma split_spec_K_bindE[wp_split]:
113  "s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
114  by simp
115
116lemma fudge_hoare:
117  "s \<turnstile> \<lbrace>P\<rbrace> \<lambda>s. f s \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
118  .
119
120lemma split_spec_whenE [wp_split]:
121  "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>  \<Longrightarrow>
122     s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> Q () s)\<rbrace> whenE G f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
123  apply (cases G, simp_all add: whenE_def)
124  apply wp
125  done
126
127lemma spec_valid_conj_lift:
128  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk>
129     \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
130  apply (simp add: spec_valid_def)
131  apply (drule(1) hoare_vcg_conj_lift)
132  apply (simp add: conj_comms)
133  done
134
135lemma spec_valid_conj_liftE1:
136  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk>
137     \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E'\<rbrace>"
138  apply (simp add: spec_validE_def)
139  apply (drule(1) hoare_vcg_conj_liftE1)
140  apply (simp add: conj_comms pred_conj_def)
141  done
142
143lemma spec_valid_conj_liftE2:
144  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk>
145     \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E'\<rbrace>"
146  apply (simp add: spec_validE_def)
147  apply (drule(1) hoare_vcg_conj_liftE1)
148  apply (simp add: conj_comms pred_conj_def)
149  done
150
151lemma hoare_pre_spec_valid:
152  "\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
153  apply (simp add: spec_valid_def)
154  apply (erule hoare_pre)
155  apply clarsimp
156  done
157
158lemma hoare_pre_spec_validE:
159  "\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
160  apply (simp add: spec_validE_def)
161  apply (erule hoare_pre)
162  apply clarsimp
163  done
164
165lemma spec_validE_if:
166  "\<lbrakk> G \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<not> G \<Longrightarrow> s \<turnstile> \<lbrace>P'\<rbrace> g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and P'\<rbrace> if G then f else g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
167  apply (cases G, simp_all)
168   apply (clarsimp elim!: hoare_pre_spec_validE)+
169  done
170
171lemma spec_strengthen_post:
172  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s r. Q' s r \<Longrightarrow> Q s r \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
173  by (simp add: spec_valid_def valid_def
174                split_def split: sum.splits)
175
176lemma spec_strengthen_postE:
177  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>; \<And>s r. Q' s r \<Longrightarrow> Q s r \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
178  by (simp add: spec_valid_def spec_validE_def validE_def valid_def
179                split_def split: sum.splits)
180
181end
182