adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Minor cleanup of proofs in the Take/Grant security model.

This commit is contained in:
Andrew Boyton 2014-07-22 14:36:53 +10:00
parent 798e891f1f
commit 36588c4359
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/take-grant/System_S.thy
View File

@ -214,7 +214,7 @@ definition
lemma takeOperation_def2:
"takeOperation e c\<^sub>1 c\<^sub>2 R s \<equiv>
s (e \<mapsto> Entity ({diminish R c\<^sub>2} \<union> direct_caps_of s e))"
by (rule eq_reflection, simp add: takeOperation_def caps_of_def)
by (clarsimp simp: takeOperation_def caps_of_def)
definition
grantOperation ::
@ -225,7 +225,7 @@ definition
lemma grantOperation_def2:
"grantOperation e c\<^sub>1 c\<^sub>2 R s \<equiv>
s (target c\<^sub>1 \<mapsto> Entity ( {diminish R c\<^sub>2} \<union> direct_caps_of s (target c\<^sub>1)))"
by (rule eq_reflection, simp add: grantOperation_def caps_of_def)
by (clarsimp simp: grantOperation_def caps_of_def)
definition
copyOperation ::