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;
     1 (*  Title:      HOL/ex/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   "~~/src/Tools/Adhoc_Overloading"
    11   "~~/src/HOL/Library/Infinite_Set"
    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 "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 \<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 "'a"}.\<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 "\<bullet>" 75)
   180 
   181 text \<open>Then we add a locale for types @{typ 'b} 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