# HG changeset patch # User wenzelm # Date 1234815813 -3600 # Node ID 7a3b5bbed31318e586506177495374f3889af715 # Parent ce2b8e6502f94457ecf9264aca6a811b1782d632 removed rudiments of glossary; diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/Makefile --- a/doc-src/IsarImplementation/Makefile Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/Makefile Mon Feb 16 21:23:33 2009 +0100 @@ -8,8 +8,6 @@ include ../Makefile.in -MAKEGLOSSARY = ./makeglossary - NAME = implementation FILES = implementation.tex Thy/document/Prelim.tex \ @@ -26,7 +24,6 @@ $(BIBTEX) $(NAME) $(LATEX) $(NAME) $(LATEX) $(NAME) - $(MAKEGLOSSARY) $(NAME) $(SEDINDEX) $(NAME) $(LATEX) $(NAME) $(LATEX) $(NAME) @@ -38,7 +35,6 @@ $(BIBTEX) $(NAME) $(PDFLATEX) $(NAME) $(PDFLATEX) $(NAME) - $(MAKEGLOSSARY) $(NAME) $(SEDINDEX) $(NAME) $(FIXBOOKMARKS) $(NAME).out $(PDFLATEX) $(NAME) diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:23:33 2009 +0100 @@ -186,12 +186,9 @@ *} - section {* Terms \label{sec:terms} *} text {* - \glossary{Term}{FIXME} - The language of terms is that of simply-typed @{text "\"}-calculus with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72} or \cite{paulson-ml2}), with the types being determined determined @@ -392,42 +389,6 @@ section {* Theorems \label{sec:thms} *} text {* - \glossary{Proposition}{FIXME A \seeglossary{term} of - \seeglossary{type} @{text "prop"}. Internally, there is nothing - special about propositions apart from their type, but the concrete - syntax enforces a clear distinction. Propositions are structured - via implication @{text "A \ B"} or universal quantification @{text - "\x. B x"} --- anything else is considered atomic. The canonical - form for propositions is that of a \seeglossary{Hereditary Harrop - Formula}. FIXME} - - \glossary{Theorem}{A proven proposition within a certain theory and - proof context, formally @{text "\ \\<^sub>\ \"}; both contexts are - rarely spelled out explicitly. Theorems are usually normalized - according to the \seeglossary{HHF} format. FIXME} - - \glossary{Fact}{Sometimes used interchangeably for - \seeglossary{theorem}. Strictly speaking, a list of theorems, - essentially an extra-logical conjunction. Facts emerge either as - local assumptions, or as results of local goal statements --- both - may be simultaneous, hence the list representation. FIXME} - - \glossary{Schematic variable}{FIXME} - - \glossary{Fixed variable}{A variable that is bound within a certain - proof context; an arbitrary-but-fixed entity within a portion of - proof text. FIXME} - - \glossary{Free variable}{Synonymous for \seeglossary{fixed - variable}. FIXME} - - \glossary{Bound variable}{FIXME} - - \glossary{Variable}{See \seeglossary{schematic variable}, - \seeglossary{fixed variable}, \seeglossary{bound variable}, or - \seeglossary{type variable}. The distinguishing feature of - different variables is their binding scope. FIXME} - A \emph{proposition} is a well-typed term of type @{text "prop"}, a \emph{theorem} is a proven proposition (depending on a context of hypotheses and the background theory). Primitive inferences include @@ -436,6 +397,7 @@ notion of equality/equivalence @{text "\"}. *} + subsection {* Primitive connectives and rules \label{sec:prim-rules} *} text {* @@ -801,16 +763,13 @@ expect a normal form: quantifiers @{text "\"} before implications @{text "\"} at each level of nesting. -\glossary{Hereditary Harrop Formula}{The set of propositions in HHF -format is defined inductively as @{text "H = (\x\<^sup>*. H\<^sup>* \ -A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. -Any proposition may be put into HHF form by normalizing with the rule -@{text "(A \ (\x. B x)) \ (\x. A \ B x)"}. In Isabelle, the outermost -quantifier prefix is represented via \seeglossary{schematic -variables}, such that the top-level structure is merely that of a -\seeglossary{Horn Clause}}. - -\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.} + The set of propositions in HHF format is defined inductively as + @{text "H = (\x\<^sup>*. H\<^sup>* \ A)"}, for variables @{text "x"} + and atomic propositions @{text "A"}. Any proposition may be put + into HHF form by normalizing with the rule @{text "(A \ (\x. B x)) \ + (\x. A \ B x)"}. In Isabelle, the outermost quantifier prefix is + represented via schematic variables, such that the top-level + structure is merely that of a Horn Clause. \[ diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Feb 16 21:23:33 2009 +0100 @@ -74,8 +74,6 @@ subsection {* Theory context \label{sec:context-theory} *} text {* - \glossary{Theory}{FIXME} - A \emph{theory} is a data container with explicit named and unique identifier. Theories are related by a (nominal) sub-theory relation, which corresponds to the dependency graph of the original @@ -201,13 +199,6 @@ subsection {* Proof context \label{sec:context-proof} *} text {* - \glossary{Proof context}{The static context of a structured proof, - acts like a local ``theory'' of the current portion of Isar proof - text, generalizes the idea of local hypotheses @{text "\"} in - judgments @{text "\ \ \"} of natural deduction calculi. There is a - generic notion of introducing and discharging hypotheses. - Arbritrary auxiliary context data may be adjoined.} - A proof context is a container for pure data with a back-reference to the theory it belongs to. The @{text "init"} operation creates a proof context from a given theory. Modifications to draft theories @@ -231,7 +222,7 @@ context is extended consecutively, and results are exported back into the original context. Note that the Isar proof states model block-structured reasoning explicitly, using a stack of proof - contexts internally, cf.\ \secref{sec:isar-proof-state}. + contexts internally. *} text %mlref {* @@ -418,10 +409,6 @@ subsection {* Strings of symbols *} text {* - \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes - plain ASCII characters as well as an infinite collection of named - symbols (for greek, math etc.).} - A \emph{symbol} constitutes the smallest textual unit in Isabelle --- raw characters are normally not encountered at all. Isabelle strings consist of a sequence of symbols, represented as a packed @@ -465,8 +452,8 @@ link to the standard collection of Isabelle. \medskip Output of Isabelle symbols depends on the print mode - (\secref{FIXME}). For example, the standard {\LaTeX} setup of the - Isabelle document preparation system would present + (\secref{print-mode}). For example, the standard {\LaTeX} setup of + the Isabelle document preparation system would present ``\verb,\,\verb,,'' as @{text "\"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text "\<^bold>\"}. diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Mon Feb 16 21:23:33 2009 +0100 @@ -18,21 +18,14 @@ section {* Goals \label{sec:tactical-goals} *} text {* - Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of - \seeglossary{Horn Clause} form stating that a number of subgoals - imply the main conclusion, which is marked as a protected - proposition.} as a theorem stating that the subgoals imply the main - goal: @{text "A\<^sub>1 \ \ \ A\<^sub>n \ C"}. The outermost goal - structure is that of a Horn Clause\glossary{Horn Clause}{An iterated - implication @{text "A\<^sub>1 \ \ \ A\<^sub>n \ C"}, without any - outermost quantifiers. Strictly speaking, propositions @{text - "A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits - arbitrary substructure here (nested @{text "\"} and @{text "\"} - connectives).}: i.e.\ an iterated implication without any - quantifiers\footnote{Recall that outermost @{text "\x. \[x]"} is - always represented via schematic variables in the body: @{text - "\[?x]"}. These variables may get instantiated during the course of - reasoning.}. For @{text "n = 0"} a goal is called ``solved''. + Isabelle/Pure represents a goal as a theorem stating that the + subgoals imply the main goal: @{text "A\<^sub>1 \ \ \ A\<^sub>n \ + C"}. The outermost goal structure is that of a Horn Clause: i.e.\ + an iterated implication without any quantifiers\footnote{Recall that + outermost @{text "\x. \[x]"} is always represented via schematic + variables in the body: @{text "\[?x]"}. These variables may get + instantiated during the course of reasoning.}. For @{text "n = 0"} + a goal is called ``solved''. The structure of each subgoal @{text "A\<^sub>i"} is that of a general Hereditary Harrop Formula @{text "\x\<^sub>1 \ \x\<^sub>k. H\<^sub>1 \ \ \ H\<^sub>m \ B"} in @@ -45,14 +38,9 @@ exceeds 1--2 in practice. The main conclusion @{text C} is internally marked as a protected - proposition\glossary{Protected proposition}{An arbitrarily - structured proposition @{text "C"} which is forced to appear as - atomic by wrapping it into a propositional identity operator; - notation @{text "#C"}. Protecting a proposition prevents basic - inferences from entering into that structure for the time being.}, - which is represented explicitly by the notation @{text "#C"}. This - ensures that the decomposition into subgoals and main conclusion is - well-defined for arbitrarily structured claims. + proposition, which is represented explicitly by the notation @{text + "#C"}. This ensures that the decomposition into subgoals and main + conclusion is well-defined for arbitrarily structured claims. \medskip Basic goal management is performed via the following Isabelle/Pure rules: @@ -405,14 +393,12 @@ section {* Tacticals \label{sec:tacticals} *} text {* - -FIXME + A \emph{tactical} is a functional combinator for building up complex + tactics from simpler ones. Typical tactical perform sequential + composition, disjunction (choice), iteration, or goal addressing. + Various search strategies may be expressed via tacticals. -\glossary{Tactical}{A functional combinator for building up complex -tactics from simpler ones. Typical tactical perform sequential -composition, disjunction (choice), iteration, or goal addressing. -Various search strategies may be expressed via tacticals.} - + \medskip FIXME *} end diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/checkglossary --- a/doc-src/IsarImplementation/checkglossary Mon Feb 16 21:04:15 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -#!/usr/bin/env perl -# $Id$ - -use strict; - -my %defs = (); -my %refs = (); - -while () { - if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) { - $defs{lc $1} = 1; - } - while (m,\\seeglossary *\{((\w|\s)+)\},g) { - $refs{lc $1} = 1; - } -} - -print "Glossary definitions:\n"; -foreach (sort(keys(%defs))) { - print " \"$_\"\n"; -} - -foreach (keys(%refs)) { - s,s$,,; - if (!defined($defs{$_})) { - print "### Undefined glossary reference: \"$_\"\n"; - } -} diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/implementation.tex --- a/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/implementation.tex Mon Feb 16 21:23:33 2009 +0100 @@ -20,9 +20,6 @@ and Larry Paulson } -%FIXME -%\makeglossary - \makeindex @@ -85,10 +82,6 @@ \bibliography{../manual} \endgroup -%FIXME -%\tocentry{\glossaryname} -%\printglossary - \tocentry{\indexname} \printindex diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/makeglossary --- a/doc-src/IsarImplementation/makeglossary Mon Feb 16 21:04:15 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -#!/bin/sh -# $Id$ - -NAME="$1" -makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo" -./checkglossary "${NAME}.glo" diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/style.sty --- a/doc-src/IsarImplementation/style.sty Mon Feb 16 21:04:15 2009 +0100 +++ b/doc-src/IsarImplementation/style.sty Mon Feb 16 21:23:33 2009 +0100 @@ -1,6 +1,3 @@ - -%% $Id$ - %% toc \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} @@ -10,13 +7,6 @@ \newcommand{\chref}[1]{chapter~\ref{#1}} \newcommand{\figref}[1]{figure~\ref{#1}} -%% glossary -\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}} -\newcommand{\seeglossary}[1]{\emph{#1}} -\newcommand{\glossaryname}{Glossary} -\renewcommand{\nomname}{\glossaryname} -\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}} - %% index \newcommand{\indexml}[1]{\index{\emph{#1}|bold}} \newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}} @@ -61,6 +51,7 @@ \isabellestyle{it} + %%% Local Variables: %%% mode: latex %%% TeX-master: "implementation"