doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Thu Aug 31 22:55:49 2006 +0200 (2006-08-31)
changeset 20451 27ea2ba48fa3
parent 20450 725a91601ed1
child 20470 c839b38a1f32
permissions -rw-r--r--
misc cleanup;
     1 
     2 (* $Id$ *)
     3 
     4 theory logic imports base begin
     5 
     6 chapter {* Primitive logic *}
     7 
     8 section {* Variable names *}
     9 
    10 text FIXME
    11 
    12 
    13 section {* Types \label{sec:types} *}
    14 
    15 text {*
    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
    32 *}
    33 
    34 
    35 section {* Terms \label{sec:terms} *}
    36 
    37 text {*
    38   \glossary{Term}{FIXME}
    39 
    40   FIXME de-Bruijn representation of lambda terms
    41 *}
    42 
    43 
    44 text {*
    45 
    46 FIXME
    47 
    48 \glossary{Schematic polymorphism}{FIXME}
    49 
    50 \glossary{Type variable}{FIXME}
    51 
    52 *}
    53 
    54 
    55 section {* Theorems \label{sec:thms} *}
    56 
    57 text {*
    58 
    59   FIXME
    60 
    61 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
    62 @{text "prop"}.  Internally, there is nothing special about
    63 propositions apart from their type, but the concrete syntax enforces a
    64 clear distinction.  Propositions are structured via implication @{text
    65 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
    66 else is considered atomic.  The canonical form for propositions is
    67 that of a \seeglossary{Hereditary Harrop Formula}.}
    68 
    69 \glossary{Theorem}{A proven proposition within a certain theory and
    70 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
    71 rarely spelled out explicitly.  Theorems are usually normalized
    72 according to the \seeglossary{HHF} format.}
    73 
    74 \glossary{Fact}{Sometimes used interchangably for
    75 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
    76 essentially an extra-logical conjunction.  Facts emerge either as
    77 local assumptions, or as results of local goal statements --- both may
    78 be simultaneous, hence the list representation.}
    79 
    80 \glossary{Schematic variable}{FIXME}
    81 
    82 \glossary{Fixed variable}{A variable that is bound within a certain
    83 proof context; an arbitrary-but-fixed entity within a portion of proof
    84 text.}
    85 
    86 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
    87 
    88 \glossary{Bound variable}{FIXME}
    89 
    90 \glossary{Variable}{See \seeglossary{schematic variable},
    91 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
    92 \seeglossary{type variable}.  The distinguishing feature of different
    93 variables is their binding scope.}
    94 
    95 *}
    96 
    97 subsection {* Primitive inferences *}
    98 
    99 text FIXME
   100 
   101 subsection {* Higher-order resolution *}
   102 
   103 text {*
   104 
   105 FIXME
   106 
   107 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   108 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   109 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   110 Any proposition may be put into HHF form by normalizing with the rule
   111 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   112 quantifier prefix is represented via \seeglossary{schematic
   113 variables}, such that the top-level structure is merely that of a
   114 \seeglossary{Horn Clause}}.
   115 
   116 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   117 
   118 *}
   119 
   120 subsection {* Equational reasoning *}
   121 
   122 text FIXME
   123 
   124 
   125 section {* Low-level specifications *}
   126 
   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 *}
   141 
   142 end