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