-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathutp_rea_wp.thy
187 lines (148 loc) · 7.71 KB
/
utp_rea_wp.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
section \<open> Reactive Weakest Preconditions \<close>
theory utp_rea_wp
imports utp_rea_prog
begin
text \<open> Here, we create a weakest precondition calculus for reactive relations, using the recast
boolean algebra and relational operators. Please see our journal paper~\cite{Foster17c} for more information. \<close>
definition wp_rea ::
"('t::trace, '\<alpha>) rp_hrel \<Rightarrow>
('t, '\<alpha>) rp_hrel \<Rightarrow>
('t, '\<alpha>) rp_hrel" (infix "wp\<^sub>r" 60)
where [pred]: "P wp\<^sub>r Q = (\<not>\<^sub>r P ;; (\<not>\<^sub>r Q))"
lemma in_var_unrest_wp_rea [unrest]: "\<lbrakk> mwb_lens x; $x\<^sup>< \<sharp> P; tr \<bowtie> x \<rbrakk> \<Longrightarrow> $x\<^sup>< \<sharp> (P wp\<^sub>r Q)"
unfolding wp_rea_def R1_def rea_not_def
by (auto intro!: unrest_pred unrest_seq_ivar, unrest)
lemma out_var_unrest_wp_rea [unrest]: "\<lbrakk> mwb_lens x; $x\<^sup>> \<sharp> Q; tr \<bowtie> x \<rbrakk> \<Longrightarrow> $x\<^sup>> \<sharp> (P wp\<^sub>r Q)"
unfolding wp_rea_def R1_def rea_not_def
by (auto intro!: unrest_intro; unrest)
lemma wp_rea_R1 [closure]: "P wp\<^sub>r Q is R1"
by (pred_auto)
lemma wp_rea_RR_closed [closure]: "\<lbrakk> P is RR; Q is RR \<rbrakk> \<Longrightarrow> P wp\<^sub>r Q is RR"
by (simp add: wp_rea_def closure)
lemma wp_rea_impl_lemma:
"((P wp\<^sub>r Q) \<longrightarrow>\<^sub>r (R1(P) ;; R1(Q \<longrightarrow>\<^sub>r R))) = ((P wp\<^sub>r Q) \<longrightarrow>\<^sub>r (R1(P) ;; R1(R)))"
by (pred_auto, blast)
lemma wpR_impl_post_spec:
assumes "P is RR"
shows "(P wp\<^sub>r Q\<^sub>1 \<longrightarrow>\<^sub>r (P ;; (Q\<^sub>1 \<longrightarrow>\<^sub>r Q\<^sub>2))) = (P ;; (Q\<^sub>1 \<longrightarrow>\<^sub>r Q\<^sub>2))"
by (simp add: R1_seqr_closure RR_implies_R1 assms rea_impl_def rea_not_R1 rea_not_not seqr_or_distr wp_rea_def)
lemma wpR_R1_right [wp]:
"P wp\<^sub>r R1(Q) = P wp\<^sub>r Q"
by (pred_auto)
lemma wp_rea_true [wp]: "P wp\<^sub>r true = true\<^sub>r"
by (pred_auto)
lemma wp_rea_conj [wp]: "P wp\<^sub>r (Q \<and> R) = (P wp\<^sub>r Q \<and> P wp\<^sub>r R)"
by (simp add: wp_rea_def seqr_or_distr)
lemma wp_rea_USUP_mem [wp]:
"A \<noteq> {} \<Longrightarrow> P wp\<^sub>r (\<Squnion> i\<in>A. Q(i)) = (\<Squnion> i\<in>A. P wp\<^sub>r Q(i))"
by (simp add: wp_rea_def seq_SUP_distl)
lemma wp_rea_Inf_pre [wp]:
"P wp\<^sub>r (\<Squnion>i\<in>{0..n::nat}. Q(i)) = (\<Squnion>i\<in>{0..n}. P wp\<^sub>r Q(i))"
by (simp add: wp_rea_def seq_SUP_distl)
lemma wp_rea_div [wp]:
"(\<not>\<^sub>r P ;; true\<^sub>r) = true\<^sub>r \<Longrightarrow> true\<^sub>r wp\<^sub>r P = false"
by (simp add: wp_rea_def rpred, pred_auto, blast)
lemma wp_rea_st_cond_div [wp]:
"P \<noteq> true \<Longrightarrow> true\<^sub>r wp\<^sub>r [P]\<^sub>S\<^sub>< = false"
by (pred_auto)
lemma wp_rea_cond [wp]:
"out\<alpha> \<sharp> b \<Longrightarrow> (P \<triangleleft> b \<triangleright> Q) wp\<^sub>r R = (P wp\<^sub>r R) \<triangleleft> b \<triangleright> (Q wp\<^sub>r R)"
by (pred_auto; blast)
lemma wp_rea_RC_false [wp]:
"P is RC \<Longrightarrow> (\<not>\<^sub>r P) wp\<^sub>r false = P"
by (metis Healthy_if RC1_def RC_implies_RC1 rea_not_false wp_rea_def)
lemma wp_rea_seq [wp]:
assumes "Q is R1"
shows "(P ;; Q) wp\<^sub>r R = P wp\<^sub>r (Q wp\<^sub>r R)" (is "?lhs = ?rhs")
proof -
have "?rhs = R1 (\<not> P ;; R1 (Q ;; R1 (\<not> R)))"
by (simp add: wp_rea_def rea_not_def R1_negate_R1 assms)
also have "... = R1 (\<not> P ;; (Q ;; R1 (\<not> R)))"
by (metis Healthy_if R1_seqr assms)
also have "... = R1 (\<not> (P ;; Q) ;; R1 (\<not> R))"
by (simp add: seqr_assoc)
finally show ?thesis
by (simp add: wp_rea_def rea_not_def)
qed
lemma wp_rea_skip [wp]:
assumes "Q is R1"
shows "II wp\<^sub>r Q = Q"
by (simp add: wp_rea_def rpred assms Healthy_if)
lemma wp_rea_rea_skip [wp]:
assumes "Q is RR"
shows "II\<^sub>r wp\<^sub>r Q = Q"
by (simp add: wp_rea_def rpred closure assms Healthy_if)
lemma power_wp_rea_RR_closed [closure]:
"\<lbrakk> R is RR; P is RR \<rbrakk> \<Longrightarrow> R \<^bold>^ i wp\<^sub>r P is RR"
by (induct i, simp_all add: wp closure)
lemma wp_rea_rea_assigns [wp]:
assumes "P is RR"
shows "\<langle>\<sigma>\<rangle>\<^sub>r wp\<^sub>r P = \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>\<sigma> \<dagger> P"
proof -
have "\<langle>\<sigma>\<rangle>\<^sub>r wp\<^sub>r (RR P) = \<lceil>\<sigma>\<rceil>\<^sub>S\<^sub>\<sigma> \<dagger> (RR P)"
by (pred_auto)
thus ?thesis
by (metis Healthy_def assms)
qed
lemma wp_rea_miracle [wp]: "false wp\<^sub>r Q = true\<^sub>r"
by (simp add: wp_rea_def)
lemma wp_rea_disj [wp]: "(P \<or> Q) wp\<^sub>r R = (P wp\<^sub>r R \<and> Q wp\<^sub>r R)"
by (pred_auto, blast)
lemma wp_rea_UINF [wp]:
assumes "A \<noteq> {}"
shows "(\<Sqinter> x\<in>A. P(x)) wp\<^sub>r Q = (\<Squnion> x\<in>A. P(x) wp\<^sub>r Q)"
by (simp add: wp_rea_def rea_not_def seq_SUP_distr not_SUP R1_UINF assms)
lemma wp_rea_choice [wp]:
"(P \<sqinter> Q) wp\<^sub>r R = (P wp\<^sub>r R \<and> Q wp\<^sub>r R)"
by (pred_auto, blast)
lemma wp_rea_UINF_ind [wp]:
"(\<Sqinter> i. P(i)) wp\<^sub>r Q = (\<Squnion> i. P(i) wp\<^sub>r Q)"
by (simp add: wp_rea_UINF)
lemma rea_assume_wp [wp]:
assumes "P is RC"
shows "([b]\<^sup>\<top>\<^sub>r wp\<^sub>r P) = ([b]\<^sub>S\<^sub>< \<longrightarrow>\<^sub>r P)"
proof -
have "([b]\<^sup>\<top>\<^sub>r wp\<^sub>r RC P) = ([b]\<^sub>S\<^sub>< \<longrightarrow>\<^sub>r RC P)"
by (pred_auto)
thus ?thesis
by (simp add: Healthy_if assms)
qed
lemma rea_star_wp [wp]:
assumes "P is RR" "Q is RR"
shows "P\<^sup>\<star>\<^sup>r wp\<^sub>r Q = (\<Squnion> i. P \<^bold>^ i wp\<^sub>r Q)"
proof -
have "P\<^sup>\<star>\<^sup>r wp\<^sub>r Q = (Q \<and> P\<^bold>+ wp\<^sub>r Q)"
by (simp add: assms rrel_theory.Star_alt_def wp_rea_choice wp_rea_rea_skip)
also have "... = (II wp\<^sub>r Q \<and> (\<Squnion> i. P \<^bold>^ Suc i wp\<^sub>r Q))"
by (simp add: uplus_power_def wp closure assms)
also have "... = (\<Squnion> i. P \<^bold>^ i wp\<^sub>r Q)"
proof -
have "P\<^sup>\<star> wp\<^sub>r Q = P\<^sup>\<star>\<^sup>r wp\<^sub>r Q"
by (metis assms(2) rea_skip_RR rrel_theory.utp_star_def wp_rea_R1 wp_rea_rea_skip wp_rea_seq)
then show ?thesis
by (simp add: calculation ustar_def wp_rea_UINF_ind)
qed
finally show ?thesis .
qed
lemma wp_rea_R2_closed [closure]:
"\<lbrakk> P is R2; Q is R2 \<rbrakk> \<Longrightarrow> P wp\<^sub>r Q is R2"
by (simp add: wp_rea_def closure)
lemma wp_rea_false_RC1': "P is R2 \<Longrightarrow> RC1(P wp\<^sub>r false) = P wp\<^sub>r false"
by (simp add: wp_rea_def RC1_def closure rpred seqr_assoc)
lemma wp_rea_false_RC1: "P is R2 \<Longrightarrow> P wp\<^sub>r false is RC1"
by (simp add :Healthy_def wp_rea_false_RC1')
lemma wp_rea_false_RR:
"\<lbrakk> $ok\<^sup>< \<sharp> P; $wait\<^sup>< \<sharp> P; P is R2 \<rbrakk> \<Longrightarrow> P wp\<^sub>r false is RR"
by (rule RR_R2_intro, simp_all add: unrest closure)
lemma wp_rea_false_RC:
"\<lbrakk> $ok\<^sup>< \<sharp> P; $wait\<^sup>< \<sharp> P; P is R2 \<rbrakk> \<Longrightarrow> P wp\<^sub>r false is RC"
by (rule RC_intro', simp_all add: wp_rea_false_RC1 wp_rea_false_RR)
lemma wp_rea_RC1: "\<lbrakk> P is RR; Q is RC \<rbrakk> \<Longrightarrow> P wp\<^sub>r Q is RC1"
by (rule Healthy_intro, simp add: wp_rea_def RC1_def rpred closure seqr_assoc RC1_prop RC_implies_RC1)
lemma wp_rea_RC [closure]: "\<lbrakk> P is RR; Q is RC \<rbrakk> \<Longrightarrow> P wp\<^sub>r Q is RC"
by (rule RC_intro', simp_all add: wp_rea_RC1 closure)
lemma wpR_power_RC_closed [closure]:
assumes "P is RR" "Q is RC"
shows "P \<^bold>^ i wp\<^sub>r Q is RC"
by (metis RC_implies_RR RR_implies_R1 assms power.power_eq_if power_Suc_RR_closed wp_rea_RC wp_rea_skip)
end