doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Thu Aug 31 18:27:40 2006 +0200 (2006-08-31) changeset 20450 725a91601ed1 parent 20437 0eb5e30fd620 child 20451 27ea2ba48fa3 permissions -rw-r--r--
tuned;
```     1
```
```     2 (* \$Id\$ *)
```
```     3
```
```     4 theory logic imports base begin
```
```     5
```
```     6 chapter {* Primitive logic *}
```
```     7
```
```     8 section {* Syntax *}
```
```     9
```
```    10 subsection {* Variable names *}
```
```    11
```
```    12 text {*
```
```    13   FIXME
```
```    14 *}
```
```    15
```
```    16
```
```    17 subsection {* Simply-typed lambda calculus *}
```
```    18
```
```    19 text {*
```
```    20
```
```    21 FIXME
```
```    22
```
```    23 \glossary{Type}{FIXME}
```
```    24 \glossary{Term}{FIXME}
```
```    25
```
```    26 *}
```
```    27
```
```    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
```
```    47 text {*
```
```    48
```
```    49 FIXME
```
```    50
```
```    51 \glossary{Schematic polymorphism}{FIXME}
```
```    52
```
```    53 \glossary{Type variable}{FIXME}
```
```    54
```
```    55 *}
```
```    56
```
```    57
```
```    58 section {* Theory *}
```
```    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
```
```    74 text {*
```
```    75
```
```    76   FIXME
```
```    77
```
```    78 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
```
```    79 @{text "prop"}.  Internally, there is nothing special about
```
```    80 propositions apart from their type, but the concrete syntax enforces a
```
```    81 clear distinction.  Propositions are structured via implication @{text
```
```    82 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
```
```    83 else is considered atomic.  The canonical form for propositions is
```
```    84 that of a \seeglossary{Hereditary Harrop Formula}.}
```
```    85
```
```    86 \glossary{Theorem}{A proven proposition within a certain theory and
```
```    87 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
```
```    88 rarely spelled out explicitly.  Theorems are usually normalized
```
```    89 according to the \seeglossary{HHF} format.}
```
```    90
```
```    91 \glossary{Fact}{Sometimes used interchangably for
```
```    92 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
```
```    93 essentially an extra-logical conjunction.  Facts emerge either as
```
```    94 local assumptions, or as results of local goal statements --- both may
```
```    95 be simultaneous, hence the list representation.}
```
```    96
```
```    97 \glossary{Schematic variable}{FIXME}
```
```    98
```
```    99 \glossary{Fixed variable}{A variable that is bound within a certain
```
```   100 proof context; an arbitrary-but-fixed entity within a portion of proof
```
```   101 text.}
```
```   102
```
```   103 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
```
```   104
```
```   105 \glossary{Bound variable}{FIXME}
```
```   106
```
```   107 \glossary{Variable}{See \seeglossary{schematic variable},
```
```   108 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
```
```   109 \seeglossary{type variable}.  The distinguishing feature of different
```
```   110 variables is their binding scope.}
```
```   111
```
```   112 *}
```
```   113
```
```   114 subsection {* Primitive inferences *}
```
```   115
```
```   116 text FIXME
```
```   117
```
```   118 subsection {* Higher-order resolution *}
```
```   119
```
```   120 text {*
```
```   121
```
```   122 FIXME
```
```   123
```
```   124 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
```
```   125 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
```
```   126 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
```
```   127 Any proposition may be put into HHF form by normalizing with the rule
```
```   128 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
```
```   129 quantifier prefix is represented via \seeglossary{schematic
```
```   130 variables}, such that the top-level structure is merely that of a
```
```   131 \seeglossary{Horn Clause}}.
```
```   132
```
```   133 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
```
```   134
```
```   135 *}
```
```   136
```
```   137 subsection {* Equational reasoning *}
```
```   138
```
```   139 text FIXME
```
```   140
```
```   141
```
```   142 section {* Proof terms *}
```
```   143
```
```   144 text FIXME
```
```   145
```
```   146 end
```