From ad6bd61332719a306fc058fbfc3d0d535a52a24c Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@nicta.com.au>
Date: Wed, 25 Jan 2017 18:26:19 +0100
Subject: [PATCH] invariant-abstract: remove unused lemma

---
 .../ARM/ArchFinalise_AI.thy                   | 45 -------------------
 1 file changed, 45 deletions(-)

diff --git a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy
index 3a065d776..072091e7c 100644
--- a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy
+++ b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy
@@ -1071,41 +1071,6 @@ lemma pd_shifting_global_refs:
   apply simp
   done
 
-lemma mapM_x_store_pde_InvalidPDE_empty:
-  "\<lbrace>(invs and  (\<lambda>s. word \<notin> global_refs s)) and K(is_aligned word pd_bits)\<rbrace>
-    mapM_x (swp store_pde InvalidPDE)
-           (map (\<lambda>a. (a << 2) + word) [0.e.(kernel_base >> 20) - 1])
-   \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (rule hoare_post_imp)
-   apply (erule obj_at_empty_tableI)
-  apply (wp hoare_vcg_conj_lift)
-    apply (rule mapM_x_swp_store_pde_invs_unmap)
-   apply (simp add: mapM_x_map)
-   apply (rule hoare_strengthen_post)
-    apply (rule mapM_x_accumulate_checks[OF store_pde_pde_wp_at])
-    defer
-    apply (rule allI)
-    apply (erule_tac x="ucast x" in ballE)
-     apply (rule impI)
-     apply (frule_tac pd="word" and ae="x" in pd_shifting_again3)
-     apply (frule_tac pd="word" and ae="x" in pd_shifting_again5)
-      apply ((simp add: kernel_mapping_slots_def kernel_base_def)+)[3]
-    apply (subst word_not_le)
-    apply (subst (asm) word_not_le)
-    apply (cut_tac x="ucast x" and y="kernel_base >> 20" in le_m1_iff_lt)
-    apply clarsimp
-    apply (simp add: le_m1_iff_lt word_less_nat_alt unat_ucast)
-    apply (simp add: pde_ref_def)
-   apply (rule conjI, rule allI, rule impI)
-    apply (rule pd_shifting_kernel_mapping_slots)
-     apply simp+
-   apply (rule allI, rule impI)
-   apply (rule pd_shifting_global_refs)
-     apply simp+
-  apply (wp store_pde_pde_wp_at2)
-  done
-
 lemma word_aligned_pt_slots:
   "\<lbrakk>is_aligned word pt_bits;
     x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk>
@@ -1243,16 +1208,6 @@ lemma store_pde_arch_objs_invalid:
   apply (simp add: pde_ref_def)
   done
 
-lemma mapM_x_store_pde_InvalidPDE_empty2:
-  "\<lbrace>invs and (\<lambda>s. word \<notin> global_refs s) and K (is_aligned word pd_bits) and K (slots = (map (\<lambda>a. (a << 2) + word) [0.e.(kernel_base >> 20) - 1])) \<rbrace>
-  mapM_x (\<lambda>x. store_pde x InvalidPDE) slots
-  \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply simp
-  apply (wp mapM_x_store_pde_InvalidPDE_empty [unfolded swp_def])
-  apply simp
-  done
-
 crunch valid_cap: invalidate_tlb_by_asid "valid_cap cap"
 crunch inv: page_table_mapped "P"
 crunch valid_objs[wp]: invalidate_tlb_by_asid "valid_objs"