src/HOL/Examples/Adhoc_Overloading.thy

 
 consts vars :: "'a \<Rightarrow> 'b set"
 
 text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
 adhoc_overloading
-  vars term_vars
+  vars \<rightleftharpoons> term_vars
 
 value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
 
 fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
   "rule_vars (l, r) = vars l \<union> vars r"
 
 adhoc_overloading
-  vars rule_vars
+  vars \<rightleftharpoons> rule_vars
 
 value [nbe] "vars (Var 1, Var 0)"
 
 definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
   "trs_vars R = \<Union>(rule_vars ` R)"
 
 adhoc_overloading
-  vars trs_vars
+  vars \<rightleftharpoons> trs_vars
 
 value [nbe] "vars {(Var 1, Var 0)}"
 
 text \<open>Sometimes it is necessary to add explicit type constraints
 before a variant can be determined.\<close>
 (*value "vars R" (*has multiple instances*)*)
 value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
 
 text \<open>It is also possible to remove variants.\<close>
 no_adhoc_overloading
-  vars term_vars rule_vars 
+  vars \<rightleftharpoons> term_vars rule_vars 
 
 (*value "vars (Var 1)" (*does not have an instance*)*)
 
 text \<open>As stated earlier, the overloaded constant is only used for
 input and output. Internally, always a variant is used, as can be
 observed by the configuration option \<open>show_variants\<close>.\<close>
 
 adhoc_overloading
-  vars term_vars
+  vars \<rightleftharpoons> term_vars
 
 declare [[show_variants]]
 
 term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
 

   assumes permute_zero [simp]: "permute 0 x = x"
     and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)"
 begin
 
 adhoc_overloading
-  PERMUTE permute
+  PERMUTE \<rightleftharpoons> permute
 
 end
 
 text \<open>Permuting atoms.\<close>
 definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
   "permute_atom p a = (Rep_perm p) a"
 
 adhoc_overloading
-  PERMUTE permute_atom
+  PERMUTE \<rightleftharpoons> permute_atom
 
 interpretation atom_permute: permute permute_atom
   by standard (simp_all add: permute_atom_def Rep_perm_simps)
 
 text \<open>Permuting permutations.\<close>
 definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
   "permute_perm p q = p + q - p"
 
 adhoc_overloading
-  PERMUTE permute_perm
+  PERMUTE \<rightleftharpoons> permute_perm
 
 interpretation perm_permute: permute permute_perm
   apply standard
   unfolding permute_perm_def
   apply simp

   for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
   and perm2 :: "'a perm \<Rightarrow> 'c \<Rightarrow> 'c"
 begin
 
 adhoc_overloading
-  PERMUTE perm1 perm2
+  PERMUTE \<rightleftharpoons> perm1 perm2
 
 definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
   "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
 
 adhoc_overloading
-  PERMUTE permute_fun
+  PERMUTE \<rightleftharpoons> permute_fun
 
 end
 
 sublocale fun_permute \<subseteq> permute permute_fun
   by (unfold_locales, auto simp: permute_fun_def)

 
 interpretation atom_fun_permute: fun_permute permute_atom permute_atom
   by (unfold_locales)
 
 adhoc_overloading
-  PERMUTE atom_fun_permute.permute_fun
+  PERMUTE \<rightleftharpoons> atom_fun_permute.permute_fun
 
 lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
   unfolding atom_fun_permute.permute_fun_def
   unfolding permute_atom_def
   by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def)