author | Rene Thiemann <rene.thiemann@uibk.ac.at> |
Fri, 17 Apr 2015 11:52:36 +0200 | |
changeset 60112 | 3eab4acaa035 |
parent 58889 | 5b7a9633cfa8 |
child 61169 | 4de9ff3ea29a |
permissions | -rw-r--r-- |
53538 | 1 |
(* Title: HOL/ex/Adhoc_Overloading_Examples.thy |
2 |
Author: Christian Sternagel |
|
52894 | 3 |
*) |
4 |
||
58889 | 5 |
section {* Ad Hoc Overloading *} |
52894 | 6 |
|
7 |
theory Adhoc_Overloading_Examples |
|
8 |
imports |
|
9 |
Main |
|
10 |
"~~/src/Tools/Adhoc_Overloading" |
|
11 |
"~~/src/HOL/Library/Infinite_Set" |
|
12 |
begin |
|
13 |
||
14 |
text {*Adhoc overloading allows to overload a constant depending on |
|
15 |
its type. Typically this involves to introduce an uninterpreted |
|
16 |
constant (used for input and output) and then add some variants (used |
|
17 |
internally).*} |
|
18 |
||
19 |
subsection {* Plain Ad Hoc Overloading *} |
|
20 |
||
21 |
text {*Consider the type of first-order terms.*} |
|
58310 | 22 |
datatype ('a, 'b) "term" = |
52894 | 23 |
Var 'b | |
24 |
Fun 'a "('a, 'b) term list" |
|
25 |
||
26 |
text {*The set of variables of a term might be computed as follows.*} |
|
27 |
fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where |
|
28 |
"term_vars (Var x) = {x}" | |
|
29 |
"term_vars (Fun f ts) = \<Union>set (map term_vars ts)" |
|
30 |
||
31 |
text {*However, also for \emph{rules} (i.e., pairs of terms) and term |
|
32 |
rewrite systems (i.e., sets of rules), the set of variables makes |
|
33 |
sense. Thus we introduce an unspecified constant @{text vars}.*} |
|
34 |
||
35 |
consts vars :: "'a \<Rightarrow> 'b set" |
|
36 |
||
37 |
text {*Which is then overloaded with variants for terms, rules, and TRSs.*} |
|
38 |
adhoc_overloading |
|
39 |
vars term_vars |
|
40 |
||
41 |
value "vars (Fun ''f'' [Var 0, Var 1])" |
|
42 |
||
43 |
fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where |
|
44 |
"rule_vars (l, r) = vars l \<union> vars r" |
|
45 |
||
46 |
adhoc_overloading |
|
47 |
vars rule_vars |
|
48 |
||
49 |
value "vars (Var 1, Var 0)" |
|
50 |
||
51 |
definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where |
|
52 |
"trs_vars R = \<Union>(rule_vars ` R)" |
|
53 |
||
54 |
adhoc_overloading |
|
55 |
vars trs_vars |
|
56 |
||
57 |
value "vars {(Var 1, Var 0)}" |
|
58 |
||
59 |
text {*Sometimes it is necessary to add explicit type constraints |
|
60 |
before a variant can be determined.*} |
|
61 |
(*value "vars R" (*has multiple instances*)*) |
|
62 |
value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)" |
|
63 |
||
64 |
text {*It is also possible to remove variants.*} |
|
65 |
no_adhoc_overloading |
|
66 |
vars term_vars rule_vars |
|
67 |
||
68 |
(*value "vars (Var 1)" (*does not have an instance*)*) |
|
69 |
||
70 |
text {*As stated earlier, the overloaded constant is only used for |
|
71 |
input and output. Internally, always a variant is used, as can be |
|
72 |
observed by the configuration option @{text show_variants}.*} |
|
73 |
||
74 |
adhoc_overloading |
|
75 |
vars term_vars |
|
76 |
||
77 |
declare [[show_variants]] |
|
78 |
||
79 |
term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*) |
|
80 |
||
81 |
||
82 |
subsection {* Adhoc Overloading inside Locales *} |
|
83 |
||
84 |
text {*As example we use permutations that are parametrized over an |
|
85 |
atom type @{typ "'a"}.*} |
|
86 |
||
87 |
definition perms :: "('a \<Rightarrow> 'a) set" where |
|
88 |
"perms = {f. bij f \<and> finite {x. f x \<noteq> x}}" |
|
89 |
||
90 |
typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set" |
|
91 |
by (default) (auto simp: perms_def) |
|
92 |
||
93 |
text {*First we need some auxiliary lemmas.*} |
|
94 |
lemma permsI [Pure.intro]: |
|
95 |
assumes "bij f" and "MOST x. f x = x" |
|
96 |
shows "f \<in> perms" |
|
97 |
using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg) |
|
98 |
||
99 |
lemma perms_imp_bij: |
|
100 |
"f \<in> perms \<Longrightarrow> bij f" |
|
101 |
by (simp add: perms_def) |
|
102 |
||
103 |
lemma perms_imp_MOST_eq: |
|
104 |
"f \<in> perms \<Longrightarrow> MOST x. f x = x" |
|
105 |
by (simp add: perms_def) (metis MOST_iff_finiteNeg) |
|
106 |
||
107 |
lemma id_perms [simp]: |
|
108 |
"id \<in> perms" |
|
109 |
"(\<lambda>x. x) \<in> perms" |
|
110 |
by (auto simp: perms_def bij_def) |
|
111 |
||
112 |
lemma perms_comp [simp]: |
|
113 |
assumes f: "f \<in> perms" and g: "g \<in> perms" |
|
114 |
shows "(f \<circ> g) \<in> perms" |
|
115 |
apply (intro permsI bij_comp) |
|
116 |
apply (rule perms_imp_bij [OF g]) |
|
117 |
apply (rule perms_imp_bij [OF f]) |
|
118 |
apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]]) |
|
119 |
apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]]) |
|
120 |
by simp |
|
121 |
||
122 |
lemma perms_inv: |
|
123 |
assumes f: "f \<in> perms" |
|
124 |
shows "inv f \<in> perms" |
|
125 |
apply (rule permsI) |
|
126 |
apply (rule bij_imp_bij_inv) |
|
127 |
apply (rule perms_imp_bij [OF f]) |
|
128 |
apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]]) |
|
129 |
apply (erule subst, rule inv_f_f) |
|
57507 | 130 |
apply (rule bij_is_inj [OF perms_imp_bij [OF f]]) |
131 |
done |
|
52894 | 132 |
|
133 |
lemma bij_Rep_perm: "bij (Rep_perm p)" |
|
134 |
using Rep_perm [of p] unfolding perms_def by simp |
|
135 |
||
136 |
instantiation perm :: (type) group_add |
|
137 |
begin |
|
138 |
||
139 |
definition "0 = Abs_perm id" |
|
140 |
definition "- p = Abs_perm (inv (Rep_perm p))" |
|
141 |
definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)" |
|
142 |
definition "(p1::'a perm) - p2 = p1 + - p2" |
|
143 |
||
144 |
lemma Rep_perm_0: "Rep_perm 0 = id" |
|
145 |
unfolding zero_perm_def by (simp add: Abs_perm_inverse) |
|
146 |
||
147 |
lemma Rep_perm_add: |
|
148 |
"Rep_perm (p1 + p2) = Rep_perm p1 \<circ> Rep_perm p2" |
|
149 |
unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm) |
|
150 |
||
151 |
lemma Rep_perm_uminus: |
|
152 |
"Rep_perm (- p) = inv (Rep_perm p)" |
|
153 |
unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm) |
|
154 |
||
155 |
instance |
|
156 |
apply default |
|
157 |
unfolding Rep_perm_inject [symmetric] |
|
158 |
unfolding minus_perm_def |
|
159 |
unfolding Rep_perm_add |
|
160 |
unfolding Rep_perm_uminus |
|
161 |
unfolding Rep_perm_0 |
|
162 |
by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) |
|
163 |
||
164 |
end |
|
165 |
||
166 |
lemmas Rep_perm_simps = |
|
167 |
Rep_perm_0 |
|
168 |
Rep_perm_add |
|
169 |
Rep_perm_uminus |
|
170 |
||
171 |
||
172 |
section {* Permutation Types *} |
|
173 |
||
174 |
text {*We want to be able to apply permutations to arbitrary types. To |
|
175 |
this end we introduce a constant @{text PERMUTE} together with |
|
176 |
convenient infix syntax.*} |
|
177 |
||
178 |
consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75) |
|
179 |
||
180 |
text {*Then we add a locale for types @{typ 'b} that support |
|
181 |
appliciation of permutations.*} |
|
182 |
locale permute = |
|
183 |
fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" |
|
184 |
assumes permute_zero [simp]: "permute 0 x = x" |
|
185 |
and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)" |
|
186 |
begin |
|
187 |
||
188 |
adhoc_overloading |
|
189 |
PERMUTE permute |
|
190 |
||
191 |
end |
|
192 |
||
193 |
text {*Permuting atoms.*} |
|
194 |
definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
195 |
"permute_atom p a = (Rep_perm p) a" |
|
196 |
||
197 |
adhoc_overloading |
|
198 |
PERMUTE permute_atom |
|
199 |
||
200 |
interpretation atom_permute: permute permute_atom |
|
201 |
by (default) (simp add: permute_atom_def Rep_perm_simps)+ |
|
202 |
||
203 |
text {*Permuting permutations.*} |
|
204 |
definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where |
|
205 |
"permute_perm p q = p + q - p" |
|
206 |
||
207 |
adhoc_overloading |
|
208 |
PERMUTE permute_perm |
|
209 |
||
210 |
interpretation perm_permute: permute permute_perm |
|
57507 | 211 |
apply default |
212 |
unfolding permute_perm_def |
|
213 |
apply simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57507
diff
changeset
|
214 |
apply (simp only: diff_conv_add_uminus minus_add add.assoc) |
57507 | 215 |
done |
52894 | 216 |
|
217 |
text {*Permuting functions.*} |
|
218 |
locale fun_permute = |
|
219 |
dom: permute perm1 + ran: permute perm2 |
|
220 |
for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" |
|
221 |
and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c" |
|
222 |
begin |
|
223 |
||
224 |
adhoc_overloading |
|
225 |
PERMUTE perm1 perm2 |
|
226 |
||
227 |
definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where |
|
228 |
"permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))" |
|
229 |
||
230 |
adhoc_overloading |
|
231 |
PERMUTE permute_fun |
|
232 |
||
233 |
end |
|
234 |
||
235 |
sublocale fun_permute \<subseteq> permute permute_fun |
|
236 |
by (unfold_locales, auto simp: permute_fun_def) |
|
237 |
(metis dom.permute_plus minus_add) |
|
238 |
||
239 |
lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0" |
|
240 |
unfolding permute_atom_def |
|
241 |
by (metis Rep_perm_0 id_apply zero_perm_def) |
|
242 |
||
243 |
interpretation atom_fun_permute: fun_permute permute_atom permute_atom |
|
244 |
by (unfold_locales) |
|
245 |
||
246 |
adhoc_overloading |
|
247 |
PERMUTE atom_fun_permute.permute_fun |
|
248 |
||
249 |
lemma "(Abs_perm id :: 'a perm) \<bullet> id = id" |
|
250 |
unfolding atom_fun_permute.permute_fun_def |
|
251 |
unfolding permute_atom_def |
|
252 |
by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def) |
|
253 |
||
254 |
end |
|
255 |