1(*  Title:      HOL/ex/Adhoc_Overloading_Examples.thy
2    Author:     Christian Sternagel
3*)
4
5section \<open>Ad Hoc Overloading\<close>
6
7theory Adhoc_Overloading_Examples
8imports
9  Main
10  "HOL-Library.Infinite_Set"
11  "HOL-Library.Adhoc_Overloading"
12begin
13
14text \<open>Adhoc overloading allows to overload a constant depending on
15its type. Typically this involves to introduce an uninterpreted
16constant (used for input and output) and then add some variants (used
17internally).\<close>
18
19subsection \<open>Plain Ad Hoc Overloading\<close>
20
21text \<open>Consider the type of first-order terms.\<close>
22datatype ('a, 'b) "term" =
23  Var 'b |
24  Fun 'a "('a, 'b) term list"
25
26text \<open>The set of variables of a term might be computed as follows.\<close>
27fun 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
31text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
32rewrite systems (i.e., sets of rules), the set of variables makes
33sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
34
35consts vars :: "'a \<Rightarrow> 'b set"
36
37text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
38adhoc_overloading
39  vars term_vars
40
41value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
42
43fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
44  "rule_vars (l, r) = vars l \<union> vars r"
45
46adhoc_overloading
47  vars rule_vars
48
49value [nbe] "vars (Var 1, Var 0)"
50
51definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
52  "trs_vars R = \<Union>(rule_vars ` R)"
53
54adhoc_overloading
55  vars trs_vars
56
57value [nbe] "vars {(Var 1, Var 0)}"
58
59text \<open>Sometimes it is necessary to add explicit type constraints
60before a variant can be determined.\<close>
61(*value "vars R" (*has multiple instances*)*)
62value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
63
64text \<open>It is also possible to remove variants.\<close>
65no_adhoc_overloading
66  vars term_vars rule_vars 
67
68(*value "vars (Var 1)" (*does not have an instance*)*)
69
70text \<open>As stated earlier, the overloaded constant is only used for
71input and output. Internally, always a variant is used, as can be
72observed by the configuration option \<open>show_variants\<close>.\<close>
73
74adhoc_overloading
75  vars term_vars
76
77declare [[show_variants]]
78
79term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
80
81
82subsection \<open>Adhoc Overloading inside Locales\<close>
83
84text \<open>As example we use permutations that are parametrized over an
85atom type \<^typ>\<open>'a\<close>.\<close>
86
87definition perms :: "('a \<Rightarrow> 'a) set" where
88  "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
89
90typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
91  by standard (auto simp: perms_def)
92
93text \<open>First we need some auxiliary lemmas.\<close>
94lemma 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
99lemma perms_imp_bij:
100  "f \<in> perms \<Longrightarrow> bij f"
101  by (simp add: perms_def)
102
103lemma 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
107lemma id_perms [simp]:
108  "id \<in> perms"
109  "(\<lambda>x. x) \<in> perms"
110  by (auto simp: perms_def bij_def)
111
112lemma 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
122lemma 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
133lemma bij_Rep_perm: "bij (Rep_perm p)"
134  using Rep_perm [of p] unfolding perms_def by simp
135
136instantiation perm :: (type) group_add
137begin
138
139definition "0 = Abs_perm id"
140definition "- p = Abs_perm (inv (Rep_perm p))"
141definition "p + q = Abs_perm (Rep_perm p \<circ> Rep_perm q)"
142definition "(p1::'a perm) - p2 = p1 + - p2"
143
144lemma Rep_perm_0: "Rep_perm 0 = id"
145  unfolding zero_perm_def by (simp add: Abs_perm_inverse)
146
147lemma 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
151lemma 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
155instance
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
165end
166
167lemmas Rep_perm_simps =
168  Rep_perm_0
169  Rep_perm_add
170  Rep_perm_uminus
171
172
173section \<open>Permutation Types\<close>
174
175text \<open>We want to be able to apply permutations to arbitrary types. To
176this end we introduce a constant \<open>PERMUTE\<close> together with
177convenient infix syntax.\<close>
178
179consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
180
181text \<open>Then we add a locale for types \<^typ>\<open>'b\<close> that support
182appliciation of permutations.\<close>
183locale 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)"
187begin
188
189adhoc_overloading
190  PERMUTE permute
191
192end
193
194text \<open>Permuting atoms.\<close>
195definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
196  "permute_atom p a = (Rep_perm p) a"
197
198adhoc_overloading
199  PERMUTE permute_atom
200
201interpretation atom_permute: permute permute_atom
202  by standard (simp_all add: permute_atom_def Rep_perm_simps)
203
204text \<open>Permuting permutations.\<close>
205definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
206  "permute_perm p q = p + q - p"
207
208adhoc_overloading
209  PERMUTE permute_perm
210
211interpretation 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
218text \<open>Permuting functions.\<close>
219locale 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"
223begin
224
225adhoc_overloading
226  PERMUTE perm1 perm2
227
228definition 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
231adhoc_overloading
232  PERMUTE permute_fun
233
234end
235
236sublocale fun_permute \<subseteq> permute permute_fun
237  by (unfold_locales, auto simp: permute_fun_def)
238     (metis dom.permute_plus minus_add)
239
240lemma "(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
244interpretation atom_fun_permute: fun_permute permute_atom permute_atom
245  by (unfold_locales)
246
247adhoc_overloading
248  PERMUTE atom_fun_permute.permute_fun
249
250lemma "(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
255end
256
257