1.1 --- a/doc-src/IsarImplementation/Makefile Mon Feb 16 21:04:15 2009 +0100
1.2 +++ b/doc-src/IsarImplementation/Makefile Mon Feb 16 21:23:33 2009 +0100
1.3 @@ -8,8 +8,6 @@
1.4
1.5 include ../Makefile.in
1.6
1.7 -MAKEGLOSSARY = ./makeglossary
1.8 -
1.9 NAME = implementation
1.10
1.11 FILES = implementation.tex Thy/document/Prelim.tex \
1.12 @@ -26,7 +24,6 @@
1.13 $(BIBTEX) $(NAME)
1.14 $(LATEX) $(NAME)
1.15 $(LATEX) $(NAME)
1.16 - $(MAKEGLOSSARY) $(NAME)
1.17 $(SEDINDEX) $(NAME)
1.18 $(LATEX) $(NAME)
1.19 $(LATEX) $(NAME)
1.20 @@ -38,7 +35,6 @@
1.21 $(BIBTEX) $(NAME)
1.22 $(PDFLATEX) $(NAME)
1.23 $(PDFLATEX) $(NAME)
1.24 - $(MAKEGLOSSARY) $(NAME)
1.25 $(SEDINDEX) $(NAME)
1.26 $(FIXBOOKMARKS) $(NAME).out
1.27 $(PDFLATEX) $(NAME)
2.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:04:15 2009 +0100
2.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:23:33 2009 +0100
2.3 @@ -186,12 +186,9 @@
2.4 *}
2.5
2.6
2.7 -
2.8 section {* Terms \label{sec:terms} *}
2.9
2.10 text {*
2.11 - \glossary{Term}{FIXME}
2.12 -
2.13 The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
2.14 with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
2.15 or \cite{paulson-ml2}), with the types being determined determined
2.16 @@ -392,42 +389,6 @@
2.17 section {* Theorems \label{sec:thms} *}
2.18
2.19 text {*
2.20 - \glossary{Proposition}{FIXME A \seeglossary{term} of
2.21 - \seeglossary{type} @{text "prop"}. Internally, there is nothing
2.22 - special about propositions apart from their type, but the concrete
2.23 - syntax enforces a clear distinction. Propositions are structured
2.24 - via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
2.25 - "\<And>x. B x"} --- anything else is considered atomic. The canonical
2.26 - form for propositions is that of a \seeglossary{Hereditary Harrop
2.27 - Formula}. FIXME}
2.28 -
2.29 - \glossary{Theorem}{A proven proposition within a certain theory and
2.30 - proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
2.31 - rarely spelled out explicitly. Theorems are usually normalized
2.32 - according to the \seeglossary{HHF} format. FIXME}
2.33 -
2.34 - \glossary{Fact}{Sometimes used interchangeably for
2.35 - \seeglossary{theorem}. Strictly speaking, a list of theorems,
2.36 - essentially an extra-logical conjunction. Facts emerge either as
2.37 - local assumptions, or as results of local goal statements --- both
2.38 - may be simultaneous, hence the list representation. FIXME}
2.39 -
2.40 - \glossary{Schematic variable}{FIXME}
2.41 -
2.42 - \glossary{Fixed variable}{A variable that is bound within a certain
2.43 - proof context; an arbitrary-but-fixed entity within a portion of
2.44 - proof text. FIXME}
2.45 -
2.46 - \glossary{Free variable}{Synonymous for \seeglossary{fixed
2.47 - variable}. FIXME}
2.48 -
2.49 - \glossary{Bound variable}{FIXME}
2.50 -
2.51 - \glossary{Variable}{See \seeglossary{schematic variable},
2.52 - \seeglossary{fixed variable}, \seeglossary{bound variable}, or
2.53 - \seeglossary{type variable}. The distinguishing feature of
2.54 - different variables is their binding scope. FIXME}
2.55 -
2.56 A \emph{proposition} is a well-typed term of type @{text "prop"}, a
2.57 \emph{theorem} is a proven proposition (depending on a context of
2.58 hypotheses and the background theory). Primitive inferences include
2.59 @@ -436,6 +397,7 @@
2.60 notion of equality/equivalence @{text "\<equiv>"}.
2.61 *}
2.62
2.63 +
2.64 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
2.65
2.66 text {*
2.67 @@ -801,16 +763,13 @@
2.68 expect a normal form: quantifiers @{text "\<And>"} before implications
2.69 @{text "\<Longrightarrow>"} at each level of nesting.
2.70
2.71 -\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
2.72 -format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
2.73 -A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
2.74 -Any proposition may be put into HHF form by normalizing with the rule
2.75 -@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost
2.76 -quantifier prefix is represented via \seeglossary{schematic
2.77 -variables}, such that the top-level structure is merely that of a
2.78 -\seeglossary{Horn Clause}}.
2.79 -
2.80 -\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
2.81 + The set of propositions in HHF format is defined inductively as
2.82 + @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> A)"}, for variables @{text "x"}
2.83 + and atomic propositions @{text "A"}. Any proposition may be put
2.84 + into HHF form by normalizing with the rule @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv>
2.85 + (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost quantifier prefix is
2.86 + represented via schematic variables, such that the top-level
2.87 + structure is merely that of a Horn Clause.
2.88
2.89
2.90 \[
3.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:04:15 2009 +0100
3.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:23:33 2009 +0100
3.3 @@ -74,8 +74,6 @@
3.4 subsection {* Theory context \label{sec:context-theory} *}
3.5
3.6 text {*
3.7 - \glossary{Theory}{FIXME}
3.8 -
3.9 A \emph{theory} is a data container with explicit named and unique
3.10 identifier. Theories are related by a (nominal) sub-theory
3.11 relation, which corresponds to the dependency graph of the original
3.12 @@ -201,13 +199,6 @@
3.13 subsection {* Proof context \label{sec:context-proof} *}
3.14
3.15 text {*
3.16 - \glossary{Proof context}{The static context of a structured proof,
3.17 - acts like a local ``theory'' of the current portion of Isar proof
3.18 - text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in
3.19 - judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi. There is a
3.20 - generic notion of introducing and discharging hypotheses.
3.21 - Arbritrary auxiliary context data may be adjoined.}
3.22 -
3.23 A proof context is a container for pure data with a back-reference
3.24 to the theory it belongs to. The @{text "init"} operation creates a
3.25 proof context from a given theory. Modifications to draft theories
3.26 @@ -231,7 +222,7 @@
3.27 context is extended consecutively, and results are exported back
3.28 into the original context. Note that the Isar proof states model
3.29 block-structured reasoning explicitly, using a stack of proof
3.30 - contexts internally, cf.\ \secref{sec:isar-proof-state}.
3.31 + contexts internally.
3.32 *}
3.33
3.34 text %mlref {*
3.35 @@ -418,10 +409,6 @@
3.36 subsection {* Strings of symbols *}
3.37
3.38 text {*
3.39 - \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
3.40 - plain ASCII characters as well as an infinite collection of named
3.41 - symbols (for greek, math etc.).}
3.42 -
3.43 A \emph{symbol} constitutes the smallest textual unit in Isabelle
3.44 --- raw characters are normally not encountered at all. Isabelle
3.45 strings consist of a sequence of symbols, represented as a packed
3.46 @@ -465,8 +452,8 @@
3.47 link to the standard collection of Isabelle.
3.48
3.49 \medskip Output of Isabelle symbols depends on the print mode
3.50 - (\secref{FIXME}). For example, the standard {\LaTeX} setup of the
3.51 - Isabelle document preparation system would present
3.52 + (\secref{print-mode}). For example, the standard {\LaTeX} setup of
3.53 + the Isabelle document preparation system would present
3.54 ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
3.55 ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
3.56 "\<^bold>\<alpha>"}.
4.1 --- a/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:04:15 2009 +0100
4.2 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:23:33 2009 +0100
4.3 @@ -18,21 +18,14 @@
4.4 section {* Goals \label{sec:tactical-goals} *}
4.5
4.6 text {*
4.7 - Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
4.8 - \seeglossary{Horn Clause} form stating that a number of subgoals
4.9 - imply the main conclusion, which is marked as a protected
4.10 - proposition.} as a theorem stating that the subgoals imply the main
4.11 - goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}. The outermost goal
4.12 - structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
4.13 - implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
4.14 - outermost quantifiers. Strictly speaking, propositions @{text
4.15 - "A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
4.16 - arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
4.17 - connectives).}: i.e.\ an iterated implication without any
4.18 - quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
4.19 - always represented via schematic variables in the body: @{text
4.20 - "\<phi>[?x]"}. These variables may get instantiated during the course of
4.21 - reasoning.}. For @{text "n = 0"} a goal is called ``solved''.
4.22 + Isabelle/Pure represents a goal as a theorem stating that the
4.23 + subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
4.24 + C"}. The outermost goal structure is that of a Horn Clause: i.e.\
4.25 + an iterated implication without any quantifiers\footnote{Recall that
4.26 + outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
4.27 + variables in the body: @{text "\<phi>[?x]"}. These variables may get
4.28 + instantiated during the course of reasoning.}. For @{text "n = 0"}
4.29 + a goal is called ``solved''.
4.30
4.31 The structure of each subgoal @{text "A\<^sub>i"} is that of a general
4.32 Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} in
4.33 @@ -45,14 +38,9 @@
4.34 exceeds 1--2 in practice.
4.35
4.36 The main conclusion @{text C} is internally marked as a protected
4.37 - proposition\glossary{Protected proposition}{An arbitrarily
4.38 - structured proposition @{text "C"} which is forced to appear as
4.39 - atomic by wrapping it into a propositional identity operator;
4.40 - notation @{text "#C"}. Protecting a proposition prevents basic
4.41 - inferences from entering into that structure for the time being.},
4.42 - which is represented explicitly by the notation @{text "#C"}. This
4.43 - ensures that the decomposition into subgoals and main conclusion is
4.44 - well-defined for arbitrarily structured claims.
4.45 + proposition, which is represented explicitly by the notation @{text
4.46 + "#C"}. This ensures that the decomposition into subgoals and main
4.47 + conclusion is well-defined for arbitrarily structured claims.
4.48
4.49 \medskip Basic goal management is performed via the following
4.50 Isabelle/Pure rules:
4.51 @@ -405,14 +393,12 @@
4.52 section {* Tacticals \label{sec:tacticals} *}
4.53
4.54 text {*
4.55 + A \emph{tactical} is a functional combinator for building up complex
4.56 + tactics from simpler ones. Typical tactical perform sequential
4.57 + composition, disjunction (choice), iteration, or goal addressing.
4.58 + Various search strategies may be expressed via tacticals.
4.59
4.60 -FIXME
4.61 -
4.62 -\glossary{Tactical}{A functional combinator for building up complex
4.63 -tactics from simpler ones. Typical tactical perform sequential
4.64 -composition, disjunction (choice), iteration, or goal addressing.
4.65 -Various search strategies may be expressed via tacticals.}
4.66 -
4.67 + \medskip FIXME
4.68 *}
4.69
4.70 end
5.1 --- a/doc-src/IsarImplementation/checkglossary Mon Feb 16 21:04:15 2009 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,28 +0,0 @@
5.4 -#!/usr/bin/env perl
5.5 -# $Id$
5.6 -
5.7 -use strict;
5.8 -
5.9 -my %defs = ();
5.10 -my %refs = ();
5.11 -
5.12 -while (<ARGV>) {
5.13 - if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
5.14 - $defs{lc $1} = 1;
5.15 - }
5.16 - while (m,\\seeglossary *\{((\w|\s)+)\},g) {
5.17 - $refs{lc $1} = 1;
5.18 - }
5.19 -}
5.20 -
5.21 -print "Glossary definitions:\n";
5.22 -foreach (sort(keys(%defs))) {
5.23 - print " \"$_\"\n";
5.24 -}
5.25 -
5.26 -foreach (keys(%refs)) {
5.27 - s,s$,,;
5.28 - if (!defined($defs{$_})) {
5.29 - print "### Undefined glossary reference: \"$_\"\n";
5.30 - }
5.31 -}
6.1 --- a/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:04:15 2009 +0100
6.2 +++ b/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:23:33 2009 +0100
6.3 @@ -20,9 +20,6 @@
6.4 and Larry Paulson
6.5 }
6.6
6.7 -%FIXME
6.8 -%\makeglossary
6.9 -
6.10 \makeindex
6.11
6.12
6.13 @@ -85,10 +82,6 @@
6.14 \bibliography{../manual}
6.15 \endgroup
6.16
6.17 -%FIXME
6.18 -%\tocentry{\glossaryname}
6.19 -%\printglossary
6.20 -
6.21 \tocentry{\indexname}
6.22 \printindex
6.23
7.1 --- a/doc-src/IsarImplementation/makeglossary Mon Feb 16 21:04:15 2009 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,6 +0,0 @@
7.4 -#!/bin/sh
7.5 -# $Id$
7.6 -
7.7 -NAME="$1"
7.8 -makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
7.9 -./checkglossary "${NAME}.glo"
8.1 --- a/doc-src/IsarImplementation/style.sty Mon Feb 16 21:04:15 2009 +0100
8.2 +++ b/doc-src/IsarImplementation/style.sty Mon Feb 16 21:23:33 2009 +0100
8.3 @@ -1,6 +1,3 @@
8.4 -
8.5 -%% $Id$
8.6 -
8.7 %% toc
8.8 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
8.9 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
8.10 @@ -10,13 +7,6 @@
8.11 \newcommand{\chref}[1]{chapter~\ref{#1}}
8.12 \newcommand{\figref}[1]{figure~\ref{#1}}
8.13
8.14 -%% glossary
8.15 -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
8.16 -\newcommand{\seeglossary}[1]{\emph{#1}}
8.17 -\newcommand{\glossaryname}{Glossary}
8.18 -\renewcommand{\nomname}{\glossaryname}
8.19 -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
8.20 -
8.21 %% index
8.22 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
8.23 \newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
8.24 @@ -61,6 +51,7 @@
8.25
8.26 \isabellestyle{it}
8.27
8.28 +
8.29 %%% Local Variables:
8.30 %%% mode: latex
8.31 %%% TeX-master: "implementation"