# HG changeset patch # User wenzelm # Date 1164560836 -3600 # Node ID 7843e2fd14a94449c407be542a7414e29c5449a0 # Parent a267ecd51f90f25e6277b16b67f0e3351bcdf74e updated (binder) syntax/notation; diff -r a267ecd51f90 -r 7843e2fd14a9 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/CTT/CTT.thy Sun Nov 26 18:07:16 2006 +0100 @@ -72,25 +72,25 @@ "A * B == SUM _:A. B" notation (xsymbols) + lambda (binder "\\" 10) and Elem ("(_ /\ _)" [10,10] 5) and Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and Arrow (infixr "\" 30) and Times (infixr "\" 50) notation (HTML output) + lambda (binder "\\" 10) and Elem ("(_ /\ _)" [10,10] 5) and Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and Times (infixr "\" 50) syntax (xsymbols) - "@SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "@PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "lam " :: "[idts, i] => i" ("(3\\_./ _)" 10) + "_PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "_SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) syntax (HTML output) - "@SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "@PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "lam " :: "[idts, i] => i" ("(3\\_./ _)" 10) + "_PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "_SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) axioms diff -r a267ecd51f90 -r 7843e2fd14a9 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/FOL/IFOL.thy Sun Nov 26 18:07:16 2006 +0100 @@ -54,24 +54,23 @@ notation (HTML output) not_equal (infixl "\" 50) -syntax (xsymbols) - Not :: "o => o" ("\ _" [40] 40) - "op &" :: "[o, o] => o" (infixr "\" 35) - "op |" :: "[o, o] => o" (infixr "\" 30) - "ALL " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX! " :: "[idts, o] => o" ("(3\!_./ _)" [0, 10] 10) - "op -->" :: "[o, o] => o" (infixr "\" 25) - "op <->" :: "[o, o] => o" (infixr "\" 25) +notation (xsymbols) + Not ("\ _" [40] 40) and + "op &" (infixr "\" 35) and + "op |" (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) and + "op -->" (infixr "\" 25) and + "op <->" (infixr "\" 25) -syntax (HTML output) - Not :: "o => o" ("\ _" [40] 40) - "op &" :: "[o, o] => o" (infixr "\" 35) - "op |" :: "[o, o] => o" (infixr "\" 30) - "ALL " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX! " :: "[idts, o] => o" ("(3\!_./ _)" [0, 10] 10) - +notation (HTML output) + Not ("\ _" [40] 40) and + "op &" (infixr "\" 35) and + "op |" (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) local diff -r a267ecd51f90 -r 7843e2fd14a9 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/HOL/HOL.thy Sun Nov 26 18:07:16 2006 +0100 @@ -115,21 +115,22 @@ *} syntax (xsymbols) - "ALL " :: "[idts, bool] => bool" ("(3\_./ _)" [0, 10] 10) - "EX " :: "[idts, bool] => bool" ("(3\_./ _)" [0, 10] 10) - "EX! " :: "[idts, bool] => bool" ("(3\!_./ _)" [0, 10] 10) "_case1" :: "['a, 'b] => case_syn" ("(2_ \/ _)" 10) -(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \ _")*) + +notation (xsymbols) + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) -syntax (HTML output) - "ALL " :: "[idts, bool] => bool" ("(3\_./ _)" [0, 10] 10) - "EX " :: "[idts, bool] => bool" ("(3\_./ _)" [0, 10] 10) - "EX! " :: "[idts, bool] => bool" ("(3\!_./ _)" [0, 10] 10) +notation (HTML output) + All (binder "\" 10) and + Ex (binder "\" 10) and + Ex1 (binder "\!" 10) -syntax (HOL) - "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) - "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) - "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) +notation (HOL) + All (binder "! " 10) and + Ex (binder "? " 10) and + Ex1 (binder "?! " 10) subsubsection {* Axioms and basic definitions *} @@ -179,27 +180,35 @@ subsubsection {* Generic algebraic operations *} class zero = - fixes zero :: "'a" ("\<^loc>0") + fixes zero :: "'a" ("\<^loc>0") class one = - fixes one :: "'a" ("\<^loc>1") + fixes one :: "'a" ("\<^loc>1") hide (open) const zero one class plus = - fixes plus :: "'a \ 'a \ 'a" (infixl "\<^loc>+" 65) + fixes plus :: "'a \ 'a \ 'a" (infixl "\<^loc>+" 65) class minus = fixes uminus :: "'a \ 'a" - fixes minus :: "'a \ 'a \ 'a" (infixl "\<^loc>-" 65) - fixes abs :: "'a \ 'a" + and minus :: "'a \ 'a \ 'a" (infixl "\<^loc>-" 65) + and abs :: "'a \ 'a" class times = fixes times :: "'a \ 'a \ 'a" (infixl "\<^loc>*" 70) class inverse = fixes inverse :: "'a \ 'a" - fixes divide :: "'a \ 'a \ 'a" (infixl "\<^loc>'/" 70) + and divide :: "'a \ 'a \ 'a" (infixl "\<^loc>'/" 70) + +notation + uminus ("- _" [81] 80) + +notation (xsymbols) + abs ("\_\") +notation (HTML output) + abs ("\_\") syntax "_index1" :: index ("\<^sub>1") @@ -215,14 +224,6 @@ in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end; *} -- {* show types that are presumably too general *} -notation - uminus ("- _" [81] 80) - -notation (xsymbols) - abs ("\_\") -notation (HTML output) - abs ("\_\") - subsection {* Fundamental rules *} diff -r a267ecd51f90 -r 7843e2fd14a9 src/HOL/Modelcheck/EindhovenSyn.thy --- a/src/HOL/Modelcheck/EindhovenSyn.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Sun Nov 26 18:07:16 2006 +0100 @@ -16,8 +16,8 @@ "op &" :: "[bool, bool] => bool" (infixr "AND" 35) "op |" :: "[bool, bool] => bool" (infixr "OR" 30) - "ALL " :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10) - "EX " :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10) + All_binder :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10) + Ex_binder :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10) "_lambda" :: "[pttrns, 'a] => 'b" ("(3L _./ _)" 10) "_idts" :: "[idt, idts] => idts" ("_,/_" [1, 0] 0) diff -r a267ecd51f90 -r 7843e2fd14a9 src/HOL/Modelcheck/MuckeSyn.thy --- a/src/HOL/Modelcheck/MuckeSyn.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Sun Nov 26 18:07:16 2006 +0100 @@ -29,8 +29,8 @@ "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) "_not_equal" :: "['a, 'a] => bool" ("(_ !=/ _)" [51, 51] 50) - "ALL " :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10) - "EX " :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10) + All_binder :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10) + Ex_binder :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10) "_lambda" :: "[idts, 'a] => 'b" ("(3L _./ _)" 10) "_applC" :: "[('b => 'a), cargs] => aprop" ("(1_/ '(_'))" [1000,1000] 999) diff -r a267ecd51f90 -r 7843e2fd14a9 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/HOL/Orderings.thy Sun Nov 26 18:07:16 2006 +0100 @@ -547,16 +547,19 @@ print_translation {* let val syntax_name = Sign.const_syntax_name (the_context ()); + val binder_name = Syntax.binder_name o syntax_name; + val All_binder = binder_name "All"; + val Ex_binder = binder_name "Ex"; val impl = syntax_name "op -->"; val conj = syntax_name "op &"; val less = syntax_name "Orderings.less"; val less_eq = syntax_name "Orderings.less_eq"; val trans = - [(("ALL ", impl, less), ("_All_less", "_All_greater")), - (("ALL ", impl, less_eq), ("_All_less_eq", "_All_greater_eq")), - (("EX ", conj, less), ("_Ex_less", "_Ex_greater")), - (("EX ", conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; + [((All_binder, impl, less), ("_All_less", "_All_greater")), + ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), + ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")), + ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; fun mk v v' c n P = if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n) @@ -572,7 +575,7 @@ | (n, Const ("_bound", _) $ Free (v', _)) => mk v v' g n P | _ => raise Match)) | _ => raise Match); -in [tr' "ALL ", tr' "EX "] end +in [tr' All_binder, tr' Ex_binder] end *} diff -r a267ecd51f90 -r 7843e2fd14a9 src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/HOL/Set.thy Sun Nov 26 18:07:16 2006 +0100 @@ -249,7 +249,7 @@ then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P else raise Match) in -[("ALL ", all_tr'), ("EX ", ex_tr')] +[("All_binder", all_tr'), ("Ex_binder", ex_tr')] end *} diff -r a267ecd51f90 -r 7843e2fd14a9 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/HOLCF/Porder.thy Sun Nov 26 18:07:16 2006 +0100 @@ -87,14 +87,13 @@ lub :: "'a set \ 'a::po" "lub S \ THE x. S <<| x" -syntax - "@LUB" :: "('b \ 'a) \ 'a" (binder "LUB " 10) +abbreviation + Lub (binder "LUB " 10) where + "LUB n. t n == lub (range t)" -syntax (xsymbols) - "LUB " :: "[idts, 'a] \ 'a" ("(3\_./ _)" [0,10] 10) +notation (xsymbols) + Lub (binder "\ " 10) -translations - "\n. t" == "lub(CONST range(\n. t))" text {* lubs are unique *} diff -r a267ecd51f90 -r 7843e2fd14a9 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Nov 24 22:05:19 2006 +0100 +++ b/src/Pure/pure_thy.ML Sun Nov 26 18:07:16 2006 +0100 @@ -569,12 +569,12 @@ ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", "[tid, sort] => type", Mixfix ("_\\_", [1000, 0], 1000)), ("_constrain", "['a, type] => 'a", Mixfix ("_\\_", [4, 0], 3)), - ("_idtyp", "[id, type] => idt", Mixfix ("_\\_", [], 0)), + ("_idtyp", "[id, type] => idt", Mixfix ("_\\_", [], 0)), ("_idtypdummy", "type => idt", Mixfix ("'_()\\_", [], 0)), ("_type_constraint_", "'a", NoSyn), ("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), ("==", "['a, 'a] => prop", InfixrName ("\\", 2)), - ("!!", "[idts, prop] => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), + ("all_binder", "[idts, prop] => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), ("==>", "[prop, prop] => prop", InfixrName ("\\", 1)), ("_DDDOT", "aprop", Delimfix "\\"), ("_bigimpl", "[asms, prop] => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), diff -r a267ecd51f90 -r 7843e2fd14a9 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/Sequents/LK0.thy Sun Nov 26 18:07:16 2006 +0100 @@ -20,7 +20,7 @@ consts - Trueprop :: "two_seqi" + Trueprop :: "two_seqi" True :: o False :: o @@ -50,18 +50,16 @@ "op |" :: "[o, o] => o" (infixr "\" 30) "op -->" :: "[o, o] => o" (infixr "\" 25) "op <->" :: "[o, o] => o" (infixr "\" 25) - "ALL " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX! " :: "[idts, o] => o" ("(3\!_./ _)" [0, 10] 10) + All_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) + Ex_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) "_not_equal" :: "['a, 'a] => o" (infixl "\" 50) syntax (HTML output) Not :: "o => o" ("\ _" [40] 40) "op &" :: "[o, o] => o" (infixr "\" 35) "op |" :: "[o, o] => o" (infixr "\" 30) - "ALL " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX " :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - "EX! " :: "[idts, o] => o" ("(3\!_./ _)" [0, 10] 10) + All_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) + Ex_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) "_not_equal" :: "['a, 'a] => o" (infixl "\" 50) local diff -r a267ecd51f90 -r 7843e2fd14a9 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Fri Nov 24 22:05:19 2006 +0100 +++ b/src/ZF/Cardinal.thy Sun Nov 26 18:07:16 2006 +0100 @@ -33,15 +33,16 @@ Card :: "i=>o" "Card(i) == (i = |i|)" -syntax (xsymbols) - "eqpoll" :: "[i,i] => o" (infixl "\" 50) - "lepoll" :: "[i,i] => o" (infixl "\" 50) - "lesspoll" :: "[i,i] => o" (infixl "\" 50) - "LEAST " :: "[pttrn, o] => i" ("(3\_./ _)" [0, 10] 10) +notation (xsymbols) + eqpoll (infixl "\" 50) and + lepoll (infixl "\" 50) and + lesspoll (infixl "\" 50) and + Least (binder "\" 10) -syntax (HTML output) - "eqpoll" :: "[i,i] => o" (infixl "\" 50) - "LEAST " :: "[pttrn, o] => i" ("(3\_./ _)" [0, 10] 10) +notation (HTML output) + eqpoll (infixl "\" 50) and + Least (binder "\" 10) + subsection{*The Schroeder-Bernstein Theorem*} text{*See Davey and Priestly, page 106*}