doc-src/IsarImplementation/Thy/logic.thy
changeset 20451 27ea2ba48fa3
parent 20450 725a91601ed1
child 20470 c839b38a1f32
equal deleted inserted replaced
20450:725a91601ed1 20451:27ea2ba48fa3
     3 
     3 
     4 theory logic imports base begin
     4 theory logic imports base begin
     5 
     5 
     6 chapter {* Primitive logic *}
     6 chapter {* Primitive logic *}
     7 
     7 
     8 section {* Syntax *}
     8 section {* Variable names *}
     9 
     9 
    10 subsection {* Variable names *}
    10 text FIXME
       
    11 
       
    12 
       
    13 section {* Types \label{sec:types} *}
    11 
    14 
    12 text {*
    15 text {*
    13   FIXME
    16   \glossary{Type class}{FIXME}
       
    17 
       
    18   \glossary{Type arity}{FIXME}
       
    19 
       
    20   \glossary{Sort}{FIXME}
       
    21 
       
    22   FIXME classes and sorts
       
    23 
       
    24 
       
    25   \glossary{Type}{FIXME}
       
    26 
       
    27   \glossary{Type constructor}{FIXME}
       
    28 
       
    29   \glossary{Type variable}{FIXME}
       
    30 
       
    31   FIXME simple types
    14 *}
    32 *}
    15 
    33 
    16 
    34 
    17 subsection {* Simply-typed lambda calculus *}
    35 section {* Terms \label{sec:terms} *}
    18 
    36 
    19 text {*
    37 text {*
       
    38   \glossary{Term}{FIXME}
    20 
    39 
    21 FIXME
    40   FIXME de-Bruijn representation of lambda terms
    22 
       
    23 \glossary{Type}{FIXME}
       
    24 \glossary{Term}{FIXME}
       
    25 
       
    26 *}
    41 *}
    27 
    42 
    28 subsection {* The order-sorted algebra of types *}
       
    29 
       
    30 text {*
       
    31 
       
    32 FIXME
       
    33 
       
    34 \glossary{Type constructor}{FIXME}
       
    35 
       
    36 \glossary{Type class}{FIXME}
       
    37 
       
    38 \glossary{Type arity}{FIXME}
       
    39 
       
    40 \glossary{Sort}{FIXME}
       
    41 
       
    42 *}
       
    43 
       
    44 
       
    45 subsection {* Type-inference and schematic polymorphism *}
       
    46 
    43 
    47 text {*
    44 text {*
    48 
    45 
    49 FIXME
    46 FIXME
    50 
    47 
    53 \glossary{Type variable}{FIXME}
    50 \glossary{Type variable}{FIXME}
    54 
    51 
    55 *}
    52 *}
    56 
    53 
    57 
    54 
    58 section {* Theory *}
    55 section {* Theorems \label{sec:thms} *}
    59 
       
    60 text {*
       
    61 
       
    62 FIXME
       
    63 
       
    64 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
       
    65 theory context, but slightly more flexible since it may be used at
       
    66 different type-instances, due to \seeglossary{schematic
       
    67 polymorphism.}}
       
    68 
       
    69 *}
       
    70 
       
    71 
       
    72 section {* Deduction *}
       
    73 
    56 
    74 text {*
    57 text {*
    75 
    58 
    76   FIXME
    59   FIXME
    77 
    60 
   137 subsection {* Equational reasoning *}
   120 subsection {* Equational reasoning *}
   138 
   121 
   139 text FIXME
   122 text FIXME
   140 
   123 
   141 
   124 
   142 section {* Proof terms *}
   125 section {* Low-level specifications *}
   143 
   126 
   144 text FIXME
   127 text {*
       
   128 
       
   129 FIXME
       
   130 
       
   131 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
       
   132 theory context, but slightly more flexible since it may be used at
       
   133 different type-instances, due to \seeglossary{schematic
       
   134 polymorphism.}}
       
   135 
       
   136 \glossary{Axiom}{FIXME}
       
   137 
       
   138 \glossary{Primitive definition}{FIXME}
       
   139 
       
   140 *}
   145 
   141 
   146 end
   142 end