-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDaC_synthesis2.thy
314 lines (242 loc) · 10.1 KB
/
DaC_synthesis2.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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
(* ****************************************************************************************
Theory DaC_synthesis2.thy is part of a package supplementing
'Structured development of implementations for divide-and-conquer specifications'.
Copyright (c) 2023 M. Bortin
The package is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
For more details see the license agreement (LICENSE) you should have
received along with the package.
*************************************************************************************** *)
theory DaC_synthesis2
imports Preliminaries
begin
section "The divide-and-conquer tactic for another relator"
text "To illustrate how the design tactic may work also without support for
type constructor classes, this theory sets up the same synthesis rule
but for another relator instance which enables two recursive calls of
the synthesised function (e.g. the quicksort algorithm proceeds this way)."
datatype ('u, 'a) Relt = Empty | Dcmp 'u 'a 'a
definition Relt :: "'a \<rightarrow> 'b \<Rightarrow> ('v, 'a) Relt \<rightarrow> ('v, 'b) Relt"
where "Relt r = {(Empty, Empty)} \<union>
{(Dcmp x A A', Dcmp x B B') |x A B A' B'. (A, B) \<in> r \<and> (A', B') \<in> r}"
subsection "The relator axioms"
lemma Relt_mono:
"mono Relt"
unfolding Relt_def
by(rule monoI, fast)
lemma Relt_comp:
"Relt r \<diamondop> Relt s = Relt (r \<diamondop> s)"
unfolding Relt_def
by(rule equalityI, blast+)
lemma Relt_Id:
"Relt Id = Id"
unfolding Relt_def
by (clarsimp, rule set_eqI, smt (verit, best) IdE IdI Relt.exhaust insert_iff mem_Collect_eq)
lemma Relt_conv:
"(Relt r)\<^sup>\<circ> \<subseteq> Relt (r\<^sup>\<circ>)"
unfolding Relt_def
by blast
subsection "Derived properties"
lemma Relt_conv_eq :
"(Relt r)\<^sup>\<circ> = Relt (r\<^sup>\<circ>)"
by (metis Relt_conv converse_converse converse_subset_swap subset_antisym)
lemma Relt_simple :
"simple r \<Longrightarrow> simple(Relt r)"
by (metis (no_types, opaque_lifting) Relt_Id Relt_comp Relt_conv_eq Relt_mono monoD simple_def)
lemma Relt_entire :
"entire r \<Longrightarrow> entire(Relt r)"
by (metis Relt_Id Relt_comp Relt_conv_eq Relt_mono entire_def monoE)
lemma Relt_graph_of :
"\<exists>g. Relt(graph_of f) = graph_of g"
apply(subgoal_tac "simple (graph_of f)")
apply(subgoal_tac "entire (graph_of f)")
apply (simp add: Relt_entire Relt_simple mapping)
by(simp add: graph_of_def simple_def entire_def, fast)+
subsubsection "The induced endofunctor"
definition
"ReltF f = funct_of(Relt (graph_of f))"
lemma ReltF_eqs :
"ReltF f Empty = Empty"
"ReltF f (Dcmp x u v) = Dcmp x (f u) (f v)"
by(simp add: ReltF_def Relt_def funct_of_def graph_of_def)+
lemma ReltF :
"Relt(graph_of f) = graph_of(ReltF f)"
by (metis ReltF_def Relt_graph_of graph_of_funct_of)
text "the functor axioms:"
lemma ReltF1 :
"ReltF id = id"
by (metis ReltF_def Relt_Id graph_of_funct_of graph_of_id)
lemma ReltF2 :
"ReltF (g \<circ> f) = ReltF g \<circ> ReltF f"
by (metis ReltF Relt_comp graph_of_comp graph_of_funct_of)
text "Note that we actually just copy-and-paste the respective section
from the theory DaC-synthesis.thy"
definition
"DaC_scheme decompose compose = (\<lambda>r. decompose \<diamondop> Relt r \<diamondop> compose)"
lemma DaC_mono :
"decompose \<subseteq> decompose' \<Longrightarrow> compose \<subseteq> compose' \<Longrightarrow> r \<subseteq> r' \<Longrightarrow>
DaC_scheme decompose compose r \<subseteq> DaC_scheme decompose' compose' r'"
apply(simp add: DaC_scheme_def, erule relcomp_mono, erule relcomp_mono[rotated 1])
by(rule monoD[OF Relt_mono])
corollary DaC_mono' :
"mono (DaC_scheme decompose compose)"
by (simp add: DaC_mono monoI)
locale DaC_synthesis =
fixes \<alpha>\<^sub>1 :: "'a \<rightarrow> 'b"
and \<alpha>\<^sub>2 :: "'c \<rightarrow> 'd"
and spec :: "'b \<rightarrow> 'd"
and abs_dcmp :: "'b \<rightarrow> ('x, 'b) Relt"
and abs_cmp :: "('x, 'd) Relt \<rightarrow> 'd"
and dcmp :: "'a \<Rightarrow> ('x, 'a) Relt"
and cmp :: "('x, 'c) Relt \<Rightarrow> 'c"
assumes
DaC : "DaC_scheme abs_dcmp abs_cmp spec \<subseteq> spec"
and
decomp : "\<alpha>\<^sub>1\<^sup>\<circ> \<diamondop> (graph_of dcmp) \<subseteq> abs_dcmp \<diamondop> Relt (\<alpha>\<^sub>1\<^sup>\<circ>)"
and
comp : "(graph_of cmp) \<diamondop> \<alpha>\<^sub>2 \<subseteq> Relt \<alpha>\<^sub>2 \<diamondop> abs_cmp"
and
reduct : "Id \<subseteq> lfp(\<lambda>x. monotypeF (graph_of dcmp) (Relt x))"
begin
lemma DaC_simple :
"simple d \<Longrightarrow> simple c \<Longrightarrow> simple (lfp (DaC_scheme d c))"
apply(simp add: simple_def)
apply(subst rdiv_univ)
apply(rule lfp_lowerbound)
apply(subst rdiv_univ[THEN sym])
apply(subst lfp_unfold)
apply(rule monoI, rule DaC_mono, rule subset_refl, rule subset_refl, assumption)
apply(simp add: DaC_scheme_def)
apply(fold DaC_scheme_def)
apply(subst converse_relcomp)+
apply(subst Relt_conv_eq)
apply(subst O_assoc)+
apply(rule subset_trans)
apply(rule relcomp_mono[rotated 1])
apply(rule relcomp_mono[rotated 1])
apply(subst O_assoc[THEN sym])+
apply(rule relcomp_mono)
apply(erule relcomp_mono)
apply(rule subset_refl)+
apply simp
apply(rule subset_trans)
apply(rule relcomp_mono[rotated 1])
apply(subst O_assoc[THEN sym])
apply(rule relcomp_mono)
apply(subst Relt_comp)
apply(rule monoD[OF Relt_mono])
apply(rule rdiv_univ[THEN iffD2])
apply(rule subset_refl)+
apply(subst Relt_Id)
by simp
lemma DaC_entire :
"entire c \<Longrightarrow> entire(lfp(DaC_scheme (graph_of dcmp) c))"
apply(simp add: entire_def)
apply(rule subset_trans, rule reduct)
apply(rule_tac H="\<lambda>x. x \<diamondop> x\<^sup>\<circ>" in lfp_fusion)
apply(rule monoI, rule DaC_mono, simp+)
apply(rule allI)
apply(subgoal_tac "monotypeF (graph_of dcmp) (Relt (x \<diamondop> x\<^sup>\<circ>)) \<subseteq>
(monotypeF (graph_of dcmp) (Relt (x \<diamondop> x\<^sup>\<circ>)) \<diamondop> (graph_of dcmp)) \<diamondop> (graph_of dcmp)\<^sup>\<circ>")
apply(erule subset_trans)
apply(rule subset_trans)
apply(rule relcomp_mono)
apply(rule monotypeF1)
apply(rule subset_refl)
apply(subst Relt_comp[THEN sym])
apply(simp add: DaC_scheme_def)
apply(subst converse_relcomp)+
apply(subst Relt_conv_eq)
apply(subst O_assoc)+
apply(rule relcomp_mono, rule subset_refl)+
apply(rule subset_trans[rotated 1])
apply(subst O_assoc[THEN sym])+
apply(rule relcomp_mono)
apply(erule relcomp_mono)
apply(rule subset_refl)+
apply simp
apply(subst O_assoc)+
apply(rule subset_trans[rotated 1])
apply(rule_tac s'=Id in relcomp_mono)
apply(rule subset_refl)
apply(clarsimp simp: graph_of_def, fast)
by simp
lemma DaC_impl :
"\<alpha>\<^sub>1\<^sup>\<circ> \<diamondop> lfp(DaC_scheme (graph_of dcmp) (graph_of cmp)) \<diamondop> \<alpha>\<^sub>2 \<subseteq> spec"
apply(subst O_assoc[THEN sym])
apply(subst ldiv_univ)
apply(subst rdiv_univ)
apply(rule lfp_lowerbound)
apply(subst rdiv_univ[THEN sym])
apply(subst ldiv_univ[THEN sym])
apply(simp add: DaC_scheme_def)
apply(rule subset_trans[rotated 1])
apply(rule DaC)
apply(subst O_assoc[THEN sym])+
apply(rule subset_trans)
apply(rule relcomp_mono)
apply(rule relcomp_mono)
apply(rule relcomp_mono)
apply(rule decomp)
apply(rule subset_refl)+
apply(subst O_assoc)+
apply(rule subset_trans)
apply(rule relcomp_mono[rotated 1])
apply(rule relcomp_mono[rotated 1])
apply(rule relcomp_mono[rotated 1])
apply(rule comp)
apply(rule subset_refl)+
apply(simp add: DaC_scheme_def)
apply(rule relcomp_mono, rule subset_refl)
apply(subst O_assoc[THEN sym])+
apply(subst Relt_comp)+
apply(rule relcomp_mono[rotated 1], rule subset_refl)
apply(rule monoD[OF Relt_mono])
apply(rule subset_trans)
apply(rule relcomp_mono)
apply(rule rdiv_univ[THEN iffD2])
apply(rule subset_refl)+
apply(rule ldiv_univ[THEN iffD2])
by(rule subset_refl)
theorem DaC_synthesis :
"\<exists>\<phi>. lfp(DaC_scheme (graph_of dcmp) (graph_of cmp)) = graph_of \<phi> \<and>
\<alpha>\<^sub>1\<^sup>\<circ> \<diamondop> graph_of \<phi> \<diamondop> \<alpha>\<^sub>2 \<subseteq> spec"
apply(subgoal_tac "\<exists>\<phi>. lfp(DaC_scheme (graph_of dcmp) (graph_of cmp)) = graph_of \<phi>")
apply clarify
apply(rule exI, rule conjI, assumption)
apply(erule subst)
apply(rule DaC_impl)
apply(rule mapping)
apply(rule DaC_simple)
apply(clarsimp simp: simple_def graph_of_def)
apply(clarsimp simp: simple_def graph_of_def)
apply(rule DaC_entire)
apply(clarsimp simp: entire_def graph_of_def)
by fast
definition "dac = (THE \<phi>. lfp(DaC_scheme (graph_of dcmp) (graph_of cmp)) = graph_of \<phi>)"
lemma dac_lfp :
"graph_of dac = lfp(DaC_scheme (graph_of dcmp) (graph_of cmp))"
by (smt (verit, del_insts) DaC_synthesis dac_def graph_of_funct_of theI')
lemma dac_unq :
"lfp (DaC_scheme (graph_of dcmp) (graph_of cmp)) = graph_of f \<Longrightarrow> f = dac"
by(rule injD[OF graph_of_inj], simp add: dac_lfp)
lemma dac_unfold' :
"graph_of dac = (graph_of dcmp) \<diamondop> Relt(graph_of dac) \<diamondop> (graph_of cmp)"
apply(subst dac_lfp)+
apply(subst lfp_unfold, rule DaC_mono')
by(simp add: DaC_scheme_def)
lemma dac_unq_function' :
"(graph_of dcmp) \<diamondop> Relt(graph_of f) \<diamondop> (graph_of cmp) \<subseteq> graph_of f \<Longrightarrow> dac = f"
by (simp add: DaC_scheme_def dac_lfp graph_of_sub lfp_lowerbound)
lemma dac_unfold :
"dac = cmp \<circ> ReltF dac \<circ> dcmp"
by (metis ReltF dac_lfp dac_unfold' dac_unq graph_of_comp)
lemma dac_unq_function :
"f = cmp \<circ> ReltF f \<circ> dcmp \<Longrightarrow> f = dac"
by (metis ReltF dac_unq_function' graph_of_comp subset_refl)
lemma dac_impl :
"\<alpha>\<^sub>1\<^sup>\<circ> \<diamondop> (graph_of dac) \<diamondop> \<alpha>\<^sub>2 \<subseteq> spec"
by (simp add: DaC_impl dac_lfp)
end (* the synthesis tactic *)
end