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