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

arm AInvs: add more valid_global_objs and valid_global_vspace_mappings lemmas (in BCorres2_AI)

This commit is contained in:
Miki Tanaka 2017-05-25 21:49:45 +10:00 committed by Alejandro Gomez-Londono
parent 18a7a76715
commit 93eed88af7
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/invariant-abstract/BCorres2_AI.thy
View File

@ -172,6 +172,10 @@ lemma valid_vspace_objs[wp]: "I valid_vspace_objs" by (rule lift_inv,simp)
lemma valid_arch_caps[wp]: "I valid_arch_caps" by (rule lift_inv,simp)
lemma valid_global_objs[wp]: "I valid_global_objs" by (rule lift_inv,simp)
lemma valid_global_vspace_mappings[wp]: "I valid_global_vspace_mappings" by (rule lift_inv,simp)
lemma valid_kernel_mappings[wp]: "I valid_kernel_mappings" by (rule lift_inv,simp)
lemma equal_kernel_mappings[wp]: "I equal_kernel_mappings" by (rule lift_inv,simp)