-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPowerset.thy
207 lines (154 loc) · 7.5 KB
/
Powerset.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
(* ****************************************************************************************
Theory Powerset.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 Powerset
imports DaC_synthesis
begin
text "The following theory contains an introductory example application of the
divide-and-conquer design tactic synthesising a function that computes a
list representation for the power set of a given finite set."
text "Note that the explicit typing merely caters better readability and
would be inferred by the type system if omitted."
definition pow :: "'a set \<rightarrow> 'a set set"
where "pow = {(S, P) |S P. \<forall>X. (X \<in> P) = (X \<subseteq> S)}"
definition decomp_spec :: "'a set \<rightarrow> ('a, 'a set) Relt"
where "decomp_spec = {({}, Empty)} \<union> {(G, Dcmp a (G - {a})) |G a. a \<in> G}"
definition comp_spec :: "('a, 'a set set) Relt \<rightarrow> 'a set set"
where "comp_spec = {(Empty, {{}})} \<union>
{(Dcmp a P, P \<union> {{a} \<union> A |A. A \<in> P}) |a P. True}"
definition decomp_impl :: "'a list \<Rightarrow> ('a, 'a list) Relt"
where "decomp_impl = (\<lambda>xs. case xs of
[] \<Rightarrow> Empty
| x # xs' \<Rightarrow> Dcmp x xs')"
definition comp_impl :: "('a, 'a list list) Relt \<Rightarrow> 'a list list"
where "comp_impl = (\<lambda>x. case x of
Empty \<Rightarrow> [[]]
| Dcmp a xxs \<Rightarrow> xxs @ map (\<lambda>xs. a#xs) xxs)"
text "Next we apply the divide-and-conquer tactic: "
interpretation powerset: DaC_synthesis
"{(xs, set xs) |xs. distinct xs}" (* \<alpha>\<^sub>1 *)
"{(xxs, {set xs |xs. xs \<in> set xxs}) |xxs. True}" (* \<alpha>\<^sub>2 *)
pow decomp_spec comp_spec decomp_impl comp_impl
apply(unfold_locales)
text "problem reduction principle:"
apply(clarsimp simp: DaC_scheme_def decomp_spec_def comp_spec_def Relt_def pow_def)
apply(elim disjE, clarsimp+)
apply (metis insert_Diff insert_mono subset_Diff_insert subset_insert_iff)
text "decomposition implementation:"
apply(clarsimp simp: decomp_spec_def decomp_impl_def graph_of_def Relt_def)
apply(case_tac xs, simp)
apply(rule_tac b=Empty in relcompI, clarsimp+)
apply(rename_tac x xs)
apply(rule_tac b="Dcmp x (set xs)" in relcompI)
apply simp+
text "composition implementation:"
apply(clarsimp simp: comp_spec_def comp_impl_def graph_of_def Relt_def)
apply(rename_tac xxs)
apply(case_tac xxs, simp)
apply(rule_tac b=Empty in relcompI, clarsimp+)
apply(rename_tac x xxs)
apply(rule_tac b="Dcmp x {set xs |xs. xs \<in> set xxs}" in relcompI)
apply fast
apply clarsimp
apply(rule set_eqI, rule iffI)
apply (clarsimp, metis imageE list.simps(15))
apply (clarsimp, metis imageI list.simps(15))
text "reductivity:"
apply clarsimp
apply(rename_tac xs)
apply(induct_tac xs rule: length_induct, clarsimp)
apply(rename_tac xs)
apply(subst lfp_unfold)
apply(rule monoI)
apply(rule monoD[OF monotypeF_mono])
apply(erule monoD[OF Relt_mono])
apply(subst singleton_eq)
apply(rule monotypeF_univ[THEN iffD1])
apply(subst graph_of_def, subst graph_of_def)
apply(clarsimp simp: decomp_impl_def)
apply(rename_tac xs)
apply(case_tac xs, simp)
apply(rule_tac b="Empty" in relcompI, simp, simp add: Relt_def)
apply clarsimp
apply(rename_tac x xs)
apply(rule_tac b="Dcmp x xs" in relcompI, simp)
apply(subst Relt_def, simp)
done
text "Deriving the recursive equations for the synthesised function:"
lemma syn_powerset_eqs[simp] :
"powerset.dac [] = [[]]"
"powerset.dac (x#xs) = (let xxs = powerset.dac xs in xxs @ map (\<lambda>xs. x#xs) xxs)"
by(subst powerset.dac_unfold, simp add: Let_def decomp_impl_def comp_impl_def ReltF_eqs)+
text "The correctness of the synthesised @{term powerset.dac} follows from the
implementation property @{thm powerset.dac_impl} :"
lemma syn_powerset_corr :
"distinct xs \<Longrightarrow> (X \<subseteq> set xs) = (\<exists>ys \<in> set(powerset.dac xs). set ys = X)"
apply(insert powerset.dac_impl)
apply(drule_tac c="(set xs, {set ys |ys. ys \<in> set(powerset.dac xs)})" in subsetD)
apply(rule_tac b=xs in relcompI, simp)
apply(rule_tac b="powerset.dac xs" in relcompI, simp add: graph_of_def)
apply simp
apply(clarsimp simp: pow_def)
by metis
text "Further effects of the restriction of inputs to distinct lists are
(a) no more list representations will be generated than needed:"
lemma syn_powerset_length' :
"length(powerset.dac xs) = 2^(length xs)"
by(induct xs, (simp add: Let_def)+)
lemma syn_powerset_length :
"distinct xs \<Longrightarrow> length(powerset.dac xs) = 2^(card(set xs))"
by (simp add: distinct_card syn_powerset_length')
text "and (b) each of the representations is in turn distinct:"
lemma syn_powerset_distinct :
"distinct xs \<Longrightarrow> \<forall>ys\<in>set(powerset.dac xs). distinct ys"
apply(induct xs, (clarsimp simp: Let_def)+)
apply(erule disjE, fast)
by (smt (verit, ccfv_SIG) distinct.simps(2) imageE subsetD syn_powerset_corr)
text "For computation of power set representations the synthesised function
can also be replaced by the tail-recursive version:"
fun pow_tr where
"pow_tr [] rs = rs" |
"pow_tr (x#xs) rs = pow_tr xs (rs @ map (\<lambda>xs. x#xs) rs)"
lemma pow_tr_app :
"pow_tr (xs @ ys) rs = pow_tr ys (pow_tr xs rs)"
by(induct xs arbitrary: rs, simp+)
lemma dac_pow_tr :
"powerset.dac (xs @ ys) = pow_tr (rev xs) (powerset.dac ys)"
by(induct xs arbitrary: ys, simp_all add: Let_def pow_tr_app)
corollary pow_tr :
"pow_tr xs [[]] = powerset.dac (rev xs)"
by (metis append_Nil2 dac_pow_tr rev_rev_ident syn_powerset_eqs(1))
text "The correctness of @{term pow_tr} now follows straight:"
lemma pow_tr_corr :
"distinct xs \<Longrightarrow> (X \<subseteq> set xs) = (\<exists>ys \<in> set(pow_tr xs [[]]). set ys = X)"
apply(subst pow_tr)
apply(subst syn_powerset_corr[THEN sym])
by simp+
lemma pow_tr_length :
"distinct xs \<Longrightarrow> length(pow_tr xs [[]]) = 2^(card(set xs))"
by(subst pow_tr, subst syn_powerset_length, simp+)
lemma pow_tr_distinct :
"distinct xs \<Longrightarrow> \<forall>ys\<in>set(pow_tr xs [[]]). distinct ys"
by(subst pow_tr, rule syn_powerset_distinct, simp)
text "We can ultimately lift the restriction of inputs to distinct lists as follows
(the function @{term remdups} removes all duplicates):"
definition "powerset_repr xs = pow_tr (remdups xs) [[]]"
lemma powerset_repr_corr :
"(X \<subseteq> set xs) = (\<exists>ys \<in> set(powerset_repr xs). set ys = X)"
by(unfold powerset_repr_def, subst pow_tr_corr[THEN sym], simp+)
lemma powerset_repr_length :
"length(powerset_repr xs) = 2^(card(set xs))"
by (simp add: pow_tr_length powerset_repr_def)
lemma powerset_repr_distinct :
"ys \<in> set(powerset_repr xs) \<Longrightarrow> distinct ys"
by(unfold powerset_repr_def, erule pow_tr_distinct[rule_format, rotated 1], simp)
text "so for instance: "
value "powerset_repr [(1::nat), 2, 3]"
end