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