# HG changeset patch # User wenzelm # Date 939162700 -7200 # Node ID 5b9c45b217820e05ef1d4258ee59f3f7a8fb2852 # Parent ca4e3b75345a26e849cc651f2050376cc530bf20 improved presentation; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/BasicLogic.thy --- a/src/HOL/Isar_examples/BasicLogic.thy Tue Oct 05 21:20:28 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 06 00:31:40 1999 +0200 @@ -5,9 +5,10 @@ Basic propositional and quantifier reasoning. *) +header {* Basic reasoning *}; + theory BasicLogic = Main:; - subsection {* Some trivialities *}; text {* Just a few toy examples to get an idea of how Isabelle/Isar @@ -19,7 +20,6 @@ show A; .; qed; - lemma K: "A --> B --> A"; proof; assume A; @@ -44,7 +44,6 @@ lemma K''': "A --> B --> A"; by intro; - lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"; proof; assume "A --> B --> C"; @@ -63,7 +62,6 @@ qed; qed; - text {* Variations of backward vs.\ forward reasoning \dots *}; lemma "A & B --> B & A"; @@ -178,5 +176,4 @@ qed; qed; - end; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/Cantor.thy --- a/src/HOL/Isar_examples/Cantor.thy Tue Oct 05 21:20:28 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Wed Oct 06 00:31:40 1999 +0200 @@ -6,30 +6,25 @@ chapter of "Isabelle's Object-Logics" (Larry Paulson). *) -theory Cantor = Main:; +header {* More classical proofs: Cantor's Theorem *}; - -section {* Example: Cantor's Theorem *}; +theory Cantor = Main:; text {* Cantor's Theorem states that every set has more subsets than it has - elements. It has become a favourite example in higher-order logic - since it is so easily expressed: @{display term[show_types] "ALL f - :: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"} - - Viewing types as sets, @{type "'a => bool"} represents the powerset - of @{type 'a}. This version states that for every function from - @{type 'a} to its powerset, some subset is outside its range. - - The Isabelle/Isar proofs below use HOL's set theory, with the type - @{type "'a set"} and the operator @{term range}. -*}; - - -text {* - We first consider a rather verbose version of the proof, with the - reasoning expressed quite naively. We only make use of the pure - core of the Isar proof language. + elements. It has become a favourite basic example in higher-order logic + since it is so easily expressed: \[\all{f::\alpha \To \alpha \To \idt{bool}} + \ex{S::\alpha \To \idt{bool}} \all{x::\alpha}. f \ap x \not= S\] + + Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of + $\alpha$. This version of the theorem states that for every function from + $\alpha$ to its powerset, some subset is outside its range. The + Isabelle/Isar proofs below use HOL's set theory, with the type $\alpha \ap + \idt{set}$ and the operator $\idt{range}$. + + \bigskip We first consider a rather verbose version of the proof, with the + reasoning expressed quite naively. We only make use of the pure core of the + Isar proof language. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -58,11 +53,10 @@ qed; qed; - text {* - The following version essentially does the same reasoning, only that - it is expressed more neatly, with some derived Isar language - elements involved. + The following version of the proof essentially does the same reasoning, only + that it is expressed more neatly, with some derived Isar language elements + involved. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -89,27 +83,24 @@ qed; qed; - text {* - How much creativity is required? As it happens, Isabelle can prove - this theorem automatically. The default classical set contains - rules for most of the constructs of HOL's set theory. We must - augment it with @{thm equalityCE} to break up set equalities, and - then apply best-first search. Depth-first search would diverge, but - best-first search successfully navigates through the large search - space. + How much creativity is required? As it happens, Isabelle can prove this + theorem automatically. The default classical set contains rules for most of + the constructs of HOL's set theory. We must augment it with + \name{equalityCE} to break up set equalities, and then apply best-first + search. Depth-first search would diverge, but best-first search + successfully navigates through the large search space. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; by (best elim: equalityCE); text {* - While this establishes the same theorem internally, we do not get - any idea of how the proof actually works. There is currently no way - to transform internal system-level representations of Isabelle - proofs back into Isar documents. Writing Isabelle/Isar proof - documents actually \emph{is} a creative process. + While this establishes the same theorem internally, we do not get any idea + of how the proof actually works. There is currently no way to transform + internal system-level representations of Isabelle proofs back into Isar + documents. Note that writing Isabelle/Isar proof documents actually + \emph{is} a creative process. *}; - end; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Tue Oct 05 21:20:28 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Oct 06 00:31:40 1999 +0200 @@ -5,23 +5,22 @@ Correctness of a simple expression/stack-machine compiler. *) +header {* Correctness of a simple expression compiler *}; + theory ExprCompiler = Main:; -chapter {* Correctness of a simple expression/stack-machine compiler *}; - - -section {* Basics *}; +subsection {* Basics *}; text {* First we define a type abbreviation for binary operations over some - type @{type "'val"} of values. + type of values. *}; types 'val binop = "'val => 'val => 'val"; -section {* Machine *}; +subsection {* Machine *}; text {* Next we model a simple stack machine, with three instructions. @@ -53,7 +52,7 @@ "execute instrs env == hd (exec instrs [] env)"; -section {* Expressions *}; +subsection {* Expressions *}; text {* We introduce a simple language of expressions: variables --- @@ -78,7 +77,7 @@ "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"; -section {* Compiler *}; +subsection {* Compiler *}; text {* So we are ready to define the compilation function of expressions to @@ -95,12 +94,13 @@ text {* - The main result of this development is the correctness theorem for - @{term "comp"}. We first establish some lemmas. + The main result of this development is the correctness theorem for + $\idt{comp}$. We first establish some lemmas about $\idt{exec}$. *}; lemma exec_append: - "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs"); + "ALL stack. exec (xs @ ys) stack env = + exec ys (exec xs stack env) env" (is "?P xs"); proof (induct ?P xs type: list); show "?P []"; by simp; @@ -117,7 +117,8 @@ qed; lemma exec_comp: - "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e"); + "ALL stack. exec (comp e) stack env = + eval e env # stack" (is "?P e"); proof (induct ?P e type: expr); fix adr; show "?P (Variable adr)"; by (simp!); next; @@ -133,5 +134,4 @@ theorem correctness: "execute (comp e) env = eval e env"; by (simp add: execute_def exec_comp); - end; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/Group.thy --- a/src/HOL/Isar_examples/Group.thy Tue Oct 05 21:20:28 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Wed Oct 06 00:31:40 1999 +0200 @@ -3,15 +3,15 @@ Author: Markus Wenzel, TU Muenchen *) +header {* Basic group theory *}; + theory Group = Main:; -chapter {* Basic group theory *}; - -section {* Groups *}; +subsection {* Groups *}; text {* We define an axiomatic type class of general groups over signature - (op *, one, inv). + $({\times}, \idt{one}, \idt{inv})$. *}; consts @@ -53,8 +53,8 @@ qed; text {* - With group_right_inverse already at our disposal, group_right_unit is - now obtained much easier as follows. + With \name{group-right-inverse} already at our disposal, + \name{group-right-unit} is now obtained much easier as follows. *}; theorem group_right_unit: "x * one = (x::'a::group)"; @@ -72,16 +72,17 @@ text {* There are only two Isar language elements for calculational proofs: - 'also' for initial or intermediate calculational steps, and 'finally' - for building the result of a calculation. These constructs are not - hardwired into Isabelle/Isar, but defined on top of the basic Isar/VM - interpreter. Expanding the 'also' or 'finally' derived language - elements, calculations may be simulated as demonstrated below. + \isakeyword{also} for initial or intermediate calculational steps, + and \isakeyword{finally} for building the result of a calculation. + These constructs are not hardwired into Isabelle/Isar, but defined on + top of the basic Isar/VM interpreter. Expanding the + \isakeyword{also} and \isakeyword{finally} derived language elements, + calculations may be simulated as demonstrated below. - Note that "..." is just a special term binding that happens to be - bound automatically to the argument of the last fact established by - assume or any local goal. In contrast to ?thesis, "..." is bound - after the proof is finished. + Note that ``$\dots$'' is just a special term binding that happens to + be bound automatically to the argument of the last fact established + by assume or any local goal. In contrast to $\var{thesis}$, the + ``$\dots$'' variable is bound \emph{after} the proof is finished. *}; theorem "x * one = (x::'a::group)"; @@ -116,7 +117,7 @@ qed; -section {* Groups and monoids *}; +subsection {* Groups and monoids *}; text {* Monoids are usually defined like this. @@ -128,12 +129,12 @@ monoid_right_unit: "x * one = x"; text {* - Groups are *not* yet monoids directly from the definition. For - monoids, right_unit had to be included as an axiom, but for groups - both right_unit and right_inverse are derivable from the other - axioms. With group_right_unit derived as a theorem of group theory - (see above), we may still instantiate group < monoid properly as - follows. + Groups are \emph{not} yet monoids directly from the definition. For + monoids, \name{right-unit} had to be included as an axiom, but for + groups both \name{right-unit} and \name{right-inverse} are + derivable from the other axioms. With \name{group-right-unit} + derived as a theorem of group theory (see above), we may still + instantiate $\idt{group} \subset \idt{monoid}$ properly as follows. *}; instance group < monoid; @@ -142,5 +143,4 @@ rule group_left_unit, rule group_right_unit); - end; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/Peirce.thy --- a/src/HOL/Isar_examples/Peirce.thy Tue Oct 05 21:20:28 1999 +0200 +++ b/src/HOL/Isar_examples/Peirce.thy Wed Oct 06 00:31:40 1999 +0200 @@ -3,9 +3,9 @@ Author: Markus Wenzel, TU Muenchen *) -theory Peirce = Main:; +header {* Examples of classical proof: Peirce's Law *}; -section {* Examples of classical proof --- Peirce's law. *}; +theory Peirce = Main:; theorem "((A --> B) --> A) --> A"; proof; @@ -22,7 +22,6 @@ qed; qed; - theorem "((A --> B) --> A) --> A"; proof; assume aba: "(A --> B) --> A"; @@ -40,5 +39,4 @@ qed; qed; - end; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/Summation.thy --- a/src/HOL/Isar_examples/Summation.thy Tue Oct 05 21:20:28 1999 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Wed Oct 06 00:31:40 1999 +0200 @@ -7,13 +7,11 @@ calculational proof. *) +header {* Summing natural numbers *}; theory Summation = Main:; - -section {* Summing natural numbers *}; - -text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *}; +subsection {* A summation operator *}; consts sum :: "[nat => nat, nat] => nat"; @@ -30,9 +28,7 @@ subsection {* Summation laws *}; -(* FIXME binary arithmetic does not yet work here *) - -syntax +syntax (* FIXME binary arithmetic does not yet work here *) "3" :: nat ("3") "4" :: nat ("4") "6" :: nat ("6"); @@ -93,5 +89,4 @@ finally; show "?P (Suc n)"; by simp; qed; - end; diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/document/style.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_examples/document/style.tex Wed Oct 06 00:31:40 1999 +0200 @@ -0,0 +1,25 @@ + +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,pdfsetup} + +\renewcommand{\isamarkupheader}[1]{\section{#1}} +%\parindent 0pt \parskip 0.5ex + +\newcommand{\name}[1]{\textsf{#1}} + +\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}} +\newcommand{\var}[1]{{?\!#1}} +\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} +\newcommand{\dsh}{\dshsym} + +\newcommand{\To}{\to} +\newcommand{\dt}{{\mathpunct.}} +\newcommand{\ap}{\mathbin{\!}} +\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;} +\newcommand{\all}[1]{\forall #1\dt\;} +\newcommand{\ex}[1]{\exists #1\dt\;} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: