forked from seL4/l4v
-
Notifications
You must be signed in to change notification settings - Fork 0
/
DetWPLib.thy
127 lines (103 loc) · 3.99 KB
/
DetWPLib.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
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory DetWPLib
imports HaskellLemmaBucket
begin
definition
"det_wp P f \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r}, False))"
lemma det_result:
"\<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>"
by (fastforce simp: det_wp_def valid_def split_def)
lemma det_wp_use:
"det_wp P f \<Longrightarrow> P s \<Longrightarrow> (fst (f s) = {s'}) = (s' \<in> fst (f s))"
by (fastforce simp: det_wp_def)
lemma det_wp_det:
"det f \<Longrightarrow> det_wp \<top> f"
by (clarsimp simp: det_def det_wp_def)
lemma det_wp_no_fail:
"det_wp P f \<Longrightarrow> no_fail P f"
by (fastforce simp: det_wp_def no_fail_def)
lemma det_wp_bind [wp]:
"\<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))"
apply (simp add: det_wp_def valid_def split_def bind_def)
apply fastforce
done
lemma det_wp_pre:
"det_wp P' f \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> det_wp P f"
by (simp add: det_wp_def)
lemma det_wp_return [wp]:
"det_wp \<top> (return x)"
by (simp add: det_wp_def return_def)
lemma det_wp_case_option [wp]:
"\<lbrakk> x = None \<Longrightarrow> det_wp P f;
\<And>y. x = Some y \<Longrightarrow> det_wp (Q y) (g y) \<rbrakk> \<Longrightarrow>
det_wp (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q y s)) (case_option f g x)"
by (cases x) auto
lemma det_wp_mapM [wp]:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> det_wp (P x) (f x)"
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>"
shows "det_wp (\<lambda>s. \<forall>x \<in> set xs. P x s) (mapM f xs)" using assms
proof (induct xs)
case Nil thus ?case
by (simp add: mapM_Nil) (rule det_wp_pre, wp)
next
case (Cons z zs)
show ?case
apply (simp add: mapM_Cons)
apply (rule det_wp_pre)
apply (wp Cons.hyps Cons.prems hoare_vcg_const_Ball_lift|simp)+
done
qed
lemma det_wp_get [wp]:
"det_wp \<top> get"
by (simp add: get_def det_wp_def)
lemma det_wp_gets [wp]:
"det_wp \<top> (gets f)"
by (simp add: simpler_gets_def det_wp_def)
lemma det_wp_fail [wp]:
"det_wp \<bottom> fail"
by (simp add: fail_def det_wp_def)
lemma det_wp_assert [wp]:
"det_wp (\<lambda>_. P) (assert P)"
by (simp add: assert_def det_wp_fail det_wp_return)
lemma det_wp_stateAssert [wp]:
"det_wp P (stateAssert P xs)"
apply (simp add: stateAssert_def)
apply (rule det_wp_pre, wp)
apply simp
done
lemma det_wp_select_f:
"det_wp (\<lambda>_. P s) f \<Longrightarrow> det_wp (\<lambda>_. P s) (select_f (f s))"
apply (clarsimp simp: select_f_def det_wp_def)
apply (erule_tac x=s in allE)
apply clarsimp
done
lemma det_wp_modify [wp]:
"det_wp \<top> (modify f)"
by (simp add: det_wp_def simpler_modify_def)
(* DetWP.thy:det_wp_liftM line 31 annotation [wp]*)
lemma det_wp_liftM [wp]:
"det_wp P g \<Longrightarrow> det_wp P (liftM f g)"
apply (simp add: liftM_def)
apply (rule det_wp_pre)
apply (wp|simp)+
done
(* DetWP.thy:det_wp_when line 37 annotation [wp]*)
lemma det_wp_when [wp]:
"det_wp P f \<Longrightarrow> det_wp (\<lambda>s. Q \<longrightarrow> P s) (when Q f)"
by (clarsimp simp: when_def det_wp_return)
(* DetWP.thy:det_wp_unless line 41 annotation [wp]*)
lemma det_wp_unless [wp]:
"det_wp P f \<Longrightarrow> det_wp (\<lambda>s. \<not>Q \<longrightarrow> P s) (unless Q f)"
by (simp add: unless_def det_wp_when)
(* DetWP.thy:det_wp_assert_opt line 38 annotation [wp]*)
lemma det_wp_assert_opt :
"det_wp (\<lambda>_. x \<noteq> None) (assert_opt x)"
apply (simp add: assert_opt_def)
apply (rule det_wp_pre, wp)
apply simp
done
end