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