# HG changeset patch
# User wenzelm
# Date 1734271197 -3600
# Node ID ed264056f5dc875d156d808b8a399d9f68a44d98
# Parent  7e1b66416b7fd23cf85afab73795da44ae4534f8
more syntax bundles, e.g. to explore terms without notation;

diff -r 7e1b66416b7f -r ed264056f5dc NEWS
--- a/NEWS	Sat Dec 14 23:48:45 2024 +0100
+++ b/NEWS	Sun Dec 15 14:59:57 2024 +0100
@@ -98,19 +98,28 @@
 * Various HOL declaration bundles support adhoc modification of
 notation, notably like this:
 
-  unbundle no list_syntax
-  unbundle no list_enumeration_syntax
+  unbundle no abs_syntax
+  unbundle no binomial_syntax
+  unbundle no converse_syntax
+  unbundle no floor_ceiling_syntax
+  unbundle no funcset_syntax
+  unbundle no let_syntax
   unbundle no list_comprehension_syntax
+  unbundle no list_enumeration_syntax
+  unbundle no list_maplet_syntax
+  unbundle no list_syntax
+  unbundle no list_update_syntax
+  unbundle no maplet_syntax
+  unbundle no prod_list_syntax
+  unbundle no reflcl_syntax
   unbundle no relcomp_syntax
-  unbundle no converse_syntax
   unbundle no rtrancl_syntax
+  unbundle no set_enumeration_syntax
+  unbundle no sum_list_syntax
   unbundle no trancl_syntax
-  unbundle no reflcl_syntax
-  unbundle no abs_syntax
-  unbundle no floor_ceiling_syntax
+  unbundle no tuple_syntax
   unbundle no uminus_syntax
-  unbundle no binomial_syntax
-  unbundle no funcset_syntax
+  unbundle no update_syntax
 
 This is more robust than individual 'no_syntax' / 'no_notation'
 commands, which need to copy mixfix declarations from elsewhere and thus
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Fun.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -840,6 +840,9 @@
 
 nonterminal updbinds and updbind
 
+open_bundle update_syntax
+begin
+
 syntax
   "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   ""         :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
@@ -852,6 +855,8 @@
   "_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
   "f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
 
+end
+
 (* Hint: to define the sum of two functions (or maps), use case_sum.
          A nice infix syntax could be defined by
 notation
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Groups_List.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -97,6 +97,10 @@
 end
 
 text \<open>Some syntactic sugar for summing a function over a list:\<close>
+
+open_bundle sum_list_syntax
+begin
+
 syntax (ASCII)
   "_sum_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _<-_. _)\<close> [0, 51, 10] 10)
 syntax
@@ -106,6 +110,8 @@
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
 
+end
+
 context
   includes lifting_syntax
 begin
@@ -596,6 +602,9 @@
 
 text \<open>Some syntactic sugar:\<close>
 
+open_bundle prod_list_syntax
+begin
+
 syntax (ASCII)
   "_prod_list" :: "pttrn => 'a list => 'b => 'b"    (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _<-_. _)\<close> [0, 51, 10] 10)
 syntax
@@ -605,6 +614,8 @@
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
 
+end
+
 context
   includes lifting_syntax
 begin
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/HOL.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -233,6 +233,10 @@
   where "Let s f \<equiv> f s"
 
 nonterminal letbinds and letbind
+
+open_bundle let_syntax
+begin
+
 syntax
   "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              (\<open>(\<open>indent=2 notation=\<open>mixfix let binding\<close>\<close>_ =/ _)\<close> 10)
   ""            :: "letbind \<Rightarrow> letbinds"                 (\<open>_\<close>)
@@ -244,6 +248,8 @@
   "_Let (_binds b bs) e"  \<rightleftharpoons> "_Let b (_Let bs e)"
   "let x = a in e"        \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
 
+end
+
 axiomatization undefined :: 'a
 
 class default = fixes default :: 'a
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/List.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -53,15 +53,17 @@
 
 open_bundle list_enumeration_syntax
 begin
+
 syntax
   "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
-end
 syntax_consts
   "_list" \<rightleftharpoons> Cons
 translations
   "[x, xs]" \<rightleftharpoons> "x#[xs]"
   "[x]" \<rightleftharpoons> "x#[]"
 
+end
+
 
 subsection \<open>Basic list processing functions\<close>
 
@@ -90,7 +92,9 @@
 "filter P [] = []" |
 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
 
-text \<open>Special input syntax for filter:\<close>
+open_bundle filter_syntax  \<comment> \<open>Special input syntax for filter\<close>
+begin
+
 syntax (ASCII)
   "_filter" :: "[pttrn, 'a list, bool] => 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix filter\<close>\<close>[_<-_./ _])\<close>)
 syntax
@@ -100,6 +104,8 @@
 translations
   "[x<-xs . P]" \<rightharpoonup> "CONST filter (\<lambda>x. P) xs"
 
+end
+
 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
 fold_Nil:  "fold f [] = id" |
 fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"
@@ -140,6 +146,9 @@
 
 nonterminal lupdbinds and lupdbind
 
+open_bundle list_update_syntax
+begin
+
 syntax
   "_lupdbind":: "['a, 'a] => lupdbind"    (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
   "" :: "lupdbind => lupdbinds"    (\<open>_\<close>)
@@ -152,6 +161,8 @@
   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "CONST list_update xs i x"
 
+end
+
 primrec takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "takeWhile P [] = []" |
 "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Map.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -56,6 +56,9 @@
 
 nonterminal maplet and maplets
 
+open_bundle maplet_syntax
+begin
+
 syntax
   "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"  (\<open>(\<open>open_block notation=\<open>mixfix maplet\<close>\<close>_ /\<mapsto>/ _)\<close>)
   ""         :: "maplet \<Rightarrow> updbind"  (\<open>_\<close>)
@@ -79,6 +82,8 @@
   "_Map (_maplet x y)"  \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplet x y)"
   "_Map (_updbinds m (_maplet x y))"  \<leftharpoondown> "_Update (_Map m) (_maplet x y)"
 
+end
+
 
 text \<open>Updating with lists:\<close>
 
@@ -96,6 +101,9 @@
 
 text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close>
 
+open_bundle list_maplet_syntax
+begin
+
 syntax
   "_maplets"  :: "['a, 'a] \<Rightarrow> maplet"  (\<open>(\<open>open_block notation=\<open>mixfix maplet\<close>\<close>_ /[\<mapsto>]/ _)\<close>)
 
@@ -111,6 +119,8 @@
   "_Map (_maplets xs ys)"  \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplets xs ys)"
   "_Map (_updbinds m (_maplets xs ys))"  \<leftharpoondown> "_Update (_Map m) (_maplets xs ys)"
 
+end
+
 
 subsection \<open>@{term [source] empty}\<close>
 
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Product_Type.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -285,6 +285,10 @@
 \<close>
 
 nonterminal tuple_args and patterns
+
+open_bundle tuple_syntax
+begin
+
 syntax
   "_tuple"      :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b"        (\<open>(\<open>indent=1 notation=\<open>mixfix tuple\<close>\<close>'(_,/ _'))\<close>)
   "_tuple_arg"  :: "'a \<Rightarrow> tuple_args"                   (\<open>_\<close>)
@@ -310,6 +314,8 @@
   "\<lambda>(). b" \<rightleftharpoons> "CONST case_unit b"
   "_abs (CONST Unity) t" \<rightharpoonup> "\<lambda>(). t"
 
+end
+
 text \<open>print \<^term>\<open>case_prod f\<close> as \<^term>\<open>\<lambda>(x, y). f x y\<close> and
   \<^term>\<open>case_prod (\<lambda>x. f x)\<close> as \<^term>\<open>\<lambda>(x, y). f x y\<close>\<close>
 
diff -r 7e1b66416b7f -r ed264056f5dc src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Set.thy	Sun Dec 15 14:59:57 2024 +0100
@@ -156,6 +156,9 @@
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
+open_bundle set_enumeration_syntax
+begin
+
 syntax
   "_Finset" :: "args \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 syntax_consts
@@ -164,6 +167,8 @@
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
 
+end
+
 
 subsection \<open>Subsets and bounded quantifiers\<close>