-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathL1Valid.thy
166 lines (144 loc) · 6.66 KB
/
L1Valid.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
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
(*
* Proofs about L1.
*)
theory L1Valid
imports L1Defs
begin
(* Weakest Precondition Proofs (WP) *)
lemma L1_skip_wp [wp]: "\<lbrace> P () \<rbrace> L1_skip \<lbrace> P \<rbrace>, \<lbrace> Q \<rbrace>"
apply (clarsimp simp: L1_skip_def, wp)
done
lemma L1_modify_wp [wp]: "\<lbrace> \<lambda>s. P () (f s) \<rbrace> L1_modify f \<lbrace> P \<rbrace>, \<lbrace> Q \<rbrace>"
apply (clarsimp simp: L1_modify_def, wp)
done
lemma L1_spec_wp [wp]: "\<lbrace> \<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t \<rbrace> L1_spec f \<lbrace> P \<rbrace>, \<lbrace> Q \<rbrace>"
apply (unfold L1_spec_def)
apply wp
done
lemma L1_init_wp [wp]: "\<lbrace> \<lambda>s. \<forall>x. P () (f (\<lambda>_. x) s) \<rbrace> L1_init f \<lbrace> P \<rbrace>, \<lbrace> Q \<rbrace>"
apply (unfold L1_init_def)
apply wp
apply fastforce
done
(* Liveness proofs. (LP) *)
lemma L1_skip_lp: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q () s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_skip \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_skip_def)
apply (clarsimp simp: returnOk_def return_def validE_def valid_def)
done
lemma L1_guard_lp: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q () s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_guard e \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_guard_def guard_def)
apply (clarsimp simp: returnOk_def return_def validE_def valid_def get_def bind_def fail_def)
done
lemma L1_fail_lp: "\<lbrace>P\<rbrace> L1_fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_fail_def)
done
lemma L1_throw_lp: "\<lbrakk> \<And>s. P s \<Longrightarrow> E () s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_throw \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_throw_def)
apply (clarsimp simp: throwError_def validE_def valid_def return_def)
done
lemma L1_spec_lp: "\<lbrakk> \<And>s r. \<lbrakk> (s, r) \<in> e; P s \<rbrakk> \<Longrightarrow> Q () r \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_spec e \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_spec_def)
apply (clarsimp simp: spec_def validE_def valid_def)
done
lemma L1_modify_lp: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q () (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_modify f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_modify_def)
apply (clarsimp simp: modify_def validE_def valid_def return_def get_def put_def bind_def)
done
lemma L1_call_lp:
"\<lbrakk> \<And>s r. P s \<Longrightarrow> Q () (return_xf r (scope_teardown s r)) \<rbrakk> \<Longrightarrow>
\<lbrace>P\<rbrace> L1_call scope_setup dest_fn scope_teardown return_xf \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_call_def)
apply (clarsimp simp: modify_def validE_def valid_def return_def
get_def put_def bind_def bindE_def liftE_def throwError_def lift_def
handleE_def handleE'_def fail_def split: sum.splits)
done
lemma L1_seq_lp: "\<lbrakk>
\<lbrace>P1\<rbrace> A \<lbrace>Q1\<rbrace>,\<lbrace>E1\<rbrace>;
\<lbrace>P2\<rbrace> B \<lbrace>Q2\<rbrace>,\<lbrace>E2\<rbrace>;
\<And>s. P s \<Longrightarrow> P1 s;
\<And>s. Q1 () s \<Longrightarrow> P2 s;
\<And>s. Q2 () s \<Longrightarrow> Q () s;
\<And>s. E1 () s \<Longrightarrow> E () s;
\<And>s. E2 () s \<Longrightarrow> E () s
\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_seq A B \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_seq_def)
apply (rule bindE_wp)
apply (erule hoare_chainE, simp+)[1]
apply (erule hoare_chainE, simp+)[1]
done
lemma L1_condition_lp: "
\<lbrakk> \<lbrace>P1\<rbrace> A \<lbrace>Q1\<rbrace>,\<lbrace>E1\<rbrace>;
\<lbrace>P2\<rbrace> B \<lbrace>Q2\<rbrace>,\<lbrace>E2\<rbrace>;
\<And>s. P s \<Longrightarrow> P1 s;
\<And>s. P s \<Longrightarrow> P2 s;
\<And>s. Q1 () s \<Longrightarrow> Q () s;
\<And>s. Q2 () s \<Longrightarrow> Q () s;
\<And>s. E1 () s \<Longrightarrow> E () s;
\<And>s. E2 () s \<Longrightarrow> E () s \<rbrakk> \<Longrightarrow>
\<lbrace>P\<rbrace> L1_condition c A B \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_condition_def)
apply wp
apply (erule hoare_chainE, simp+)[1]
apply (erule hoare_chainE, simp+)[1]
apply simp
done
lemma L1_catch_lp: "
\<lbrakk> \<lbrace>P1\<rbrace> A \<lbrace>Q1\<rbrace>,\<lbrace>E1\<rbrace>;
\<lbrace>P2\<rbrace> B \<lbrace>Q2\<rbrace>,\<lbrace>E2\<rbrace>;
\<And>s. P s \<Longrightarrow> P1 s;
\<And>s. E1 () s \<Longrightarrow> P2 s;
\<And>s. Q1 () s \<Longrightarrow> Q () s;
\<And>s. Q2 () s \<Longrightarrow> Q () s;
\<And>s. E2 () s \<Longrightarrow> E () s \<rbrakk> \<Longrightarrow>
\<lbrace>P\<rbrace> L1_catch A B \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_catch_def)
including no_pre
apply wp
apply (erule hoare_chainE, simp+)[1]
apply (erule hoare_chainE, simp+)[1]
done
lemma L1_init_lp: "\<lbrakk> \<And>s. P s \<Longrightarrow> \<forall>x. Q () (f (\<lambda>_. x) s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> L1_init f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply wp
apply clarsimp
done
lemma L1_while_lp:
assumes body_lp: "\<lbrace> P' \<rbrace> B \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>"
and p_impl: "\<And>s. P s \<Longrightarrow> P' s"
and q_impl: "\<And>s. Q' () s \<Longrightarrow> Q () s"
and e_impl: "\<And>s. E' () s \<Longrightarrow> E () s"
and inv: " \<And>s. Q' () s \<Longrightarrow> P' s"
and inv': " \<And>s. P' s \<Longrightarrow> Q' () s"
shows "\<lbrace> P \<rbrace> L1_while c B \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>"
apply (rule hoare_chainE [where P'=P' and Q'=Q' and E'=E'])
apply (clarsimp simp: L1_while_def)
apply (rule validE_whileLoopE [where I="\<lambda>r s. P' s"])
apply simp
apply (rule hoare_chainE [OF body_lp])
apply (clarsimp simp: p_impl)
apply (clarsimp simp: inv)
apply simp
apply (clarsimp simp: inv')
apply (clarsimp simp: p_impl)
apply (clarsimp simp: q_impl)
apply (clarsimp simp: e_impl)
done
lemma L1_recguard_lp:
"\<lbrakk>\<lbrace>P1\<rbrace> A \<lbrace>Q1\<rbrace>, \<lbrace>E1\<rbrace>;
\<And>s. P s \<Longrightarrow> P1 s;
\<And>s. Q1 () s \<Longrightarrow> Q () s;
\<And>s. E1 () s \<Longrightarrow> E () s\<rbrakk> \<Longrightarrow>
\<lbrace>P\<rbrace> L1_recguard v A \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
apply (clarsimp simp: L1_recguard_def)
apply wp
apply (erule hoare_chainE)
apply assumption
apply simp
apply simp
apply simp
done
end