trivial: remove some redundant uses of split_if rule
This commit is contained in:
parent
4905a589bf
commit
c25817b553
|
@ -93,7 +93,7 @@ lemma separate_cnode_cap_rab:
|
||||||
(throwError (GuardMismatch (length cref) guard))
|
(throwError (GuardMismatch (length cref) guard))
|
||||||
| _ \<Rightarrow> throwError InvalidRoot)"
|
| _ \<Rightarrow> throwError InvalidRoot)"
|
||||||
unfolding separate_cnode_cap_def resolve_address_bits_def
|
unfolding separate_cnode_cap_def resolve_address_bits_def
|
||||||
by (auto simp: word_bits_def split: cap.split_asm split_if)
|
by (auto simp: word_bits_def split: cap.split_asm)
|
||||||
|
|
||||||
definition
|
definition
|
||||||
"separate_state s \<equiv> \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)"
|
"separate_state s \<equiv> \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)"
|
||||||
|
|
|
@ -199,7 +199,7 @@ lemma not_empty_returnOk [wp]:
|
||||||
|
|
||||||
lemma not_empty_if [wp_split]:
|
lemma not_empty_if [wp_split]:
|
||||||
"\<lbrakk> not_empty Pt m; not_empty Pf m' \<rbrakk> \<Longrightarrow> not_empty (\<lambda>s. (b \<longrightarrow> Pt s) \<and> ( \<not> b \<longrightarrow> Pf s)) (if b then m else m')"
|
"\<lbrakk> not_empty Pt m; not_empty Pf m' \<rbrakk> \<Longrightarrow> not_empty (\<lambda>s. (b \<longrightarrow> Pt s) \<and> ( \<not> b \<longrightarrow> Pf s)) (if b then m else m')"
|
||||||
by (clarsimp split: split_if)
|
by clarsimp
|
||||||
|
|
||||||
lemma not_empty_lsft:
|
lemma not_empty_lsft:
|
||||||
shows "not_empty (tcb_at t and valid_objs and separate_state) (lookup_slot_for_thread t cptr)"
|
shows "not_empty (tcb_at t and valid_objs and separate_state) (lookup_slot_for_thread t cptr)"
|
||||||
|
|
Loading…
Reference in New Issue