--- a/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 21:31:02 2025 +0100
@@ -1111,11 +1111,11 @@
\<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
\<^rail>\<open>
- (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
- (@{syntax name} (@{syntax term} + ) + @'and')
+ (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) \<newline>
+ (@{syntax name} ('==' | '\<rightleftharpoons>') (@{syntax term} + ) + @'and')
\<close>
- \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
+ \<^descr> @{command "adhoc_overloading"}~\<open>c \<rightleftharpoons> v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
existing constant.
\<^descr> @{command "no_adhoc_overloading"} is similar to @{command
--- a/src/HOL/Examples/Adhoc_Overloading.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Examples/Adhoc_Overloading.thy Mon Jan 27 21:31:02 2025 +0100
@@ -35,7 +35,7 @@
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])"
@@ -43,7 +43,7 @@
"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)"
@@ -51,7 +51,7 @@
"trs_vars R = \<Union>(rule_vars ` R)"
adhoc_overloading
- vars trs_vars
+ vars \<rightleftharpoons> trs_vars
value [nbe] "vars {(Var 1, Var 0)}"
@@ -62,7 +62,7 @@
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*)*)
@@ -71,7 +71,7 @@
observed by the configuration option \<open>show_variants\<close>.\<close>
adhoc_overloading
- vars term_vars
+ vars \<rightleftharpoons> term_vars
declare [[show_variants]]
@@ -186,7 +186,7 @@
begin
adhoc_overloading
- PERMUTE permute
+ PERMUTE \<rightleftharpoons> permute
end
@@ -195,7 +195,7 @@
"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)
@@ -205,7 +205,7 @@
"permute_perm p q = p + q - p"
adhoc_overloading
- PERMUTE permute_perm
+ PERMUTE \<rightleftharpoons> permute_perm
interpretation perm_permute: permute permute_perm
apply standard
@@ -222,13 +222,13 @@
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
@@ -244,7 +244,7 @@
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
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jan 27 21:31:02 2025 +0100
@@ -250,7 +250,7 @@
| None \<Rightarrow> None)"
adhoc_overloading
- Monad_Syntax.bind Heap_Monad.bind
+ Monad_Syntax.bind \<rightleftharpoons> Heap_Monad.bind
lemma execute_bind [execute_simps]:
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<bind> g) h = execute (g x) h'"
--- a/src/HOL/Library/Monad_Syntax.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Mon Jan 27 21:31:02 2025 +0100
@@ -70,6 +70,6 @@
"(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
adhoc_overloading
- bind Set.bind Predicate.bind Option.bind List.bind
+ bind \<rightleftharpoons> Set.bind Predicate.bind Option.bind List.bind
end
--- a/src/HOL/Library/State_Monad.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Library/State_Monad.thy Mon Jan 27 21:31:02 2025 +0100
@@ -89,7 +89,7 @@
"run_state (bind x f) s = (case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"
unfolding bind_def by auto
-adhoc_overloading Monad_Syntax.bind bind
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind
lemma bind_left_identity[simp]: "bind (return a) f = f a"
unfolding return_def bind_def by simp
--- a/src/HOL/Probability/Giry_Monad.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Mon Jan 27 21:31:02 2025 +0100
@@ -1092,7 +1092,7 @@
"bind M f = (if space M = {} then count_space {} else
join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
-adhoc_overloading Monad_Syntax.bind bind
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind
lemma bind_empty:
"space M = {} \<Longrightarrow> bind M f = count_space {}"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Mon Jan 27 21:31:02 2025 +0100
@@ -367,7 +367,7 @@
done
qed
-adhoc_overloading Monad_Syntax.bind bind_pmf
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind_pmf
lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
unfolding pmf.rep_eq bind_pmf.rep_eq
--- a/src/HOL/Probability/SPMF.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/SPMF.thy Mon Jan 27 21:31:02 2025 +0100
@@ -513,7 +513,7 @@
definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
where "bind_spmf x f = bind_pmf x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
-adhoc_overloading Monad_Syntax.bind bind_spmf
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind_spmf
lemma return_None_bind_spmf [simp]: "return_pmf None \<bind> (f :: 'a \<Rightarrow> _) = return_pmf None"
by(simp add: bind_spmf_def bind_return_pmf)
--- a/src/Pure/Pure.thy Mon Jan 27 20:29:02 2025 +0100
+++ b/src/Pure/Pure.thy Mon Jan 27 21:31:02 2025 +0100
@@ -1422,16 +1422,19 @@
ML \<open>
local
+val adhoc_overloading_args =
+ Parse.and_list1 ((Parse.const --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) -- Scan.repeat Parse.term);
+
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close>
"add adhoc overloading for constants / fixed variables"
- (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+ (adhoc_overloading_args
>> Adhoc_Overloading.adhoc_overloading_cmd true);
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>no_adhoc_overloading\<close>
"delete adhoc overloading for constants / fixed variables"
- (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+ (adhoc_overloading_args
>> Adhoc_Overloading.adhoc_overloading_cmd false);
in end