Syntax of the Mizar Language
Last modified: October 8, 1997
Edited by Freek: June 25, 1999
keywords (86+1+8): and antonym as assume attr be begin being by canceled case
cases cluster clusters coherence commutativity compatibility connectedness
consider consistency constructors contradiction correctness def deffunc
definition definitions defpred end environ equals ex existence for from
func given hence holds if iff implies irreflexivity is it let means mode
non not notation now of or otherwise over per pred proof @proof provided
qua reconsider redefine reflexivity requirements reserve scheme schemes set
st struct such suppose symmetry synonym take that the then theorem theorems
thesis thus uniqueness vocabulary where $1 $2 $3 $4 $5 $6 $7 $8
extra keywords (15): according aggregate antisymmetry associativity define
exactly hereby idempotency prefix properties section selector signature to
transitivity
interpunction (15): , ; : -> = .= & ( ) [ ] { } (# #)
extra interpunction (3): ... "<<" ">>"
Mizar-Article =
"environ"
{ "vocabulary" File-Name-List ";" |
( "notation" |
"constructors" |
"clusters" |
"definitions" |
"theorems" |
"schemes" ) File-Name-List ";" |
"requirements" File-Name-List ";" }
( "begin" { Text-Item } ) { ... } .
Text-Item =
"reserve" Identifier-List "for" Type-Expression-List ";" |
"definition"
{ Definition-Item }
[ "redefine" { Definition-Item } ]
"end" ";" |
Structure-Definition |
"theorem" Proposition Justification ";" |
[ "scheme" ] Identifier
"{" ( Identifier-List "[" Type-Expression-List "]" |
Identifier-List "(" Type-Expression-List ")" "->" Type-Expression )
{ "," ... } "}"
":" Formula-Expression
[ "provided" Proposition { "and" ... } ]
Justification ";" |
Auxiliary-Item |
"canceled" [ Numeral ] ";" .
Definition-Item =
Assumption |
Auxiliary-Item |
Structure-Definition |
"mode" M-Symbol [ "of" Identifier-List ]
( [ "->" Type-Expression ] [ "means" Definiens ] ";"
Correctness-Conditions |
"is" Type-Expression ";" )
{ "synonym" M-Symbol [ "of" Identifier-List ] ";" } |
"func" Functor-Pattern [ "->" Type-Expression ]
[ ( "means" | "equals" ) Definiens ] ";"
Correctness-Conditions
{ "commutativity" Justification ";" }
{ "synonym" Functor-Pattern ";" } |
"pred" Predicate-Pattern [ "means" Definiens ] ";"
Correctness-Conditions
{ "symmetry" Justification ";" |
"connectedness" Justification ";" |
"reflexivity" Justification ";" |
"irreflexivity" Justification ";" }
{ ( "synonym" | "antonym" ) Predicate-Pattern ";" } |
"attr" Identifier "is" V-Symbol "means" Definiens ";"
[ Correctness-Conditions ]
{ ( "synonym" | "antonym" )
( Identifier "is" V-Symbol | Predicate-Pattern ) ";" } |
"canceled" [ Numeral ] |
"cluster" Adjective-Cluster Type-Expression ";" Correctness-Conditions |
"cluster" Adjective-Cluster "->" Adjective-Cluster Type-Expression ";"
Correctness-Conditions |
"cluster" Term-Expression "->" Adjective-Cluster ";" Correctness-Conditions .
Structure-Definition =
"struct" [ "(" Type-Expression-List ")" ] G-Symbol [ "over" Identifier-List ]
"(#" ( U-Symbol { "," ... } "->" Type-Expression ) { "," ... } "#)" ";" .
Definiens =
[ ":" Identifier ":" ] ( Formula-Expression | Term-Expression ) |
[ ":" Identifier ":" ]
( ( Formula-Expression | Term-Expression ) "if" Formula-Expression )
{ "," ... }
[ "otherwise" ( Formula-Expression | Term-Expression ) ] .
Functor-Pattern =
[ Functor-Loci ] O-Symbol [ Functor-Loci ] |
K-Symbol Identifier-List L-Symbol .
Functor-Loci =
Identifier |
"(" Identifier-List ")" .
Predicate-Pattern = [ Identifier-List ] R-Symbol [ Identifier-List ] .
Correctness-Conditions =
{ "existence" Justification ";" |
"uniqueness" Justification ";" |
"coherence" Justification ";" |
"compatibility" Justification ";" |
"consistency" Justification ";" }
[ "correctness" Justification ";" ] .
Justification =
Simple-Justification |
( "proof" | "@proof" ) Reasoning "end" .
Reasoning =
{ Reasoning-Item }
[ "per" "cases" Simple-Justification ";"
( ( "case" ( Proposition | Conditions ) ";" { Reasoning-Item } )
{ ... } |
( "suppose" ( Proposition | Conditions ) ";" { Reasoning-Item } )
{ ... } ) ] .
Reasoning-Item =
Auxiliary-Item |
Assumption |
( "thus" | "hence" ) Statement |
"take" ( Term-Expression | Identifier "=" Term-Expression ) { "," ... } ";" .
Auxiliary-Item =
[ "then" ] Statement |
"set" ( Identifier "=" Term-Expression ) { "," ... } ";" |
"deffunc" Identifier "(" [ Type-Expression-List ] ")" "=" Term-Expression |
"defpred" Identifier "[" [ Type-Expression-List ] "]" "means"
Formula-Expression .
Assumption =
( "let" | "given" ) Qualified-Variables [ "such" Conditions ] ";" |
"assume" ( Proposition | Conditions ) ";" .
Statement =
[ "then" ]
( Proposition Justification ";" |
"consider" Qualified-Variables [ "such" Conditions ]
Simple-Justification ";" |
"reconsider"
( Identifier "=" Term-Expression | Identifier ) { "," ... }
"as" Type-Expression Simple-Justification ";" |
Term-Expression "=" Term-Expression Simple-Justification
".=" ( Term-Expression Simple-Justification ) { ".=" ... } ) |
[ Identifier ":" ] "now" Reasoning "end" ";" .
Simple-Justification =
[ "by" Reference { "," ... } ] |
"from" Identifier [ "(" Reference { "," ... } ")" ] .
Reference =
Identifier |
File-Name ":" ( Numeral | "def" Numeral ) { "," ... } .
Conditions = "that" Proposition { "and" ... } .
Proposition = [ Identifier ":" ] Formula-Expression .
Formula-Expression =
"(" Formula-Expression ")" |
[ Term-Expression-List ] R-Symbol [ Term-Expression-List ] |
Identifier [ "[" Term-Expression-List "]" ] |
Term-Expression "is" { [ "non" ] V-Symbol } |
Term-Expression "is" Type-Expression |
Quantified-Formula-Expression |
Formula-Expression "&" Formula-Expression |
Formula-Expression "or" Formula-Expression |
Formula-Expression "implies" Formula-Expression |
Formula-Expression "iff" Formula-Expression |
"not" Formula-Expression |
"contradiction" |
"thesis" .
Quantified-Formula-Expression =
"for" Qualified-Variables [ "st" Formula-Expression ]
( "holds" Formula-Expression | Quantified-Formula-Expression ) |
"ex" Qualified-Variables "st" Formula-Expression .
Qualified-Variables =
Identifier-List |
( Identifier-List ( "being" | "be" ) Type-Expression ) { "," ... }
[ "," Identifier-List ] .
Type-Expression =
"(" Type-Expression ")" |
Adjective-Cluster M-Symbol [ "of" Term-Expression-List ] |
Adjective-Cluster G-Symbol [ "over" Term-Expression-List ] .
Adjective-Cluster = { [ "non" ] V-Symbol } .
Term-Expression =
"(" Term-Expression ")" |
[ Arguments ] O-Symbol [ Arguments ] |
K-Symbol Term-Expression-List L-Symbol |
Identifier "(" [ Term-Expression-List ] ")" |
G-Symbol "(#" Term-Expression-List "#)" |
Identifier |
"{" Term-Expression
[ ( "where" Identifier-List "is" Type-Expression ) { "," ... } ]
":" Formula-Expression "}" |
Numeral |
Term-Expression "qua" Type-Expression |
"the" U-Symbol "of" Term-Expression |
"the" U-Symbol |
"$1" | "$2" | "$3" | "$4" | "$5" | "$6" | "$7" | "$8" |
"it" .
Arguments =
Term-Expression |
"(" Term-Expression-List ")" .
File-Name-List = File-Name { "," ... } .
Identifier-List = Identifier { "," ... } .
Type-Expression-List = Type-Expression { "," ... } .
Term-Expression-List = Term-Expression { "," ... } .