doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Mon Sep 04 16:28:27 2006 +0200 (2006-09-04) changeset 20470 c839b38a1f32 parent 20451 27ea2ba48fa3 child 20472 e993073eda4c permissions -rw-r--r--
more on variables;
tuned;
     1

     2 (* $Id$ *)

     3

     4 theory logic imports base begin

     5

     6 chapter {* Primitive logic \label{ch: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