isabelle-2021: clib update

Mostly related to Word_Lib changes.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

lib/clib/CCorresLemmas.thy

@@ -112,9 +112,9 @@ lemma exec_handlers_Hoare_from_vcg_might_fail:
     \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # hs) Q A'"
   apply (clarsimp simp: exec_handlers_Hoare_def
              split del: if_split split: if_split_asm)
-   apply (erule exec_handlers.cases, simp_all)
-    apply (case_tac hsa, simp_all)
-     apply (erule exec_handlers.cases, simp_all)
+   apply (erule exec_handlers.cases; simp)
+    apply (cases hs; simp)
+     apply (erule exec_handlers.cases; simp)
     apply (frule exec_handlers_Cons_le, simp)
    apply (drule hoare_sound)
    apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def)
@@ -872,10 +872,11 @@ proof -
       apply (rule diff_Suc_less [OF lt0])
       done
   qed
-  thus ?thesis using lxs
-    apply (auto simp: init_xs_def dest!: spec[where x=Nil]
-                simp: j pn word_less_nat_alt neq_Nil_conv unat_word_ariths unat_of_nat push_mods
-            elim!: ccorres_guard_imp2)
+  thus ?thesis using lxs j pn
+    apply (auto simp: init_xs_def word_less_nat_alt neq_Nil_conv unat_word_ariths unat_of_nat push_mods
+                simp del: unsigned_of_nat
+                elim!: ccorres_guard_imp2
+                dest!: spec[where x=Nil])
     done
 qed
 
@@ -897,8 +898,7 @@ lemma ccorres_abstract_cslift:
   fixes p :: "'a :: c_type ptr"
   shows "(\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c) \<Longrightarrow>
   ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P ((f::'a \<Rightarrow> ('b::{type})) s) \<longrightarrow> s \<in> G' (f s)} \<inter> {s. P (f s)}) hs a c"
-  apply (erule ccorres_abstract_h_val)
-  done
+  by (fact ccorres_abstract_h_val)
 
 lemma ccorres_cond2:
   assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P  = (s' \<in> P') "

lib/clib/CTranslationNICTA.thy

@@ -7,7 +7,6 @@
 theory CTranslationNICTA
 imports
   "CParser.CTranslation"
-  "Word_Lib.Word_Lib"
 begin
 
 declare len_of_numeral_defs [simp del]

lib/clib/LemmaBucket_C.thy

@@ -23,9 +23,8 @@ lemma hrs_mem_f: "f (hrs_mem s) = hrs_mem (hrs_mem_update f s)"
   done
 
 lemma hrs_mem_heap_update:
-     "heap_update p v (hrs_mem s) = hrs_mem (hrs_mem_update (heap_update p v) s)"
-  apply (rule hrs_mem_f)
-  done
+  "heap_update p v (hrs_mem s) = hrs_mem (hrs_mem_update (heap_update p v) s)"
+  by (rule hrs_mem_f)
 
 lemma addr_card_wb:
   "addr_card = 2 ^ word_bits"
@@ -188,7 +187,7 @@ next
     apply (rule set_eqI)
     apply clarsimp
     apply (rename_tac w)
-    apply (case_tac w)
+    apply (case_tac w rule: word_nat_cases)
     apply (rename_tac m)
     apply (rule_tac x=m in exI)
     apply simp
@@ -210,10 +209,7 @@ lemma upto_intvl_eq':
     apply (subst field_simps [symmetric], rule word_plus_mono_right)
      apply simp
     apply assumption
-   apply (subst Word_Lemmas.of_nat_mono_maybe_le [symmetric])
-     apply simp
-    apply simp
-   apply simp
+   apply (rule of_nat_mono_maybe_le; simp)
   apply clarsimp
   apply (rule_tac x = "unat (xa - x)" in exI)
   apply simp
@@ -221,13 +217,8 @@ lemma upto_intvl_eq':
   apply (rule nat_diff_less)
    apply (subst (asm) word_le_nat_alt, erule order_le_less_trans)
    apply (subst add_diff_eq[symmetric], subst unat_plus_if')
-   apply (simp add: no_olen_add_nat)
-   apply (simp add: le_eq_less_or_eq)
-   apply (erule disjE)
-    apply (subst unat_minus_one)
-     apply (erule (1) of_nat_neq_0)
-    apply (simp add: unat_of_nat)
-   apply (erule ssubst, rule unat_lt2p)
+   apply (simp add: no_olen_add_nat le_eq_less_or_eq)
+   apply (metis gt0_iff_gem1 unat_less_helper unat_ucast_less_no_overflow unsigned_0 unsigned_less)
   apply (simp add: word_le_nat_alt)
   done
 
@@ -275,8 +266,8 @@ next
 qed
 
 lemma intvl_nowrap:
-  fixes x :: "'a::len word"
-  shows "\<lbrakk>y \<noteq> 0; unat y + z \<le> 2 ^ len_of TYPE('a)\<rbrakk> \<Longrightarrow> x \<notin> {x + y ..+ z}"
+  "\<lbrakk>y \<noteq> 0; unat y + z \<le> 2 ^ len_of TYPE('a)\<rbrakk> \<Longrightarrow> x \<notin> {x + y ..+ z}" for x :: "'a::len word"
+  supply unsigned_of_nat[simp del]
   apply clarsimp
   apply (drule intvlD)
   apply clarsimp
@@ -391,7 +382,7 @@ proof (rule disjointI, rule notI)
 
   also have "\<dots> \<le> c" by (rule abc)
   also have "\<dots> \<le> c + of_nat ky" using cld dlt ky
-    by - (rule word_random [OF _ iffD1 [OF Word_Lemmas.of_nat_mono_maybe_le]], simp+ )
+    by (meson less_imp_le of_nat_mono_maybe word_random)
   finally show False using ac by simp
 qed
 
@@ -413,6 +404,7 @@ lemma intvl_off_disj:
   and    zoff: "z + off < 2 ^ word_bits"
   shows   "{x ..+ y} \<inter> {x + of_nat off ..+ z} = {}"
   using ylt zoff
+  supply unsigned_of_nat[simp del]
   apply (cases "off = 0")
    apply simp
   apply (rule contrapos_pp [OF TrueI])
@@ -461,9 +453,7 @@ qed
 
 lemma typ_slice_t_self:
   "td \<in> fst ` set (typ_slice_t td m)"
-  apply (cases td)
-  apply (simp split: if_split)
-  done
+  by (fact ladder_set_self)
 
 lemma drop_heap_list_le2:
   "heap_list h n (x + of_nat k)
@@ -777,6 +767,7 @@ proof -
          \<Longrightarrow> unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: addr))
                  = x * size_of TYPE('a) + k"
     using size
+    supply unsigned_of_nat[simp del]
     apply (case_tac "size_of TYPE('a)", simp_all)
     apply (case_tac "CARD('b)", simp_all)
     apply (subst unat_add_lem[THEN iffD1])
@@ -881,6 +872,7 @@ lemma typ_slice_t_array:
 lemma h_t_valid_Array_element':
   "\<lbrakk> htd \<Turnstile>\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); coerce \<or> n < CARD('b) \<rbrakk>
     \<Longrightarrow> htd \<Turnstile>\<^sub>t array_ptr_index p coerce n"
+  supply unsigned_of_nat[simp del]
   apply (clarsimp simp only: h_t_valid_def valid_footprint_def Let_def
                              c_guard_def c_null_guard_def)
   apply (subgoal_tac "\<exists>offs. array_ptr_index p coerce n = ptr_add (ptr_coerce p) (of_nat offs)
@@ -958,10 +950,7 @@ lemma ptr_safe_Array_element:
 
 lemma from_bytes_eq:
   "from_bytes [x] = x"
-  apply (clarsimp simp:from_bytes_def update_ti_t_def typ_info_word)
-  apply (simp add:word_rcat_def)
-  apply (simp add:bin_rcat_def)
-  by (metis len8 word_of_int_uint word_ubin.Abs_norm)
+  by (clarsimp simp:from_bytes_def update_ti_t_def typ_info_word word_rcat_def)
 
 lemma bytes_disjoint:"(x::('a::c_type) ptr) \<noteq> y \<Longrightarrow> {ptr_val x + a ..+ 1} \<inter> {ptr_val y + a ..+ 1} = {}"
   by (clarsimp simp:intvl_def)
@@ -1076,7 +1065,7 @@ lemma neq_imp_bytes_disjoint:
     apply (subgoal_tac "(ptr_val x + j && ~~ mask n) = (ptr_val y + i && ~~ mask n)")
      apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt)
      apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt)
-     apply (clarsimp simp: is_aligned_neg_mask_eq)
+     apply clarsimp
     apply simp
    apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def)
   apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def)
@@ -1206,7 +1195,7 @@ proof (rule classical)
       by blast
 
   then obtain k' where mv: "mv = ptr_val p' + of_nat k'" and klt: "k' < size_td (typ_info_t TYPE('b))"
-    by (clarsimp dest!: intvlD simp: size_of_def typ_uinfo_size)
+    by (clarsimp dest!: intvlD simp: size_of_def)
 
   let ?mv = "ptr_val p' + of_nat k'"
 

lib/clib/SimplRewrite.thy

@@ -28,7 +28,7 @@ where
 
 lemma add_statefn_id1:
   "add_statefn id x = x"
-  by (induct x, simp_all add: inv_id[simplified id_def])
+  by (induct x) auto
 
 lemma add_statefn_id[simp]:
   "add_statefn id = id"