1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* A folding operation for separation algebra, to facilitate mappings with sharing 8 * 9 * Ordinarily when we map over a list, we require that the heap initially satisfies some 10 * precondition P for every element of the list, and we transform it into a heap which satisfies 11 * a post-condition Q for every element, i.e. 12 * 13 * \<And>* map P xs \<and>* ((\<And>* map Q xs) \<longrightarrow>* R)) 14 * 15 * However, what if we only have one copy of some resource required by P, and we want to share it 16 * between iterations? The above formulation is insufficient, as it would require a copy of the 17 * resource for every x \<in> xs. That's where sep_fold comes in. 18 * 19 * As you can see in the definition below, sep_fold nests each iteration's pre-condition under 20 * the post-conditions for previous iterations, which allows a shared resource to be passed down. 21 * 22 * For a real-world example of sep_fold usage, see the lemmas in SysInit.InitVSpace 23 * 24 * See also the Sep_Fold_Cancel lemmas and tactics, which automatically detect and cancel sharing 25 *) 26 27theory Sep_Fold 28imports 29 Separation_Algebra 30 Sep_ImpI 31begin 32 33definition 34 sep_fold :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 35 ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 36 ('a \<Rightarrow> bool) \<Rightarrow> 37 'b list \<Rightarrow> 38 ('a::sep_algebra \<Rightarrow> bool)" 39 where 40 "sep_fold P Q R xs \<equiv> foldr (\<lambda>x R. (P x \<and>* (Q x \<longrightarrow>* R))) xs R" 41 42notation sep_fold ("\<lparr>{_} \<and>* ({_} \<longrightarrow>* {_})\<rparr> _") 43 44lemma sep_map_sep_foldI: "(\<And>* map P xs \<and>* ((\<And>* map Q xs) \<longrightarrow>* R)) s \<Longrightarrow> sep_fold P Q R xs s" 45 apply (clarsimp simp: sep_fold_def) 46 apply (induct xs arbitrary: s; clarsimp) 47 apply (metis sep_add_zero sep_disj_zero sep_empty_zero sep_impl_def) 48 apply (clarsimp simp: sep_conj_ac) 49 apply (erule (1) sep_conj_impl) 50 apply (erule sep_conj_sep_impl) 51 apply (clarsimp simp: sep_conj_ac) 52 apply (drule meta_spec) 53 apply (erule meta_mp) 54 apply (subst (asm) sep_conj_assoc[symmetric]) 55 apply (erule sep_conj_sep_impl2) 56 apply (erule sep_conj_sep_impl2) 57 apply (rule sep_wand_collapse) 58 apply (rule sep_wand_match, assumption) 59 apply (erule sep_curry[rotated]) 60 apply (metis (no_types) sep_conj_sep_impl2 sep_conj_commute sep_wand_collapse) 61 done 62 63lemma sep_factor_foldI: 64 "(R' \<and>* (sep_fold P Q R xs)) s \<Longrightarrow> 65 sep_fold (\<lambda>x. R' \<and>* P x) (\<lambda>x. R' \<and>* Q x) (R' \<and>* R) xs s" 66 apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) 67 apply (clarsimp simp: sep_conj_ac) 68 apply (erule (1) sep_conj_impl) 69 apply (erule (1) sep_conj_impl) 70 apply (erule sep_conj_sep_impl) 71 apply (clarsimp simp: sep_conj_ac) 72 apply (drule (1) sep_conj_impl) 73 apply (subst (asm) sep_conj_commute, erule (1) sep_conj_sep_impl2) 74 by blast 75 76end 77