-
Notifications
You must be signed in to change notification settings - Fork 108
/
MachineMonad.thy
94 lines (74 loc) · 2.7 KB
/
MachineMonad.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
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory MachineMonad
imports MachineTypes
begin
arch_requalify_types
machine_state
machine_state_rest
arch_requalify_consts
underlying_memory
underlying_memory_update
device_state
device_state_update
irq_masks
machine_state_rest
machine_state_rest_update
text \<open>
The machine monad is used for operations on the state defined above.
\<close>
type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
translations
(type) "'c machine_monad" <= (type) "machine_state \<Rightarrow> ('c \<times> machine_state) set \<times> bool"
type_synonym 'a machine_rest_monad = "(machine_state_rest, 'a) nondet_monad"
definition
machine_rest_lift :: "'a machine_rest_monad \<Rightarrow> 'a machine_monad"
where
"machine_rest_lift f \<equiv> do
mr \<leftarrow> gets machine_state_rest;
(r, mr') \<leftarrow> select_f (f mr);
modify (\<lambda>s. s \<lparr> machine_state_rest := mr' \<rparr>);
return r
od"
definition
ignore_failure :: "('s,unit) nondet_monad \<Rightarrow> ('s,unit) nondet_monad"
where
"ignore_failure f \<equiv>
\<lambda>s. if fst (f s) = {} then ({((),s)},False) else (fst (f s), False)"
text \<open>The wrapper doesn't do anything for usual operations:\<close>
lemma failure_consistent:
"\<lbrakk> empty_fail f; no_fail \<top> f \<rbrakk> \<Longrightarrow> ignore_failure f = f"
apply (simp add: ignore_failure_def empty_fail_def no_fail_def)
apply (rule ext)
apply (auto intro: prod_eqI)
done
text \<open>And it has the desired properties\<close>
lemma ef_ignore_failure [simp]:
"empty_fail (ignore_failure f)"
by (simp add: empty_fail_def ignore_failure_def)
lemma no_fail_ignore_failure [simp, intro!]:
"no_fail \<top> (ignore_failure f)"
by (simp add: no_fail_def ignore_failure_def)
lemma ef_machine_rest_lift [simp, intro!]:
"empty_fail f \<Longrightarrow> empty_fail (machine_rest_lift f)"
apply (clarsimp simp: empty_fail_def machine_rest_lift_def simpler_gets_def
select_f_def bind_def simpler_modify_def return_def)
apply force
done
lemma no_fail_machine_state_rest [intro!]:
"no_fail P f \<Longrightarrow> no_fail (P o machine_state_rest) (machine_rest_lift f)"
apply (simp add: no_fail_def machine_rest_lift_def simpler_gets_def
select_f_def bind_def simpler_modify_def return_def)
apply force
done
lemma no_fail_machine_state_rest_T [simp, intro!]:
"no_fail \<top> f \<Longrightarrow> no_fail \<top> (machine_rest_lift f)"
apply (drule no_fail_machine_state_rest)
apply (simp add: o_def)
done
definition
"machine_op_lift \<equiv> machine_rest_lift o ignore_failure"
end