--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- /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: