# HG changeset patch # User paulson # Date 1724617645 -3600 # Node ID fe7ffe7eb265777f2c3a34dacd0a3ad016158530 # Parent c7723cc15de8c8d8e5341d06bb586d16c9d92913# Parent 77f7aa898ced4f3a2c3561b490256078d657c72d merged diff -r 77f7aa898ced -r fe7ffe7eb265 src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sun Aug 25 21:27:25 2024 +0100 @@ -28,6 +28,8 @@ syntax "_MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" == MPair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST MPair x y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/CCL/Set.thy --- a/src/CCL/Set.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/CCL/Set.thy Sun Aug 25 21:27:25 2024 +0100 @@ -19,10 +19,10 @@ syntax "_Coll" :: "[idt, o] \ 'a set" ("(1{_./ _})") +syntax_consts + "_Coll" == Collect translations "{x. P}" == "CONST Collect(\x. P)" -syntax_consts - "_Coll" == Collect lemma CollectI: "P(a) \ a : {x. P(x)}" apply (rule mem_Collect_iff [THEN iffD2]) @@ -52,12 +52,12 @@ syntax "_Ball" :: "[idt, 'a set, o] \ o" ("(ALL _:_./ _)" [0, 0, 0] 10) "_Bex" :: "[idt, 'a set, o] \ o" ("(EX _:_./ _)" [0, 0, 0] 10) +syntax_consts + "_Ball" == Ball and + "_Bex" == Bex translations "ALL x:A. P" == "CONST Ball(A, \x. P)" "EX x:A. P" == "CONST Bex(A, \x. P)" -syntax_consts - "_Ball" == Ball and - "_Bex" == Bex lemma ballI: "(\x. x:A \ P(x)) \ ALL x:A. P(x)" by (simp add: Ball_def) @@ -129,12 +129,12 @@ syntax "_INTER" :: "[idt, 'a set, 'b set] \ 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) "_UNION" :: "[idt, 'a set, 'b set] \ 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) +syntax_consts + "_INTER" == INTER and + "_UNION" == UNION translations "INT x:A. B" == "CONST INTER(A, \x. B)" "UN x:A. B" == "CONST UNION(A, \x. B)" -syntax_consts - "_INTER" == INTER and - "_UNION" == UNION definition Inter :: "(('a set)set) \ 'a set" where "Inter(S) == (INT x:S. x)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/CCL/Term.thy --- a/src/CCL/Term.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/CCL/Term.thy Sun Aug 25 21:27:25 2024 +0100 @@ -49,8 +49,8 @@ where let_def: "let1(t, f) == case(t,f(true),f(false), \x y. f(), \u. f(lam x. u(x)))" syntax "_let1" :: "[idt,i,i]\i" ("(3let _ be _/ in _)" [0,0,60] 60) +syntax_consts "_let1" == let1 translations "let x be a in e" == "CONST let1(a, \x. e)" -syntax_consts "_let1" == let1 definition letrec :: "[[i,i\i]\i,(i\i)\i]\i" where "letrec(h, b) == b(\x. fix(\f. lam x. h(x,\y. f`y))`x)" @@ -68,6 +68,10 @@ "_letrec" :: "[idt,idt,i,i]\i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) "_letrec2" :: "[idt,idt,idt,i,i]\i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) "_letrec3" :: "[idt,idt,idt,idt,i,i]\i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) +syntax_consts + "_letrec" == letrec and + "_letrec2" == letrec2 and + "_letrec3" == letrec3 parse_translation \ let fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; @@ -123,10 +127,6 @@ (\<^const_syntax>\letrec3\, K letrec3_tr')] end \ -syntax_consts - "_letrec" == letrec and - "_letrec2" == letrec2 and - "_letrec3" == letrec3 definition nrec :: "[i,i,[i,i]\i]\i" where "nrec(n,b,c) == letrec g x be ncase(x, b, \y. c(y,g(y))) in g(n)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/CCL/Type.thy --- a/src/CCL/Type.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/CCL/Type.thy Sun Aug 25 21:27:25 2024 +0100 @@ -14,10 +14,10 @@ syntax "_Subtype" :: "[idt, 'a set, o] \ 'a set" ("(1{_: _ ./ _})") +syntax_consts + "_Subtype" == Subtype translations "{x: A. B}" == "CONST Subtype(A, \x. B)" -syntax_consts - "_Subtype" == Subtype definition Unit :: "i set" where "Unit == {x. x=one}" @@ -39,6 +39,9 @@ "_Sigma" :: "[idt, i set, i set] \ i set" ("(3SUM _:_./ _)" [0,0,60] 60) "_arrow" :: "[i set, i set] \ i set" ("(_ ->/ _)" [54, 53] 53) "_star" :: "[i set, i set] \ i set" ("(_ */ _)" [56, 55] 55) +syntax_consts + "_Pi" "_arrow" \ Pi and + "_Sigma" "_star" \ Sigma translations "PROD x:A. B" \ "CONST Pi(A, \x. B)" "A -> B" \ "CONST Pi(A, \_. B)" @@ -50,9 +53,6 @@ (\<^const_syntax>\Sigma\, fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\_Sigma\, \<^syntax_const>\_star\))] \ -syntax_consts - "_Pi" "_arrow" \ Pi and - "_Sigma" "_star" \ Sigma definition Nat :: "i set" where "Nat == lfp(\X. Unit + X)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/CTT/CTT.thy Sun Aug 25 21:27:25 2024 +0100 @@ -58,12 +58,12 @@ syntax "_PROD" :: "[idt,t,t]\t" ("(3\_:_./ _)" 10) "_SUM" :: "[idt,t,t]\t" ("(3\_:_./ _)" 10) +syntax_consts + "_PROD" \ Prod and + "_SUM" \ Sum translations "\x:A. B" \ "CONST Prod(A, \x. B)" "\x:A. B" \ "CONST Sum(A, \x. B)" -syntax_consts - "_PROD" \ Prod and - "_SUM" \ Sum abbreviation Arrow :: "[t,t]\t" (infixr "\" 30) where "A \ B \ \_:A. B" diff -r 77f7aa898ced -r fe7ffe7eb265 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/Cube/Cube.thy Sun Aug 25 21:27:25 2024 +0100 @@ -39,6 +39,13 @@ "_Lam" :: "[idt, term, term] \ term" ("(3\<^bold>\_:_./ _)" [0, 0, 0] 10) "_Pi" :: "[idt, term, term] \ term" ("(3\_:_./ _)" [0, 0] 10) "_arrow" :: "[term, term] \ term" (infixr "\" 10) +syntax_consts + "_Trueprop" \ Trueprop and + "_MT_context" \ MT_context and + "_Context" \ Context and + "_Has_type" \ Has_type and + "_Lam" \ Abs and + "_Pi" "_arrow" \ Prod translations "_Trueprop(G, t)" \ "CONST Trueprop(G, t)" ("prop") "x:X" \ ("prop") "\ x:X" @@ -52,13 +59,6 @@ [(\<^const_syntax>\Prod\, fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\_Pi\, \<^syntax_const>\_arrow\))] \ -syntax_consts - "_Trueprop" \ Trueprop and - "_MT_context" \ MT_context and - "_Context" \ Context and - "_Has_type" \ Has_type and - "_Lam" \ Abs and - "_Pi" "_arrow" \ Prod axiomatization where s_b: "*: \" and diff -r 77f7aa898ced -r fe7ffe7eb265 src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/Doc/Tutorial/Protocol/Message.thy Sun Aug 25 21:27:25 2024 +0100 @@ -81,6 +81,8 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" == MPair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST MPair x y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/FOL/IFOL.thy Sun Aug 25 21:27:25 2024 +0100 @@ -102,8 +102,8 @@ where \x \ y \ \ (x = y)\ syntax "_Uniq" :: "pttrn \ o \ o" ("(2\\<^sub>\\<^sub>1 _./ _)" [0, 10] 10) +syntax_consts "_Uniq" \ Uniq translations "\\<^sub>\\<^sub>1x. P" \ "CONST Uniq (\x. P)" -syntax_consts "_Uniq" \ Uniq print_translation \ [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\Uniq\ \<^syntax_const>\_Uniq\] @@ -747,10 +747,10 @@ "" :: \letbind => letbinds\ (\_\) "_binds" :: \[letbind, letbinds] => letbinds\ (\_;/ _\) "_Let" :: \[letbinds, 'a] => 'a\ (\(let (_)/ in (_))\ 10) +syntax_consts "_Let" \ Let translations "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" "let x = a in e" == "CONST Let(a, \x. e)" -syntax_consts "_Let" \ Let lemma LetI: assumes \\x. x = t \ P(u(x))\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Sun Aug 25 21:27:25 2024 +0100 @@ -308,6 +308,8 @@ syntax "_finprod" :: "index \ idt \ 'a set \ 'b \ 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) +syntax_consts + "_finprod" \ finprod translations "\\<^bsub>G\<^esub>i\A. b" \ "CONST finprod G (%i. b) A" \ \Beware of argument permutation!\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Algebra/Lattice.thy Sun Aug 25 21:27:25 2024 +0100 @@ -36,6 +36,10 @@ "_sup1" :: "('a, 'b) gorder_scheme \ pttrns \ 'a \ 'a" ("(3SSUP\ _./ _)" [0, 10] 10) "_sup" :: "('a, 'b) gorder_scheme \ pttrn \ 'c set \ 'a \ 'a" ("(3SSUP\ _:_./ _)" [0, 0, 10] 10) +syntax_consts + "_inf1" "_inf" == infi and + "_sup1" "_sup" == supr + translations "IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)" "IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Algebra/Ring.thy Sun Aug 25 21:27:25 2024 +0100 @@ -46,6 +46,8 @@ syntax "_finsum" :: "index \ idt \ 'a set \ 'b \ 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) +syntax_consts + "_finsum" \ finsum translations "\\<^bsub>G\<^esub>i\A. b" \ "CONST finsum G (\i. b) A" \ \Beware of argument permutation!\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Abstract_Metric_Spaces.thy --- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Aug 25 21:27:25 2024 +0100 @@ -1588,7 +1588,7 @@ by (force simp: Cauchy_def Met_TC.MCauchy_def) lemma mcomplete_iff_complete [iff]: - "Met_TC.mcomplete (Pure.type ::'a::metric_space itself) \ complete (UNIV::'a set)" + "Met_TC.mcomplete TYPE('a::metric_space) \ complete (UNIV::'a set)" by (auto simp: Met_TC.mcomplete_def complete_def) context Submetric diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Bochner_Integration.thy --- a/src/HOL/Analysis/Bochner_Integration.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Bochner_Integration.thy Sun Aug 25 21:27:25 2024 +0100 @@ -892,12 +892,18 @@ syntax "_lebesgue_integral" :: "pttrn \ real \ 'a measure \ real" ("\((2 _./ _)/ \_)" [60,61] 110) +syntax_consts + "_lebesgue_integral" == lebesgue_integral + translations "\ x. f \M" == "CONST lebesgue_integral M (\x. f)" syntax "_ascii_lebesgue_integral" :: "pttrn \ 'a measure \ real \ real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60) +syntax_consts + "_ascii_lebesgue_integral" == lebesgue_integral + translations "LINT x|M. f" == "CONST lebesgue_integral M (\x. f)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Euclidean_Space.thy --- a/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 21:27:25 2024 +0100 @@ -34,6 +34,7 @@ "(\u\Basis. inner x u = 0) \ (x = 0)" syntax "_type_dimension" :: "type \ nat" ("(1DIM/(1'(_')))") +syntax_consts "_type_dimension" \ card translations "DIM('a)" \ "CONST card (CONST Basis :: 'a set)" typed_print_translation \ [(\<^const_syntax>\card\, diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Aug 25 21:27:25 2024 +0100 @@ -40,6 +40,7 @@ \<^item> \'a^'b::_\ becomes \('a, 'b) vec\ without extra sort-constraint \ syntax "_vec_type" :: "type \ type \ type" (infixl "^" 15) +syntax_types "_vec_type" \ vec parse_translation \ let fun vec t u = Syntax.const \<^type_syntax>\vec\ $ t $ u; diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Finite_Product_Measure.thy --- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 25 21:27:25 2024 +0100 @@ -170,6 +170,8 @@ syntax "_PiM" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>M _\_./ _)" 10) +syntax_consts + "_PiM" == PiM translations "\\<^sub>M x\I. M" == "CONST PiM I (%x. M)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Infinite_Set_Sum.thy --- a/src/HOL/Analysis/Infinite_Set_Sum.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Sun Aug 25 21:27:25 2024 +0100 @@ -100,6 +100,8 @@ syntax "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_\_./ _)" [0, 51, 10] 10) +syntax_consts + "_infsetsum" \ infsetsum translations \ \Beware of argument permutation!\ "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A" @@ -109,6 +111,8 @@ syntax "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_./ _)" [0, 10] 10) +syntax_consts + "_uinfsetsum" \ infsetsum translations \ \Beware of argument permutation!\ "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)" @@ -118,6 +122,8 @@ syntax "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(2\\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) +syntax_consts + "_qinfsetsum" \ infsetsum translations "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Infinite_Sum.thy --- a/src/HOL/Analysis/Infinite_Sum.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Infinite_Sum.thy Sun Aug 25 21:27:25 2024 +0100 @@ -50,6 +50,8 @@ "_infsum" :: "pttrn \ 'a set \ 'b \ 'b::topological_comm_monoid_add" ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10) syntax "_infsum" :: "pttrn \ 'a set \ 'b \ 'b::topological_comm_monoid_add" ("(2\\<^sub>\(_/\_)./ _)" [0, 51, 10] 10) +syntax_consts + "_infsum" \ infsum translations \ \Beware of argument permutation!\ "\\<^sub>\i\A. b" \ "CONST infsum (\i. b) A" @@ -57,6 +59,8 @@ "_univinfsum" :: "pttrn \ 'a \ 'a" ("(3INFSUM _./ _)" [0, 10] 10) syntax "_univinfsum" :: "pttrn \ 'a \ 'a" ("(2\\<^sub>\_./ _)" [0, 10] 10) +syntax_consts + "_univinfsum" \ infsum translations "\\<^sub>\x. t" \ "CONST infsum (\x. t) (CONST UNIV)" @@ -64,6 +68,8 @@ "_qinfsum" :: "pttrn \ bool \ 'a \ 'a" ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10) syntax "_qinfsum" :: "pttrn \ bool \ 'a \ 'a" ("(2\\<^sub>\_ | (_)./ _)" [0, 0, 10] 10) +syntax_consts + "_qinfsum" \ infsum translations "\\<^sub>\x|P. t" => "CONST infsum (\x. t) {x. P}" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Interval_Integral.thy --- a/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 21:27:25 2024 +0100 @@ -148,6 +148,9 @@ "_ascii_interval_lebesgue_integral" :: "pttrn \ real \ real \ real measure \ real \ real" ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60) +syntax_consts + "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral + translations "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\x. f)" @@ -159,6 +162,9 @@ "_ascii_interval_lebesgue_borel_integral" :: "pttrn \ real \ real \ real \ real" ("(4LBINT _=_.._. _)" [0,60,60,61] 60) +syntax_consts + "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral + translations "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\x. f)" @@ -1045,11 +1051,17 @@ syntax "_complex_lebesgue_borel_integral" :: "pttrn \ real \ complex" ("(2CLBINT _. _)" [0,60] 60) +syntax_consts + "_complex_lebesgue_borel_integral" == complex_lebesgue_integral + translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\x. f)" syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \ real set \ real \ complex" ("(3CLBINT _:_. _)" [0,60,61] 60) +syntax_consts + "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral + translations "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\x. f)" @@ -1065,6 +1077,9 @@ "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \ ereal \ ereal \ real \ complex" ("(4CLBINT _=_.._. _)" [0,60,60,61] 60) +syntax_consts + "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral + translations "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\x. f)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 21:27:25 2024 +0100 @@ -1006,6 +1006,9 @@ syntax "_almost_everywhere" :: "pttrn \ 'a \ bool \ bool" ("AE _ in _. _" [0,0,10] 10) +syntax_consts + "_almost_everywhere" \ almost_everywhere + translations "AE x in M. P" \ "CONST almost_everywhere M (\x. P)" @@ -1016,6 +1019,9 @@ "_set_almost_everywhere" :: "pttrn \ 'a set \ 'a \ bool \ bool" ("AE _\_ in _./ _" [0,0,0,10] 10) +syntax_consts + "_set_almost_everywhere" \ set_almost_everywhere + translations "AE x\A in M. P" \ "CONST set_almost_everywhere A M (\x. P)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 21:27:25 2024 +0100 @@ -586,6 +586,9 @@ syntax "_simple_integral" :: "pttrn \ ennreal \ 'a measure \ ennreal" ("\\<^sup>S _. _ \_" [60,61] 110) +syntax_consts + "_simple_integral" == simple_integral + translations "\\<^sup>S x. f \M" == "CONST simple_integral M (%x. f)" @@ -819,6 +822,9 @@ syntax "_nn_integral" :: "pttrn \ ennreal \ 'a measure \ ennreal" ("\\<^sup>+((2 _./ _)/ \_)" [60,61] 110) +syntax_consts + "_nn_integral" == nn_integral + translations "\\<^sup>+x. f \M" == "CONST nn_integral M (\x. f)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Set_Integral.thy --- a/src/HOL/Analysis/Set_Integral.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Set_Integral.thy Sun Aug 25 21:27:25 2024 +0100 @@ -26,6 +26,9 @@ "_ascii_set_lebesgue_integral" :: "pttrn \ 'a set \ 'a measure \ real \ real" ("(4LINT (_):(_)/|(_)./ _)" [0,0,0,10] 10) +syntax_consts + "_ascii_set_lebesgue_integral" == set_lebesgue_integral + translations "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\x. f)" @@ -576,6 +579,9 @@ "_complex_lebesgue_integral" :: "pttrn \ complex \ 'a measure \ complex" ("\\<^sup>C _. _ \_" [0,0] 110) +syntax_consts + "_complex_lebesgue_integral" == complex_lebesgue_integral + translations "\\<^sup>Cx. f \M" == "CONST complex_lebesgue_integral M (\x. f)" @@ -583,6 +589,9 @@ "_ascii_complex_lebesgue_integral" :: "pttrn \ 'a measure \ real \ real" ("(3CLINT _|_. _)" [0,0,10] 10) +syntax_consts + "_ascii_complex_lebesgue_integral" == complex_lebesgue_integral + translations "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\x. f)" @@ -617,6 +626,9 @@ "_ascii_complex_set_lebesgue_integral" :: "pttrn \ 'a set \ 'a measure \ real \ real" ("(4CLINT _:_|_. _)" [0,0,0,10] 10) +syntax_consts + "_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral + translations "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\x. f)" @@ -640,6 +652,10 @@ "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal" ("(\((_)\(_)./ _)/\_)" [0,0,0,110] 10) +syntax_consts +"_set_nn_integral" == set_nn_integral and +"_set_lebesgue_integral" == set_lebesgue_integral + translations "\\<^sup>+x \ A. f \M" == "CONST set_nn_integral M A (\x. f)" "\x \ A. f \M" == "CONST set_lebesgue_integral M A (\x. f)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Analysis/Sparse_In.thy --- a/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 21:27:25 2024 +0100 @@ -166,11 +166,15 @@ syntax "_eventually_cosparse" :: "pttrn => 'a set => bool => bool" ("(3\\<^sub>\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_eventually_cosparse" == eventually translations "\\<^sub>\x\A. P" == "CONST eventually (\x. P) (CONST cosparse A)" syntax "_qeventually_cosparse" :: "pttrn \ bool \ 'a \ 'a" ("(3\\<^sub>\_ | (_)./ _)" [0, 0, 10] 10) +syntax_consts + "_qeventually_cosparse" == eventually translations "\\<^sub>\x|P. t" => "CONST eventually (\x. t) (CONST cosparse {x. P})" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Auth/Message.thy Sun Aug 25 21:27:25 2024 +0100 @@ -51,6 +51,8 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" \ MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/BNF_Cardinal_Arithmetic.thy --- a/src/HOL/BNF_Cardinal_Arithmetic.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Sun Aug 25 21:27:25 2024 +0100 @@ -275,6 +275,9 @@ "pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set" ("(3CSUM _:_. _)" [0, 51, 10] 10) +syntax_consts + "_Csum" == Csum + translations "CSUM i:r. rs" == "CONST Csum r (%i. rs)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Bali/AxSem.thy Sun Aug 25 21:27:25 2024 +0100 @@ -205,6 +205,8 @@ syntax "_peek_res" :: "pttrn \ 'a assn \ 'a assn" ("\_:. _" [0,3] 3) +syntax_consts + "_peek_res" == peek_res translations "\w:. P" == "CONST peek_res (\w. P)" @@ -266,6 +268,8 @@ syntax "_peek_st" :: "pttrn \ 'a assn \ 'a assn" ("\_.. _" [0,3] 3) +syntax_consts + "_peek_st" == peek_st translations "\s.. P" == "CONST peek_st (\s. P)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Bali/Basis.thy Sun Aug 25 21:27:25 2024 +0100 @@ -195,6 +195,10 @@ "_Oall" :: "[pttrn, 'a option, bool] \ bool" ("(3\_\_:/ _)" [0,0,10] 10) "_Oex" :: "[pttrn, 'a option, bool] \ bool" ("(3\_\_:/ _)" [0,0,10] 10) +syntax_consts + "_Oall" \ Ball and + "_Oex" \ Bex + translations "\x\A: P" \ "\x\CONST set_option A. P" "\x\A: P" \ "\x\CONST set_option A. P" @@ -257,6 +261,8 @@ text \list patterns -- extends pre-defined type "pttrn" used in abstractions\ syntax "_lpttrn" :: "[pttrn, pttrn] \ pttrn" ("_#/_" [901,900] 900) +syntax_consts + "_lpttrn" \ lsplit translations "\y # x # xs. b" \ "CONST lsplit (\y x # xs. b)" "\x # xs. b" \ "CONST lsplit (\x xs. b)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Bali/State.thy Sun Aug 25 21:27:25 2024 +0100 @@ -135,6 +135,10 @@ Heap :: "loc \ oref" Stat :: "qtname \ oref" +syntax_consts + Heap == Inl and + Stat == Inr + translations "Heap" => "CONST Inl" "Stat" => "CONST Inr" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy --- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 21:27:25 2024 +0100 @@ -24,6 +24,7 @@ no_notation lazy_llist ("_") syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]") +syntax_consts "_llist" == lazy_llist translations "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Complete_Lattices.thy Sun Aug 25 21:27:25 2024 +0100 @@ -32,6 +32,10 @@ "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_INF1" "_INF" \ Inf and + "_SUP1" "_SUP" \ Sup + translations "\x y. f" \ "\x. \y. f" "\x. f" \ "\(CONST range (\x. f))" @@ -850,6 +854,9 @@ "_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3\(\unbreakable\\<^bsub>_\<^esub>)/ _)" [0, 10] 10) "_INTER" :: "pttrn \ 'a set \ 'b set \ 'b set" ("(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10) +syntax_consts + "_INTER1" "_INTER" \ Inter + translations "\x y. f" \ "\x. \y. f" "\x. f" \ "\(CONST range (\x. f))" @@ -1013,6 +1020,9 @@ "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\(\unbreakable\\<^bsub>_\<^esub>)/ _)" [0, 10] 10) "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10) +syntax_consts + "_UNION1" "_UNION" \ Union + translations "\x y. f" \ "\x. \y. f" "\x. f" \ "\(CONST range (\x. f))" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Filter.thy --- a/src/HOL/Filter.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Filter.thy Sun Aug 25 21:27:25 2024 +0100 @@ -41,6 +41,8 @@ syntax "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\\<^sub>F _ in _./ _)" [0, 0, 10] 10) +syntax_consts + "_eventually" == eventually translations "\\<^sub>Fx in F. P" == "CONST eventually (\x. P) F" @@ -159,6 +161,8 @@ syntax "_frequently" :: "pttrn \ 'a filter \ bool \ bool" ("(3\\<^sub>F _ in _./ _)" [0, 0, 10] 10) +syntax_consts + "_frequently" == frequently translations "\\<^sub>Fx in F. P" == "CONST frequently (\x. P) F" @@ -1305,6 +1309,9 @@ syntax "_LIM" :: "pttrns \ 'a \ 'b \ 'a \ bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10) +syntax_consts + "_LIM" == filterlim + translations "LIM x F1. f :> F2" == "CONST filterlim (\x. f) F2 F1" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Fun.thy Sun Aug 25 21:27:25 2024 +0100 @@ -846,6 +846,9 @@ "_updbinds":: "updbind \ updbinds \ updbinds" ("_,/ _") "_Update" :: "'a \ updbinds \ 'a" ("_/'((_)')" [1000, 0] 900) +syntax_consts + "_updbind" "_updbinds" "_Update" \ fun_upd + translations "_Update f (_updbinds b bs)" \ "_Update (_Update f b) bs" "f(x:=y)" \ "CONST fun_upd f x y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/GCD.thy Sun Aug 25 21:27:25 2024 +0100 @@ -153,6 +153,10 @@ "_LCM1" :: "pttrns \ 'b \ 'b" ("(3LCM _./ _)" [0, 10] 10) "_LCM" :: "pttrn \ 'a set \ 'b \ 'b" ("(3LCM _\_./ _)" [0, 0, 10] 10) +syntax_consts + "_GCD1" "_GCD" \ Gcd and + "_LCM1" "_LCM" \ Lcm + translations "GCD x y. f" \ "GCD x. GCD y. f" "GCD x. f" \ "CONST Gcd (CONST range (\x. f))" @@ -2847,18 +2851,23 @@ definition (in semiring_1) semiring_char :: "'a itself \ nat" where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}" +syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))") +syntax_consts "_type_char" \ semiring_char +translations "CHAR('t)" \ "CONST semiring_char (CONST Pure.type :: 't itself)" +print_translation \ + let + fun char_type_tr' ctxt [Const (\<^const_syntax>\Pure.type\, Type (_, [T]))] = + Syntax.const \<^syntax_const>\_type_char\ $ Syntax_Phases.term_of_typ ctxt T + in [(\<^const_syntax>\semiring_char\, char_type_tr')] end +\ + context semiring_1 begin -context - fixes CHAR :: nat - defines "CHAR \ semiring_char (Pure.type :: 'a itself)" -begin - -lemma of_nat_CHAR [simp]: "of_nat CHAR = (0 :: 'a)" +lemma of_nat_CHAR [simp]: "of_nat CHAR('a) = (0 :: 'a)" proof - - have "CHAR \ {n. of_nat n = (0::'a)}" - unfolding CHAR_def semiring_char_def + have "CHAR('a) \ {n. of_nat n = (0::'a)}" + unfolding semiring_char_def proof (rule Gcd_in, clarify) fix a b :: nat assume *: "of_nat a = (0 :: 'a)" "of_nat b = (0 :: 'a)" @@ -2882,14 +2891,14 @@ by simp qed -lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \ CHAR dvd n" +lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \ CHAR('a) dvd n" proof assume "of_nat n = (0 :: 'a)" - thus "CHAR dvd n" - unfolding CHAR_def semiring_char_def by (intro Gcd_dvd) auto + thus "CHAR('a) dvd n" + unfolding semiring_char_def by (intro Gcd_dvd) auto next - assume "CHAR dvd n" - then obtain m where "n = CHAR * m" + assume "CHAR('a) dvd n" + then obtain m where "n = CHAR('a) * m" by auto thus "of_nat n = (0 :: 'a)" by simp @@ -2898,51 +2907,36 @@ lemma CHAR_eqI: assumes "of_nat c = (0 :: 'a)" assumes "\x. of_nat x = (0 :: 'a) \ c dvd x" - shows "CHAR = c" + shows "CHAR('a) = c" using assms by (intro dvd_antisym) (auto simp: of_nat_eq_0_iff_char_dvd) -lemma CHAR_eq0_iff: "CHAR = 0 \ (\n>0. of_nat n \ (0::'a))" +lemma CHAR_eq0_iff: "CHAR('a) = 0 \ (\n>0. of_nat n \ (0::'a))" by (auto simp: of_nat_eq_0_iff_char_dvd) -lemma CHAR_pos_iff: "CHAR > 0 \ (\n>0. of_nat n = (0::'a))" +lemma CHAR_pos_iff: "CHAR('a) > 0 \ (\n>0. of_nat n = (0::'a))" using CHAR_eq0_iff neq0_conv by blast lemma CHAR_eq_posI: assumes "c > 0" "of_nat c = (0 :: 'a)" "\x. x > 0 \ x < c \ of_nat x \ (0 :: 'a)" - shows "CHAR = c" + shows "CHAR('a) = c" proof (rule antisym) - from assms have "CHAR > 0" + from assms have "CHAR('a) > 0" by (auto simp: CHAR_pos_iff) - from assms(3)[OF this] show "CHAR \ c" + from assms(3)[OF this] show "CHAR('a) \ c" by force next - have "CHAR dvd c" + have "CHAR('a) dvd c" using assms by (auto simp: of_nat_eq_0_iff_char_dvd) - thus "CHAR \ c" + thus "CHAR('a) \ c" using \c > 0\ by (intro dvd_imp_le) auto qed end -end - -lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char (Pure.type :: 'a itself) = 0" + +lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0" by (simp add: CHAR_eq0_iff) -(* nicer notation *) - -syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))") - -translations "CHAR('t)" => "CONST semiring_char (CONST Pure.type :: 't itself)" - -print_translation \ - let - fun char_type_tr' ctxt [Const (\<^const_syntax>\Pure.type\, Type (_, [T]))] = - Syntax.const \<^syntax_const>\_type_char\ $ Syntax_Phases.term_of_typ ctxt T - in [(\<^const_syntax>\semiring_char\, char_type_tr')] end -\ - - lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \ Suc 0" by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one) diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Groups_Big.thy Sun Aug 25 21:27:25 2024 +0100 @@ -654,32 +654,41 @@ "_sum" :: "pttrn \ 'a set \ 'b \ 'b::comm_monoid_add" ("(3SUM (_/:_)./ _)" [0, 51, 10] 10) syntax "_sum" :: "pttrn \ 'a set \ 'b \ 'b::comm_monoid_add" ("(2\(_/\_)./ _)" [0, 51, 10] 10) + +syntax_consts + "_sum" \ sum + translations \ \Beware of argument permutation!\ "\i\A. b" \ "CONST sum (\i. b) A" + text \Instead of \<^term>\\x\{x. P}. e\ we introduce the shorter \\x|P. e\.\ syntax (ASCII) "_qsum" :: "pttrn \ bool \ 'a \ 'a" ("(3SUM _ |/ _./ _)" [0, 0, 10] 10) syntax "_qsum" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0, 0, 10] 10) + +syntax_consts + "_qsum" == sum + translations "\x|P. t" => "CONST sum (\x. t) {x. P}" print_translation \ -let - fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = - if x <> y then raise Match - else - let - val x' = Syntax_Trans.mark_bound_body (x, Tx); - val t' = subst_bound (x', t); - val P' = subst_bound (x', P); - in - Syntax.const \<^syntax_const>\_qsum\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' - end - | sum_tr' _ = raise Match; -in [(\<^const_syntax>\sum\, K sum_tr')] end + let + fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = + if x <> y then raise Match + else + let + val x' = Syntax_Trans.mark_bound_body (x, Tx); + val t' = subst_bound (x', t); + val P' = subst_bound (x', P); + in + Syntax.const \<^syntax_const>\_qsum\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' + end + | sum_tr' _ = raise Match; + in [(\<^const_syntax>\sum\, K sum_tr')] end \ @@ -1415,18 +1424,43 @@ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD (_/:_)./ _)" [0, 51, 10] 10) syntax "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\(_/\_)./ _)" [0, 51, 10] 10) + +syntax_consts + "_prod" == prod + translations \ \Beware of argument permutation!\ "\i\A. b" == "CONST prod (\i. b) A" + text \Instead of \<^term>\\x\{x. P}. e\ we introduce the shorter \\x|P. e\.\ syntax (ASCII) "_qprod" :: "pttrn \ bool \ 'a \ 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10) syntax "_qprod" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0, 0, 10] 10) + +syntax_consts + "_qprod" == prod + translations "\x|P. t" => "CONST prod (\x. t) {x. P}" +print_translation \ + let + fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = + if x <> y then raise Match + else + let + val x' = Syntax_Trans.mark_bound_body (x, Tx); + val t' = subst_bound (x', t); + val P' = subst_bound (x', P); + in + Syntax.const \<^syntax_const>\_qprod\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' + end + | prod_tr' _ = raise Match; + in [(\<^const_syntax>\prod\, K prod_tr')] end +\ + context comm_monoid_mult begin diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Groups_List.thy --- a/src/HOL/Groups_List.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Groups_List.thy Sun Aug 25 21:27:25 2024 +0100 @@ -101,6 +101,8 @@ "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) syntax "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) +syntax_consts + "_sum_list" == sum_list translations \ \Beware of argument permutation!\ "\x\xs. b" == "CONST sum_list (CONST map (\x. b) xs)" @@ -598,6 +600,8 @@ "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) syntax "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) +syntax_consts + "_prod_list" \ prod_list translations \ \Beware of argument permutation!\ "\x\xs. b" \ "CONST prod_list (CONST map (\x. b) xs)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOL.thy Sun Aug 25 21:27:25 2024 +0100 @@ -129,6 +129,9 @@ syntax (ASCII) "_Uniq" :: "pttrn \ bool \ bool" ("(4?< _./ _)" [0, 10] 10) syntax "_Uniq" :: "pttrn \ bool \ bool" ("(2\\<^sub>\\<^sub>1 _./ _)" [0, 10] 10) + +syntax_consts "_Uniq" \ Uniq + translations "\\<^sub>\\<^sub>1x. P" \ "CONST Uniq (\x. P)" print_translation \ @@ -141,6 +144,9 @@ syntax (input) "_Ex1" :: "pttrn \ bool \ bool" ("(3?! _./ _)" [0, 10] 10) syntax "_Ex1" :: "pttrn \ bool \ bool" ("(3\!_./ _)" [0, 10] 10) + +syntax_consts "_Ex1" \ Ex1 + translations "\!x. P" \ "CONST Ex1 (\x. P)" print_translation \ @@ -151,6 +157,9 @@ syntax "_Not_Ex" :: "idts \ bool \ bool" ("(3\_./ _)" [0, 10] 10) "_Not_Ex1" :: "pttrn \ bool \ bool" ("(3\!_./ _)" [0, 10] 10) +syntax_consts + "_Not_Ex" \ Ex and + "_Not_Ex1" \ Ex1 translations "\x. P" \ "\ (\x. P)" "\!x. P" \ "\ (\!x. P)" @@ -171,6 +180,7 @@ where "A \ B \ A = B" syntax "_The" :: "[pttrn, bool] \ 'a" ("(3THE _./ _)" [0, 10] 10) +syntax_consts "_The" \ The translations "THE x. P" \ "CONST The (\x. P)" print_translation \ [(\<^const_syntax>\The\, fn _ => fn [Abs abs] => @@ -178,13 +188,6 @@ in Syntax.const \<^syntax_const>\_The\ $ x $ t end)] \ \ \To avoid eta-contraction of body\ -nonterminal letbinds and letbind -syntax - "_bind" :: "[pttrn, 'a] \ letbind" ("(2_ =/ _)" 10) - "" :: "letbind \ letbinds" ("_") - "_binds" :: "[letbind, letbinds] \ letbinds" ("_;/ _") - "_Let" :: "[letbinds, 'a] \ 'a" ("(let (_)/ in (_))" [0, 10] 10) - nonterminal case_syn and cases_syn syntax "_case_syntax" :: "['a, cases_syn] \ 'b" ("(case _ of/ _)" 10) @@ -227,6 +230,14 @@ definition Let :: "'a \ ('a \ 'b) \ 'b" where "Let s f \ f s" +nonterminal letbinds and letbind +syntax + "_bind" :: "[pttrn, 'a] \ letbind" ("(2_ =/ _)" 10) + "" :: "letbind \ letbinds" ("_") + "_binds" :: "[letbind, letbinds] \ letbinds" ("_;/ _") + "_Let" :: "[letbinds, 'a] \ 'a" ("(let (_)/ in (_))" [0, 10] 10) +syntax_consts + "_bind" "_binds" "_Let" \ Let translations "_Let (_binds b bs) e" \ "_Let b (_Let bs e)" "let x = a in e" \ "CONST Let a (\x. e)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/Cfun.thy Sun Aug 25 21:27:25 2024 +0100 @@ -52,6 +52,9 @@ syntax "_Lambda" :: "[cargs, logic] \ logic" ("(3\ _./ _)" [1000, 10] 10) +syntax_consts + "_Lambda" \ Abs_cfun + parse_ast_translation \ (* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *) (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *) diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/ConvexPD.thy Sun Aug 25 21:27:25 2024 +0100 @@ -181,6 +181,9 @@ syntax "_convex_pd" :: "args \ logic" ("{_}\") +syntax_consts + "_convex_pd" == convex_add + translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST convex_unit\x" @@ -348,6 +351,9 @@ "_convex_bind" :: "[logic, logic, logic] \ logic" ("(3\\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_convex_bind" == convex_bind + translations "\\x\xs. e" == "CONST convex_bind\xs\(\ x. e)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/IOA/Sequence.thy --- a/src/HOL/HOLCF/IOA/Sequence.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/IOA/Sequence.thy Sun Aug 25 21:27:25 2024 +0100 @@ -72,6 +72,8 @@ syntax "_totlist" :: "args \ 'a Seq" ("[(_)!]") "_partlist" :: "args \ 'a Seq" ("[(_)?]") +syntax_consts + "_totlist" "_partlist" \ Consq translations "[x, xs!]" \ "x \ [xs!]" "[x!]" \ "x\nil" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/LowerPD.thy Sun Aug 25 21:27:25 2024 +0100 @@ -136,6 +136,9 @@ syntax "_lower_pd" :: "args \ logic" ("{_}\") +syntax_consts + "_lower_pd" == lower_add + translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST lower_unit\x" @@ -342,6 +345,9 @@ "_lower_bind" :: "[logic, logic, logic] \ logic" ("(3\\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_lower_bind" == lower_bind + translations "\\x\xs. e" == "CONST lower_bind\xs\(\ x. e)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/Pcpo.thy --- a/src/HOL/HOLCF/Pcpo.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/Pcpo.thy Sun Aug 25 21:27:25 2024 +0100 @@ -153,6 +153,7 @@ text \Old "UU" syntax:\ syntax UU :: logic +syntax_consts UU \ bottom translations "UU" \ "CONST bottom" text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/Porder.thy --- a/src/HOL/HOLCF/Porder.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/Porder.thy Sun Aug 25 21:27:25 2024 +0100 @@ -118,6 +118,9 @@ syntax "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" ("(3\_\_./ _)" [0,0, 10] 10) +syntax_consts + "_BLub" \ lub + translations "LUB x:A. t" \ "CONST lub ((\x. t) ` A)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/Representable.thy --- a/src/HOL/HOLCF/Representable.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/Representable.thy Sun Aug 25 21:27:25 2024 +0100 @@ -32,6 +32,7 @@ assumes cast_liftdefl: "cast\(liftdefl TYPE('a)) = liftemb oo liftprj" syntax "_LIFTDEFL" :: "type \ logic" ("(1LIFTDEFL/(1'(_')))") +syntax_consts "_LIFTDEFL" \ liftdefl translations "LIFTDEFL('t)" \ "CONST liftdefl TYPE('t)" definition liftdefl_of :: "udom defl \ udom u defl" @@ -51,6 +52,7 @@ assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\(defl TYPE('a))" syntax "_DEFL" :: "type \ logic" ("(1DEFL/(1'(_')))") +syntax_consts "_DEFL" \ defl translations "DEFL('t)" \ "CONST defl TYPE('t)" instance "domain" \ predomain diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/Sprod.thy --- a/src/HOL/HOLCF/Sprod.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/Sprod.thy Sun Aug 25 21:27:25 2024 +0100 @@ -41,6 +41,7 @@ where "ssplit = (\ f p. seq\p\(f\(sfst\p)\(ssnd\p)))" syntax "_stuple" :: "[logic, args] \ logic" ("(1'(:_,/ _:'))") +syntax_consts "_stuple" \ spair translations "(:x, y, z:)" \ "(:x, (:y, z:):)" "(:x, y:)" \ "CONST spair\x\y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/UpperPD.thy Sun Aug 25 21:27:25 2024 +0100 @@ -134,6 +134,9 @@ syntax "_upper_pd" :: "args \ logic" ("{_}\") +syntax_consts + "_upper_pd" == upper_add + translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST upper_unit\x" @@ -335,6 +338,9 @@ "_upper_bind" :: "[logic, logic, logic] \ logic" ("(3\\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_upper_bind" == upper_bind + translations "\\x\xs. e" == "CONST upper_bind\xs\(\ x. e)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/HOLCF/ex/Letrec.thy --- a/src/HOL/HOLCF/ex/Letrec.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/HOLCF/ex/Letrec.thy Sun Aug 25 21:27:25 2024 +0100 @@ -22,6 +22,9 @@ "_recbinds" :: "[recbindt, recbinds] \ recbinds" ("_;/ _") "_Letrec" :: "[recbinds, logic] \ logic" ("(Letrec (_)/ in (_))" 10) +syntax_consts + "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec + translations (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)" (recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Hilbert_Choice.thy Sun Aug 25 21:27:25 2024 +0100 @@ -22,6 +22,9 @@ "_Eps" :: "pttrn \ bool \ 'a" ("(3@ _./ _)" [0, 10] 10) syntax "_Eps" :: "pttrn \ bool \ 'a" ("(3SOME _./ _)" [0, 10] 10) + +syntax_consts "_Eps" \ Eps + translations "SOME x. P" \ "CONST Eps (\x. P)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Lattices_Big.thy Sun Aug 25 21:27:25 2024 +0100 @@ -470,6 +470,10 @@ "_MAX1" :: "pttrns \ 'b \ 'b" ("(3MAX _./ _)" [0, 10] 10) "_MAX" :: "pttrn \ 'a set \ 'b \ 'b" ("(3MAX _\_./ _)" [0, 0, 10] 10) +syntax_consts + "_MIN1" "_MIN" \ Min and + "_MAX1" "_MAX" \ Max + translations "MIN x y. f" \ "MIN x. MIN y. f" "MIN x. f" \ "CONST Min (CONST range (\x. f))" @@ -478,6 +482,7 @@ "MAX x. f" \ "CONST Max (CONST range (\x. f))" "MAX x\A. f" \ "CONST Max ((\x. f) ` A)" + text \An aside: \<^const>\Min\/\<^const>\Max\ on linear orders as special case of \<^const>\Inf_fin\/\<^const>\Sup_fin\\ lemma Inf_fin_Min: @@ -919,6 +924,8 @@ syntax "_arg_min" :: "('b \ 'a) \ pttrn \ bool \ 'b" ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10) +syntax_consts + "_arg_min" \ arg_min translations "ARG_MIN f x. P" \ "CONST arg_min f (\x. P)" @@ -1028,6 +1035,8 @@ syntax "_arg_max" :: "('b \ 'a) \ pttrn \ bool \ 'a" ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10) +syntax_consts + "_arg_max" \ arg_max translations "ARG_MAX f x. P" \ "CONST arg_max f (\x. P)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Cardinality.thy Sun Aug 25 21:27:25 2024 +0100 @@ -32,6 +32,8 @@ syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") +syntax_consts "_type_card" == card + translations "CARD('t)" => "CONST card (CONST UNIV :: 't set)" print_translation \ diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/FSet.thy Sun Aug 25 21:27:25 2024 +0100 @@ -167,6 +167,9 @@ syntax "_insert_fset" :: "args => 'a fset" ("{|(_)|}") +syntax_consts + "_insert_fset" == finsert + translations "{|x, xs|}" == "CONST finsert x {|xs|}" "{|x|}" == "CONST finsert x {||}" @@ -200,6 +203,10 @@ "_fBall" :: "pttrn \ 'a fset \ bool \ bool" ("(3\(_/|\|_)./ _)" [0, 0, 10] 10) "_fBex" :: "pttrn \ 'a fset \ bool \ bool" ("(3\(_/|\|_)./ _)" [0, 0, 10] 10) +syntax_consts + "_fBall" \ FSet.Ball and + "_fBex" \ FSet.Bex + translations "\x|\|A. P" \ "CONST FSet.Ball A (\x. P)" "\x|\|A. P" \ "CONST FSet.Bex A (\x. P)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/FuncSet.thy Sun Aug 25 21:27:25 2024 +0100 @@ -25,6 +25,9 @@ syntax "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\ _\_./ _)" 10) "_lam" :: "pttrn \ 'a set \ ('a \ 'b) \ ('a \ 'b)" ("(3\_\_./ _)" [0,0,3] 3) +syntax_consts + "_Pi" \ Pi and + "_lam" \ restrict translations "\ x\A. B" \ "CONST Pi A (\x. B)" "\x\A. f" \ "CONST restrict (\x. f) A" @@ -350,6 +353,8 @@ syntax "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\\<^sub>E _\_./ _)" 10) +syntax_consts + "_PiE" \ Pi\<^sub>E translations "\\<^sub>E x\A. B" \ "CONST Pi\<^sub>E A (\x. B)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Groups_Big_Fun.thy --- a/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 21:27:25 2024 +0100 @@ -202,6 +202,8 @@ "_Sum_any" :: "pttrn \ 'a \ 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10) syntax "_Sum_any" :: "pttrn \ 'a \ 'a::comm_monoid_add" ("(3\_. _)" [0, 10] 10) +syntax_consts + "_Sum_any" \ Sum_any translations "\a. b" \ "CONST Sum_any (\a. b)" @@ -255,6 +257,8 @@ "_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10) syntax "_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3\_. _)" [0, 10] 10) +syntax_consts + "_Prod_any" == Prod_any translations "\a. b" == "CONST Prod_any (\a. b)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Monad_Syntax.thy Sun Aug 25 21:27:25 2024 +0100 @@ -46,6 +46,11 @@ "_do_bind" :: "[pttrn, 'a] \ do_bind" ("(2_ <-/ _)" 13) "_thenM" :: "['a, 'b] \ 'c" (infixl ">>" 54) +syntax_consts + "_do_block" "_do_cons" \ bind_do and + "_do_bind" "_thenM" \ bind and + "_do_let" \ Let + translations "_do_block (_do_cons (_do_then t) (_do_final e))" \ "CONST bind_do t (\_. e)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Multiset.thy Sun Aug 25 21:27:25 2024 +0100 @@ -93,6 +93,8 @@ syntax "_multiset" :: "args \ 'a multiset" ("{#(_)#}") +syntax_consts + "_multiset" == add_mset translations "{#x, xs#}" == "CONST add_mset x {#xs#}" "{#x#}" == "CONST add_mset x {#}" @@ -169,6 +171,10 @@ "_MBall" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#_./ _)" [0, 0, 10] 10) "_MBex" :: "pttrn \ 'a set \ bool \ bool" ("(3\_:#_./ _)" [0, 0, 10] 10) +syntax_consts + "_MBall" \ Multiset.Ball and + "_MBex" \ Multiset.Bex + translations "\x\#A. P" \ "CONST Multiset.Ball A (\x. P)" "\x\#A. P" \ "CONST Multiset.Bex A (\x. P)" @@ -1248,6 +1254,8 @@ "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{#_ :# _./ _#})") syntax "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{#_ \# _./ _#})") +syntax_consts + "_MCollect" == filter_mset translations "{#x \# M. P#}" == "CONST filter_mset (\x. P) M" @@ -1821,6 +1829,8 @@ "_comprehension_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ :# _#})") syntax "_comprehension_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ \# _#})") +syntax_consts + "_comprehension_mset" \ image_mset translations "{#e. x \# M#}" \ "CONST image_mset (\x. e) M" @@ -1828,6 +1838,8 @@ "_comprehension_mset'" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ :# _./ _#})") syntax "_comprehension_mset'" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ \# _./ _#})") +syntax_consts + "_comprehension_mset'" \ image_mset translations "{#e | x\#M. P#}" \ "{#e. x \# {# x\#M. P#}#}" @@ -2675,6 +2687,8 @@ "_sum_mset_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10) syntax "_sum_mset_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3\_\#_. _)" [0, 51, 10] 10) +syntax_consts + "_sum_mset_image" \ sum_mset translations "\i \# A. b" \ "CONST sum_mset (CONST image_mset (\i. b) A)" @@ -2854,6 +2868,8 @@ "_prod_mset_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10) syntax "_prod_mset_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" ("(3\_\#_. _)" [0, 51, 10] 10) +syntax_consts + "_prod_mset_image" \ prod_mset translations "\i \# A. b" \ "CONST prod_mset (CONST image_mset (\i. b) A)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Sun Aug 25 21:27:25 2024 +0100 @@ -540,6 +540,10 @@ "_NumeralType0" :: type ("0") "_NumeralType1" :: type ("1") +syntax_types + "_NumeralType0" == num0 and + "_NumeralType1" == num1 + translations (type) "1" == (type) "num1" (type) "0" == (type) "num0" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Phantom_Type.thy --- a/src/HOL/Library/Phantom_Type.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Phantom_Type.thy Sun Aug 25 21:27:25 2024 +0100 @@ -18,6 +18,7 @@ by(simp_all add: o_def id_def) syntax "_Phantom" :: "type \ logic" ("(1Phantom/(1'(_')))") +syntax_consts "_Phantom" == phantom translations "Phantom('t)" => "CONST phantom :: _ \ ('t, _) phantom" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Library/Type_Length.thy --- a/src/HOL/Library/Type_Length.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Library/Type_Length.thy Sun Aug 25 21:27:25 2024 +0100 @@ -19,6 +19,9 @@ syntax "_type_length" :: "type \ nat" (\(1LENGTH/(1'(_')))\) +syntax_consts + "_type_length" \ len_of + translations "LENGTH('a)" \ "CONST len_of (CONST Pure.type :: 'a itself)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/List.thy --- a/src/HOL/List.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/List.thy Sun Aug 25 21:27:25 2024 +0100 @@ -46,6 +46,9 @@ \ \list Enumeration\ "_list" :: "args => 'a list" ("[(_)]") +syntax_consts + "_list" == Cons + translations "[x, xs]" == "x#[xs]" "[x]" == "x#[]" @@ -83,6 +86,8 @@ "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])") syntax "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_\_ ./ _])") +syntax_consts + "_filter" \ filter translations "[x<-xs . P]" \ "CONST filter (\x. P) xs" @@ -132,6 +137,9 @@ "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _") "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [1000,0] 900) +syntax_consts + "_lupdbind" "_lupdbinds" "_LUpdate" == list_update + translations "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" "xs[i:=x]" == "CONST list_update xs i x" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Map.thy --- a/src/HOL/Map.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Map.thy Sun Aug 25 21:27:25 2024 +0100 @@ -67,6 +67,9 @@ syntax (ASCII) "_maplet" :: "['a, 'a] \ maplet" ("_ /|->/ _") +syntax_consts + "_maplet" "_Maplets" "_Map" \ fun_upd + translations "_Update f (_maplet x y)" \ "f(x := CONST Some y)" "_Maplets m ms" \ "_updbinds m ms" @@ -76,6 +79,7 @@ "_Map (_maplet x y)" \ "_Update (\u. CONST None) (_maplet x y)" "_Map (_updbinds m (_maplet x y))" \ "_Update (_Map m) (_maplet x y)" + text \Updating with lists:\ primrec map_of :: "('a \ 'b) list \ 'a \ 'b" where @@ -98,6 +102,9 @@ syntax (ASCII) "_maplets" :: "['a, 'a] \ maplet" ("_ /[|->]/ _") +syntax_consts + "_maplets" \ map_upds + translations "_Update m (_maplets xs ys)" \ "CONST map_upds m xs ys" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Metis_Examples/Message.thy Sun Aug 25 21:27:25 2024 +0100 @@ -50,6 +50,8 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" == MPair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST MPair x y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Orderings.thy Sun Aug 25 21:27:25 2024 +0100 @@ -745,6 +745,10 @@ "_All_neq" :: "[idt, 'a, bool] => bool" ("(3! _~=_./ _)" [0, 0, 10] 10) "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3? _~=_./ _)" [0, 0, 10] 10) +syntax_consts + "_All_less" "_All_less_eq" "_All_greater" "_All_greater_eq" "_All_neq" \ All and + "_Ex_less" "_Ex_less_eq" "_Ex_greater" "_Ex_greater_eq" "_Ex_neq" \ Ex + translations "\x "\x. x < y \ P" "\x "\x. x < y \ P" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Probability/Fin_Map.thy --- a/src/HOL/Probability/Fin_Map.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Probability/Fin_Map.thy Sun Aug 25 21:27:25 2024 +0100 @@ -90,6 +90,8 @@ syntax "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\'' _\_./ _)" 10) +syntax_consts + "_Pi'" == Pi' translations "\' x\A. B" == "CONST Pi' A (\x. B)" @@ -635,6 +637,8 @@ syntax "_PiF" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>F _\_./ _)" 10) +syntax_consts + "_PiF" == PiF translations "\\<^sub>F x\I. M" == "CONST PiF I (%x. M)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Sun Aug 25 21:27:25 2024 +0100 @@ -250,6 +250,9 @@ syntax "_prob" :: "pttrn \ logic \ logic \ logic" (\('\

'((/_ in _./ _)'))\) +syntax_consts + "_prob" == measure + translations "\

(x in M. P)" => "CONST measure M {x \ CONST space M. P}" @@ -322,6 +325,9 @@ syntax "_conditional_prob" :: "pttrn \ logic \ logic \ logic \ logic" (\('\

'(_ in _. _ \/ _'))\) +syntax_consts + "_conditional_prob" == cond_prob + translations "\

(x in M. P \ Q)" => "CONST cond_prob M (\x. P) (\x. Q)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Product_Type.thy Sun Aug 25 21:27:25 2024 +0100 @@ -293,6 +293,10 @@ "" :: "pttrn \ patterns" ("_") "_patterns" :: "pttrn \ patterns \ patterns" ("_,/ _") "_unit" :: pttrn ("'(')") +syntax_consts + "_tuple" "_tuple_arg" "_tuple_args" \ Pair and + "_pattern" "_patterns" \ case_prod and + "_unit" \ case_unit translations "(x, y)" \ "CONST Pair x y" "_pattern x y" \ "CONST Pair x y" @@ -1010,6 +1014,8 @@ syntax "_Sigma" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) +syntax_consts + "_Sigma" \ Sigma translations "SIGMA x:A. B" \ "CONST Sigma A (\x. B)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Aug 25 21:27:25 2024 +0100 @@ -98,6 +98,9 @@ syntax "_insert_fset" :: "args => 'a fset" ("{|(_)|}") +syntax_consts + "_insert_fset" == fcons + translations "{|x, xs|}" == "CONST fcons x {|xs|}" "{|x|}" == "CONST fcons x {||}" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Quotient_Examples/Quotient_FSet.thy --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 25 21:27:25 2024 +0100 @@ -291,6 +291,9 @@ syntax "_insert_fset" :: "args => 'a fset" ("{|(_)|}") +syntax_consts + "_insert_fset" == insert_fset + translations "{|x, xs|}" == "CONST insert_fset x {|xs|}" "{|x|}" == "CONST insert_fset x {||}" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/SET_Protocol/Message_SET.thy Sun Aug 25 21:27:25 2024 +0100 @@ -70,6 +70,8 @@ (*Concrete syntax: messages appear as \\A,B,NA\\, etc...*) syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" == MPair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST MPair x y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/SPARK/SPARK_Setup.thy --- a/src/HOL/SPARK/SPARK_Setup.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/SPARK/SPARK_Setup.thy Sun Aug 25 21:27:25 2024 +0100 @@ -57,6 +57,9 @@ syntax "_updsbind" :: "['a, 'a] => updbind" ("(2_ [:=]/ _)") +syntax_consts + "_updsbind" == fun_upds + translations "f(xs[:=]y)" == "CONST fun_upds f xs y" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Set.thy --- a/src/HOL/Set.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Set.thy Sun Aug 25 21:27:25 2024 +0100 @@ -40,6 +40,8 @@ syntax "_Coll" :: "pttrn \ bool \ 'a set" ("(1{_./ _})") +syntax_consts + "_Coll" \ Collect translations "{x. P}" \ "CONST Collect (\x. P)" @@ -47,6 +49,8 @@ "_Collect" :: "pttrn \ 'a set \ bool \ 'a set" ("(1{(_/: _)./ _})") syntax "_Collect" :: "pttrn \ 'a set \ bool \ 'a set" ("(1{(_/ \ _)./ _})") +syntax_consts + "_Collect" \ Collect translations "{p:A. P}" \ "CONST Collect (\p. p \ A \ P)" @@ -141,6 +145,8 @@ syntax "_Finset" :: "args \ 'a set" ("{(_)}") +syntax_consts + "_Finset" \ insert translations "{x, xs}" \ "CONST insert x {xs}" "{x}" \ "CONST insert x {}" @@ -203,6 +209,12 @@ "_Bex1" :: "pttrn \ 'a set \ bool \ bool" ("(3\!(_/\_)./ _)" [0, 0, 10] 10) "_Bleast" :: "id \ 'a set \ bool \ 'a" ("(3LEAST(_/\_)./ _)" [0, 0, 10] 10) +syntax_consts + "_Ball" \ Ball and + "_Bex" \ Bex and + "_Bex1" \ Ex1 and + "_Bleast" \ Least + translations "\x\A. P" \ "CONST Ball A (\x. P)" "\x\A. P" \ "CONST Bex A (\x. P)" @@ -223,12 +235,17 @@ "_setleEx" :: "[idt, 'a, bool] \ bool" ("(3\_\_./ _)" [0, 0, 10] 10) "_setleEx1" :: "[idt, 'a, bool] \ bool" ("(3\!_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_setlessAll" "_setleAll" \ All and + "_setlessEx" "_setleEx" \ Ex and + "_setleEx1" \ Ex1 + translations - "\A\B. P" \ "\A. A \ B \ P" - "\A\B. P" \ "\A. A \ B \ P" - "\A\B. P" \ "\A. A \ B \ P" - "\A\B. P" \ "\A. A \ B \ P" - "\!A\B. P" \ "\!A. A \ B \ P" + "\A\B. P" \ "\A. A \ B \ P" + "\A\B. P" \ "\A. A \ B \ P" + "\A\B. P" \ "\A. A \ B \ P" + "\A\B. P" \ "\A. A \ B \ P" + "\!A\B. P" \ "\!A. A \ B \ P" print_translation \ let @@ -272,6 +289,8 @@ syntax "_Setcompr" :: "'a \ idts \ bool \ 'a set" ("(1{_ |/_./ _})") +syntax_consts + "_Setcompr" \ Collect parse_translation \ let diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Set_Interval.thy Sun Aug 25 21:27:25 2024 +0100 @@ -84,6 +84,10 @@ "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) +syntax_consts + "_UNION_le" "_UNION_less" \ Union and + "_INTER_le" "_INTER_less" \ Inter + translations "\i\n. A" \ "\i\{..n}. A" "\i "\i\{.. 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) +syntax_consts + "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum + translations "\x=a..b. t" == "CONST sum (\x. t) {a..b}" "\x=a..x. t) {a.. 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) +syntax_consts + "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \ prod + translations "\x=a..b. t" \ "CONST prod (\x. t) {a..b}" "\x=a.. "CONST prod (\x. t) {a.. char" ("CHR _") "_Char_ord" :: "num_const \ char" ("CHR _") +syntax_consts + "_Char" "_Char_ord" \ Char type_synonym string = "char list" @@ -522,6 +524,8 @@ syntax "_Literal" :: "str_position \ String.literal" ("STR _") "_Ascii" :: "num_const \ String.literal" ("STR _") +syntax_consts + "_Literal" "_Ascii" \ String.Literal ML_file \Tools/literal.ML\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/Typerep.thy Sun Aug 25 21:27:25 2024 +0100 @@ -19,6 +19,8 @@ syntax "_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))") +syntax_consts + "_TYPEREP" \ typerep parse_translation \ let diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/UNITY/PPROD.thy Sun Aug 25 21:27:25 2024 +0100 @@ -16,6 +16,8 @@ syntax "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set" ("(3plam _:_./ _)" 10) +syntax_consts + "_PLam" == PLam translations "plam x : A. B" == "CONST PLam A (%x. B)" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/UNITY/Union.thy Sun Aug 25 21:27:25 2024 +0100 @@ -41,6 +41,8 @@ syntax "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\_./ _)" 10) "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\_\_./ _)" 10) +syntax_consts + "_JOIN1" "_JOIN" == JOIN translations "\x \ A. B" == "CONST JOIN A (\x. B)" "\x y. B" == "\x. \y. B" diff -r 77f7aa898ced -r fe7ffe7eb265 src/HOL/ex/Code_Lazy_Demo.thy --- a/src/HOL/ex/Code_Lazy_Demo.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/HOL/ex/Code_Lazy_Demo.thy Sun Aug 25 21:27:25 2024 +0100 @@ -40,6 +40,7 @@ | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65) syntax "_llist" :: "args => 'a list" ("\<^bold>\(_)\<^bold>\") +syntax_consts "_llist" == LCons translations "\<^bold>\x, xs\<^bold>\" == "x###\<^bold>\xs\<^bold>\" "\<^bold>\x\<^bold>\" == "x###\<^bold>\\<^bold>\" diff -r 77f7aa898ced -r fe7ffe7eb265 src/Pure/Examples/Higher_Order_Logic.thy --- a/src/Pure/Examples/Higher_Order_Logic.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/Pure/Examples/Higher_Order_Logic.thy Sun Aug 25 21:27:25 2024 +0100 @@ -402,6 +402,7 @@ where someI: "P x \ P (Eps P)" syntax "_Eps" :: "pttrn \ o \ 'a" ("(3SOME _./ _)" [0, 10] 10) +syntax_consts "_Eps" \ Eps translations "SOME x. P" \ "CONST Eps (\x. P)" text \ diff -r 77f7aa898ced -r fe7ffe7eb265 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Aug 25 17:24:42 2024 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sun Aug 25 21:27:25 2024 +0100 @@ -135,11 +135,11 @@ in Sign.syntax_deps (maps check args) thy end; fun check_const ctxt (s, pos) = - Proof_Context.check_const {proper = false, strict = true} ctxt (s, [pos]) + Proof_Context.check_const {proper = true, strict = false} ctxt (s, [pos]) |>> (Term.dest_Const_name #> Lexicon.mark_const); fun check_type_name ctxt arg = - Proof_Context.check_type_name {proper = false, strict = true} ctxt arg + Proof_Context.check_type_name {proper = true, strict = false} ctxt arg |>> (Term.dest_Type_name #> Lexicon.mark_type); in diff -r 77f7aa898ced -r fe7ffe7eb265 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Aug 25 17:24:42 2024 +0100 +++ b/src/Pure/Syntax/syntax.ML Sun Aug 25 21:27:25 2024 +0100 @@ -442,7 +442,9 @@ | NONE => Printer.get_binder prtabs c) |> Option.map Prefix); -fun is_const (Syntax ({consts, ...}, _)) = Graph.defined consts; +fun is_const (Syntax ({consts, ...}, _)) c = + Graph.defined consts c andalso not (Lexicon.is_marked c); + fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram); diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/Bin.thy --- a/src/ZF/Bin.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/Bin.thy Sun Aug 25 21:27:25 2024 +0100 @@ -117,10 +117,11 @@ "_Int" :: "num_token \ i" (\#_\ 1000) "_Neg_Int" :: "num_token \ i" (\#-_\ 1000) +syntax_consts + "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \ integ_of + ML_file \Tools/numeral_syntax.ML\ -syntax_consts - "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \ integ_of declare bin.intros [simp,TC] diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/Induct/Multiset.thy --- a/src/ZF/Induct/Multiset.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/Induct/Multiset.thy Sun Aug 25 21:27:25 2024 +0100 @@ -75,9 +75,9 @@ syntax "_MColl" :: "[pttrn, i, o] \ i" (\(1{# _ \ _./ _#})\) +syntax_consts "_MColl" \ MCollect translations "{#x \ M. P#}" == "CONST MCollect(M, \x. P)" -syntax_consts "_MColl" \ MCollect (* multiset orderings *) diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/List.thy --- a/src/ZF/List.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/List.thy Sun Aug 25 21:27:25 2024 +0100 @@ -17,11 +17,11 @@ syntax "_Nil" :: i (\[]\) "_List" :: "is \ i" (\[(_)]\) +syntax_consts "_List" \ Cons translations "[x, xs]" == "CONST Cons(x, [xs])" "[x]" == "CONST Cons(x, [])" "[]" == "CONST Nil" -syntax_consts "_List" \ Cons consts length :: "i\i" diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/OrdQuant.thy Sun Aug 25 21:27:25 2024 +0100 @@ -26,14 +26,14 @@ "_oall" :: "[idt, i, o] \ o" (\(3\_<_./ _)\ 10) "_oex" :: "[idt, i, o] \ o" (\(3\_<_./ _)\ 10) "_OUNION" :: "[idt, i, i] \ i" (\(3\_<_./ _)\ 10) +syntax_consts + "_oall" \ oall and + "_oex" \ oex and + "_OUNION" \ OUnion translations "\x "CONST oall(a, \x. P)" "\x "CONST oex(a, \x. P)" "\x "CONST OUnion(a, \x. B)" -syntax_consts - "_oall" \ oall and - "_oex" \ oex and - "_OUNION" \ OUnion subsubsection \simplification of the new quantifiers\ @@ -198,12 +198,12 @@ syntax "_rall" :: "[pttrn, i\o, o] \ o" (\(3\_[_]./ _)\ 10) "_rex" :: "[pttrn, i\o, o] \ o" (\(3\_[_]./ _)\ 10) +syntax_consts + "_rall" \ rall and + "_rex" \ rex translations "\x[M]. P" \ "CONST rall(M, \x. P)" "\x[M]. P" \ "CONST rex(M, \x. P)" -syntax_consts - "_rall" \ rall and - "_rex" \ rex subsubsection\Relativized universal quantifier\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/QPair.thy Sun Aug 25 21:27:25 2024 +0100 @@ -46,10 +46,10 @@ syntax "_QSUM" :: "[idt, i, i] \ i" (\(3QSUM _ \ _./ _)\ 10) +syntax_consts + "_QSUM" \ QSigma translations "QSUM x \ A. B" => "CONST QSigma(A, \x. B)" -syntax_consts - "_QSUM" \ QSigma abbreviation qprod (infixr \<*>\ 80) where diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/UNITY/Union.thy --- a/src/ZF/UNITY/Union.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/UNITY/Union.thy Sun Aug 25 21:27:25 2024 +0100 @@ -43,12 +43,12 @@ syntax "_JOIN1" :: "[pttrns, i] \ i" (\(3\_./ _)\ 10) "_JOIN" :: "[pttrn, i, i] \ i" (\(3\_ \ _./ _)\ 10) +syntax_consts + "_JOIN1" "_JOIN" == JOIN translations "\x \ A. B" == "CONST JOIN(A, (\x. B))" "\x y. B" == "\x. \y. B" "\x. B" == "CONST JOIN(CONST state, (\x. B))" -syntax_consts - "_JOIN1" "_JOIN" == JOIN subsection\SKIP\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/ZF_Base.thy --- a/src/ZF/ZF_Base.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/ZF_Base.thy Sun Aug 25 21:27:25 2024 +0100 @@ -38,12 +38,12 @@ syntax "_Ball" :: "[pttrn, i, o] \ o" (\(3\_\_./ _)\ 10) "_Bex" :: "[pttrn, i, o] \ o" (\(3\_\_./ _)\ 10) +syntax_consts + "_Ball" \ Ball and + "_Bex" \ Bex translations "\x\A. P" \ "CONST Ball(A, \x. P)" "\x\A. P" \ "CONST Bex(A, \x. P)" -syntax_consts - "_Ball" \ Ball and - "_Bex" \ Bex subsection \Variations on Replacement\ @@ -56,10 +56,10 @@ syntax "_Replace" :: "[pttrn, pttrn, i, o] \ i" (\(1{_ ./ _ \ _, _})\) +syntax_consts + "_Replace" \ Replace translations "{y. x\A, Q}" \ "CONST Replace(A, \x y. Q)" -syntax_consts - "_Replace" \ Replace (* Functional form of replacement -- analgous to ML's map functional *) @@ -69,10 +69,10 @@ syntax "_RepFun" :: "[i, pttrn, i] \ i" (\(1{_ ./ _ \ _})\ [51,0,51]) +syntax_consts + "_RepFun" \ RepFun translations "{b. x\A}" \ "CONST RepFun(A, \x. b)" -syntax_consts - "_RepFun" \ RepFun (* Separation and Pairing can be derived from the Replacement and Powerset Axioms using the following definitions. *) @@ -81,10 +81,10 @@ syntax "_Collect" :: "[pttrn, i, o] \ i" (\(1{_ \ _ ./ _})\) +syntax_consts + "_Collect" \ Collect translations "{x\A. P}" \ "CONST Collect(A, \x. P)" -syntax_consts - "_Collect" \ Collect subsection \General union and intersection\ @@ -95,12 +95,12 @@ syntax "_UNION" :: "[pttrn, i, i] \ i" (\(3\_\_./ _)\ 10) "_INTER" :: "[pttrn, i, i] \ i" (\(3\_\_./ _)\ 10) +syntax_consts + "_UNION" == Union and + "_INTER" == Inter translations "\x\A. B" == "CONST Union({B. x\A})" "\x\A. B" == "CONST Inter({B. x\A})" -syntax_consts - "_UNION" == Union and - "_INTER" == Inter subsection \Finite sets and binary operations\ @@ -134,11 +134,11 @@ "" :: "i \ is" (\_\) "_Enum" :: "[i, is] \ is" (\_,/ _\) "_Finset" :: "is \ i" (\{(_)}\) +syntax_consts + "_Finset" == cons translations "{x, xs}" == "CONST cons(x, {xs})" "{x}" == "CONST cons(x, 0)" -syntax_consts - "_Finset" == cons subsection \Axioms\ @@ -199,14 +199,14 @@ "" :: "pttrn \ patterns" (\_\) "_patterns" :: "[pttrn, patterns] \ patterns" (\_,/_\) "_Tuple" :: "[i, is] \ i" (\\(_,/ _)\\) +syntax_consts + "_pattern" "_patterns" == split and + "_Tuple" == Pair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST Pair(x, y)" "\\x,y,zs\.b" == "CONST split(\x \y,zs\.b)" "\\x,y\.b" == "CONST split(\x y. b)" -syntax_consts - "_pattern" "_patterns" == split and - "_Tuple" == Pair definition Sigma :: "[i, i \ i] \ i" where "Sigma(A,B) \ \x\A. \y\B(x). {\x,y\}" @@ -268,14 +268,14 @@ "_PROD" :: "[pttrn, i, i] \ i" (\(3\_\_./ _)\ 10) "_SUM" :: "[pttrn, i, i] \ i" (\(3\_\_./ _)\ 10) "_lam" :: "[pttrn, i, i] \ i" (\(3\_\_./ _)\ 10) +syntax_consts + "_PROD" == Pi and + "_SUM" == Sigma and + "_lam" == Lambda translations "\x\A. B" == "CONST Pi(A, \x. B)" "\x\A. B" == "CONST Sigma(A, \x. B)" "\x\A. f" == "CONST Lambda(A, \x. f)" -syntax_consts - "_PROD" == Pi and - "_SUM" == Sigma and - "_lam" == Lambda subsection \ASCII syntax\ diff -r 77f7aa898ced -r fe7ffe7eb265 src/ZF/func.thy --- a/src/ZF/func.thy Sun Aug 25 17:24:42 2024 +0100 +++ b/src/ZF/func.thy Sun Aug 25 21:27:25 2024 +0100 @@ -452,10 +452,10 @@ "" :: "updbind \ updbinds" (\_\) "_updbinds" :: "[updbind, updbinds] \ updbinds" (\_,/ _\) "_Update" :: "[i, updbinds] \ i" (\_/'((_)')\ [900,0] 900) +syntax_consts "_Update" "_updbind" \ update translations "_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)" "f(x:=y)" == "CONST update(f,x,y)" -syntax_consts "_Update" "_updbind" \ update lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)" apply (simp add: update_def)