# HG changeset patch # User wenzelm # Date 1738009862 -3600 # Node ID d67dadd69d072a3d0f8d35a576c2caed993ab7ff # Parent 5e50a2b5280986e0e4fae43ec3d7bd2272537416 clarified syntax; diff -r 5e50a2b52809 -r d67dadd69d07 src/Doc/Isar_Ref/Spec.thy --- 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>\~~/src/HOL/Library/Monad_Syntax.thy\. \<^rail>\ - (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) - (@{syntax name} (@{syntax term} + ) + @'and') + (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) \ + (@{syntax name} ('==' | '\') (@{syntax term} + ) + @'and') \ - \<^descr> @{command "adhoc_overloading"}~\c v\<^sub>1 ... v\<^sub>n\ associates variants with an + \<^descr> @{command "adhoc_overloading"}~\c \ v\<^sub>1 ... v\<^sub>n\ associates variants with an existing constant. \<^descr> @{command "no_adhoc_overloading"} is similar to @{command diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Examples/Adhoc_Overloading.thy --- 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 \Which is then overloaded with variants for terms, rules, and TRSs.\ adhoc_overloading - vars term_vars + vars \ term_vars value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" @@ -43,7 +43,7 @@ "rule_vars (l, r) = vars l \ vars r" adhoc_overloading - vars rule_vars + vars \ rule_vars value [nbe] "vars (Var 1, Var 0)" @@ -51,7 +51,7 @@ "trs_vars R = \(rule_vars ` R)" adhoc_overloading - vars trs_vars + vars \ trs_vars value [nbe] "vars {(Var 1, Var 0)}" @@ -62,7 +62,7 @@ text \It is also possible to remove variants.\ no_adhoc_overloading - vars term_vars rule_vars + vars \ term_vars rule_vars (*value "vars (Var 1)" (*does not have an instance*)*) @@ -71,7 +71,7 @@ observed by the configuration option \show_variants\.\ adhoc_overloading - vars term_vars + vars \ term_vars declare [[show_variants]] @@ -186,7 +186,7 @@ begin adhoc_overloading - PERMUTE permute + PERMUTE \ permute end @@ -195,7 +195,7 @@ "permute_atom p a = (Rep_perm p) a" adhoc_overloading - PERMUTE permute_atom + PERMUTE \ 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 \ permute_perm interpretation perm_permute: permute permute_perm apply standard @@ -222,13 +222,13 @@ begin adhoc_overloading - PERMUTE perm1 perm2 + PERMUTE \ perm1 perm2 definition permute_fun :: "'a perm \ ('b \ 'c) \ ('b \ 'c)" where "permute_fun p f = (\x. p \ (f (-p \ x)))" adhoc_overloading - PERMUTE permute_fun + PERMUTE \ permute_fun end @@ -244,7 +244,7 @@ by (unfold_locales) adhoc_overloading - PERMUTE atom_fun_permute.permute_fun + PERMUTE \ atom_fun_permute.permute_fun lemma "(Abs_perm id :: 'a perm) \ id = id" unfolding atom_fun_permute.permute_fun_def diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ None)" adhoc_overloading - Monad_Syntax.bind Heap_Monad.bind + Monad_Syntax.bind \ Heap_Monad.bind lemma execute_bind [execute_simps]: "execute f h = Some (x, h') \ execute (f \ g) h = execute (g x) h'" diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Library/Monad_Syntax.thy --- 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 \ n)" \ "(m \ (\_. n))" adhoc_overloading - bind Set.bind Predicate.bind Option.bind List.bind + bind \ Set.bind Predicate.bind Option.bind List.bind end diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Library/State_Monad.thy --- 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') \ run_state (f a) s')" unfolding bind_def by auto -adhoc_overloading Monad_Syntax.bind bind +adhoc_overloading Monad_Syntax.bind \ bind lemma bind_left_identity[simp]: "bind (return a) f = f a" unfolding return_def bind_def by simp diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/Giry_Monad.thy --- 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 \ space M))) f))" -adhoc_overloading Monad_Syntax.bind bind +adhoc_overloading Monad_Syntax.bind \ bind lemma bind_empty: "space M = {} \ bind M f = count_space {}" diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/Probability_Mass_Function.thy --- 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 \ bind_pmf lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\\<^sup>+x. pmf (f x) i \measure_pmf N)" unfolding pmf.rep_eq bind_pmf.rep_eq diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/SPMF.thy --- 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 \ ('a \ 'b spmf) \ 'b spmf" where "bind_spmf x f = bind_pmf x (\a. case a of None \ return_pmf None | Some a' \ f a')" -adhoc_overloading Monad_Syntax.bind bind_spmf +adhoc_overloading Monad_Syntax.bind \ bind_spmf lemma return_None_bind_spmf [simp]: "return_pmf None \ (f :: 'a \ _) = return_pmf None" by(simp add: bind_spmf_def bind_return_pmf) diff -r 5e50a2b52809 -r d67dadd69d07 src/Pure/Pure.thy --- 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 \ local +val adhoc_overloading_args = + Parse.and_list1 ((Parse.const --| (\<^keyword>\\\ || \<^keyword>\==\)) -- Scan.repeat Parse.term); + val _ = Outer_Syntax.local_theory \<^command_keyword>\adhoc_overloading\ "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>\no_adhoc_overloading\ "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