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 { "," ... } .