author wenzelm Wed, 06 Oct 1999 00:31:40 +0200 changeset 7748 5b9c45b21782 parent 7747 ca4e3b75345a child 7749 dfb8beddbefe
improved presentation;
 src/HOL/Isar_examples/BasicLogic.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Cantor.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/ExprCompiler.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Group.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Peirce.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Summation.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/document/style.tex file | annotate | diff | comparison | revisions
--- 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.
*)

+
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);
next;
@@ -133,5 +134,4 @@
theorem correctness: "execute (comp e) env = eval e env";

-
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}
+
+%\parindent 0pt \parskip 0.5ex
+
+\newcommand{\name}{\textsf{#1}}
+
+\newcommand{\idt}{{\mathord{\mathit{#1}}}}
+\newcommand{\var}{{?\!#1}}
+\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
+\newcommand{\dsh}{\dshsym}
+
+\newcommand{\To}{\to}
+\newcommand{\dt}{{\mathpunct.}}
+\newcommand{\ap}{\mathbin{\!}}
+\newcommand{\lam}{\mathop{\lambda} #1\dt\;}
+\newcommand{\all}{\forall #1\dt\;}
+\newcommand{\ex}{\exists #1\dt\;}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: