# HG changeset patch # User wenzelm # Date 1267045790 -3600 # Node ID 613e133966ea02d9d93cebfb064a32a43cb2a674 # Parent 2e8dc3c6443015e6b782ccc797d0a668b265711a modernized syntax declarations, and make them actually work with authentic syntax; diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/Algebra/Congruence.thy Wed Feb 24 22:09:50 2010 +0100 @@ -35,15 +35,17 @@ eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\ _") "is_closed A == (A \ carrier S \ closure_of A = A)" -syntax +abbreviation not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50) - not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) - set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50) + where "x .\\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)" -translations - "x .\\ y" == "~(x .=\ y)" - "x .\\ A" == "~(x .\\ A)" - "A {.\}\ B" == "~(A {.=}\ B)" +abbreviation + not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) + where "x .\\<^bsub>S\<^esub> A == ~(x .\\<^bsub>S\<^esub> A)" + +abbreviation + set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50) + where "A {.\}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)" locale equivalence = fixes S (structure) diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/Bali/Basis.thy Wed Feb 24 22:09:50 2010 +0100 @@ -222,12 +222,12 @@ section "quantifiers for option type" syntax - Oall :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) - Oex :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10) + "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) + "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10) syntax (symbols) - Oall :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) - Oex :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) + "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) + "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) translations "! x:A: P" == "! x:CONST Option.set A. P" diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/Bali/Table.thy Wed Feb 24 22:09:50 2010 +0100 @@ -37,11 +37,9 @@ section "map of / table of" -syntax - table_of :: "('a \ 'b) list \ ('a, 'b) table" --{* concrete table *} - abbreviation - "table_of \ map_of" + table_of :: "('a \ 'b) list \ ('a, 'b) table" --{* concrete table *} + where "table_of \ map_of" translations (type)"'a \ 'b" <= (type)"'a \ 'b Datatype.option" diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:09:50 2010 +0100 @@ -60,9 +60,8 @@ ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q" -syntax (xsymbols) - Valid :: "'a bexp => 'a com => 'a bexp => bool" - ("(3\ _/ (2_)/ _)" [100, 55, 100] 50) +notation (xsymbols) + Valid ("(3\ _/ (2_)/ _)" [100, 55, 100] 50) lemma ValidI [intro?]: "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q" diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 22:09:50 2010 +0100 @@ -66,9 +66,8 @@ | Some x \ frs = []" -syntax (xsymbols) - correct_state :: "[jvm_prog,prog_type,jvm_state] \ bool" - ("_,_ \JVM _ \" [51,51] 50) +notation (xsymbols) + correct_state ("_,_ \JVM _ \" [51,51] 50) lemma sup_ty_opt_OK: diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/BV/JVMType.thy --- a/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 22:09:50 2010 +0100 @@ -59,15 +59,11 @@ "sup_state_opt G == Opt.le (sup_state G)" -syntax (xsymbols) - sup_ty_opt :: "['code prog,ty err,ty err] \ bool" - ("_ \ _ <=o _" [71,71] 70) - sup_loc :: "['code prog,locvars_type,locvars_type] \ bool" - ("_ \ _ <=l _" [71,71] 70) - sup_state :: "['code prog,state_type,state_type] \ bool" - ("_ \ _ <=s _" [71,71] 70) - sup_state_opt :: "['code prog,state_type option,state_type option] \ bool" - ("_ \ _ <=' _" [71,71] 70) +notation (xsymbols) + sup_ty_opt ("_ \ _ <=o _" [71,71] 70) and + sup_loc ("_ \ _ <=l _" [71,71] 70) and + sup_state ("_ \ _ <=s _" [71,71] 70) and + sup_state_opt ("_ \ _ <=' _" [71,71] 70) lemma JVM_states_unfold: diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/Comp/TranslCompTp.thy --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:09:50 2010 +0100 @@ -19,9 +19,8 @@ comb_nil :: "'a \ 'b list \ 'a" "comb_nil a == ([], a)" -syntax (xsymbols) - "comb" :: "['a \ 'b list \ 'c, 'c \ 'b list \ 'd, 'a] \ 'b list \ 'd" - (infixr "\" 55) +notation (xsymbols) + comb (infixr "\" 55) lemma comb_nil_left [simp]: "comb_nil \ f = f" by (simp add: comb_def comb_nil_def split_beta) diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/DFA/Semilat.thy --- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 22:09:50 2010 +0100 @@ -32,16 +32,19 @@ "lesssub" ("(_ /\\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and "plussub" ("(_ /\\<^bsub>_\<^esub> _)" [65, 0, 66] 65) (*<*) -syntax - (* allow \ instead of \..\ *) - "_lesub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) - "_lesssub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) - "_plussub" :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /\\<^sub>_ _)" [65, 1000, 66] 65) +(* allow \ instead of \..\ *) + +abbreviation (input) + lesub1 :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) + where "x \\<^sub>r y == x \\<^bsub>r\<^esub> y" -translations - "x \\<^sub>r y" => "x \\<^bsub>r\<^esub> y" - "x \\<^sub>r y" => "x \\<^bsub>r\<^esub> y" - "x \\<^sub>f y" => "x \\<^bsub>f\<^esub> y" +abbreviation (input) + lesssub1 :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) + where "x \\<^sub>r y == x \\<^bsub>r\<^esub> y" + +abbreviation (input) + plussub1 :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /\\<^sub>_ _)" [65, 1000, 66] 65) + where "x \\<^sub>f y == x \\<^bsub>f\<^esub> y" (*>*) defs diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 22:09:50 2010 +0100 @@ -38,24 +38,13 @@ xconf (heap (store s)) (abrupt s)" -syntax (xsymbols) - hext :: "aheap => aheap => bool" - ("_ \| _" [51,51] 50) - - conf :: "'c prog => aheap => val => ty => bool" - ("_,_ \ _ ::\ _" [51,51,51,51] 50) - - lconf :: "'c prog => aheap => ('a \ val) => ('a \ ty) => bool" - ("_,_ \ _ [::\] _" [51,51,51,51] 50) - - oconf :: "'c prog => aheap => obj => bool" - ("_,_ \ _ \" [51,51,51] 50) - - hconf :: "'c prog => aheap => bool" - ("_ \h _ \" [51,51] 50) - - conforms :: "state => java_mb env' => bool" - ("_ ::\ _" [51,51] 50) +notation (xsymbols) + hext ("_ \| _" [51,51] 50) and + conf ("_,_ \ _ ::\ _" [51,51,51,51] 50) and + lconf ("_,_ \ _ [::\] _" [51,51,51,51] 50) and + oconf ("_,_ \ _ \" [51,51,51] 50) and + hconf ("_ \h _ \" [51,51] 50) and + conforms ("_ ::\ _" [51,51] 50) section "hext" diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/JVM/JVMDefensive.thy --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 22:09:50 2010 +0100 @@ -123,19 +123,15 @@ | Normal s' \ if check G s' then Normal (exec (G, s')) else TypeError" -consts - "exec_all_d" :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" +constdefs + exec_all_d :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" ("_ |- _ -jvmd-> _" [61,61,61]60) + "G |- s -jvmd-> t \ + (s,t) \ ({(s,t). exec_d G s = TypeError \ t = TypeError} \ + {(s,t). \t'. exec_d G s = Normal (Some t') \ t = Normal t'})\<^sup>*" -syntax (xsymbols) - "exec_all_d" :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" - ("_ \ _ -jvmd\ _" [61,61,61]60) - -defs - exec_all_d_def: - "G \ s -jvmd\ t \ - (s,t) \ ({(s,t). exec_d G s = TypeError \ t = TypeError} \ - {(s,t). \t'. exec_d G s = Normal (Some t') \ t = Normal t'})\<^sup>*" +notation (xsymbols) + exec_all_d ("_ \ _ -jvmd\ _" [61,61,61]60) declare split_paired_All [simp del] diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/MicroJava/JVM/JVMExec.thy --- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 22:09:50 2010 +0100 @@ -32,9 +32,8 @@ "G |- s -jvm-> t == (s,t) \ {(s,t). exec(G,s) = Some t}^*" -syntax (xsymbols) - exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" - ("_ \ _ -jvm\ _" [61,61,61]60) +notation (xsymbols) + exec_all ("_ \ _ -jvm\ _" [61,61,61]60) text {* The start configuration of the JVM: in the start heap, we call a diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 22:09:50 2010 +0100 @@ -33,14 +33,14 @@ cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60) "A ||=e t \ \n. ||=n: A --> |=n:e t" -syntax (xsymbols) - valid :: "[assn,stmt, assn] => bool" ( "\ {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - evalid :: "[assn,expr,vassn] => bool" ("\\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - nvalid :: "[nat, triple ] => bool" ("\_: _" [61,61] 60) - envalid :: "[nat,etriple ] => bool" ("\_:\<^sub>e _" [61,61] 60) - nvalids :: "[nat, triple set] => bool" ("|\_: _" [61,61] 60) - cnvalids :: "[triple set,triple set] => bool" ("_ |\/ _" [61,61] 60) -cenvalid :: "[triple set,etriple ] => bool" ("_ |\\<^sub>e/ _"[61,61] 60) +notation (xsymbols) + valid ("\ {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and + evalid ("\\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and + nvalid ("\_: _" [61,61] 60) and + envalid ("\_:\<^sub>e _" [61,61] 60) and + nvalids ("|\_: _" [61,61] 60) and + cnvalids ("_ |\/ _" [61,61] 60) and + cenvalid ("_ |\\<^sub>e/ _"[61,61] 60) lemma nvalid_def2: "\n: (P,c,Q) \ \s t. s -c-n\ t \ P s \ Q t" @@ -164,10 +164,10 @@ "MGT c Z \ (\s. Z = s, c, \ t. \n. Z -c- n\ t)" MGTe :: "expr => state => etriple" "MGTe e Z \ (\s. Z = s, e, \v t. \n. Z -e\v-n\ t)" -syntax (xsymbols) - MGTe :: "expr => state => etriple" ("MGT\<^sub>e") -syntax (HTML output) - MGTe :: "expr => state => etriple" ("MGT\<^sub>e") +notation (xsymbols) + MGTe ("MGT\<^sub>e") +notation (HTML output) + MGTe ("MGT\<^sub>e") lemma MGF_implies_complete: "\Z. {} |\ { MGT c Z} \ \ {P} c {Q} \ {} \ {P} c {Q}" diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/NanoJava/State.thy --- a/src/HOL/NanoJava/State.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/NanoJava/State.thy Wed Feb 24 22:09:50 2010 +0100 @@ -84,9 +84,9 @@ lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000) "lupd x v s \ s (| locals := ((locals s)(x\v ))|)" -syntax (xsymbols) - hupd :: "loc => obj => state => state" ("hupd'(_\_')" [10,10] 1000) - lupd :: "vname => val => state => state" ("lupd'(_\_')" [10,10] 1000) +notation (xsymbols) + hupd ("hupd'(_\_')" [10,10] 1000) and + lupd ("lupd'(_\_')" [10,10] 1000) constdefs diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Wed Feb 24 22:09:50 2010 +0100 @@ -17,8 +17,8 @@ LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) "A LeadsTo B == {F. F \ (reachable F \ A) leadsTo B}" -syntax (xsymbols) - "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \w " 60) +notation (xsymbols) + LeadsTo (infixl " \w " 60) text{*Resembles the previous definition of LeadsTo*} diff -r 2e8dc3c64430 -r 613e133966ea src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOL/UNITY/WFair.thy Wed Feb 24 22:09:50 2010 +0100 @@ -69,8 +69,8 @@ --{*predicate transformer: the largest set that leads to @{term B}*} "wlt F B == Union {A. F \ A leadsTo B}" -syntax (xsymbols) - "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\" 60) +notation (xsymbols) + leadsTo (infixl "\" 60) subsection{*transient*} diff -r 2e8dc3c64430 -r 613e133966ea src/HOLCF/IOA/meta_theory/Pred.thy --- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 22:09:50 2010 +0100 @@ -24,25 +24,25 @@ IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 25) -syntax ("" output) - "NOT" ::"'a predicate => 'a predicate" ("~ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "&" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "|" 30) - "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25) +notation (output) + NOT ("~ _" [40] 40) and + AND (infixr "&" 35) and + OR (infixr "|" 30) and + IMPLIES (infixr "-->" 25) -syntax (xsymbols output) - "NOT" ::"'a predicate => 'a predicate" ("\ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 30) - "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 25) +notation (xsymbols output) + NOT ("\ _" [40] 40) and + AND (infixr "\" 35) and + OR (infixr "\" 30) and + IMPLIES (infixr "\" 25) -syntax (xsymbols) - "satisfies" ::"'a => 'a predicate => bool" ("_ \ _" [100,9] 8) +notation (xsymbols) + satisfies ("_ \ _" [100,9] 8) -syntax (HTML output) - "NOT" ::"'a predicate => 'a predicate" ("\ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 30) +notation (HTML output) + NOT ("\ _" [40] 40) and + AND (infixr "\" 35) and + OR (infixr "\" 30) defs diff -r 2e8dc3c64430 -r 613e133966ea src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Wed Feb 24 22:04:10 2010 +0100 +++ b/src/Sequents/LK0.thy Wed Feb 24 22:09:50 2010 +0100 @@ -43,23 +43,23 @@ not_equal (infixl "~=" 50) where "x ~= y == ~ (x = y)" -syntax (xsymbols) - Not :: "o => o" ("\ _" [40] 40) - conj :: "[o, o] => o" (infixr "\" 35) - disj :: "[o, o] => o" (infixr "\" 30) - imp :: "[o, o] => o" (infixr "\" 25) - iff :: "[o, o] => o" (infixr "\" 25) - 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) +notation (xsymbols) + Not ("\ _" [40] 40) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and + imp (infixr "\" 25) and + iff (infixr "\" 25) and + All (binder "\" 10) and + Ex (binder "\" 10) and + not_equal (infixl "\" 50) -syntax (HTML output) - Not :: "o => o" ("\ _" [40] 40) - conj :: "[o, o] => o" (infixr "\" 35) - disj :: "[o, o] => o" (infixr "\" 30) - 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) +notation (HTML output) + Not ("\ _" [40] 40) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + not_equal (infixl "\" 50) local