From 93eed88af7bce893cdf3ef5cc1521d28fdecc4e4 Mon Sep 17 00:00:00 2001 From: Miki Tanaka Date: Thu, 25 May 2017 21:49:45 +1000 Subject: [PATCH] arm AInvs: add more valid_global_objs and valid_global_vspace_mappings lemmas (in BCorres2_AI) --- proof/invariant-abstract/BCorres2_AI.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/proof/invariant-abstract/BCorres2_AI.thy b/proof/invariant-abstract/BCorres2_AI.thy index 805887d91..c493239e4 100644 --- a/proof/invariant-abstract/BCorres2_AI.thy +++ b/proof/invariant-abstract/BCorres2_AI.thy @@ -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)