doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 05 22:05:41 2006 +0200 (2006-09-05) changeset 20480 4e0522d38968 parent 20477 e623b0e30541 child 20491 98ba42f19995 permissions -rw-r--r--
more on types and type classes;
     1

     2 (* $Id$ *)

     3

     4 theory logic imports base begin

     5

     6 chapter {* Primitive logic \label{ch:logic} *}

     7

     8 text {*

     9   The logical foundations of Isabelle/Isar are that of the Pure logic,

    10   which has been introduced as a natural-deduction framework in

    11   \cite{paulson700}.  This is essentially the same logic as @{text

    12   "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)

    13   \cite{Barendregt-Geuvers:2001}, although there are some key

    14   differences in the practical treatment of simple types.

    15

    16   Following type-theoretic parlance, the Pure logic consists of three

    17   levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text

    18   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text

    19   "\<And>"} for universal quantification (proofs depending on terms), and

    20   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).

    21

    22   Pure derivations are relative to a logical theory, which declares

    23   type constructors, term constants, and axioms.  Term constants and

    24   axioms support schematic polymorphism.

    25 *}

    26

    27

    28 section {* Types \label{sec:types} *}

    29

    30 text {*

    31   The language of types is an uninterpreted order-sorted first-order

    32   algebra; types are qualified by ordered type classes.

    33

    34   \medskip A \emph{type class} is an abstract syntactic entity

    35   declared in the theory context.  The \emph{subclass relation} @{text

    36   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic

    37   generating relation; the transitive closure maintained internally.

    38

    39   A \emph{sort} is a list of type classes written as @{text

    40   "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic

    41   intersection.  Notationally, the curly braces are omitted for

    42   singleton intersections, i.e.\ any class @{text "c"} may be read as

    43   a sort @{text "{c}"}.  The ordering on type classes is extended to

    44   sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>

    45   {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>

    46   d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the

    47   universal sort, which is the largest element wrt.\ the sort order.

    48   The intersections of all (i.e.\ finitely many) classes declared in

    49   the current theory are the minimal elements wrt.\ sort order.

    50

    51   \medskip A \emph{fixed type variable} is pair of a basic name

    52   (starting with @{text "'"} character) and a sort constraint.  For

    53   example, @{text "('a, s)"} which is usually printed as @{text

    54   "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an

    55   indexname and a sort constraint.  For example, @{text "(('a, 0),

    56   s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.

    57

    58   Note that \emph{all} syntactic components contribute to the identity

    59   of a type variables, including the literal sort constraint.  The

    60   core logic handles type variables with the same name but different

    61   sorts as different, even though the outer layers of the system make

    62   it hard to produce anything like this.

    63

    64   A \emph{type constructor} is an @{text "k"}-ary type operator

    65   declared in the theory.

    66

    67   A \emph{type} is defined inductively over type variables and type

    68   constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,

    69   \<tau>\<^sub>k)c"}.  Type constructor application is usually written

    70   postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\

    71   @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the

    72   parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text

    73   "(\<tau>) list"}.  Further notation is provided for specific

    74   constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>

    75   \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}

    76   constructor.

    77

    78   A \emph{type abbreviation} is a syntactic abbreviation of an

    79   arbitrary type expression of the theory.  Type abbreviations looks

    80   like type constructors at the surface, but are expanded before the

    81   core logic encounters them.

    82

    83   A \emph{type arity} declares the image behavior of a type

    84   constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,

    85   s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is

    86   of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of

    87   sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as

    88   \emph{coregular}, which means that type arities are consistent with

    89   the subclass relation: for each type constructor @{text "c"} and

    90   classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::

    91   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c

    92   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>

    93   \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.

    94

    95   The key property of the order-sorted algebra of types is that sort

    96   constraints may be always fulfilled in a most general fashion: for

    97   each type constructor @{text "c"} and sort @{text "s"} there is a

    98   most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,

    99   s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,

   100   \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of

   101   sort @{text "s\<^isub>i"}.  This means the unification problem on

   102   the algebra of types has most general solutions (modulo renaming and

   103   equivalence of sorts).  As a consequence, type-inference is able to

   104   produce primary types.

   105 *}

   106

   107 text %mlref {*

   108   \begin{mldecls}

   109   @{index_ML_type class} \\

   110   @{index_ML_type sort} \\

   111   @{index_ML_type typ} \\

   112   @{index_ML_type arity} \\

   113   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\

   114   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\

   115   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\

   116   @{index_ML Sign.add_tyabbrs_i: "

   117   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\

   118   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\

   119   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\

   120   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\

   121   \end{mldecls}

   122

   123   \begin{description}

   124

   125   \item @{ML_type class} represents type classes; this is an alias for

   126   @{ML_type string}.

   127

   128   \item @{ML_type sort} represents sorts; this is an alias for

   129   @{ML_type "class list"}.

   130

   131   \item @{ML_type arity} represents type arities; this is an alias for

   132   triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::

   133   (\<^vec>s)s"} described above.

   134

   135   \item @{ML_type typ} represents types; this is a datatype with

   136   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.

   137

   138   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}

   139   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.

   140

   141   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type

   142   expression of of a given sort.

   143

   144   \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new

   145   type constructors @{text "c"} with @{text "k"} arguments, and

   146   optional mixfix syntax.

   147

   148   \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}

   149   defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional

   150   mixfix syntax) as @{text "\<tau>"}.

   151

   152   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,

   153   c\<^isub>n])"} declares new class @{text "c"} derived together with

   154   class relations @{text "c \<subseteq> c\<^isub>i"}.

   155

   156   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,

   157   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>

   158   c\<^isub>2"}.

   159

   160   \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares

   161   arity @{text "c :: (\<^vec>s)s"}.

   162

   163   \end{description}

   164 *}

   165

   166

   167

   168 section {* Terms \label{sec:terms} *}

   169

   170 text {*

   171   \glossary{Term}{FIXME}

   172

   173   FIXME de-Bruijn representation of lambda terms

   174

   175   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}

   176   and application @{text "t u"}, while types are usually implicit

   177   thanks to type-inference.

   178

   179   Terms of type @{text "prop"} are called

   180   propositions.  Logical statements are composed via @{text "\<And>x ::

   181   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.

   182 *}

   183

   184

   185 text {*

   186

   187 FIXME

   188

   189 \glossary{Schematic polymorphism}{FIXME}

   190

   191 \glossary{Type variable}{FIXME}

   192

   193 *}

   194

   195

   196 section {* Proof terms *}

   197

   198 text {*

   199   FIXME

   200 *}

   201

   202

   203 section {* Theorems \label{sec:thms} *}

   204

   205 text {*

   206

   207   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>

   208   \<phi>"}, with standard introduction and elimination rules for @{text

   209   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and

   210   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The

   211   corresponding proof terms are left implicit in the classic

   212   LCF-approach'', although they could be exploited separately

   213   \cite{Berghofer-Nipkow:2000}.

   214

   215   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>

   216   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal

   217   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of

   218   assumptions and conclusions emerging uniformly as simultaneous

   219   statements.

   220

   221

   222

   223   FIXME

   224

   225 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}

   226 @{text "prop"}.  Internally, there is nothing special about

   227 propositions apart from their type, but the concrete syntax enforces a

   228 clear distinction.  Propositions are structured via implication @{text

   229 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything

   230 else is considered atomic.  The canonical form for propositions is

   231 that of a \seeglossary{Hereditary Harrop Formula}.}

   232

   233 \glossary{Theorem}{A proven proposition within a certain theory and

   234 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are

   235 rarely spelled out explicitly.  Theorems are usually normalized

   236 according to the \seeglossary{HHF} format.}

   237

   238 \glossary{Fact}{Sometimes used interchangably for

   239 \seeglossary{theorem}.  Strictly speaking, a list of theorems,

   240 essentially an extra-logical conjunction.  Facts emerge either as

   241 local assumptions, or as results of local goal statements --- both may

   242 be simultaneous, hence the list representation.}

   243

   244 \glossary{Schematic variable}{FIXME}

   245

   246 \glossary{Fixed variable}{A variable that is bound within a certain

   247 proof context; an arbitrary-but-fixed entity within a portion of proof

   248 text.}

   249

   250 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}

   251

   252 \glossary{Bound variable}{FIXME}

   253

   254 \glossary{Variable}{See \seeglossary{schematic variable},

   255 \seeglossary{fixed variable}, \seeglossary{bound variable}, or

   256 \seeglossary{type variable}.  The distinguishing feature of different

   257 variables is their binding scope.}

   258

   259 *}

   260

   261 subsection {* Primitive inferences *}

   262

   263 text FIXME

   264

   265

   266 subsection {* Higher-order resolution *}

   267

   268 text {*

   269

   270 FIXME

   271

   272 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF

   273 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>

   274 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.

   275 Any proposition may be put into HHF form by normalizing with the rule

   276 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost

   277 quantifier prefix is represented via \seeglossary{schematic

   278 variables}, such that the top-level structure is merely that of a

   279 \seeglossary{Horn Clause}}.

   280

   281 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}

   282

   283 *}

   284

   285 subsection {* Equational reasoning *}

   286

   287 text FIXME

   288

   289

   290 end