From be04eb0b509167bdc2e498f8f21e5cf358c7f631 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Fri, 14 Jan 2022 09:50:46 +1100
Subject: [PATCH] isabelle2021-1: SepDSpec

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 proof/sep-capDL/Helpers_SD.thy    | 10 +++-------
 proof/sep-capDL/Separation_SD.thy |  2 --
 2 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/proof/sep-capDL/Helpers_SD.thy b/proof/sep-capDL/Helpers_SD.thy
index 8c01f3ba4..dbc1289b1 100644
--- a/proof/sep-capDL/Helpers_SD.thy
+++ b/proof/sep-capDL/Helpers_SD.thy
@@ -78,7 +78,7 @@ lemma restrict_map_comp' [simp]:
 
 lemma nat_list_not_UNIV [simp]:
   "set (xs::nat list) \<noteq> UNIV"
-  by (metis finite'_code(1) Cardinality.finite'_def infinite_UNIV_nat)
+  by (metis UNIV_I gt_ex leD maximum_ge)
 
 (***********************************
  * End of generic Isabelle lemmas. *
@@ -574,10 +574,6 @@ lemma ko_at_tcb_at:
 abbreviation
   "type_at T \<equiv> object_at (\<lambda>ob. object_type ob = T)"
 
-lemma length_sorted_list_of_set [simp]:
-  "finite A \<Longrightarrow> length (sorted_list_of_set A) = card A"
-  by (metis sorted_list_of_set distinct_card)
-
 lemma length_used_irq_list [simp]:
   "length (used_irq_list spec) = card (used_irqs spec)"
   by (clarsimp simp: used_irq_list_def)
@@ -849,13 +845,13 @@ lemma cap_has_object_update_cap_object [simp]:
 lemma cap_object_default_cap' [simp]:
   "\<lbrakk>\<not>is_untyped obj; \<not>is_irq_node obj\<rbrakk>
   \<Longrightarrow> cap_object (default_cap (object_type obj) {obj_id} sz dev) = obj_id"
-  by (clarsimp simp: default_cap_def  object_type_def is_untyped_def is_irq_node_def cap_object_simps
+  by (clarsimp simp: default_cap_def  object_type_def is_untyped_def is_irq_node_def
               split: cdl_object_type.splits cdl_object.splits)
 
 lemma cap_object_default_cap [simp]:
   "\<lbrakk>type \<noteq> UntypedType; type \<noteq> IRQNodeType\<rbrakk>
   \<Longrightarrow> cap_object (default_cap type {obj_id} sz dev) = obj_id"
-  by (clarsimp simp: default_cap_def  object_type_def is_untyped_def cap_object_simps
+  by (clarsimp simp: default_cap_def  object_type_def is_untyped_def
               split: cdl_object_type.splits cdl_object.splits)
 
 lemma cap_object_default_cap_frame:
diff --git a/proof/sep-capDL/Separation_SD.thy b/proof/sep-capDL/Separation_SD.thy
index 42026bf58..89fb386bb 100644
--- a/proof/sep-capDL/Separation_SD.thy
+++ b/proof/sep-capDL/Separation_SD.thy
@@ -296,8 +296,6 @@ lemma offset_slot':
   "\<lbrakk>slot < 2^radix\<rbrakk> \<Longrightarrow> offset slot radix = unat slot"
   by (clarsimp simp: offset_def Word.less_mask_eq)
 
-lemmas word_bits_def = Word_32.word_bits_def
-
 lemma offset_slot:
   "\<lbrakk>slot < 2^radix; radix < word_bits\<rbrakk> \<Longrightarrow> offset (of_nat slot) radix = slot"
   apply (clarsimp simp: offset_def)