Isabelle2018: TakeGrant
This commit is contained in:
parent
eea38b25c4
commit
bdb3c592b8
|
@ -274,10 +274,10 @@ lemma tgs_connected_comm_eq:
|
||||||
by (metis tgs_connected_comm)
|
by (metis tgs_connected_comm)
|
||||||
|
|
||||||
lemmas tgs_connected_trans =
|
lemmas tgs_connected_trans =
|
||||||
rtrancl_trans [where r="directly_tgs_connected s", simplified tgs_connected_def[symmetric]]
|
rtrancl_trans [where r="directly_tgs_connected s" for s, simplified tgs_connected_def[symmetric]]
|
||||||
|
|
||||||
lemmas directly_tgs_connected_rtrancl_into_rtrancl =
|
lemmas directly_tgs_connected_rtrancl_into_rtrancl =
|
||||||
rtrancl_into_rtrancl [where r="directly_tgs_connected s", simplified tgs_connected_def[symmetric]]
|
rtrancl_into_rtrancl [where r="directly_tgs_connected s" for s, simplified tgs_connected_def[symmetric]]
|
||||||
|
|
||||||
lemma take_caps_directly_tgs_connected:
|
lemma take_caps_directly_tgs_connected:
|
||||||
"\<lbrakk>c \<in> caps_of s e; Take \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c"
|
"\<lbrakk>c \<in> caps_of s e; Take \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c"
|
||||||
|
|
|
@ -18,7 +18,7 @@ lemma direct_caps_of_update [simp]:
|
||||||
by (rule ext, simp add: direct_caps_of_def split:option.splits)
|
by (rule ext, simp add: direct_caps_of_def split:option.splits)
|
||||||
|
|
||||||
lemma direct_caps_of_empty [simp]:
|
lemma direct_caps_of_empty [simp]:
|
||||||
"direct_caps_of empty = ( \<lambda> x. {})"
|
"direct_caps_of Map.empty = ( \<lambda> x. {})"
|
||||||
by (simp add: direct_caps_of_def fun_eq_iff)
|
by (simp add: direct_caps_of_def fun_eq_iff)
|
||||||
|
|
||||||
definition "id\<^sub>0 \<equiv> 0"
|
definition "id\<^sub>0 \<equiv> 0"
|
||||||
|
|
Loading…
Reference in New Issue