--- a/src/HOL/Induct/Acc.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Induct/Acc.thy Fri Oct 08 15:09:14 1999 +0200
@@ -18,10 +18,12 @@
inductive "acc r"
intrs
- accI [rulify_prems]: "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
-
+ accI [rulify_prems]:
+ "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
-syntax termi :: "('a * 'a)set => 'a set"
-translations "termi r" == "acc(r^-1)"
+syntax
+ termi :: "('a * 'a)set => 'a set"
+translations
+ "termi r" == "acc(r^-1)"
end
--- a/src/HOL/Isar_examples/Cantor.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Fri Oct 08 15:09:14 1999 +0200
@@ -6,15 +6,16 @@
chapter of "Isabelle's Object-Logics" (Larry Paulson).
*)
-header {* More classical proofs: Cantor's Theorem *};
+header {* 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 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\]
+ elements. It has become a favorite basic example in pure
+ 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
--- a/src/HOL/Isar_examples/Group.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Fri Oct 08 15:09:14 1999 +0200
@@ -11,7 +11,8 @@
text {*
We define an axiomatic type class of general groups over signature
- $({\times}, \idt{one}, \idt{inv})$.
+ $({\times} :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha,
+ \idt{inv} :: \alpha \To \alpha)$.
*};
consts
--- a/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 08 15:09:14 1999 +0200
@@ -25,12 +25,14 @@
let ?case1 = "?case1 {(N, M). ?R N M}";
assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
- hence "EX a' M0' K. M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;
+ hence "EX a' M0' K.
+ M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;
thus "?case1 | ?case2";
proof (elim exE conjE);
fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'";
assume "M0 + {#a#} = M0' + {#a'#}";
- hence "M0 = M0' & a = a' | (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})";
+ hence "M0 = M0' & a = a' |
+ (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})";
by (simp only: add_eq_conv_ex);
thus ?thesis;
proof (elim disjE conjE exE);
@@ -59,14 +61,14 @@
{{;
fix M M0 a;
- assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
- and M0: "M0 : ?W"
+ assume M0: "M0 : ?W"
+ and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
have "M0 + {#a#} : ?W";
proof (rule accI [of "M0 + {#a#}"]);
fix N; assume "(N, M0 + {#a#}) : ?R";
hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
- (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
+ (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
by (rule less_add);
thus "N : ?W";
proof (elim exE disjE conjE);
@@ -88,7 +90,7 @@
proof;
assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
hence "(x, a) : r"; by simp;
- with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..;
+ with wf_hyp; have b: "ALL M:?W. M + {#x#} : ?W"; by blast;
from a hyp; have "M0 + K : ?W"; by simp;
with b; have "(M0 + K) + {#x#} : ?W"; ..;
@@ -114,11 +116,13 @@
fix M a; assume "M : ?W";
from wf; have "ALL M:?W. M + {#a#} : ?W";
proof (rule wf_induct [of r]);
- fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
+ fix a;
+ assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
show "ALL M:?W. M + {#a#} : ?W";
proof;
fix M; assume "M : ?W";
- thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning);
+ thus "M + {#a#} : ?W";
+ by (rule acc_induct) (rule tedious_reasoning);
qed;
qed;
thus "M + {#a#} : ?W"; ..;
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 08 15:09:14 1999 +0200
@@ -23,13 +23,15 @@
inductive "tiling A"
intrs
empty: "{} : tiling A"
- Un: "[| a : A; t : tiling A; a <= - t |] ==> a Un t : tiling A";
+ Un: "[| a : A; t : tiling A; a <= - t |]
+ ==> a Un t : tiling A";
-text "The union of two disjoint tilings is a tiling";
+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";
+ "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");
@@ -119,7 +121,8 @@
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"
+lemma dominoes_tile_row:
+ "{i} Times below (2 * n) : tiling domino"
(is "?P n" is "?B n : ?T");
proof (induct n);
show "?P 0"; by (simp add: below_0 tiling.empty);
@@ -268,9 +271,11 @@
note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
have "card (?e ?t'' 0) < card (?e ?t' 0)";
proof -;
- have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)";
+ have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
+ < card (?e ?t' 0)";
proof (rule card_Diff1_less);
- show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force;
+ show "finite (?e ?t' 0)";
+ by (rule finite_subset, rule fin) force;
show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
qed;
thus ?thesis; by simp;
@@ -282,7 +287,8 @@
by (rule card_Diff1_less);
thus ?thesis; by simp;
qed;
- also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
+ 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]);
--- a/src/HOL/Isar_examples/ROOT.ML Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML Fri Oct 08 15:09:14 1999 +0200
@@ -6,8 +6,8 @@
*)
time_use_thy "BasicLogic";
+time_use_thy "Cantor";
time_use_thy "Peirce";
-time_use_thy "Cantor";
time_use_thy "ExprCompiler";
time_use_thy "Group";
time_use_thy "Summation";
--- a/src/HOL/Isar_examples/Summation.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Fri Oct 08 15:09:14 1999 +0200
@@ -22,13 +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 *};
+verbatim {* \begin{comment} *};
+
(* FIXME binary arithmetic does not yet work here *)
syntax
@@ -43,8 +46,11 @@
theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
+verbatim {* \end{comment} *};
-theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
+
+theorem sum_of_naturals:
+ "2 * (SUM i < n + 1. i) = n * (n + 1)"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;
@@ -56,7 +62,8 @@
finally; show "?P (Suc n)"; by simp;
qed;
-theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
+theorem sum_of_odds:
+ "(SUM i < n. 2 * i + 1) = n^2"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;
@@ -77,12 +84,13 @@
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;
-theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
+theorem sum_of_cubes:
+ "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;
--- a/src/HOL/Isar_examples/W_correct.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Fri Oct 08 15:09:14 1999 +0200
@@ -6,7 +6,7 @@
Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
*)
-header {* Correctness of Milner's type inference algorithm~W (let-free version) *};
+header {* Milner's type inference algorithm~W (let-free version) *};
theory W_correct = Main + Type:;
@@ -47,8 +47,10 @@
hence "n < length (map ($ s) a)"; by simp;
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!? *)
+ 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;
@@ -114,10 +116,11 @@
proof (intro allI impI);
fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
hence "EX s1 t1 n1 s2 t2 n2 u.
- s = $ u o $ s2 o s1 & t = u n2 &
- mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
- W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
- W e1 a n = Ok (s1, t1, n1)"; by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
+ s = $ u o $ s2 o s1 & t = u n2 &
+ mgu ($ s2 t1) (t2 -> TVar n2) = Ok u &
+ W e2 ($ s1 a) n1 = Ok (s2, t2, n2) &
+ W e1 a n = Ok (s1, t1, n1)";
+ by (rule rev_mp) (simp, force); (* FIXME force fails !??*)
thus "$ s a |- App e1 e2 :: t";
proof (elim exE conjE);
fix s1 t1 n1 s2 t2 n2 u;
@@ -132,7 +135,8 @@
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;
+ from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1";
+ by blast;
hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
by (intro has_type_subst_closed);
with s' t mgu_ok; show ?thesis; by simp;
--- a/src/HOL/Isar_examples/document/root.tex Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/document/root.tex Fri Oct 08 15:09:14 1999 +0200
@@ -3,7 +3,6 @@
\hyphenation{Isabelle}
-
\begin{document}
\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
@@ -18,7 +17,6 @@
\end{abstract}
\tableofcontents
-
\input{session}
\end{document}
--- a/src/HOL/Isar_examples/document/style.tex Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex Fri Oct 08 15:09:14 1999 +0200
@@ -2,7 +2,7 @@
%% $Id$
\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,pdfsetup}
+\usepackage{comment,isabelle,pdfsetup}
\renewcommand{\isamarkupheader}[1]{\section{#1}}
\parindent 0pt \parskip 0.5ex
--- a/src/Pure/Thy/latex.ML Fri Oct 08 15:08:47 1999 +0200
+++ b/src/Pure/Thy/latex.ML Fri Oct 08 15:09:14 1999 +0200
@@ -26,25 +26,16 @@
"%" => "\\%" |
"#" => "\\#" |
"_" => "\\_" |
- "{" => "{\\textbraceleft}" |
- "}" => "{\\textbraceright}" |
- "~" => "{\\textasciitilde}" |
- "^" => "{\\textasciicircum}" |
+ "{" => "{\\isabraceleft}" |
+ "}" => "{\\isabraceright}" |
+ "~" => "{\\isatilde}" |
+ "^" => "{\\isacircum}" |
"\"" => "{\"}" |
- "\\" => "\\verb,\\," |
+ "\\" => "{\\isabackslash}" |
c => c;
-val output_chr' = fn
- "\\" => "{\\textbackslash}" |
- "|" => "{\\textbar}" |
- "<" => "{\\textless}" |
- ">" => "{\\textgreater}" |
- c => output_chr c;
-
-
(* FIXME replace \<forall> etc. *)
val output_sym = implode o map output_chr o explode;
-val output_sym' = implode o map output_chr' o explode;
(* token output *)
@@ -63,14 +54,18 @@
fun output_tok (Basic tok) =
let val s = T.val_of tok in
if invisible_token tok then ""
- else if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym' s ^ "}"
- else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym' s ^ "}"
+ else if T.is_kind T.Command tok then
+ if s = "{{" then "{\\isabeginblock}"
+ else if s = "}}" then "{\\isaendblock}"
+ else "\\isacommand{" ^ output_sym s ^ "}"
+ else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
+ "\\isakeyword{" ^ output_sym s ^ "}"
else if T.is_kind T.String tok then output_sym (quote s)
else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
else output_sym s
end
- | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n"
- | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n";
+ | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
+ | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n";
val output_tokens = implode o map output_tok;