doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Mon Jan 02 20:16:52 2006 +0100 (2006-01-02) changeset 18537 2681f9e34390 child 20437 0eb5e30fd620 permissions -rw-r--r--
"The Isabelle/Isar Implementation" manual;
```     1
```
```     2 (* \$Id\$ *)
```
```     3
```
```     4 theory logic imports base begin
```
```     5
```
```     6 chapter {* Pure logic *}
```
```     7
```
```     8 section {* Syntax *}
```
```     9
```
```    10 subsection {* Simply-typed lambda calculus *}
```
```    11
```
```    12 text {*
```
```    13
```
```    14 FIXME
```
```    15
```
```    16 \glossary{Type}{FIXME}
```
```    17 \glossary{Term}{FIXME}
```
```    18
```
```    19 *}
```
```    20
```
```    21 subsection {* The order-sorted algebra of types *}
```
```    22
```
```    23 text {*
```
```    24
```
```    25 FIXME
```
```    26
```
```    27 \glossary{Type constructor}{FIXME}
```
```    28
```
```    29 \glossary{Type class}{FIXME}
```
```    30
```
```    31 \glossary{Type arity}{FIXME}
```
```    32
```
```    33 \glossary{Sort}{FIXME}
```
```    34
```
```    35 *}
```
```    36
```
```    37
```
```    38 subsection {* Type-inference and schematic polymorphism *}
```
```    39
```
```    40 text {*
```
```    41
```
```    42 FIXME
```
```    43
```
```    44 \glossary{Schematic polymorphism}{FIXME}
```
```    45
```
```    46 \glossary{Type variable}{FIXME}
```
```    47
```
```    48 *}
```
```    49
```
```    50
```
```    51 section {* Theory *}
```
```    52
```
```    53 text {*
```
```    54
```
```    55 FIXME
```
```    56
```
```    57 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
```
```    58 theory context, but slightly more flexible since it may be used at
```
```    59 different type-instances, due to \seeglossary{schematic
```
```    60 polymorphism.}}
```
```    61
```
```    62 *}
```
```    63
```
```    64
```
```    65 section {* Deduction *}
```
```    66
```
```    67 text {*
```
```    68
```
```    69   FIXME
```
```    70
```
```    71 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
```
```    72 @{text "prop"}.  Internally, there is nothing special about
```
```    73 propositions apart from their type, but the concrete syntax enforces a
```
```    74 clear distinction.  Propositions are structured via implication @{text
```
```    75 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
```
```    76 else is considered atomic.  The canonical form for propositions is
```
```    77 that of a \seeglossary{Hereditary Harrop Formula}.}
```
```    78
```
```    79 \glossary{Theorem}{A proven proposition within a certain theory and
```
```    80 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
```
```    81 rarely spelled out explicitly.  Theorems are usually normalized
```
```    82 according to the \seeglossary{HHF} format.}
```
```    83
```
```    84 \glossary{Fact}{Sometimes used interchangably for
```
```    85 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
```
```    86 essentially an extra-logical conjunction.  Facts emerge either as
```
```    87 local assumptions, or as results of local goal statements --- both may
```
```    88 be simultaneous, hence the list representation.}
```
```    89
```
```    90 \glossary{Schematic variable}{FIXME}
```
```    91
```
```    92 \glossary{Fixed variable}{A variable that is bound within a certain
```
```    93 proof context; an arbitrary-but-fixed entity within a portion of proof
```
```    94 text.}
```
```    95
```
```    96 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
```
```    97
```
```    98 \glossary{Bound variable}{FIXME}
```
```    99
```
```   100 \glossary{Variable}{See \seeglossary{schematic variable},
```
```   101 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
```
```   102 \seeglossary{type variable}.  The distinguishing feature of different
```
```   103 variables is their binding scope.}
```
```   104
```
```   105 *}
```
```   106
```
```   107 subsection {* Primitive inferences *}
```
```   108
```
```   109 text FIXME
```
```   110
```
```   111 subsection {* Higher-order resolution *}
```
```   112
```
```   113 text {*
```
```   114
```
```   115 FIXME
```
```   116
```
```   117 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
```
```   118 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
```
```   119 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
```
```   120 Any proposition may be put into HHF form by normalizing with the rule
```
```   121 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
```
```   122 quantifier prefix is represented via \seeglossary{schematic
```
```   123 variables}, such that the top-level structure is merely that of a
```
```   124 \seeglossary{Horn Clause}}.
```
```   125
```
```   126 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
```
```   127
```
```   128 *}
```
```   129
```
```   130 subsection {* Equational reasoning *}
```
```   131
```
```   132 text FIXME
```
```   133
```
```   134
```
```   135 section {* Proof terms *}
```
```   136
```
```   137 text FIXME
```
```   138
```
```   139 end
```