--- a/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 06 18:50:51 1999 +0200
@@ -9,6 +9,7 @@
theory BasicLogic = Main:;
+
subsection {* Some trivialities *};
text {* Just a few toy examples to get an idea of how Isabelle/Isar
@@ -62,7 +63,8 @@
qed;
qed;
-text {* Variations of backward vs.\ forward reasoning \dots *};
+
+subsection {* Variations of backward vs.\ forward reasoning \dots *};
lemma "A & B --> B & A";
proof;
--- a/src/HOL/Isar_examples/ExprCompiler.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Oct 06 18:50:51 1999 +0200
@@ -37,7 +37,8 @@
*};
consts
- exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";
+ exec :: "(('adr, 'val) instr) list
+ => 'val list => ('adr => 'val) => 'val list";
primrec
"exec [] stack env = stack"
@@ -45,7 +46,8 @@
(case instr of
Const c => exec instrs (c # stack) env
| Load x => exec instrs (env x # stack) env
- | Apply f => exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)";
+ | Apply f => exec instrs (f (hd stack) (hd (tl stack))
+ # (tl (tl stack))) env)";
constdefs
execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
@@ -55,8 +57,8 @@
subsection {* Expressions *};
text {*
- We introduce a simple language of expressions: variables ---
- constants --- binary operations.
+ We introduce a simple language of expressions: variables, constants,
+ binary operations.
*};
datatype ('adr, 'val) expr =
--- a/src/HOL/Isar_examples/Group.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Wed Oct 06 18:50:51 1999 +0200
@@ -71,11 +71,11 @@
qed;
text {*
- There are only two Isar language elements for calculational proofs:
- \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
+ \bigskip There are only two Isar language elements for calculational
+ proofs: \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.
@@ -117,7 +117,7 @@
qed;
-subsection {* Groups and monoids *};
+subsection {* Groups as monoids *};
text {*
Monoids are usually defined like this.
--- a/src/HOL/Isar_examples/KnasterTarski.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Wed Oct 06 18:50:51 1999 +0200
@@ -5,16 +5,20 @@
Typical textbook proof example.
*)
+header {* Textbook-style reasoning: the Knaster-Tarski Theorem *};
theory KnasterTarski = Main:;
+
+subsection {* Prose version *};
+
text {*
According to the book ``Introduction to Lattices and Order'' (by
B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
- fixpoint theorem is as follows (pages 93--94). Note that we have
- dualized their argument, and tuned the notation a little bit.
+ fixpoint theorem is as follows (pages 93--94).\footnote{We have
+ dualized their argument, and tuned the notation a little bit.}
- \paragraph{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a
+ \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a
complete lattice and $f \colon L \to L$ an order-preserving map.
Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
@@ -27,9 +31,12 @@
\le f(a)$.
*};
+
+subsection {* Formal version *};
+
text {*
- Our proof below closely follows this presentation. Virtually all of
- the prose narration has been rephrased in terms of formal Isar
+ Our proof below closely follows the original presentation. Virtually
+ all of the prose narration has been rephrased in terms of formal Isar
language elements. Just as many textbook-style proofs, there is a
strong bias towards forward reasoning, and little hierarchical
structure.
@@ -62,5 +69,4 @@
qed;
qed;
-
end;
--- a/src/HOL/Isar_examples/MultisetOrder.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Wed Oct 06 18:50:51 1999 +0200
@@ -8,10 +8,13 @@
HOL/Induct/Multiset). Pen-and-paper proof by Wilfried Buchholz.
*)
+header {* Wellfoundedness of multiset ordering *};
theory MultisetOrder = Multiset:;
+subsection {* A technical lemma *};
+
lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
(EX M. (M, M0) : mult1 r & N = M + {#a#}) |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
@@ -47,12 +50,13 @@
qed;
+subsection {* The key property *};
+
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
proof;
let ?R = "mult1 r";
let ?W = "acc ?R";
-
{{;
fix M M0 a;
assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
@@ -97,7 +101,6 @@
qed;
}}; note tedious_reasoning = this;
-
assume wf: "wf r";
fix M;
show "M : ?W";
@@ -123,11 +126,12 @@
qed;
+subsection {* Main result *};
+
theorem wf_mult1: "wf r ==> wf (mult1 r)";
by (rule acc_wfI, rule all_accessible);
theorem wf_mult: "wf r ==> wf (mult r)";
by (unfold mult_def, rule wf_trancl, rule wf_mult1);
-
end;
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Oct 06 18:50:51 1999 +0200
@@ -10,10 +10,12 @@
See also HOL/Induct/Mutil for the original Isabelle tactic scripts.
*)
+header {* The Mutilated Checker Board Problem *};
+
theory MutilatedCheckerboard = Main:;
-section {* Tilings *};
+subsection {* Tilings *};
consts
tiling :: "'a set set => 'a set set";
@@ -26,7 +28,8 @@
text "The union of two disjoint tilings is a tiling";
-lemma tiling_Un: "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
+lemma tiling_Un:
+ "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
proof;
assume "t : tiling A" (is "_ : ?T");
thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
@@ -41,14 +44,15 @@
have hyp: "t Un u: ?T"; by (blast!);
have "a <= - (t Un u)"; by (blast!);
with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
- also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
+ also; have "a Un (t Un u) = (a Un t) Un u";
+ by (simp only: Un_assoc);
finally; show "... : ?T"; .;
qed;
qed;
qed;
-section {* Basic properties of below *};
+subsection {* Basic properties of below *};
constdefs
below :: "nat => nat set"
@@ -60,22 +64,25 @@
lemma below_0: "below 0 = {}";
by (simp add: below_def);
-lemma Sigma_Suc1: "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
+lemma Sigma_Suc1:
+ "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
by (simp add: below_def less_Suc_eq) blast;
-lemma Sigma_Suc2: "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
+lemma Sigma_Suc2:
+ "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
by (simp add: below_def less_Suc_eq) blast;
lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
-section {* Basic properties of evnodd *};
+subsection {* Basic properties of evnodd *};
constdefs
evnodd :: "(nat * nat) set => nat => (nat * nat) set"
"evnodd A b == A Int {(i, j). (i + j) mod 2 = b}";
-lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)";
+lemma evnodd_iff:
+ "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)";
by (simp add: evnodd_def);
lemma evnodd_subset: "evnodd A b <= A";
@@ -97,11 +104,12 @@
by (simp add: evnodd_def);
lemma evnodd_insert: "evnodd (insert (i, j) C) b =
- (if (i + j) mod 2 = b then insert (i, j) (evnodd C b) else evnodd C b)";
+ (if (i + j) mod 2 = b
+ then insert (i, j) (evnodd C b) else evnodd C b)";
by (simp add: evnodd_def) blast;
-section {* Dominoes *};
+subsection {* Dominoes *};
consts
domino :: "(nat * nat) set set";
@@ -111,7 +119,6 @@
horiz: "{(i, j), (i, j + 1)} : domino"
vertl: "{(i, j), (i + 1, j)} : domino";
-
lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
(is "?P n" is "?B n : ?T");
proof (induct n);
@@ -123,7 +130,8 @@
have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
also; have "... : ?T";
proof (rule tiling.Un);
- have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz);
+ have "{(i, 2 * n), (i, 2 * n + 1)} : domino";
+ by (rule domino.horiz);
also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast;
finally; show "... : domino"; .;
from hyp; show "?B n : ?T"; .;
@@ -132,7 +140,8 @@
finally; show "?P (Suc n)"; .;
qed;
-lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino"
+lemma dominoes_tile_matrix:
+ "below m Times below (2 * n) : tiling domino"
(is "?P m" is "?B m : ?T");
proof (induct m);
show "?P 0"; by (simp add: below_0 tiling.empty);
@@ -150,8 +159,8 @@
finally; show "?P (Suc m)"; .;
qed;
-
-lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
+lemma domino_singleton:
+ "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
proof -;
assume b: "b < 2";
assume "d : domino";
@@ -173,9 +182,10 @@
qed;
-section {* Tilings of dominoes *};
+subsection {* Tilings of dominoes *};
-lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
+lemma tiling_domino_finite:
+ "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
proof -;
assume "t : ?T";
thus "?F t";
@@ -187,7 +197,8 @@
qed;
qed;
-lemma tiling_domino_01: "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
+lemma tiling_domino_01:
+ "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
(is "t : ?T ==> ?P t");
proof -;
assume "t : ?T";
@@ -201,7 +212,8 @@
and hyp: "card (?e t 0) = card (?e t 1)"
and "a <= - t";
- have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
+ have card_suc:
+ "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
proof -;
fix b; assume "b < 2";
have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
@@ -212,7 +224,8 @@
also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
also; have "card ... = Suc (card (?e t b))";
proof (rule card_insert_disjoint);
- show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
+ show "finite (?e t b)";
+ by (rule evnodd_finite, rule tiling_domino_finite);
have "(i, j) : ?e a b"; by (simp!);
thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
qed;
@@ -221,18 +234,20 @@
qed;
hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp;
also; from hyp; have "card (?e t 0) = card (?e t 1)"; .;
- also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp;
+ also; from card_suc; have "Suc ... = card (?e (a Un t) 1)";
+ by simp;
finally; show "?P (a Un t)"; .;
qed;
qed;
-section {* Main theorem *};
+subsection {* Main theorem *};
constdefs
mutilated_board :: "nat => nat => (nat * nat) set"
- "mutilated_board m n == below (2 * (m + 1)) Times below (2 * (n + 1))
- - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
+ "mutilated_board m n ==
+ below (2 * (m + 1)) Times below (2 * (n + 1))
+ - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
proof (unfold mutilated_board_def);
@@ -240,13 +255,15 @@
let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
let ?t' = "?t - {(0, 0)}";
let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
+
show "?t'' ~: ?T";
proof;
have t: "?t : ?T"; by (rule dominoes_tile_matrix);
assume t'': "?t'' : ?T";
let ?e = evnodd;
- have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
+ have fin: "finite (?e ?t 0)";
+ by (rule evnodd_finite, rule tiling_domino_finite, rule t);
note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
have "card (?e ?t'' 0) < card (?e ?t' 0)";
@@ -261,15 +278,16 @@
also; have "... < card (?e ?t 0)";
proof -;
have "(0, 0) : ?e ?t 0"; by simp;
- with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less);
+ with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)";
+ by (rule card_Diff1_less);
thus ?thesis; by simp;
qed;
also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
- also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]);
+ also; from t''; have "card ... = card (?e ?t'' 0)";
+ by (rule tiling_domino_01 [RS sym]);
finally; show False; ..;
qed;
qed;
-
end;
--- a/src/HOL/Isar_examples/Summation.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Wed Oct 06 18:50:51 1999 +0200
@@ -11,6 +11,7 @@
theory Summation = Main:;
+
subsection {* A summation operator *};
consts
@@ -21,14 +22,16 @@
"sum f (Suc n) = f n + sum f n";
syntax
- "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10);
+ "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10);
translations
"SUM i < k. b" == "sum (%i. b) k";
subsection {* Summation laws *};
-syntax (* FIXME binary arithmetic does not yet work here *)
+(* FIXME binary arithmetic does not yet work here *)
+
+syntax
"3" :: nat ("3")
"4" :: nat ("4")
"6" :: nat ("6");
@@ -65,7 +68,8 @@
finally; show "?P (Suc n)"; by simp;
qed;
-theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
+theorem sum_of_squares:
+ "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;
@@ -73,7 +77,8 @@
fix n;
have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
also; assume "?S n = n * (n + 1) * (2 * n + 1)";
- also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
+ also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)";
+ by simp;
finally; show "?P (Suc n)"; by simp;
qed;
@@ -85,7 +90,8 @@
fix n;
have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
also; assume "?S n = (n * (n + 1))^2";
- also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
+ also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
+ by simp;
finally; show "?P (Suc n)"; by simp;
qed;
--- a/src/HOL/Isar_examples/W_correct.thy Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Wed Oct 06 18:50:51 1999 +0200
@@ -6,22 +6,25 @@
Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
*)
+header {* Correctness of Milner's type inference algorithm~W (let-free version) *};
+
theory W_correct = Main + Type:;
-section "Mini ML with type inference rules";
+subsection "Mini ML with type inference rules";
datatype
expr = Var nat | Abs expr | App expr expr;
-text {* type inference rules *};
+text {* Type inference rules. *};
consts
has_type :: "(typ list * expr * typ) set";
syntax
- "@has_type" :: "[typ list, expr, typ] => bool" ("((_) |-/ (_) :: (_))" [60, 0, 60] 60);
+ "@has_type" :: "[typ list, expr, typ] => bool"
+ ("((_) |-/ (_) :: (_))" [60, 0, 60] 60);
translations
"a |- e :: t" == "(a,e,t) : has_type";
@@ -32,6 +35,8 @@
AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
==> a |- App e1 e2 :: t1";
+text {* Type assigment is close wrt.\ substitution. *};
+
lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
proof -;
assume "a |- e :: t";
@@ -40,15 +45,18 @@
fix a n;
assume "n < length a";
hence "n < length (map ($ s) a)"; by simp;
- hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI);
+ hence "map ($ s) a |- Var n :: map ($ s) a ! n";
+ by (rule has_type.VarI);
also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map);
also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list); (* FIXME unfold fails!? *)
finally; show "?P a (Var n) (a ! n)"; .;
next;
fix a e t1 t2;
assume "?P (t1 # a) e t2";
- hence "$ s t1 # map ($ s) a |- e :: $ s t2"; by (simp add: app_subst_list);
- hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; by (rule has_type.AbsI);
+ hence "$ s t1 # map ($ s) a |- e :: $ s t2";
+ by (simp add: app_subst_list);
+ hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2";
+ by (rule has_type.AbsI);
thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list);
next;
fix a e1 e2 t1 t2;
@@ -58,7 +66,7 @@
qed;
-section {* Type inference algorithm W *};
+subsection {* Type inference algorithm W *};
consts
W :: "[expr, typ list, nat] => (subst * typ * nat) maybe";
@@ -76,13 +84,16 @@
Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))";
+subsection {* Correctness theorem *};
+
(* FIXME proper split att/mod *)
ML_setup {* Addsplits [split_bind]; *};
theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
proof -;
assume W_ok: "W e a n = Ok (s, t, m)";
- have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e");
+ have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t"
+ (is "?P e");
proof (induct e);
fix n; show "?P (Var n)"; by simp;
next;
@@ -91,7 +102,8 @@
proof (intro allI impI);
fix a s t m n;
assume "Ok (s, t, m) = W (Abs e) a n";
- hence "EX t'. t = s n -> t' & Ok (s, t', m) = W e (TVar n # a) (Suc n)";
+ hence "EX t'. t = s n -> t' &
+ Ok (s, t', m) = W e (TVar n # a) (Suc n)";
by (rule rev_mp) simp;
with hyp; show "$ s a |- Abs e :: t";
by (force intro: has_type.AbsI);
@@ -116,7 +128,8 @@
and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
show ?thesis;
proof (rule has_type.AppI);
- from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; by (simp add: subst_comp_tel o_def);
+ from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";
+ by (simp add: subst_comp_tel o_def);
show "$s a |- e1 :: $ u t2 -> t";
proof -;
from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast;
@@ -126,7 +139,8 @@
qed;
show "$ s a |- e2 :: $ u t2";
proof -;
- from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
+ from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2";
+ by blast;
hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
by (rule has_type_subst_closed);
with s'; show ?thesis; by simp;
@@ -138,5 +152,4 @@
with W_ok [RS sym]; show ?thesis; by blast;
qed;
-
end;
--- a/src/HOL/Isar_examples/document/style.tex Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex Wed Oct 06 18:50:51 1999 +0200
@@ -1,9 +1,11 @@
+
+%% $Id$
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,pdfsetup}
\renewcommand{\isamarkupheader}[1]{\section{#1}}
-%\parindent 0pt \parskip 0.5ex
+\parindent 0pt \parskip 0.5ex
\newcommand{\name}[1]{\textsf{#1}}