Some changes for Lib, December '24 edition

lib/Lib.thy

@@ -2268,6 +2268,16 @@ lemma in_set_zip2:
   "(x, y) \<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
   by (erule in_set_zipE)
 
+lemma in_set_zipD:
+  "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys"
+  by (clarsimp simp add: set_zip)
+
+lemma set_map_fst_filter_zip:
+  "set (map fst (filter P (zip xs ys))) \<subseteq> set xs"
+  apply (induct xs, simp)
+  apply (case_tac ys; simp)
+  by (metis (mono_tags, lifting) image_Collect_subsetI insertI2 in_set_zipD)
+
 lemma map_zip_snd_take:
   "map (\<lambda>(x, y). f y) (zip xs ys) = map f (take (length xs) ys)"
   apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp)

lib/Monad_Lists.thy

@@ -512,6 +512,33 @@ lemma mapM_wp':
   apply simp
   done
 
+lemma mapM_gets_the_wp:
+  "\<lbrace>\<lambda>s. \<forall>vs. map (\<lambda>t. f t s) ts = map Some vs \<longrightarrow> P vs s\<rbrace>
+   mapM (gets_the \<circ> f) ts
+   \<lbrace>P\<rbrace>"
+  unfolding comp_def
+proof (induct ts arbitrary: P)
+  case Nil thus ?case by (wpsimp simp: mapM_Nil)
+next
+  case (Cons x xs) show ?case by (wpsimp simp: mapM_Cons wp: Cons)
+qed
+
+lemma mapM_gets_the_wp_nth:
+  "\<lbrace>\<lambda>s. \<forall>vs. (\<forall>i < length vs. f (ts ! i) s = Some (vs ! i)) \<longrightarrow> P vs s\<rbrace>
+   mapM (gets_the \<circ> f) ts
+   \<lbrace>P\<rbrace>"
+  apply (wpsimp wp: mapM_gets_the_wp)
+  by (simp add: map_equality_iff)
+
+lemma mapM_gets_the_sp:
+  "\<lbrace>P\<rbrace> mapM (gets_the \<circ> f) ts \<lbrace>\<lambda>rv s. P s \<and> map (\<lambda>t. f t s) ts = map Some rv\<rbrace>"
+  by (wpsimp wp: mapM_gets_the_wp simp: comp_def)
+
+lemma mapM_gets_the_sp_nth:
+  "\<lbrace>P\<rbrace> mapM (gets_the \<circ> f) ts \<lbrace>\<lambda>rv s. P s \<and> (\<forall>i < length rv. f (ts ! i) s = Some (rv ! i))\<rbrace>"
+  apply (wpsimp wp: mapM_gets_the_wp simp: comp_def)
+  by (simp add: map_equality_iff)
+
 lemma mapM_set:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>"

lib/Monads/reader_option/Reader_Option_Monad.thy

@@ -29,7 +29,7 @@ definition opt_map :: "('s,'a) lookup \<Rightarrow> ('a \<Rightarrow> 'b option)
   "f |> g \<equiv> \<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x"
 
 abbreviation opt_map_Some :: "('s \<rightharpoonup> 'a) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 's \<rightharpoonup> 'b" (infixl "||>" 54) where
-  "f ||> g \<equiv> f |> (Some \<circ> g)"
+  "f ||> g \<equiv> f |> (\<lambda>s. Some (g s))"
 
 lemmas opt_map_Some_def = opt_map_def
 
@@ -118,7 +118,7 @@ lemma opt_map_Some_foldr_upd:
 
 lemmas opt_map_foldr_upd_simps = opt_map_foldr_upd opt_map_Some_foldr_upd
 
-lemma opt_map_Some_comp[simp]:
+lemma opt_map_Some_comp:
   "f ||> g ||> h = f ||> h o g"
   by (fastforce simp: opt_map_def split: option.split)
 
@@ -143,10 +143,6 @@ lemma opt_map_zero_r[simp]:
   "f |> Map.empty = Map.empty"
   by (fastforce simp: opt_map_def split: option.split)
 
-lemma opt_map_Some_eta_fold:
-  "f |> (\<lambda>x. Some (g x)) = f ||> g"
-  by (simp add: o_def)
-
 lemma case_opt_map_distrib:
   "(\<lambda>s. case_option None g (f s)) |> h = (\<lambda>s. case_option None (g |> h) (f s))"
   by (fastforce simp: opt_map_def split: option.splits)

proof/access-control/Syscall_AC.thy

@@ -976,7 +976,7 @@ crunch_ignore (add: cap_swap_ext cap_move_ext cap_insert_ext create_cap_ext set_
 
 lemma zet_zip_contrapos:
   "fst t \<notin> set xs  \<Longrightarrow> t \<notin> set (zip xs ys)"
-  by (auto simp: set_zip_helper)
+  by (auto simp: in_set_zipD)
 
 lemma ct_active_update[simp]:
   "ct_active (s\<lparr>cdt := b\<rparr>) = ct_active s"

proof/crefine/AARCH64/Retype_C.thy

@@ -7301,7 +7301,7 @@ lemma ccorres_typ_region_bytes_dummy:
   apply (simp add: hrs_htd_update gsCNodes_typ_region_bytes
                    cnodes_retype_have_size_mono[where T=S]
                    tcb_ctes_typ_region_bytes[OF _ _ invs_pspace_aligned']
-                   pte_typ_region_bytes o_def)
+                   pte_typ_region_bytes)
   (* True for either version of config_ARM_PA_SIZE_BITS_40 with corresponding max vm level change *)
   apply (simp add: cmap_array_typ_region_bytes_triv invs_pspace_aligned' bit_simps
                    objBitsT_simps word_bits_def zero_ranges_are_zero_typ_region_bytes
@@ -8005,7 +8005,7 @@ crunch placeNewDataObject
   for ksArchState[wp]: "\<lambda>s. P (ksArchState s)"
   (simp: crunch_simps)
 
-lemma createObject_cnodes_have_size_pt[unfolded o_def]:
+lemma createObject_cnodes_have_size_pt:
   "\<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits newType userSize)
       \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsPTTypes (ksArchState s) ||> (\<lambda>pt_t. pt_bits pt_t - cte_level_bits))\<rbrace>
     createObject newType ptr userSize dev
@@ -8014,8 +8014,7 @@ lemma createObject_cnodes_have_size_pt[unfolded o_def]:
   apply (simp add: createObject_def)
   apply (rule hoare_pre)
    apply (wp mapM_x_wp' | wpc | simp add: createObjects_def AARCH64_H.createObject_def updatePTType_def)+
-  apply (cases newType, simp_all add: AARCH64_H.toAPIType_def o_def)
-   apply (rule conjI, clarsimp)+
+  apply (cases newType, simp_all add: AARCH64_H.toAPIType_def)
    apply clarsimp
   supply fun_upd_def[symmetric, simp del] fun_upd_apply[simp]
   apply (clarsimp simp: APIType_capBits_def cnodes_retype_have_size_def bit_simps cte_level_bits_def

proof/crefine/ARM_HYP/Arch_C.thy

@@ -2102,7 +2102,7 @@ lemma performPageInvocationMapPDE_ccorres:
           apply (simp add: typ_at_to_obj_at_arches[symmetric])
           apply ((wp mapM_x_storePDE_pde_mappings' mapM_x_wp' valid_pde_slots_lift2 | simp add: split_def)+)[2]
          apply (clarsimp simp: valid_pde_mapping'_def valid_pde_slots'2_def)
-         apply (drule set_zip_helper, clarsimp)
+         apply (drule in_set_zipD, clarsimp)
         apply clarsimp
         apply (simp add: typ_at_to_obj_at_arches)
         apply (frule bspec, erule hd_in_zip_set)

proof/invariant-abstract/Untyped_AI.thy

@@ -1380,12 +1380,6 @@ lemma retype_ret_valid_caps:
  done
 end
 
-(* FIXME: move to Lib *)
-lemma set_zip_helper:
-  "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys"
-  by (clarsimp simp add: set_zip)
-
-
 lemma ex_cte_cap_protects:
   "\<lbrakk> ex_cte_cap_wp_to P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s;
      descendants_range_in S p' s; untyped_children_in_mdb s; S\<subseteq> untyped_range (UntypedCap dev ptr bits idx);
@@ -3277,7 +3271,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs:
   apply (rule hoare_gen_asm)
   apply (subgoal_tac "set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)")
    prefer 2
-   apply (auto dest!: set_zip_helper)[1]
+   apply (auto dest!: in_set_zipD)[1]
   apply (induct ("zip crefs orefs"))
    apply (simp add: mapM_x_def sequence_x_def)
    apply wpsimp
@@ -3567,7 +3561,7 @@ lemma retype_region_post_retype_invs_folded:
 
 lemma tup_in_fst_image_set_zipD:
   "x \<in> fst ` set (zip xs ys) \<Longrightarrow> x \<in> set xs"
-  by (auto dest!: set_zip_helper)
+  by (auto dest!: in_set_zipD)
 
 lemma distinct_map_fst_zip:
   "distinct xs \<Longrightarrow> distinct (map fst (zip xs ys))"