sys-init: Isabelle2020 update
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
parent
913026178a
commit
698d7a913b
|
@ -13,7 +13,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory ExampleSpecIRQ_SI
|
theory ExampleSpecIRQ_SI
|
||||||
imports WellFormed_SI
|
imports SysInit.WellFormed_SI
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
@ -206,9 +206,6 @@ definition
|
||||||
cdl_current_domain = minBound\<rparr>"
|
cdl_current_domain = minBound\<rparr>"
|
||||||
|
|
||||||
|
|
||||||
declare cap_object_simps [simp]
|
|
||||||
|
|
||||||
|
|
||||||
lemmas cnode_defs = cnode_a1_def cnode_a2_def cnode_b_def cnode_extra_def
|
lemmas cnode_defs = cnode_a1_def cnode_a2_def cnode_b_def cnode_extra_def
|
||||||
lemmas obj_defs = cnode_defs tcb_a_def tcb_b_def pd_a_def pd_b_def pt_a_def
|
lemmas obj_defs = cnode_defs tcb_a_def tcb_b_def pd_a_def pd_b_def pt_a_def
|
||||||
|
|
||||||
|
|
|
@ -13,13 +13,11 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory ExampleSpec_SI
|
theory ExampleSpec_SI
|
||||||
imports WellFormed_SI
|
imports SysInit.WellFormed_SI
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
declare cap_object_simps [simp]
|
|
||||||
|
|
||||||
lemma object_slots_empty_object [simp]:
|
lemma object_slots_empty_object [simp]:
|
||||||
"object_slots (Frame \<lparr>cdl_frame_size_bits = small_frame_size\<rparr>) slot = Some cap \<Longrightarrow> cap = NullCap"
|
"object_slots (Frame \<lparr>cdl_frame_size_bits = small_frame_size\<rparr>) slot = Some cap \<Longrightarrow> cap = NullCap"
|
||||||
"object_slots (PageDirectory \<lparr>cdl_page_directory_caps = empty_cap_map pd_size\<rparr>) slot = Some cap \<Longrightarrow> cap = NullCap"
|
"object_slots (PageDirectory \<lparr>cdl_page_directory_caps = empty_cap_map pd_size\<rparr>) slot = Some cap \<Longrightarrow> cap = NullCap"
|
||||||
|
|
Loading…
Reference in New Issue