| author | lcp |
| Tue, 03 May 1994 18:38:28 +0200 | |
| changeset 359 | b5a2e9503a7a |
| parent 358 | df8f0fbf7dbd |
| child 360 | 2b74eebdbdb8 |
--- a/doc-src/Intro/intro.bbl Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Intro/intro.bbl Tue May 03 18:38:28 1994 +0200 @@ -5,28 +5,28 @@ \newblock {\em Logic for Information Technology}. \newblock Wiley, 1990. -\bibitem{gordon88a} -Michael J.~C. Gordon. -\newblock {HOL}: A proof generating system for higher-order logic. -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI} - Specification, Verification and Synthesis}, pages 73--128. Kluwer Academic - Publishers, 1988. +\bibitem{mgordon-hol} +M.~J.~C. Gordon and T.~F. Melham. +\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher + Order Logic}. +\newblock Cambridge University Press, 1993. -\bibitem{gordon79} +\bibitem{mgordon79} Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth. \newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}. -\newblock Springer LNCS 78, 1979. +\newblock Springer, 1979. +\newblock LNCS 78. \bibitem{haskell-tutorial} Paul Hudak and Joseph~H. Fasel. \newblock A gentle introduction to {Haskell}. -\newblock {\em {ACM} {SIGPLAN} Notices}, 27(5), May 1992. +\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992. \bibitem{haskell-report} Paul Hudak, Simon~Peyton Jones, and Philip Wadler. \newblock Report on the programming language {Haskell}: A non-strict, purely functional language. -\newblock {\em {ACM} {SIGPLAN} Notices}, 27(5), May 1992. +\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992. \newblock Version 1.2. \bibitem{huet75} @@ -34,7 +34,7 @@ \newblock A unification algorithm for typed $\lambda$-calculus. \newblock {\em Theoretical Computer Science}, 1:27--57, 1975. -\bibitem{miller-jsc} +\bibitem{miller-mixed} Dale Miller. \newblock Unification under a mixed prefix. \newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992. @@ -42,13 +42,15 @@ \bibitem{nipkow-prehofer} Tobias Nipkow and Christian Prehofer. \newblock Type checking type classes. -\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993. -\newblock To appear. +\newblock In {\em 20th Principles of Programming Languages}, pages 409--418. + ACM Press, 1993. +\newblock Revised version to appear in \bgroup\em Journal of Functional + Programming\egroup. \bibitem{nordstrom90} Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. -\newblock Oxford, 1990. +\newblock Oxford University Press, 1990. \bibitem{paulson86} Lawrence~C. Paulson. @@ -63,7 +65,7 @@ \bibitem{paulson89} Lawrence~C. Paulson. \newblock The foundation of a generic theorem prover. -\newblock {\em Journal of Automated Reasoning}, 5:363--397, 1989. +\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989. \bibitem{paulson700} Lawrence~C. Paulson.
--- a/doc-src/Intro/intro.ind Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Intro/intro.ind Tue May 03 18:38:28 1994 +0200 @@ -1,251 +1,265 @@ \begin{theindex} - \item $\Forall$, \bold{5}, 7 - \item $\Imp$, \bold{5} - \item $\To$, \bold{1}, \bold{3} - \item $\equiv$, \bold{5} - - \indexspace - - \item {\tt allI}, 35 - \item arities - \subitem declaring, 3, \bold{46} - \item {\tt asm_simp_tac}, 55 - \item associativity of addition, 54 - \item {\tt assume_tac}, \bold{27}, 29, 30, 35, 43, 44 - \item assumptions, 6 + \item {\ptt !!} symbol, 24 + \subitem in main goal, 44 + \item {\tt\%} symbol, 24 + \item {\ptt ::} symbol, 24 + \item {\ptt ==} symbol, 24 + \item {\ptt ==>} symbol, 24 + \item {\ptt =>} symbol, 24 + \item {\ptt =?=} symbol, 24 + \item {\ptt [} symbol, 24 + \item {\ptt [|} symbol, 24 + \item {\ptt ]} symbol, 24 + \item {\tt\ttlbrace} symbol, 24 + \item {\tt\ttrbrace} symbol, 24 + \item {\ptt |]} symbol, 24 \indexspace - \item {\tt ba}, \bold{28} - \item {\tt back}, 54, 57 - \item backtracking, 57 - \item {\tt bd}, \bold{28} - \item {\tt be}, \bold{28} - \item {\tt br}, \bold{28} - \item {\tt by}, \bold{28} + \item {\ptt allI} theorem, 35 + \item arities + \subitem declaring, 4, \bold{46} + \item {\ptt asm_simp_tac}, 56 + \item {\ptt assume_tac}, 28, 30, 35, 44 + \item assumptions + \subitem deleting, 19 + \subitem discharge of, 7 + \subitem lifting over, 13 + \subitem of main goal, 39 + \subitem use of, 16, 27 + \item axioms + \subitem Peano, 51 \indexspace - \item {\tt choplev}, 34, 35, 59 - \item classes, \bold{3} - \subitem built-in, \bold{23} - \item classical reasoning package, 36 - \item classical sets, \bold{36} - \item {\tt conjunct1}, 25 - \item constants - \subitem declaring, \bold{45} + \item {\ptt ba}, 29 + \item {\ptt back}, 54, 55, 58 + \item backtracking + \subitem Prolog style, 58 + \item {\ptt bd}, 29 + \item {\ptt be}, 29 + \item {\ptt br}, 29 + \item {\ptt by}, 29 \indexspace - \item definitions, \bold{5} - \subitem reasoning about, \bold{40} - \item {\tt DEPTH_FIRST}, 59 - \item destruct-resolution, \bold{20} - \item destruction rules, \bold{20} - \item {\tt disjE}, 29 - \item {\tt dres_inst_tac}, \bold{52} - \item {\tt dresolve_tac}, \bold{28}, 30, 33, 36 + \item {\ptt choplev}, 34, 35, 60 + \item classes, 3 + \subitem built-in, \bold{24} + \item classical reasoner, 37 + \item {\ptt conjunct1} theorem, 26 + \item constants, 1 + \subitem clashes with variables, 9 + \subitem declaring, \bold{46} + \subitem overloaded, 50 + \subitem polymorphic, 3 + + \indexspace + + \item definitions, 5, \bold{46} + \subitem and derived rules, 41--44 + \item {\ptt DEPTH_FIRST}, 59 + \item destruct-resolution, 21, 29 + \item {\ptt disjE} theorem, 30 + \item {\ptt dres_inst_tac}, 53 + \item {\ptt dresolve_tac}, 29, 31, 36 \indexspace \item eigenvariables, \see{parameters}{7} - \item elim-resolution, \bold{18} + \item elim-resolution, \bold{19}, 28 \item equality - \subitem meta-level, \bold{5} - \item {\tt eres_inst_tac}, \bold{52} - \item {\tt eresolve_tac}, \bold{27}, 30, 36, 43, 44 + \subitem polymorphic, 3 + \item {\ptt eres_inst_tac}, 53 + \item {\ptt eresolve_tac}, 28, 31, 36, 44 \item examples - \subitem of deriving rules, 38 - \subitem of induction, 52, 53 - \subitem of rewriting, 54 + \subitem of deriving rules, 39 + \subitem of induction, 53, 54 + \subitem of simplification, 55 \subitem of tacticals, 35 - \subitem of theories, 45--51, 56 - \subitem propositional, 16, 28, 30 - \subitem with quantifiers, 17, 31, 33, 35 - \item {\tt exE}, 35 + \subitem of theories, 46--52, 57 + \subitem propositional, 16, 29, 31 + \subitem with quantifiers, 17, 32, 33, 36 + \item {\ptt exE} theorem, 36 \indexspace - \item {\tt FalseE}, 42 - \item {\tt fast_tac}, 36, 37 - \item flex-flex equations, \bold{5}, 23, \bold{26} - \item {\tt flexflex_rule}, 26 - \item {\tt FOL}, 56 - \item {\tt FOL.thy}, 28 - \item folding, \bold{40} - - \indexspace - - \item {\tt goal}, \bold{28}, 38, 39, 41--43 - \item {\tt goalw}, 42, 43 + \item {\ptt FalseE} theorem, 43 + \item {\ptt fast_tac}, 37 + \item first-order logic, 1 + \item flex-flex constraints, 5, 24, \bold{27} + \item {\ptt flexflex_rule}, 27 + \item forward proof, 20, 23--29 + \item {\ptt fun} type, 1, 4 + \item function applications, 1, 7 \indexspace - \item {\tt has_fewer_prems}, 59 + \item {\ptt goal}, 29, 39, 44 + \item {\ptt goalw}, 42--44 + + \indexspace + + \item {\ptt has_fewer_prems}, 60 + \item higher-order logic, 4 \indexspace - \item identifiers, \bold{22} - \item imitation, \bold{10} - \item {\tt impI}, 29, 41 - \item implication - \subitem meta-level, \bold{5} - \item infix operators, \bold{47} - \item instantiation - \subitem explicit, \bold{52} + \item identifiers, 23 + \item {\ptt impI} theorem, 30, 42 + \item infixes, 48 + \item instantiation, 53--56 \item Isabelle - \subitem definitions in, 40 - \subitem formalizing rules, \bold{5} - \subitem formalizing syntax, \bold{1} - \subitem getting started, 22 \subitem object-logics supported, i \subitem overview, i - \subitem proof construction in, \bold{9} \subitem release history, i - \subitem syntax of, 23 \indexspace - \item LCF, i, 14, 24 - \item level, \bold{29} + \item $\lambda$-abstractions, 1, 7, 24 + \item $\lambda$-calculus, 1 + \item LCF, i + \item LCF system, 15, 25 + \item level of a proof, 29 \item lifting, \bold{13} - \subitem over assumptions, \bold{13} - \subitem over parameters, \bold{13} - \item {\tt logic}, 23 + \item {\ptt logic} class, 3, 6, 24 \indexspace - \item main goal, \bold{14} - \item major premise, \bold{19} - \item {\tt Match}, 39 - \item meta-formulae - \subitem syntax, \bold{23} - \item meta-logic, \bold{5} - \item mixfix operators, \bold{47} - \item ML, i, 22, 25 - \item {\tt mp}, 25 + \item major premise, \bold{20} + \item {\ptt Match} exception, 40 + \item meta-assumptions + \subitem syntax of, 21 + \item meta-equality, \bold{5}, 24 + \item meta-implication, \bold{5}, 6, 24 + \item meta-quantifiers, \bold{5}, 7, 24 + \item meta-rewriting, 41 + \item mixfix declarations, 49, 52 + \item ML, i + \item {\ptt ML} section, 45 + \item {\ptt mp} theorem, 26 \indexspace - \item {\tt Nat}, \bold{51} - \item {\tt Nat.thy}, 53 - \item {\tt not_def}, 41 - \item {\tt notE}, \bold{43}, 53 - \item {\tt notI}, \bold{41}, 53 + \item {\ptt Nat} theory, 52 + \item {\ptt nat} type, 1, 3 + \item {\ptt not_def} theorem, 42 + \item {\ptt notE} theorem, \bold{43}, 54 + \item {\ptt notI} theorem, \bold{42}, 54 \indexspace - \item {\tt ORELSE}, 35 - \item overloading, \bold{4}, 48 + \item {\ptt o} type, 1, 4 + \item {\ptt ORELSE}, 35 + \item overloading, \bold{4}, 50 \indexspace - \item parameters, \bold{7}, 31 - \item printing commands, \bold{25} - \item projection, \bold{10} - \item {\tt Prolog}, 56 - \item Prolog interpreter, \bold{55} - \item proof - \subitem backward, \bold{14} - \subitem by assumption, \bold{15} - \subitem by induction, 52 - \subitem commands for, \bold{28} - \subitem forward, 20 - \item proof state, \bold{14} - \item {\tt PROP}, 24 - \item {\tt prop}, 23, 24 - \item {\tt prth}, \bold{25} - \item {\tt prthq}, \bold{25}, 26 - \item {\tt prths}, \bold{25} - \item {\tt Pure}, \bold{44} + \item parameters, \bold{7}, 32 + \subitem lifting over, 14 + \item {\ptt Prolog} theory, 57 + \item Prolog interpreter, \bold{56} + \item proof state, 15 + \item proofs + \subitem commands for, 29 + \item {\ptt PROP} symbol, 25 + \item {\ptt prop} type, 6, 24 + \item {\ptt prth}, 26 + \item {\ptt prthq}, 26, 27 + \item {\ptt prths}, 26 + \item {\ptt Pure} theory, 45 + + \indexspace + + \item quantifiers, 5, 7, 32 \indexspace - \item quantifiers - \subitem meta-level, \bold{5} - \subitem reasoning about, 31 - - \indexspace - - \item {\tt read_instantiate}, 27 - \item refinement, \bold{15} - \subitem with instantiation, \bold{52} - \item {\tt refl}, 27 - \item {\tt REPEAT}, 30, 35, 57, 59 - \item {\tt res_inst_tac}, \bold{52}, 54, 55 - \item reserved words, \bold{22} - \item resolution, \bold{11} - \subitem in backward proof, 14 - \item {\tt resolve_tac}, \bold{27}, 29, 43, 53 - \item {\tt result}, \bold{28}, 29, 38, 39, 44 - \item {\tt rewrite_goals_tac}, 41, 42 - \item {\tt rewrite_rule}, 42, 43 - \item rewriting - \subitem meta-level, 40, \bold{40} - \subitem object-level, 54 - \item {\tt RL}, 27 - \item {\tt RLN}, 27 - \item {\tt RS}, \bold{25}, 27, 43 - \item {\tt RSN}, \bold{25}, 27 + \item {\ptt read_instantiate}, 28 + \item {\ptt refl} theorem, 28 + \item {\ptt REPEAT}, 31, 36, 58, 59 + \item {\ptt res_inst_tac}, 53, 55 + \item reserved words, 23 + \item resolution, 10, \bold{11} + \subitem in backward proof, 15 + \subitem with instantiation, 53 + \item {\ptt resolve_tac}, 28, 30, 43, 54 + \item {\ptt result}, 29, 40, 44 + \item {\ptt rewrite_goals_tac}, 42 + \item {\ptt rewrite_rule}, 43 + \item {\ptt RL}, 27, 28 + \item {\ptt RLN}, 27 + \item {\ptt RS}, 26, 27, 44 + \item {\ptt RSN}, 26, 27 \item rules - \subitem declaring, \bold{45} - \subitem derived, 12, \bold{20}, 38, 40 - \subitem propositional, \bold{6} - \subitem quantifier, \bold{7} + \subitem declaring, 46 + \subitem derived, 12, \bold{21}, 39, 41 + \subitem destruction, 20 + \subitem elimination, 20 + \subitem propositional, 6 + \subitem quantifier, 7 \indexspace \item search - \subitem depth-first, 58 + \subitem depth-first, 59 \item signatures, \bold{8} - \item {\tt simp_tac}, 55 - \item simplification set, \bold{54} + \item {\ptt simp_tac}, 56 + \item simplification, 55 + \item simplification sets, 55 + \item sort constraints, 24 \item sorts, \bold{4} - \item {\tt spec}, 26, 33, 35 - \item {\tt standard}, \bold{25} - \item subgoals, \bold{14} + \item {\ptt spec} theorem, 26, 34, 35 + \item {\ptt standard}, 26 \item substitution, \bold{7} - \item {\tt Suc_inject}, 53 - \item {\tt Suc_neq_0}, 53 + \item {\ptt Suc_inject}, 54 + \item {\ptt Suc_neq_0}, 54 + \item syntax + \subitem of types and terms, 24 \indexspace - \item tacticals, \bold{14}, \bold{17}, 35 - \item Tactics, \bold{14} - \item tactics, \bold{17} - \subitem basic, \bold{27} + \item tacticals, \bold{18}, 35 + \item tactics, \bold{18} + \subitem assumption, 28 + \subitem resolution, 28 + \item {\ptt term} class, 3 \item terms - \subitem syntax, \bold{23} + \subitem syntax of, 1, \bold{24} \item theorems - \subitem basic operations on, \bold{24} + \subitem basic operations on, \bold{25} + \subitem printing of, 25 \item theories, \bold{8} - \subitem defining, 44--52 - \item {\tt thm}, 24 - \item {\tt topthm}, 39 - \item {$Trueprop$}, 6, 7, 9, 23 - \item type constructors + \subitem defining, 44--53 + \item {\ptt thm} ML type, 25 + \item {\ptt topthm}, 40 + \item {\ptt Trueprop} constant, 6, 24 + \item type constraints, 24 + \item type constructors, 1 + \item type identifiers, 23 + \item type synonyms, \bold{48} + \item types \subitem declaring, \bold{46} - \item types, 1 - \subitem higher, \bold{4} + \subitem function, 1 + \subitem higher, \bold{5} \subitem polymorphic, \bold{3} \subitem simple, \bold{1} - \subitem syntax, \bold{23} + \subitem syntax of, 1, \bold{24} \indexspace - \item {\tt undo}, \bold{28} - \item unfolding, \bold{40} + \item {\ptt undo}, 29 \item unification - \subitem higher-order, \bold{10}, 53 - \item unknowns, \bold{9}, 31 - \subitem of function type, \bold{11}, 26 - \item {\tt use_thy}, \bold{44, 45} + \subitem higher-order, \bold{10}, 54 + \subitem incompleteness of, 11 + \item unknowns, 9, 23, 32 + \subitem function, \bold{11}, 27, 32 + \item {\ptt use_thy}, \bold{45} \indexspace \item variables \subitem bound, 7 - \subitem schematic, \see{unknowns}{9} \end{theindex}
--- a/doc-src/Intro/intro.toc Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Intro/intro.toc Tue May 03 18:38:28 1994 +0200 @@ -2,7 +2,7 @@ \contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1} \contentsline {subsection}{\numberline {1.1}Simple types and constants}{1} \contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3} -\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{4} +\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{5} \contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5} \contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6} \contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7} @@ -10,58 +10,61 @@ \contentsline {section}{\numberline {3}Proof construction in Isabelle}{9} \contentsline {subsection}{\numberline {3.1}Higher-order unification}{10} \contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11} -\contentsline {subsection}{\numberline {3.3}Lifting a rule into a context}{13} -\contentsline {subsubsection}{Lifting over assumptions}{13} -\contentsline {subsubsection}{Lifting over parameters}{13} -\contentsline {section}{\numberline {4}Backward proof by resolution}{14} -\contentsline {subsection}{\numberline {4.1}Refinement by resolution}{15} -\contentsline {subsection}{\numberline {4.2}Proof by assumption}{15} -\contentsline {subsection}{\numberline {4.3}A propositional proof}{16} -\contentsline {subsection}{\numberline {4.4}A quantifier proof}{17} -\contentsline {subsection}{\numberline {4.5}Tactics and tacticals}{17} -\contentsline {section}{\numberline {5}Variations on resolution}{18} -\contentsline {subsection}{\numberline {5.1}Elim-resolution}{18} -\contentsline {subsection}{\numberline {5.2}Destruction rules}{20} -\contentsline {subsection}{\numberline {5.3}Deriving rules by resolution}{20} -\contentsline {part}{\uppercase {ii}\phspace {1em}Getting started with Isabelle}{22} -\contentsline {section}{\numberline {6}Forward proof}{22} -\contentsline {subsection}{\numberline {6.1}Lexical matters}{22} -\contentsline {subsection}{\numberline {6.2}Syntax of types and terms}{23} -\contentsline {subsection}{\numberline {6.3}Basic operations on theorems}{24} -\contentsline {subsection}{\numberline {6.4}Flex-flex equations}{26} -\contentsline {section}{\numberline {7}Backward proof}{27} -\contentsline {subsection}{\numberline {7.1}The basic tactics}{27} -\contentsline {subsection}{\numberline {7.2}Commands for backward proof}{28} -\contentsline {subsection}{\numberline {7.3}A trivial example in propositional logic}{28} -\contentsline {subsection}{\numberline {7.4}Proving a distributive law}{30} -\contentsline {section}{\numberline {8}Quantifier reasoning}{31} -\contentsline {subsection}{\numberline {8.1}Two quantifier proofs, successful and not}{31} -\contentsline {subsubsection}{The successful proof}{31} -\contentsline {subsubsection}{The unsuccessful proof}{32} -\contentsline {subsection}{\numberline {8.2}Nested quantifiers}{33} -\contentsline {subsubsection}{The wrong approach}{33} -\contentsline {subsubsection}{The right approach}{34} -\contentsline {subsubsection}{A one-step proof using tacticals}{35} -\contentsline {subsection}{\numberline {8.3}A realistic quantifier proof}{35} -\contentsline {subsection}{\numberline {8.4}The classical reasoning package}{36} -\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced methods}{38} -\contentsline {section}{\numberline {9}Deriving rules in Isabelle}{38} -\contentsline {subsection}{\numberline {9.1}Deriving a rule using tactics}{38} -\contentsline {subsection}{\numberline {9.2}Definitions and derived rules}{40} -\contentsline {subsubsection}{Deriving the introduction rule}{41} -\contentsline {subsubsection}{Deriving the elimination rule}{42} -\contentsline {section}{\numberline {10}Defining theories}{44} -\contentsline {subsection}{\numberline {10.1}Declaring constants and rules}{45} -\contentsline {subsection}{\numberline {10.2}Declaring type constructors}{46} -\contentsline {subsection}{\numberline {10.3}Infixes and Mixfixes}{47} -\contentsline {subsection}{\numberline {10.4}Overloading}{48} -\contentsline {subsection}{\numberline {10.5}Extending first-order logic with the natural numbers}{50} -\contentsline {subsection}{\numberline {10.6}Declaring the theory to Isabelle}{51} -\contentsline {section}{\numberline {11}Refinement with explicit instantiation}{52} -\contentsline {subsection}{\numberline {11.1}A simple proof by induction}{52} -\contentsline {subsection}{\numberline {11.2}An example of ambiguity in {\ptt resolve_tac}}{53} -\contentsline {subsection}{\numberline {11.3}Proving that addition is associative}{54} -\contentsline {section}{\numberline {12}A {\psc Prolog} interpreter}{55} -\contentsline {subsection}{\numberline {12.1}Simple executions}{56} -\contentsline {subsection}{\numberline {12.2}Backtracking}{57} -\contentsline {subsection}{\numberline {12.3}Depth-first search}{58} +\contentsline {section}{\numberline {4}Lifting a rule into a context}{13} +\contentsline {subsection}{\numberline {4.1}Lifting over assumptions}{13} +\contentsline {subsection}{\numberline {4.2}Lifting over parameters}{14} +\contentsline {section}{\numberline {5}Backward proof by resolution}{15} +\contentsline {subsection}{\numberline {5.1}Refinement by resolution}{15} +\contentsline {subsection}{\numberline {5.2}Proof by assumption}{16} +\contentsline {subsection}{\numberline {5.3}A propositional proof}{16} +\contentsline {subsection}{\numberline {5.4}A quantifier proof}{17} +\contentsline {subsection}{\numberline {5.5}Tactics and tacticals}{18} +\contentsline {section}{\numberline {6}Variations on resolution}{18} +\contentsline {subsection}{\numberline {6.1}Elim-resolution}{19} +\contentsline {subsection}{\numberline {6.2}Destruction rules}{20} +\contentsline {subsection}{\numberline {6.3}Deriving rules by resolution}{21} +\contentsline {part}{\uppercase {ii}\phspace {1em}Getting Started with Isabelle}{23} +\contentsline {section}{\numberline {7}Forward proof}{23} +\contentsline {subsection}{\numberline {7.1}Lexical matters}{23} +\contentsline {subsection}{\numberline {7.2}Syntax of types and terms}{24} +\contentsline {subsection}{\numberline {7.3}Basic operations on theorems}{25} +\contentsline {subsection}{\numberline {7.4}*Flex-flex constraints}{27} +\contentsline {section}{\numberline {8}Backward proof}{28} +\contentsline {subsection}{\numberline {8.1}The basic tactics}{28} +\contentsline {subsection}{\numberline {8.2}Commands for backward proof}{29} +\contentsline {subsection}{\numberline {8.3}A trivial example in propositional logic}{29} +\contentsline {subsection}{\numberline {8.4}Part of a distributive law}{31} +\contentsline {section}{\numberline {9}Quantifier reasoning}{32} +\contentsline {subsection}{\numberline {9.1}Two quantifier proofs: a success and a failure}{32} +\contentsline {paragraph}{The successful proof.}{32} +\contentsline {paragraph}{The unsuccessful proof.}{33} +\contentsline {subsection}{\numberline {9.2}Nested quantifiers}{33} +\contentsline {paragraph}{The wrong approach.}{34} +\contentsline {paragraph}{The right approach.}{34} +\contentsline {paragraph}{A one-step proof using tacticals.}{35} +\contentsline {subsection}{\numberline {9.3}A realistic quantifier proof}{36} +\contentsline {subsection}{\numberline {9.4}The classical reasoner}{37} +\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced Methods}{39} +\contentsline {section}{\numberline {10}Deriving rules in Isabelle}{39} +\contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and meta-level assumptions}{39} +\contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41} +\contentsline {subsection}{\numberline {10.3}Deriving the $\neg $ introduction rule}{41} +\contentsline {subsection}{\numberline {10.4}Deriving the $\neg $ elimination rule}{42} +\contentsline {section}{\numberline {11}Defining theories}{44} +\contentsline {subsection}{\numberline {11.1}Declaring constants and rules}{46} +\contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46} +\contentsline {subsection}{\numberline {11.3}Type synonyms}{48} +\contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48} +\contentsline {subsection}{\numberline {11.5}Overloading}{50} +\contentsline {section}{\numberline {12}Theory example: the natural numbers}{51} +\contentsline {subsection}{\numberline {12.1}Extending first-order logic with the natural numbers}{51} +\contentsline {subsection}{\numberline {12.2}Declaring the theory to Isabelle}{52} +\contentsline {subsection}{\numberline {12.3}Proving some recursion equations}{52} +\contentsline {section}{\numberline {13}Refinement with explicit instantiation}{53} +\contentsline {subsection}{\numberline {13.1}A simple proof by induction}{53} +\contentsline {subsection}{\numberline {13.2}An example of ambiguity in {\ptt resolve_tac}}{54} +\contentsline {subsection}{\numberline {13.3}Proving that addition is associative}{55} +\contentsline {section}{\numberline {14}A Prolog interpreter}{56} +\contentsline {subsection}{\numberline {14.1}Simple executions}{57} +\contentsline {subsection}{\numberline {14.2}Backtracking}{58} +\contentsline {subsection}{\numberline {14.3}Depth-first search}{59}
--- a/doc-src/Logics/CTT-eg.txt Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Logics/CTT-eg.txt Tue May 03 18:38:28 1994 +0200 @@ -36,10 +36,10 @@ (*** Currying, from CTT/ex/elim.ML ***) val prems = goal CTT.thy - "[| A type; !!x. x:A ==> B(x) type; \ -\ !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \ -\ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ -\ --> (PROD x:A . PROD y:B(x) . C(<x,y>))"; + "[| A type; !!x. x:A ==> B(x) type; \ +\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \ +\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ +\ (PROD x:A . PROD y:B(x) . C(<x,y>))"; by (intr_tac prems); by (eresolve_tac [ProdE] 1); by (intr_tac prems); @@ -50,8 +50,8 @@ val prems = goal CTT.thy "[| A type; !!x. x:A ==> B(x) type; \ \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ -\ |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ -\ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; +\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ +\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; by (intr_tac prems); by (eresolve_tac [ProdE RS SumE_fst] 1); by (assume_tac 1);
--- a/doc-src/Logics/logics.bbl Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Logics/logics.bbl Tue May 03 18:38:28 1994 +0200 @@ -10,25 +10,46 @@ David Basin and Matt Kaufmann. \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison. \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical - Frameworks}, pages 89--119. Cambridge University Press, 1991. + Frameworks}, pages 89--119. 1991. \bibitem{boyer86} Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and Lawrence Wos. \newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms. -\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986. +\newblock 2(3):287--327, 1986. \bibitem{camilleri92} J.~Camilleri and T.~F. Melham. \newblock Reasoning with inductively defined relations in the {HOL} theorem prover. -\newblock Technical Report 265, University of Cambridge Computer Laboratory, - August 1992. +\newblock Technical Report 265, August 1992. \bibitem{church40} Alonzo Church. \newblock A formulation of the simple theory of types. -\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940. +\newblock 5:56--68, 1940. + +\bibitem{coen92} +Martin~D. Coen. +\newblock {\em Interactive Program Derivation}. +\newblock PhD thesis, University of Cambridge, 1992. +\newblock Computer Laboratory Technical Report 272. + +\bibitem{constable86} +R.~L. {Constable et al.} +\newblock {\em Implementing Mathematics with the Nuprl Proof Development + System}. +\newblock 1986. + +\bibitem{davey&priestley} +B.~A. Davey and H.~A. Priestley. +\newblock {\em Introduction to Lattices and Order}. +\newblock 1990. + +\bibitem{devlin79} +Keith~J. Devlin. +\newblock {\em Fundamentals of Contemporary Set Theory}. +\newblock Springer, 1979. \bibitem{dummett} Michael Dummett. @@ -38,7 +59,7 @@ \bibitem{dyckhoff} Roy Dyckhoff. \newblock Contraction-free sequent calculi for intuitionistic logic. -\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992. +\newblock 57(3):795--807, 1992. \bibitem{felty91a} Amy Felty. @@ -51,14 +72,7 @@ \bibitem{frost93} Jacob Frost. \newblock A case study of co-induction in {Isabelle HOL}. -\newblock Technical Report 308, University of Cambridge Computer Laboratory, - August 1993. - -\bibitem{OBJ} -K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer. -\newblock Principles of {OBJ2}. -\newblock In {\em Symposium on Principles of Programming Languages}, pages - 52--66, 1985. +\newblock Technical Report 308, August 1993. \bibitem{gallier86} J.~H. Gallier. @@ -66,12 +80,11 @@ Proving}. \newblock Harper \& Row, 1986. -\bibitem{mgordon88a} -Michael J.~C. Gordon. -\newblock {HOL}: A proof generating system for higher-order logic. -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI} - Specification, Verification and Synthesis}, pages 73--128. Kluwer Academic - Publishers, 1988. +\bibitem{mgordon-hol} +M.~J.~C. Gordon and T.~F. Melham. +\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher + Order Logic}. +\newblock 1993. \bibitem{halmos60} Paul~R. Halmos. @@ -84,6 +97,13 @@ second-order patterns. \newblock {\em Acta Informatica}, 11:31--55, 1978. +\bibitem{alf} +Lena Magnusson and Bengt {Nordstr\"om}. +\newblock The {ALF} proof editor and its proof engine. +\newblock In {\em : International Workshop {TYPES '93}}, pages 213--237. + Springer, published 1994. +\newblock LNCS 806. + \bibitem{mw81} Zohar Manna and Richard Waldinger. \newblock Deductive synthesis of the unification algorithm. @@ -94,6 +114,13 @@ \newblock {\em Intuitionistic type theory}. \newblock Bibliopolis, 1984. +\bibitem{melham89} +Thomas~F. Melham. +\newblock Automating recursive type definitions in higher order logic. +\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current + Trends in Hardware Verification and Automated Theorem Proving}, pages + 341--386. Springer, 1989. + \bibitem{milner-coind} Robin Milner and Mads Tofte. \newblock Co-induction in relational semantics. @@ -102,7 +129,7 @@ \bibitem{noel} Philippe {No\"el}. \newblock Experimenting with {Isabelle} in {ZF} set theory. -\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993. +\newblock 10(1):15--58, 1993. \bibitem{nordstrom90} Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. @@ -115,13 +142,6 @@ \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, December 1992. -\bibitem{paulson-set-I} -Lawrence~C. Paulson. -\newblock Set theory for verification: {I}. {From} foundations to functions. -\newblock {\em Journal of Automated Reasoning}. -\newblock In press; draft available as Report 271, University of Cambridge - Computer Laboratory. - \bibitem{paulson85} Lawrence~C. Paulson. \newblock Verifying the unification algorithm in {LCF}. @@ -130,7 +150,7 @@ \bibitem{paulson87} Lawrence~C. Paulson. \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. -\newblock Cambridge University Press, 1987. +\newblock 1987. \bibitem{paulson-COLOG} Lawrence~C. Paulson. @@ -140,44 +160,46 @@ of Sciences, Springer. \newblock LNCS 417. -\bibitem{paulson91} -Lawrence~C. Paulson. -\newblock {\em {ML} for the Working Programmer}. -\newblock Cambridge University Press, 1991. - \bibitem{paulson-coind} Lawrence~C. Paulson. \newblock Co-induction and co-recursion in higher-order logic. -\newblock Technical Report 304, University of Cambridge Computer Laboratory, - July 1993. +\newblock Technical Report 304, July 1993. \bibitem{paulson-fixedpt} Lawrence~C. Paulson. -\newblock A fixedpoint approach to implementing (co-)inductive definitions. -\newblock Technical report, University of Cambridge Computer Laboratory, 1993. -\newblock Draft. +\newblock A fixedpoint approach to implementing (co)inductive definitions. +\newblock Technical Report 320, December 1993. + +\bibitem{paulson-set-I} +Lawrence~C. Paulson. +\newblock Set theory for verification: {I}. {From} foundations to functions. +\newblock 11(3):353--389, 1993. \bibitem{paulson-set-II} Lawrence~C. Paulson. \newblock Set theory for verification: {II}. {Induction} and recursion. -\newblock Technical Report 312, University of Cambridge Computer Laboratory, - 1993. +\newblock Technical Report 312, 1993. + +\bibitem{paulson-final} +Lawrence~C. Paulson. +\newblock A concrete final coalgebra theorem for {ZF} set theory. +\newblock Technical report, 1994. \bibitem{pelletier86} F.~J. Pelletier. \newblock Seventy-five problems for testing automatic theorem provers. -\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986. +\newblock 2:191--216, 1986. \newblock Errata, JAR 4 (1988), 235--236. \bibitem{plaisted90} David~A. Plaisted. \newblock A sequent-style model elimination strategy and a positive refinement. -\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990. +\newblock 6(4):389--402, 1990. \bibitem{quaife92} Art Quaife. \newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory. -\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992. +\newblock 8(1):91--147, 1992. \bibitem{suppes72} Patrick Suppes. @@ -197,7 +219,7 @@ \bibitem{principia} A.~N. Whitehead and B.~Russell. \newblock {\em Principia Mathematica}. -\newblock Cambridge University Press, 1962. +\newblock 1962. \newblock Paperback edition to *56, abridged from the 2nd edition (1927). \end{thebibliography}
--- a/doc-src/Logics/logics.toc Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Logics/logics.toc Tue May 03 18:38:28 1994 +0200 @@ -1,7 +1,7 @@ -\contentsline {chapter}{\numberline {1}Introduction}{1} -\contentsline {section}{\numberline {1.1}Syntax definitions}{1} +\contentsline {chapter}{\numberline {1}Basic Concepts}{1} +\contentsline {section}{\numberline {1.1}Syntax definitions}{2} \contentsline {section}{\numberline {1.2}Proof procedures}{3} -\contentsline {chapter}{\numberline {2}First-order logic}{4} +\contentsline {chapter}{\numberline {2}First-Order Logic}{4} \contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4} \contentsline {section}{\numberline {2.2}Generic packages}{8} \contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8} @@ -9,92 +9,67 @@ \contentsline {section}{\numberline {2.5}An intuitionistic example}{11} \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12} \contentsline {section}{\numberline {2.7}A classical example}{14} -\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{16} -\contentsline {subsection}{Deriving the introduction rule}{17} +\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15} +\contentsline {subsection}{Deriving the introduction rule}{16} \contentsline {subsection}{Deriving the elimination rule}{17} -\contentsline {subsection}{Using the derived rules}{18} -\contentsline {subsection}{Derived rules versus definitions}{20} -\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23} -\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23} -\contentsline {section}{\numberline {3.2}The syntax of set theory}{24} -\contentsline {section}{\numberline {3.3}Binding operators}{26} -\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28} -\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33} -\contentsline {subsection}{Fundamental lemmas}{34} -\contentsline {subsection}{Unordered pairs and finite sets}{34} -\contentsline {subsection}{Subset and lattice properties}{37} -\contentsline {subsection}{Ordered pairs}{37} -\contentsline {subsection}{Relations}{37} -\contentsline {subsection}{Functions}{38} -\contentsline {section}{\numberline {3.6}Further developments}{41} -\contentsline {section}{\numberline {3.7}Simplification rules}{49} -\contentsline {section}{\numberline {3.8}The examples directory}{49} -\contentsline {section}{\numberline {3.9}A proof about powersets}{52} -\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{54} -\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{55} -\contentsline {chapter}{\numberline {4}Higher-order logic}{58} -\contentsline {section}{\numberline {4.1}Syntax}{58} -\contentsline {subsection}{Types}{58} -\contentsline {subsection}{Binders}{61} -\contentsline {section}{\numberline {4.2}Rules of inference}{61} -\contentsline {section}{\numberline {4.3}Generic packages}{65} -\contentsline {section}{\numberline {4.4}A formulation of set theory}{66} -\contentsline {subsection}{Syntax of set theory}{66} -\contentsline {subsection}{Axioms and rules of set theory}{72} -\contentsline {subsection}{Derived rules for sets}{72} -\contentsline {section}{\numberline {4.5}Types}{72} -\contentsline {subsection}{Product and sum types}{77} -\contentsline {subsection}{The type of natural numbers, $nat$}{77} -\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{77} -\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{81} -\contentsline {section}{\numberline {4.6}Classical proof procedures}{81} -\contentsline {section}{\numberline {4.7}The examples directories}{81} -\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{82} -\contentsline {subsection}{The introduction rule}{82} -\contentsline {subsection}{The elimination rule}{83} -\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{84} -\contentsline {chapter}{\numberline {5}First-order sequent calculus}{87} -\contentsline {section}{\numberline {5.1}Unification for lists}{87} -\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{88} -\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{88} -\contentsline {section}{\numberline {5.4}Tactics for sequents}{93} -\contentsline {section}{\numberline {5.5}Packaging sequent rules}{93} -\contentsline {section}{\numberline {5.6}Proof procedures}{94} -\contentsline {subsection}{Method A}{95} -\contentsline {subsection}{Method B}{95} -\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{95} -\contentsline {section}{\numberline {5.8}A more complex proof}{97} -\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99} -\contentsline {section}{\numberline {6.1}Syntax}{100} -\contentsline {section}{\numberline {6.2}Rules of inference}{100} -\contentsline {section}{\numberline {6.3}Rule lists}{105} -\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{108} -\contentsline {section}{\numberline {6.5}Rewriting tactics}{109} -\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109} -\contentsline {section}{\numberline {6.7}A theory of arithmetic}{110} -\contentsline {section}{\numberline {6.8}The examples directory}{110} -\contentsline {section}{\numberline {6.9}Example: type inference}{112} -\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113} -\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116} -\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117} -\contentsline {chapter}{\numberline {7}Defining Logics}{121} -\contentsline {section}{\numberline {7.1}Precedence grammars}{121} -\contentsline {section}{\numberline {7.2}Basic syntax}{122} -\contentsline {subsection}{Logical types and default syntax}{123} -\contentsline {subsection}{Lexical matters *}{124} -\contentsline {subsection}{Inspecting syntax *}{124} -\contentsline {section}{\numberline {7.3}Abstract syntax trees}{126} -\contentsline {subsection}{Parse trees to asts}{128} -\contentsline {subsection}{Asts to terms *}{129} -\contentsline {subsection}{Printing of terms *}{129} -\contentsline {section}{\numberline {7.4}Mixfix declarations}{130} -\contentsline {subsection}{Infixes}{133} -\contentsline {subsection}{Binders}{133} -\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{134} -\contentsline {subsection}{Specifying macros}{135} -\contentsline {subsection}{Applying rules}{136} -\contentsline {subsection}{Rewriting strategy}{138} -\contentsline {subsection}{More examples}{138} -\contentsline {section}{\numberline {7.6}Translation functions *}{141} -\contentsline {subsection}{A simple example *}{142} -\contentsline {section}{\numberline {7.7}Example: some minimal logics}{143} +\contentsline {subsection}{Using the derived rules}{17} +\contentsline {subsection}{Derived rules versus definitions}{19} +\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22} +\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22} +\contentsline {section}{\numberline {3.2}The syntax of set theory}{23} +\contentsline {section}{\numberline {3.3}Binding operators}{25} +\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27} +\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30} +\contentsline {subsection}{Fundamental lemmas}{30} +\contentsline {subsection}{Unordered pairs and finite sets}{32} +\contentsline {subsection}{Subset and lattice properties}{32} +\contentsline {subsection}{Ordered pairs}{36} +\contentsline {subsection}{Relations}{36} +\contentsline {subsection}{Functions}{37} +\contentsline {section}{\numberline {3.6}Further developments}{38} +\contentsline {section}{\numberline {3.7}Simplification rules}{47} +\contentsline {section}{\numberline {3.8}The examples directory}{47} +\contentsline {section}{\numberline {3.9}A proof about powersets}{48} +\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51} +\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52} +\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55} +\contentsline {section}{\numberline {4.1}Syntax}{55} +\contentsline {subsection}{Types}{57} +\contentsline {subsection}{Binders}{58} +\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58} +\contentsline {section}{\numberline {4.2}Rules of inference}{58} +\contentsline {section}{\numberline {4.3}A formulation of set theory}{60} +\contentsline {subsection}{Syntax of set theory}{65} +\contentsline {subsection}{Axioms and rules of set theory}{69} +\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71} +\contentsline {section}{\numberline {4.5}Types}{73} +\contentsline {subsection}{Product and sum types}{73} +\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73} +\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76} +\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76} +\contentsline {section}{\numberline {4.6}The examples directories}{79} +\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80} +\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82} +\contentsline {section}{\numberline {5.1}Unification for lists}{82} +\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84} +\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86} +\contentsline {section}{\numberline {5.4}Tactics for sequents}{87} +\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88} +\contentsline {section}{\numberline {5.6}Proof procedures}{88} +\contentsline {subsection}{Method A}{89} +\contentsline {subsection}{Method B}{89} +\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90} +\contentsline {section}{\numberline {5.8}A more complex proof}{91} +\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93} +\contentsline {section}{\numberline {6.1}Syntax}{95} +\contentsline {section}{\numberline {6.2}Rules of inference}{95} +\contentsline {section}{\numberline {6.3}Rule lists}{101} +\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101} +\contentsline {section}{\numberline {6.5}Rewriting tactics}{102} +\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103} +\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105} +\contentsline {section}{\numberline {6.8}The examples directory}{105} +\contentsline {section}{\numberline {6.9}Example: type inference}{105} +\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107} +\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110} +\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111}
--- a/doc-src/Ref/ref.bbl Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Ref/ref.bbl Tue May 03 18:38:28 1994 +0200 @@ -1,5 +1,10 @@ \begin{thebibliography}{1} +\bibitem{bm88book} +Robert~S. Boyer and J~Strother Moore. +\newblock {\em A Computational Logic Handbook}. +\newblock Academic Press, 1988. + \bibitem{charniak80} E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott. \newblock {\em Artificial Intelligence Programming}. @@ -11,11 +16,30 @@ formula manipulation, with application to the {Church-Rosser Theorem}. \newblock {\em Indagationes Mathematicae}, 34:381--392, 1972. +\bibitem{OBJ} +K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer. +\newblock Principles of {OBJ2}. +\newblock In {\em Principles of Programming Languages}, pages 52--66, 1985. + +\bibitem{martin-nipkow} +Ursula Martin and Tobias Nipkow. +\newblock Ordered rewriting and confluence. +\newblock In M.~E. Stickel, editor, {\em 10th International Conference on + Automated Deduction}, pages 366--380. Springer, 1990. +\newblock LNCS 449. + \bibitem{nipkow-prehofer} Tobias Nipkow and Christian Prehofer. \newblock Type checking type classes. -\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993. -\newblock To appear. +\newblock In {\em 20th Principles of Programming Languages}, pages 409--418. + ACM Press, 1993. +\newblock Revised version to appear in \bgroup\em Journal of Functional + Programming\egroup. + +\bibitem{nordstrom90} +Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. +\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. +\newblock Oxford University Press, 1990. \bibitem{paulson91} Lawrence~C. Paulson.
--- a/doc-src/Ref/ref.toc Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Ref/ref.toc Tue May 03 18:38:28 1994 +0200 @@ -1,151 +1,180 @@ -\contentsline {chapter}{\numberline {1}Introduction}{1} +\contentsline {chapter}{\numberline {1}Basic Use of Isabelle}{1} \contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1} \contentsline {section}{\numberline {1.2}Ending a session}{2} -\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2} -\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3} -\contentsline {subsection}{Printing limits}{3} -\contentsline {subsection}{Printing of meta-level hypotheses}{3} -\contentsline {subsection}{Printing of types and sorts}{3} -\contentsline {subsection}{$\eta $-contraction before printing}{4} -\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4} -\contentsline {section}{\numberline {1.6}Shell scripts}{5} -\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6} -\contentsline {section}{\numberline {2.1}Basic commands}{6} -\contentsline {subsection}{Starting a backward proof}{6} -\contentsline {subsection}{Applying a tactic}{7} -\contentsline {subsection}{Extracting the proved theorem}{8} -\contentsline {subsection}{Undoing and backtracking}{8} -\contentsline {subsection}{Printing the proof state}{9} -\contentsline {subsection}{Timing}{9} -\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9} -\contentsline {subsection}{Refining a given subgoal}{9} -\contentsline {subsubsection}{Resolution with a list of theorems}{9} -\contentsline {subsection}{Scanning shortcuts}{10} -\contentsline {subsubsection}{Proof by assumption and resolution}{10} -\contentsline {subsubsection}{Resolution with a list of theorems}{10} -\contentsline {subsection}{Other shortcuts}{10} -\contentsline {section}{\numberline {2.3}Advanced features}{11} -\contentsline {subsection}{Executing batch proofs}{11} -\contentsline {subsection}{Managing multiple proofs}{11} -\contentsline {subsubsection}{The stack of proof states}{12} -\contentsline {subsubsection}{Saving and restoring proof states}{12} -\contentsline {subsection}{Debugging and inspecting}{12} -\contentsline {subsubsection}{Reading and printing terms}{13} -\contentsline {subsubsection}{Inspecting the proof state}{13} -\contentsline {subsubsection}{Filtering lists of rules}{13} -\contentsline {chapter}{\numberline {3}Tactics}{14} -\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14} -\contentsline {subsection}{Resolution tactics}{14} -\contentsline {subsection}{Assumption tactics}{15} -\contentsline {subsection}{Matching tactics}{15} -\contentsline {subsection}{Resolution with instantiation}{15} -\contentsline {section}{\numberline {3.2}Other basic tactics}{16} -\contentsline {subsection}{Definitions and meta-level rewriting}{16} -\contentsline {subsection}{Tactic shortcuts}{17} -\contentsline {subsection}{Inserting premises and facts}{17} -\contentsline {subsection}{Theorems useful with tactics}{18} -\contentsline {section}{\numberline {3.3}Obscure tactics}{18} -\contentsline {subsection}{Tidying the proof state}{18} -\contentsline {subsection}{Renaming parameters in a goal}{18} -\contentsline {subsection}{Composition: resolution without lifting}{19} -\contentsline {section}{\numberline {3.4}Managing lots of rules}{19} -\contentsline {subsection}{Combined resolution and elim-resolution}{20} -\contentsline {subsection}{Discrimination nets for fast resolution}{20} -\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21} -\contentsline {subsection}{Operations on type {\ptt tactic}}{22} -\contentsline {subsection}{Tracing}{22} -\contentsline {subsection}{Sequences}{23} -\contentsline {subsubsection}{Basic operations on sequences}{23} -\contentsline {subsubsection}{Converting between sequences and lists}{23} -\contentsline {subsubsection}{Combining sequences}{23} -\contentsline {chapter}{\numberline {4}Tacticals}{25} -\contentsline {section}{\numberline {4.1}The basic tacticals}{25} -\contentsline {subsection}{Joining two tactics}{25} -\contentsline {subsection}{Joining a list of tactics}{25} -\contentsline {subsection}{Repetition tacticals}{26} -\contentsline {subsection}{Identities for tacticals}{26} -\contentsline {section}{\numberline {4.2}Control and search tacticals}{27} -\contentsline {subsection}{Filtering a tactic's results}{27} -\contentsline {subsection}{Depth-first search}{28} -\contentsline {subsection}{Other search strategies}{28} -\contentsline {subsection}{Auxiliary tacticals for searching}{29} -\contentsline {subsection}{Predicates and functions useful for searching}{29} -\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29} -\contentsline {subsection}{Restricting a tactic to one subgoal}{30} -\contentsline {subsection}{Scanning for a subgoal by number}{31} -\contentsline {subsection}{Joining tactic functions}{32} -\contentsline {subsection}{Applying a list of tactics to 1}{32} -\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33} -\contentsline {section}{\numberline {5.1}Basic operations on theorems}{33} -\contentsline {subsection}{Pretty-printing a theorem}{33} -\contentsline {subsubsection}{Top-level commands}{33} -\contentsline {subsubsection}{Operations for programming}{34} -\contentsline {subsection}{Forwards proof: joining rules by resolution}{34} -\contentsline {subsection}{Expanding definitions in theorems}{35} -\contentsline {subsection}{Instantiating a theorem}{35} -\contentsline {subsection}{Miscellaneous forward rules}{35} -\contentsline {subsection}{Taking a theorem apart}{36} -\contentsline {subsection}{Tracing flags for unification}{36} -\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{37} -\contentsline {subsection}{Propositional rules}{38} -\contentsline {subsubsection}{Assumption}{38} -\contentsline {subsubsection}{Implication}{38} -\contentsline {subsubsection}{Logical equivalence (equality)}{39} -\contentsline {subsection}{Equality rules}{39} -\contentsline {subsection}{The $\lambda $-conversion rules}{39} -\contentsline {subsection}{Universal quantifier rules}{40} -\contentsline {subsubsection}{Forall introduction}{40} -\contentsline {subsubsection}{Forall elimination}{40} -\contentsline {subsubsection}{Instantiation of unknowns}{41} -\contentsline {subsection}{Freezing/thawing type variables}{41} -\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{41} -\contentsline {subsection}{Proof by assumption}{41} -\contentsline {subsection}{Resolution}{41} -\contentsline {subsection}{Composition: resolution without lifting}{42} -\contentsline {subsection}{Other meta-rules}{42} -\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44} -\contentsline {section}{\numberline {6.1}Defining Theories}{44} -\contentsline {subsection}{Classes and types}{47} -\contentsline {section}{\numberline {6.2}Loading Theories}{47} -\contentsline {subsection}{Reading a new theory}{47} -\contentsline {subsection}{Filenames and paths}{48} -\contentsline {subsection}{Reloading a theory}{48} -\contentsline {subsection}{Pseudo theories}{48} -\contentsline {subsection}{Removing a theory}{49} -\contentsline {subsection}{Using Poly/{\psc ml}}{49} -\contentsline {section}{\numberline {6.3}Basic operations on theories}{49} -\contentsline {subsection}{Extracting an axiom from a theory}{49} -\contentsline {subsection}{Building a theory}{50} -\contentsline {subsection}{Inspecting a theory}{51} -\contentsline {section}{\numberline {6.4}Terms}{52} -\contentsline {section}{\numberline {6.5}Certified terms}{53} -\contentsline {subsection}{Printing terms}{53} -\contentsline {subsection}{Making and inspecting certified terms}{53} -\contentsline {section}{\numberline {6.6}Types}{54} -\contentsline {section}{\numberline {6.7}Certified types}{54} -\contentsline {subsection}{Printing types}{54} -\contentsline {subsection}{Making and inspecting certified types}{54} -\contentsline {chapter}{\numberline {7}Substitution Tactics}{56} -\contentsline {section}{\numberline {7.1}Simple substitution}{56} -\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{57} -\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{57} -\contentsline {chapter}{\numberline {8}Simplification}{60} -\contentsline {section}{\numberline {8.1}Simplification sets}{60} -\contentsline {subsection}{Rewrite rules}{60} -\contentsline {subsection}{Congruence rules}{61} -\contentsline {subsection}{The subgoaler}{61} -\contentsline {subsection}{The solver}{62} -\contentsline {subsection}{The looper}{62} -\contentsline {section}{\numberline {8.2}The simplification tactics}{62} -\contentsline {section}{\numberline {8.3}Example: using the simplifier}{63} -\contentsline {chapter}{\numberline {9}The classical theorem prover}{67} -\contentsline {section}{\numberline {9.1}The sequent calculus}{67} -\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68} -\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69} -\contentsline {section}{\numberline {9.4}Classical rule sets}{70} -\contentsline {section}{\numberline {9.5}The classical tactics}{71} -\contentsline {subsection}{Single-step tactics}{72} -\contentsline {subsection}{The automatic tactics}{72} -\contentsline {subsection}{Other useful tactics}{72} -\contentsline {subsection}{Creating swapped rules}{73} -\contentsline {section}{\numberline {9.6}Setting up the classical prover}{73} +\contentsline {section}{\numberline {1.3}Reading ML files}{2} +\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2} +\contentsline {subsection}{Printing limits}{2} +\contentsline {subsection}{Printing of hypotheses, types and sorts}{3} +\contentsline {subsection}{$\eta $-contraction before printing}{3} +\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{3} +\contentsline {section}{\numberline {1.6}Shell scripts}{4} +\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{5} +\contentsline {section}{\numberline {2.1}Basic commands}{5} +\contentsline {subsection}{Starting a backward proof}{5} +\contentsline {subsection}{Applying a tactic}{6} +\contentsline {subsection}{Extracting the proved theorem}{7} +\contentsline {subsection}{Undoing and backtracking}{7} +\contentsline {subsection}{Printing the proof state}{8} +\contentsline {subsection}{Timing}{8} +\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{8} +\contentsline {subsection}{Refining a given subgoal}{8} +\contentsline {subsection}{Scanning shortcuts}{9} +\contentsline {subsection}{Other shortcuts}{9} +\contentsline {section}{\numberline {2.3}Executing batch proofs}{9} +\contentsline {section}{\numberline {2.4}Managing multiple proofs}{10} +\contentsline {subsection}{The stack of proof states}{11} +\contentsline {subsection}{Saving and restoring proof states}{11} +\contentsline {section}{\numberline {2.5}Debugging and inspecting}{11} +\contentsline {subsection}{Reading and printing terms}{11} +\contentsline {subsection}{Inspecting the proof state}{12} +\contentsline {subsection}{Filtering lists of rules}{12} +\contentsline {chapter}{\numberline {3}Tactics}{13} +\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{13} +\contentsline {subsection}{Resolution tactics}{13} +\contentsline {subsection}{Assumption tactics}{14} +\contentsline {subsection}{Matching tactics}{14} +\contentsline {subsection}{Resolution with instantiation}{14} +\contentsline {section}{\numberline {3.2}Other basic tactics}{15} +\contentsline {subsection}{Definitions and meta-level rewriting}{15} +\contentsline {subsection}{Tactic shortcuts}{16} +\contentsline {subsection}{Inserting premises and facts}{16} +\contentsline {subsection}{Theorems useful with tactics}{17} +\contentsline {section}{\numberline {3.3}Obscure tactics}{17} +\contentsline {subsection}{Tidying the proof state}{17} +\contentsline {subsection}{Renaming parameters in a goal}{17} +\contentsline {subsection}{Composition: resolution without lifting}{18} +\contentsline {section}{\numberline {3.4}Managing lots of rules}{18} +\contentsline {subsection}{Combined resolution and elim-resolution}{19} +\contentsline {subsection}{Discrimination nets for fast resolution}{19} +\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{20} +\contentsline {subsection}{Operations on type {\ptt tactic}}{21} +\contentsline {subsection}{Tracing}{21} +\contentsline {section}{\numberline {3.6}Sequences}{22} +\contentsline {subsection}{Basic operations on sequences}{22} +\contentsline {subsection}{Converting between sequences and lists}{22} +\contentsline {subsection}{Combining sequences}{22} +\contentsline {chapter}{\numberline {4}Tacticals}{24} +\contentsline {section}{\numberline {4.1}The basic tacticals}{24} +\contentsline {subsection}{Joining two tactics}{24} +\contentsline {subsection}{Joining a list of tactics}{24} +\contentsline {subsection}{Repetition tacticals}{25} +\contentsline {subsection}{Identities for tacticals}{25} +\contentsline {section}{\numberline {4.2}Control and search tacticals}{26} +\contentsline {subsection}{Filtering a tactic's results}{26} +\contentsline {subsection}{Depth-first search}{26} +\contentsline {subsection}{Other search strategies}{27} +\contentsline {subsection}{Auxiliary tacticals for searching}{27} +\contentsline {subsection}{Predicates and functions useful for searching}{28} +\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{28} +\contentsline {subsection}{Restricting a tactic to one subgoal}{28} +\contentsline {subsection}{Scanning for a subgoal by number}{29} +\contentsline {subsection}{Joining tactic functions}{30} +\contentsline {subsection}{Applying a list of tactics to 1}{31} +\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{32} +\contentsline {section}{\numberline {5.1}Basic operations on theorems}{32} +\contentsline {subsection}{Pretty-printing a theorem}{32} +\contentsline {subsection}{Forward proof: joining rules by resolution}{33} +\contentsline {subsection}{Expanding definitions in theorems}{33} +\contentsline {subsection}{Instantiating a theorem}{34} +\contentsline {subsection}{Miscellaneous forward rules}{34} +\contentsline {subsection}{Taking a theorem apart}{35} +\contentsline {subsection}{Tracing flags for unification}{35} +\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{36} +\contentsline {subsection}{Assumption rule}{37} +\contentsline {subsection}{Implication rules}{37} +\contentsline {subsection}{Logical equivalence rules}{38} +\contentsline {subsection}{Equality rules}{38} +\contentsline {subsection}{The $\lambda $-conversion rules}{38} +\contentsline {subsection}{Forall introduction rules}{39} +\contentsline {subsection}{Forall elimination rules}{39} +\contentsline {subsection}{Instantiation of unknowns}{39} +\contentsline {subsection}{Freezing/thawing type unknowns}{40} +\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{40} +\contentsline {subsection}{Proof by assumption}{40} +\contentsline {subsection}{Resolution}{40} +\contentsline {subsection}{Composition: resolution without lifting}{40} +\contentsline {subsection}{Other meta-rules}{41} +\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{42} +\contentsline {section}{\numberline {6.1}Defining theories}{42} +\contentsline {subsection}{*Classes and arities}{44} +\contentsline {section}{\numberline {6.2}Loading a new theory}{44} +\contentsline {section}{\numberline {6.3}Reloading modified theories}{45} +\contentsline {subsection}{Important note for Poly/ML users}{45} +\contentsline {subsection}{*Pseudo theories}{46} +\contentsline {section}{\numberline {6.4}Basic operations on theories}{47} +\contentsline {subsection}{Extracting an axiom from a theory}{47} +\contentsline {subsection}{Building a theory}{47} +\contentsline {subsection}{Inspecting a theory}{47} +\contentsline {section}{\numberline {6.5}Terms}{48} +\contentsline {section}{\numberline {6.6}Variable binding}{49} +\contentsline {section}{\numberline {6.7}Certified terms}{50} +\contentsline {subsection}{Printing terms}{50} +\contentsline {subsection}{Making and inspecting certified terms}{50} +\contentsline {section}{\numberline {6.8}Types}{50} +\contentsline {section}{\numberline {6.9}Certified types}{51} +\contentsline {subsection}{Printing types}{51} +\contentsline {subsection}{Making and inspecting certified types}{51} +\contentsline {chapter}{\numberline {7}Defining Logics}{52} +\contentsline {section}{\numberline {7.1}Priority grammars}{52} +\contentsline {section}{\numberline {7.2}The Pure syntax}{53} +\contentsline {subsection}{Logical types and default syntax}{55} +\contentsline {subsection}{Lexical matters}{55} +\contentsline {subsection}{*Inspecting the syntax}{56} +\contentsline {section}{\numberline {7.3}Mixfix declarations}{58} +\contentsline {subsection}{Grammar productions}{58} +\contentsline {subsection}{The general mixfix form}{59} +\contentsline {subsection}{Example: arithmetic expressions}{60} +\contentsline {subsection}{The mixfix template}{61} +\contentsline {subsection}{Infixes}{61} +\contentsline {subsection}{Binders}{62} +\contentsline {section}{\numberline {7.4}Example: some minimal logics}{62} +\contentsline {chapter}{\numberline {8}Syntax Transformations}{66} +\contentsline {section}{\numberline {8.1}Abstract syntax trees}{66} +\contentsline {section}{\numberline {8.2}Transforming parse trees to {\psc ast}{}s}{67} +\contentsline {section}{\numberline {8.3}Transforming {\psc ast}{}s to terms}{69} +\contentsline {section}{\numberline {8.4}Printing of terms}{69} +\contentsline {section}{\numberline {8.5}Macros: Syntactic rewriting}{71} +\contentsline {subsection}{Specifying macros}{72} +\contentsline {subsection}{Applying rules}{73} +\contentsline {subsection}{Example: the syntax of finite sets}{75} +\contentsline {subsection}{Example: a parse macro for dependent types}{76} +\contentsline {section}{\numberline {8.6}Translation functions}{76} +\contentsline {subsection}{Declaring translation functions}{77} +\contentsline {subsection}{The translation strategy}{77} +\contentsline {subsection}{Example: a print translation for dependent types}{78} +\contentsline {chapter}{\numberline {9}Substitution Tactics}{80} +\contentsline {section}{\numberline {9.1}Substitution rules}{80} +\contentsline {section}{\numberline {9.2}Substitution in the hypotheses}{81} +\contentsline {section}{\numberline {9.3}Setting up {\ptt hyp_subst_tac}}{82} +\contentsline {chapter}{\numberline {10}Simplification}{84} +\contentsline {section}{\numberline {10.1}Simplification sets}{84} +\contentsline {subsection}{Rewrite rules}{84} +\contentsline {subsection}{*Congruence rules}{85} +\contentsline {subsection}{*The subgoaler}{85} +\contentsline {subsection}{*The solver}{86} +\contentsline {subsection}{*The looper}{86} +\contentsline {section}{\numberline {10.2}The simplification tactics}{87} +\contentsline {section}{\numberline {10.3}Examples using the simplifier}{88} +\contentsline {subsection}{A trivial example}{88} +\contentsline {subsection}{An example of tracing}{89} +\contentsline {subsection}{Free variables and simplification}{90} +\contentsline {section}{\numberline {10.4}Permutative rewrite rules}{90} +\contentsline {subsection}{Example: sums of integers}{91} +\contentsline {subsection}{Re-orienting equalities}{93} +\contentsline {section}{\numberline {10.5}*Setting up the simplifier}{93} +\contentsline {subsection}{A collection of standard rewrite rules}{94} +\contentsline {subsection}{Functions for preprocessing the rewrite rules}{94} +\contentsline {subsection}{Making the initial simpset}{96} +\contentsline {subsection}{Case splitting}{97} +\contentsline {chapter}{\numberline {11}The Classical Reasoner}{98} +\contentsline {section}{\numberline {11.1}The sequent calculus}{98} +\contentsline {section}{\numberline {11.2}Simulating sequents by natural deduction}{99} +\contentsline {section}{\numberline {11.3}Extra rules for the sequent calculus}{100} +\contentsline {section}{\numberline {11.4}Classical rule sets}{101} +\contentsline {section}{\numberline {11.5}The classical tactics}{103} +\contentsline {subsection}{The automatic tactics}{103} +\contentsline {subsection}{Single-step tactics}{103} +\contentsline {subsection}{Other useful tactics}{104} +\contentsline {subsection}{Creating swapped rules}{104} +\contentsline {section}{\numberline {11.6}Setting up the classical reasoner}{104} +\contentsline {chapter}{\numberline {A}Syntax of Isabelle Theories}{107}
--- a/doc-src/Ref/simplifier-eg.txt Tue May 03 18:36:18 1994 +0200 +++ b/doc-src/Ref/simplifier-eg.txt Tue May 03 18:38:28 1994 +0200 @@ -1,3 +1,5 @@ +Pretty.setmargin 70; + > goal Nat.thy "m+0 = m"; Level 0 m + 0 = m @@ -71,3 +73,39 @@ Level 3 f(i + j) = i + f(j) No subgoals! + + + +> goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)"; +Level 0 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) + 1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) + +> by (simp_tac natsum_ss 1); +Level 1 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) + 1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n + +> by (nat_ind_tac "n" 1); +Level 2 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) + 1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0 + 2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) = + n1 + n1 * n1 ==> + Suc(n1) + + (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) = + Suc(n1) + Suc(n1) * Suc(n1) + +> by (simp_tac natsum_ss 1); +Level 3 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) + 1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) = + n1 + n1 * n1 ==> + Suc(n1) + + (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) = + Suc(n1) + Suc(n1) * Suc(n1) + +> by (asm_simp_tac natsum_ss 1); +Level 4 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) +No subgoals!