# HG changeset patch # User wenzelm # Date 1267047914 -3600 # Node ID 413f9ba7e30818a1182b4f0937a9efabe32e2732 # Parent 5c937073e1d5ed56aeb9791b5a368cf21868c22e# Parent 613e133966ea02d9d93cebfb064a32a43cb2a674 merged diff -r 5c937073e1d5 -r 413f9ba7e308 NEWS --- a/NEWS Wed Feb 24 18:39:24 2010 +0100 +++ b/NEWS Wed Feb 24 22:45:14 2010 +0100 @@ -38,6 +38,8 @@ and ML_command "set Syntax.trace_ast" help to diagnose syntax problems. +* Type constructors admit general mixfix syntax, not just infix. + *** Pure *** diff -r 5c937073e1d5 -r 413f9ba7e308 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 22:45:14 2010 +0100 @@ -13,14 +13,14 @@ \end{matharray} \begin{rail} - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'typedef' altname? abstype '=' repset ; altname: '(' (name | 'open' | 'open' name) ')' ; - abstype: typespec infix? + abstype: typespec mixfix? ; repset: term ('morphisms' name name)? ; @@ -367,7 +367,7 @@ 'rep\_datatype' ('(' (name +) ')')? (term +) ; - dtspec: parname? typespec infix? '=' (cons + '|') + dtspec: parname? typespec mixfix? '=' (cons + '|') ; cons: name ( type * ) mixfix? \end{rail} diff -r 5c937073e1d5 -r 413f9ba7e308 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 24 22:45:14 2010 +0100 @@ -244,11 +244,9 @@ section {* Mixfix annotations *} text {* Mixfix annotations specify concrete \emph{inner syntax} of - Isabelle types and terms. Some commands such as @{command - "typedecl"} admit infixes only, while @{command "definition"} etc.\ - support the full range of general mixfixes and binders. Fixed - parameters in toplevel theorem statements, locale specifications - also admit mixfix annotations. + Isabelle types and terms. Locally fixed parameters in toplevel + theorem statements, locale specifications etc.\ also admit mixfix + annotations. \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} \begin{rail} diff -r 5c937073e1d5 -r 413f9ba7e308 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Wed Feb 24 22:45:14 2010 +0100 @@ -959,9 +959,9 @@ \end{matharray} \begin{rail} - 'types' (typespec '=' type infix? +) + 'types' (typespec '=' type mixfix? +) ; - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'arities' (nameref '::' arity +) ; diff -r 5c937073e1d5 -r 413f9ba7e308 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 24 18:39:24 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 24 22:45:14 2010 +0100 @@ -33,14 +33,14 @@ \end{matharray} \begin{rail} - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'typedef' altname? abstype '=' repset ; altname: '(' (name | 'open' | 'open' name) ')' ; - abstype: typespec infix? + abstype: typespec mixfix? ; repset: term ('morphisms' name name)? ; @@ -372,7 +372,7 @@ 'rep\_datatype' ('(' (name +) ')')? (term +) ; - dtspec: parname? typespec infix? '=' (cons + '|') + dtspec: parname? typespec mixfix? '=' (cons + '|') ; cons: name ( type * ) mixfix? \end{rail} @@ -906,6 +906,9 @@ \item[iterations] sets how many sets of assignments are generated for each particular size. + \item[no\_assms] specifies whether assumptions in + structured proofs should be ignored. + \end{description} These option can be given within square brackets. diff -r 5c937073e1d5 -r 413f9ba7e308 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 24 18:39:24 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 24 22:45:14 2010 +0100 @@ -266,10 +266,9 @@ % \begin{isamarkuptext}% Mixfix annotations specify concrete \emph{inner syntax} of - Isabelle types and terms. Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\ - support the full range of general mixfixes and binders. Fixed - parameters in toplevel theorem statements, locale specifications - also admit mixfix annotations. + Isabelle types and terms. Locally fixed parameters in toplevel + theorem statements, locale specifications etc.\ also admit mixfix + annotations. \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} \begin{rail} diff -r 5c937073e1d5 -r 413f9ba7e308 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Feb 24 18:39:24 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Feb 24 22:45:14 2010 +0100 @@ -996,9 +996,9 @@ \end{matharray} \begin{rail} - 'types' (typespec '=' type infix? +) + 'types' (typespec '=' type mixfix? +) ; - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'arities' (nameref '::' arity +) ; diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Algebra/Congruence.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Bali/Basis.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Bali/Table.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Feb 24 22:45:14 2010 +0100 @@ -256,8 +256,8 @@ (* Special syntax for guarded statements and guarded array updates: *) syntax - guarded_com :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) - array_update :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) + "_guarded_com" :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) + "_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) translations "P \ c" == "IF P THEN c ELSE CONST Abort FI" "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Feb 24 22:45:14 2010 +0100 @@ -1502,13 +1502,13 @@ by (cases M) auto syntax - comprehension1_mset :: "'a \ 'b \ 'b multiset \ 'a multiset" + "_comprehension1_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ :# _#})") translations "{#e. x:#M#}" == "CONST image_mset (%x. e) M" syntax - comprehension2_mset :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" + "_comprehension2_mset" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ :# _./ _#})") translations "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}" diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/BV/JVMType.thy --- a/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/Comp/TranslCompTp.thy --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/DFA/Semilat.thy --- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/JVM/JVMDefensive.thy --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/MicroJava/JVM/JVMExec.thy --- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/NanoJava/State.thy --- a/src/HOL/NanoJava/State.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/NanoJava/State.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Nominal/Nominal.thy Wed Feb 24 22:45:14 2010 +0100 @@ -3403,13 +3403,13 @@ where ABS_in: "(abs_fun a x)\ABS_set" -typedef (ABS) ('x,'a) ABS = "ABS_set::('x\('a noption)) set" +typedef (ABS) ('x,'a) ABS ("\_\_" [1000,1000] 1000) = + "ABS_set::('x\('a noption)) set" proof fix x::"'a" and a::"'x" show "(abs_fun a x)\ ABS_set" by (rule ABS_in) qed -syntax ABS :: "type \ type \ type" ("\_\_" [1000,1000] 1000) section {* lemmas for deciding permutation equations *} (*===================================================*) diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Feb 24 22:45:14 2010 +0100 @@ -2079,7 +2079,7 @@ local structure P = OuterParse and K = OuterKeyword in val datatype_decl = - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix -- + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix -- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix)); fun mk_datatype args = diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/TLA/Action.thy Wed Feb 24 22:45:14 2010 +0100 @@ -33,7 +33,7 @@ syntax (* Syntax for writing action expressions in arbitrary contexts *) - "ACT" :: "lift => 'a" ("(ACT _)") + "_ACT" :: "lift => 'a" ("(ACT _)") "_before" :: "lift => lift" ("($_)" [100] 99) "_after" :: "lift => lift" ("(_$)" [100] 99) diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/TLA/Intensional.thy Wed Feb 24 22:45:14 2010 +0100 @@ -51,7 +51,7 @@ "_holdsAt" :: "['a, lift] => bool" ("(_ |= _)" [100,10] 10) (* Syntax for lifted expressions outside the scope of |- or |= *) - "LIFT" :: "lift => 'a" ("LIFT _") + "_LIFT" :: "lift => 'a" ("LIFT _") (* generic syntax for lifted constants and functions *) "_const" :: "'a => lift" ("(#_)" [1000] 999) diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/TLA/Stfun.thy --- a/src/HOL/TLA/Stfun.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/TLA/Stfun.thy Wed Feb 24 22:45:14 2010 +0100 @@ -35,7 +35,7 @@ stvars :: "'a stfun => bool" syntax - "PRED" :: "lift => 'a" ("PRED _") + "_PRED" :: "lift => 'a" ("PRED _") "_stvars" :: "lift => bool" ("basevars _") translations diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Feb 24 22:45:14 2010 +0100 @@ -731,7 +731,7 @@ in (names, specs) end; val parse_datatype_decl = - (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix -- + (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix))); val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls; diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Wed Feb 24 22:45:14 2010 +0100 @@ -296,7 +296,7 @@ val quotspec_parser = OuterParse.and_list1 ((OuterParse.type_args -- OuterParse.binding) -- - OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- + OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) val _ = OuterKeyword.keyword "/" diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Wed Feb 24 22:45:14 2010 +0100 @@ -255,7 +255,7 @@ (Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => Toplevel.print o Toplevel.theory_to_proof diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOL/UNITY/WFair.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOLCF/IOA/meta_theory/Pred.thy --- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 22:45:14 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 5c937073e1d5 -r 413f9ba7e308 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Feb 24 22:45:14 2010 +0100 @@ -291,7 +291,7 @@ || Scan.succeed []; val domain_decl = - (type_args' -- P.binding -- P.opt_infix) -- + (type_args' -- P.binding -- P.opt_mixfix) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl); val domains_decl = diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Feb 24 22:45:14 2010 +0100 @@ -700,7 +700,7 @@ val parse_domain_iso : (string list * binding * mixfix * string * (binding * binding) option) parser = - (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ) -- + (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))) >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)); diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Wed Feb 24 22:45:14 2010 +0100 @@ -340,7 +340,7 @@ Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = diff -r 5c937073e1d5 -r 413f9ba7e308 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/HOLCF/Tools/repdef.ML Wed Feb 24 22:45:14 2010 +0100 @@ -167,7 +167,7 @@ Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = diff -r 5c937073e1d5 -r 413f9ba7e308 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Feb 24 22:45:14 2010 +0100 @@ -104,13 +104,13 @@ val _ = OuterSyntax.command "typedecl" "type declaration" K.thy_decl - (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) => + (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) => Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); val _ = OuterSyntax.command "types" "declare type abbreviations" K.thy_decl (Scan.repeat1 - (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) + (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix'))) >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); diff -r 5c937073e1d5 -r 413f9ba7e308 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/Pure/Isar/outer_parse.ML Wed Feb 24 22:45:14 2010 +0100 @@ -72,8 +72,6 @@ val typ: string parser val mixfix: mixfix parser val mixfix': mixfix parser - val opt_infix: mixfix parser - val opt_infix': mixfix parser val opt_mixfix: mixfix parser val opt_mixfix': mixfix parser val where_: string parser @@ -279,8 +277,6 @@ val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx); val mixfix' = annotation I (mfix || binder || infxl || infxr || infx); -val opt_infix = opt_annotation !!! (infxl || infxr || infx); -val opt_infix' = opt_annotation I (infxl || infxr || infx); val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx); val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx); diff -r 5c937073e1d5 -r 413f9ba7e308 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/Pure/Syntax/mixfix.ML Wed Feb 24 22:45:14 2010 +0100 @@ -101,20 +101,26 @@ fun syn_ext_types type_decls = let - fun mk_infix sy t p1 p2 p3 = - SynExt.Mfix ("(_ " ^ sy ^ "/ _)", - [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3); + fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT; + fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3); fun mfix_of (_, _, NoSyn) = NONE - | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p) - | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p) - | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p) - | mfix_of (t, _, _) = - error ("Bad mixfix declaration for type: " ^ quote t); (* FIXME printable!? *) + | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p)) + | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri)) + | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p) + | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p) + | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p) + | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *) - val mfix = map_filter mfix_of type_decls; + fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) = + if SynExt.mfix_args sy = n then () + else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix + | check_args _ NONE = (); + + val mfix = map mfix_of type_decls; + val _ = map2 check_args type_decls mfix; val xconsts = map #1 type_decls; - in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end; + in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end; (* syn_ext_consts *) @@ -140,7 +146,7 @@ | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p | mfix_of (c, ty, Binder (sy, p, q)) = [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] - | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c); + | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *) fun binder (c, _, Binder _) = SOME (binder_name c, c) | binder _ = NONE; diff -r 5c937073e1d5 -r 413f9ba7e308 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Wed Feb 24 18:39:24 2010 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Wed Feb 24 22:45:14 2010 +0100 @@ -28,6 +28,8 @@ val cargs: string val any: string val sprop: string + datatype mfix = Mfix of string * typ * string * int list * int + val err_in_mfix: string -> mfix -> 'a val typ_to_nonterm: typ -> string datatype xsymb = Delim of string | @@ -37,7 +39,6 @@ datatype xprod = XProd of string * xsymb list * string * int val chain_pri: int val delims_of: xprod list -> string list list - datatype mfix = Mfix of string * typ * string * int list * int datatype syn_ext = SynExt of { xprods: xprod list, diff -r 5c937073e1d5 -r 413f9ba7e308 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Wed Feb 24 18:39:24 2010 +0100 +++ b/src/Sequents/LK0.thy Wed Feb 24 22:45:14 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