1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(* Lemmas and automation for automatically cancelling shared parts of the heap predicate
8 * in a sep_fold
9 *)
10
11theory Sep_Fold_Cancel
12imports
13  Sep_Algebra_L4v
14  Sep_Forward
15begin
16
17lemma sep_fold_cong1: "(\<And>x s. P x s = P' x s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P' Q R xs s"
18  apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def)
19  apply (erule sep_conj_impl, fastforce)
20  apply (sep_cancel, sep_mp)
21  by (clarsimp)
22
23lemma sep_fold_cong2: "(\<And>x s. Q x s = Q' x s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P Q' R xs s"
24  apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def)
25  apply (erule sep_conj_impl, fastforce)
26  apply (sep_cancel)
27  apply (sep_drule (direct) sep_mp_gen)
28  by (clarsimp)
29
30lemma sep_fold_cong3: "(\<And> s. R s = R' s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P Q R' xs s"
31  apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def)
32  apply (erule sep_conj_impl, fastforce)
33  apply (sep_cancel)
34  apply (sep_drule (direct) sep_mp_gen)
35  by (clarsimp)
36
37lemma sep_fold_strengthen_final:
38  "\<lbrakk>\<And>s. R s \<Longrightarrow> R' s;
39    \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s\<rbrakk>
40   \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> xs s"
41  apply (induct xs arbitrary: s)
42   apply (clarsimp simp: sep_fold_def)
43  apply (clarsimp simp: sep_fold_def)
44  apply (sep_cancel)+
45  apply (sep_mp)
46  apply (clarsimp)
47  done
48
49lemma sep_factor_foldI__:
50  "(\<And>* map P xs \<and>* foldr (\<lambda>x R. Q x \<longrightarrow>* R) xs R) s \<Longrightarrow> sep_fold P Q R xs s"
51  apply (clarsimp simp: sep_fold_def)
52  apply (induct xs arbitrary: s; clarsimp)
53  apply sep_cancel+
54  apply sep_mp
55  apply (clarsimp simp: sep_conj_ac)
56  done
57
58lemma sep_factor_foldI_:
59  "(\<And>* map (\<lambda>_. I) xs \<and>* sep_fold P Q R xs) s \<Longrightarrow> sep_fold (\<lambda>x. I \<and>* P x) Q R xs s"
60  apply (induct xs arbitrary: s)
61   apply (clarsimp simp: sep_fold_def)
62  apply (clarsimp simp: sep_fold_def)
63  apply (sep_cancel+, clarsimp, sep_mp)
64  apply (clarsimp simp: sep_conj_ac)
65  done
66
67lemma sep_factor_foldI':
68  "(I \<and>* (sep_fold P Q (I \<longrightarrow>* R) xs)) s \<Longrightarrow> sep_fold (\<lambda>x. I \<and>* P x) (\<lambda>x. I \<and>* Q x) R xs s"
69  apply (induct xs arbitrary:s; clarsimp simp: sep_fold_def)
70   apply (sep_solve)
71  apply (sep_cancel)+
72  apply (sep_mp)
73  apply (clarsimp simp: sep_conj_ac)
74  done
75
76lemma sep_factor_foldI'':
77  "(\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s) \<Longrightarrow>
78   precise R' \<Longrightarrow>
79   (R' \<and>* sep_fold P Q (R' -* R) xs) s \<Longrightarrow>
80   sep_fold (\<lambda>x. R' \<and>* P x) (\<lambda>x. R' \<and>* Q x) R xs s"
81  apply (induct xs arbitrary:s; clarsimp simp: sep_fold_def)
82   apply (erule septract_mp[where R'=R'])
83    apply (assumption)+
84  apply (clarsimp simp: sep_conj_ac)
85  apply (sep_cancel)+
86  apply (sep_mp)
87  by (clarsimp simp: sep_conj_ac)
88
89ML \<open>
90 fun sep_fold_tactic ctxt =
91     rotator' ctxt (resolve_tac ctxt [@{thm sep_fold_cong2 }])
92                   (resolve_tac ctxt [@{thm sep_factor_foldI' }]) |>
93     rotator' ctxt (resolve_tac ctxt [@{thm sep_fold_cong1 }]);
94\<close>
95
96method_setup sep_fold_cancel_inner =
97  \<open>Scan.succeed (SIMPLE_METHOD' o sep_fold_tactic)\<close> \<open>Simple elimination of conjuncts\<close>
98
99(* Cancels out shared resources according to the rule sep_factor_foldI' *)
100
101lemma sep_map_set_sep_foldI:
102  "distinct xs \<Longrightarrow>
103   (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow>
104   \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s"
105  apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def)
106   apply (sep_solve)
107  apply (sep_cancel)+
108  apply (sep_mp)
109  apply (clarsimp simp: sep_conj_ac)
110  done
111
112lemma sep_fold_pure: "P \<Longrightarrow> sep_fold P' Q R xs s \<Longrightarrow> sep_fold (\<lambda>x s. P \<and> P' x s) Q R xs s "
113  by (clarsimp simp: sep_fold_def)
114
115lemma sep_fold_pure':
116  "sep_fold P' Q R xs s \<Longrightarrow>
117   (\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow>
118   sep_fold (\<lambda>x s. P x \<and> P' x s) Q R xs s "
119  apply (clarsimp simp: sep_fold_def)
120  apply (induct xs arbitrary: s; clarsimp)
121  apply (sep_cancel)+
122  apply (sep_mp)
123  apply (clarsimp)
124  done
125
126lemma sep_fold_pure'':
127  "sep_fold P' Q R xs s \<Longrightarrow>
128   (\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow>
129   sep_fold (\<lambda>x s. P' x s \<and> P x ) Q R xs s "
130  apply (clarsimp simp: sep_fold_def)
131  apply (induct xs arbitrary: s; clarsimp)
132  apply (sep_cancel)+
133  apply (sep_mp)
134  apply (clarsimp)
135  done
136
137method sep_fold_cancel = (
138  sep_flatten?,
139  ((rule sep_fold_pure' sep_fold_pure'')+)?,
140  (sep_fold_cancel_inner, sep_cancel, sep_flatten?)+
141)
142
143end
144