1 (* Title: HOL/Examples/Adhoc_Overloading_Examples.thy |
|
2 Author: Christian Sternagel |
|
3 *) |
|
4 |
|
5 section \<open>Ad Hoc Overloading\<close> |
|
6 |
|
7 theory Adhoc_Overloading_Examples |
|
8 imports |
|
9 Main |
|
10 "HOL-Library.Infinite_Set" |
|
11 "HOL-Library.Adhoc_Overloading" |
|
12 begin |
|
13 |
|
14 text \<open>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).\<close> |
|
18 |
|
19 subsection \<open>Plain Ad Hoc Overloading\<close> |
|
20 |
|
21 text \<open>Consider the type of first-order terms.\<close> |
|
22 datatype ('a, 'b) "term" = |
|
23 Var 'b | |
|
24 Fun 'a "('a, 'b) term list" |
|
25 |
|
26 text \<open>The set of variables of a term might be computed as follows.\<close> |
|
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 \<open>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 \<open>vars\<close>.\<close> |
|
34 |
|
35 consts vars :: "'a \<Rightarrow> 'b set" |
|
36 |
|
37 text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close> |
|
38 adhoc_overloading |
|
39 vars term_vars |
|
40 |
|
41 value [nbe] "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 [nbe] "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 [nbe] "vars {(Var 1, Var 0)}" |
|
58 |
|
59 text \<open>Sometimes it is necessary to add explicit type constraints |
|
60 before a variant can be determined.\<close> |
|
61 (*value "vars R" (*has multiple instances*)*) |
|
62 value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)" |
|
63 |
|
64 text \<open>It is also possible to remove variants.\<close> |
|
65 no_adhoc_overloading |
|
66 vars term_vars rule_vars |
|
67 |
|
68 (*value "vars (Var 1)" (*does not have an instance*)*) |
|
69 |
|
70 text \<open>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 \<open>show_variants\<close>.\<close> |
|
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 \<open>Adhoc Overloading inside Locales\<close> |
|
83 |
|
84 text \<open>As example we use permutations that are parametrized over an |
|
85 atom type \<^typ>\<open>'a\<close>.\<close> |
|
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 standard (auto simp: perms_def) |
|
92 |
|
93 text \<open>First we need some auxiliary lemmas.\<close> |
|
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) |
|
130 apply (rule bij_is_inj [OF perms_imp_bij [OF f]]) |
|
131 done |
|
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 standard |
|
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 apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) |
|
163 done |
|
164 |
|
165 end |
|
166 |
|
167 lemmas Rep_perm_simps = |
|
168 Rep_perm_0 |
|
169 Rep_perm_add |
|
170 Rep_perm_uminus |
|
171 |
|
172 |
|
173 section \<open>Permutation Types\<close> |
|
174 |
|
175 text \<open>We want to be able to apply permutations to arbitrary types. To |
|
176 this end we introduce a constant \<open>PERMUTE\<close> together with |
|
177 convenient infix syntax.\<close> |
|
178 |
|
179 consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr \<open>\<bullet>\<close> 75) |
|
180 |
|
181 text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support |
|
182 appliciation of permutations.\<close> |
|
183 locale permute = |
|
184 fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" |
|
185 assumes permute_zero [simp]: "permute 0 x = x" |
|
186 and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)" |
|
187 begin |
|
188 |
|
189 adhoc_overloading |
|
190 PERMUTE permute |
|
191 |
|
192 end |
|
193 |
|
194 text \<open>Permuting atoms.\<close> |
|
195 definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
196 "permute_atom p a = (Rep_perm p) a" |
|
197 |
|
198 adhoc_overloading |
|
199 PERMUTE permute_atom |
|
200 |
|
201 interpretation atom_permute: permute permute_atom |
|
202 by standard (simp_all add: permute_atom_def Rep_perm_simps) |
|
203 |
|
204 text \<open>Permuting permutations.\<close> |
|
205 definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where |
|
206 "permute_perm p q = p + q - p" |
|
207 |
|
208 adhoc_overloading |
|
209 PERMUTE permute_perm |
|
210 |
|
211 interpretation perm_permute: permute permute_perm |
|
212 apply standard |
|
213 unfolding permute_perm_def |
|
214 apply simp |
|
215 apply (simp only: diff_conv_add_uminus minus_add add.assoc) |
|
216 done |
|
217 |
|
218 text \<open>Permuting functions.\<close> |
|
219 locale fun_permute = |
|
220 dom: permute perm1 + ran: permute perm2 |
|
221 for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" |
|
222 and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c" |
|
223 begin |
|
224 |
|
225 adhoc_overloading |
|
226 PERMUTE perm1 perm2 |
|
227 |
|
228 definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where |
|
229 "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))" |
|
230 |
|
231 adhoc_overloading |
|
232 PERMUTE permute_fun |
|
233 |
|
234 end |
|
235 |
|
236 sublocale fun_permute \<subseteq> permute permute_fun |
|
237 by (unfold_locales, auto simp: permute_fun_def) |
|
238 (metis dom.permute_plus minus_add) |
|
239 |
|
240 lemma "(Abs_perm id :: nat perm) \<bullet> Suc 0 = Suc 0" |
|
241 unfolding permute_atom_def |
|
242 by (metis Rep_perm_0 id_apply zero_perm_def) |
|
243 |
|
244 interpretation atom_fun_permute: fun_permute permute_atom permute_atom |
|
245 by (unfold_locales) |
|
246 |
|
247 adhoc_overloading |
|
248 PERMUTE atom_fun_permute.permute_fun |
|
249 |
|
250 lemma "(Abs_perm id :: 'a perm) \<bullet> id = id" |
|
251 unfolding atom_fun_permute.permute_fun_def |
|
252 unfolding permute_atom_def |
|
253 by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def) |
|
254 |
|
255 end |
|
256 |
|