--- a/doc-src/TutorialI/Overview/FP0.thy Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP0.thy Fri Jun 21 18:40:06 2002 +0200
@@ -1,7 +1,5 @@
theory FP0 = PreList:
-section{*Functional Programming/Modelling*}
-
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
@@ -16,10 +14,8 @@
"rev [] = []"
"rev (x # xs) = (rev xs) @ (x # [])"
-subsection{*An Introductory Proof*}
-
theorem rev_rev [simp]: "rev(rev xs) = xs"
-oops
+(*<*)oops(*>*)
text{*
--- a/doc-src/TutorialI/Overview/FP1.thy Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/FP1.thy Fri Jun 21 18:40:06 2002 +0200
@@ -1,6 +1,6 @@
+(*<*)
theory FP1 = Main:
-
-subsection{*More Constructs*}
+(*>*)
lemma "if xs = ys
then rev xs = rev ys
@@ -28,14 +28,22 @@
apply(auto)
done
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+text{*
+Some examples of linear arithmetic:
+*}
+
+lemma "\<lbrakk> \<not> m < n; m < n+(1::int) \<rbrakk> \<Longrightarrow> m = n"
by(auto)
lemma "min i (max j k) = max (min k i) (min i (j::nat))"
by(arith)
-lemma "n*n = n \<Longrightarrow> n=0 \<or> n=1"
-oops
+text{*
+Not proved automatically because it involves multiplication:
+*}
+
+lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)"
+(*<*)oops(*>*)
subsubsection{*Pairs*}
@@ -67,83 +75,90 @@
lemma fst_conv[simp]: "fst(x,y) = x"
by auto
+text{*
+Setting and resetting the @{text simp} attribute:
+*}
+
declare fst_conv[simp]
declare fst_conv[simp del]
subsubsection{*The Simplification Method*}
-lemma "x*(y+1) = y*(x+1)"
+lemma "x*(y+1) = y*(x+1::nat)"
apply simp
-oops
+(*<*)oops(*>*)
subsubsection{*Adding and Deleting Simplification Rules*}
lemma "\<forall>x::nat. x*(y+z) = r"
apply (simp add: add_mult_distrib2)
-oops
+(*<*)oops(*>*)text_raw {* \isanewline\isanewline *}
lemma "rev(rev(xs @ [])) = xs"
apply (simp del: rev_rev_ident)
-oops
-
+(*<*)oops(*>*)
subsubsection{*Assumptions*}
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
-apply simp
-done
+by simp
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"
-apply(simp (no_asm))
-done
-
+by(simp (no_asm))
subsubsection{*Rewriting with Definitions*}
lemma "xor A (\<not>A)"
apply(simp only: xor_def)
-by simp
+apply simp
+done
subsubsection{*Conditional Equations*}
lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
-apply(case_tac xs, simp, simp)
-done
+by(case_tac xs, simp_all)
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"
-by(simp)
+by simp
subsubsection{*Automatic Case Splits*}
lemma "\<forall>xs. if xs = [] then A else B"
apply simp
-oops
+(*<*)oops(*>*)text_raw {* \isanewline\isanewline *}
lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y"
apply simp
apply(simp split: list.split)
-oops
+(*<*)oops(*>*)
subsubsection{*Arithmetic*}
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+text{*
+Is simple enough for the default arithmetic:
+*}
+lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n"
by simp
-lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n"
+text{*
+Contains boolean combinations and needs full arithmetic:
+*}
+lemma "\<not> m < n \<and> m < n+(1::nat) \<Longrightarrow> m = n"
apply simp
by(arith)
-
+(*<*)
subsubsection{*Tracing*}
lemma "rev [a] = []"
apply(simp)
oops
+(*>*)
@@ -189,7 +204,7 @@
"comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]"
theorem "exec (comp e) s [] = [value e s]"
-oops
+(*<*)oops(*>*)
@@ -246,8 +261,10 @@
datatype tree = C "tree list"
-term "C[]"
-term "C[C[C[]],C[]]"
+text{*Some trees:*}
+
+term "C []"
+term "C [C [C []], C []]"
consts
mirror :: "tree \<Rightarrow> tree"
@@ -262,7 +279,7 @@
lemma "mirror(mirror t) = t \<and> mirrors(mirrors ts) = ts"
apply(induct_tac t and ts)
apply simp_all
-oops
+(*<*)oops(*>*)
text{*
\begin{exercise}
@@ -275,6 +292,7 @@
datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
+text{*A big tree:*}
term "Br 0 (\<lambda>i. Br i (\<lambda>n. Tip))"
consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
@@ -287,14 +305,17 @@
apply simp_all
done
-(* This is NOT allowed:
-datatype lambda = C "lambda \<Rightarrow> lambda"
-*)
+text{* This is \emph{not} allowed:
+\begin{verbatim}
+datatype lambda = C "lambda => lambda"
+\end{verbatim}
+*}
text{*
\begin{exercise}
Define a datatype of ordinals and the ordinal $\Gamma_0$.
\end{exercise}
*}
-
+(*<*)
end
+(*>*)
--- a/doc-src/TutorialI/Overview/RECDEF.thy Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy Fri Jun 21 18:40:06 2002 +0200
@@ -1,4 +1,6 @@
+(*<*)
theory RECDEF = Main:
+(*>*)
subsection{*Wellfounded Recursion*}
@@ -7,7 +9,7 @@
consts fib :: "nat \<Rightarrow> nat";
recdef fib "measure(\<lambda>n. n)"
"fib 0 = 0"
- "fib 1 = 1"
+ "fib (Suc 0) = 1"
"fib (Suc(Suc x)) = fib x + fib (Suc x)";
consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
@@ -21,14 +23,22 @@
"last [x] = x"
"last (x#y#zs) = last (y#zs)";
-
consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
recdef sep1 "measure (\<lambda>(a,xs). length xs)"
"sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
"sep1(a, xs) = xs";
+text{*
+This is what the rules for @{term sep1} are turned into:
+@{thm[display,indent=5] sep1.simps[no_vars]}
+*}
+(*<*)
thm sep1.simps
+(*>*)
+text{*
+Pattern matching is also useful for nonrecursive functions:
+*}
consts swap12 :: "'a list \<Rightarrow> 'a list";
recdef swap12 "{}"
@@ -38,6 +48,10 @@
subsubsection{*Beyond Measure*}
+text{*
+The lexicographic product of two relations:
+*}
+
consts ack :: "nat\<times>nat \<Rightarrow> nat";
recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
"ack(0,n) = Suc n"
@@ -77,10 +91,13 @@
done
text{*
+Figure out how that proof worked!
+
\begin{exercise}
Define a function for merging two ordered lists (of natural numbers) and
show that if the two input lists are ordered, so is the output.
\end{exercise}
*}
-
+(*<*)
end
+(*>*)
--- a/doc-src/TutorialI/Overview/Rules.thy Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/Rules.thy Fri Jun 21 18:40:06 2002 +0200
@@ -1,11 +1,27 @@
+(*<*)
theory Rules = Main:
+(*>*)
-section{*The Rules of the Game*}
+section{*The Rules of the Game*}
subsection{*Introduction Rules*}
+text{* Introduction rules for propositional logic:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]impI} & @{thm impI[no_vars]} \\
+@{thm[source]conjI} & @{thm conjI[no_vars]} \\
+@{thm[source]disjI1} & @{thm disjI1[no_vars]} \\
+@{thm[source]disjI2} & @{thm disjI2[no_vars]} \\
+@{thm[source]iffI} & @{thm iffI[no_vars]}
+\end{tabular}
+\end{center}
+*}
+
+(*<*)
thm impI conjI disjI1 disjI2 iffI
+(*>*)
lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
apply(rule impI)
@@ -19,11 +35,24 @@
subsection{*Elimination Rules*}
+text{* Elimination rules for propositional logic:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]impE} & @{thm impE[no_vars]} \\
+@{thm[source]mp} & @{thm mp[no_vars]} \\
+@{thm[source]conjE} & @{thm conjE[no_vars]} \\
+@{thm[source]disjE} & @{thm disjE[no_vars]}
+\end{tabular}
+\end{center}
+*}
+
+(*<*)
thm impE mp
thm conjE
thm disjE
+(*>*)
-lemma disj_swap: "P | Q \<Longrightarrow> Q | P"
+lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
apply (erule disjE)
apply (rule disjI2)
apply assumption
@@ -34,7 +63,21 @@
subsection{*Destruction Rules*}
+text{* Destruction rules for propositional logic:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]conjunct1} & @{thm conjunct1[no_vars]} \\
+@{thm[source]conjunct2} & @{thm conjunct2[no_vars]} \\
+@{thm[source]iffD1} & @{thm iffD1[no_vars]} \\
+@{thm[source]iffD2} & @{thm iffD2[no_vars]}
+\end{tabular}
+\end{center}
+*}
+
+(*<*)
thm conjunct1 conjunct1 iffD1 iffD2
+(*>*)
+
lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"
apply (rule conjI)
apply (drule conjunct2)
@@ -46,13 +89,26 @@
subsection{*Quantifiers*}
+text{* Quantifier rules:
+\begin{center}
+\begin{tabular}{ll}
+@{thm[source]allI} & @{thm allI[no_vars]} \\
+@{thm[source]exI} & @{thm exI[no_vars]} \\
+@{thm[source]allE} & @{thm allE[no_vars]} \\
+@{thm[source]exE} & @{thm exE[no_vars]} \\
+@{thm[source]spec} & @{thm spec[no_vars]}
+\end{tabular}
+\end{center}
+*}
+(*<*)
thm allI exI
thm allE exE
thm spec
+(*>*)
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
-oops
+(*<*)oops(*>*)
subsection{*Instantiation*}
@@ -65,13 +121,6 @@
by simp
-subsection{*Hilbert's epsilon Operator*}
-
-theorem axiom_of_choice:
- "\<forall>x. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
-by (fast elim!: someI)
-
-
subsection{*Automation*}
lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
@@ -93,12 +142,32 @@
subsection{*Forward Proof*}
-thm rev_rev_ident
-thm rev_rev_ident[of "[]"]
+text{*
+Instantiation of unknowns (in left-to-right order):
+\begin{center}
+\begin{tabular}{@ {}ll@ {}}
+@{thm[source]append_self_conv} & @{thm append_self_conv} \\
+@{thm[source]append_self_conv[of _ "[]"]} & @{thm append_self_conv[of _ "[]"]}
+\end{tabular}
+\end{center}
+Applying one theorem to another
+by unifying the premise of one theorem with the conclusion of another:
+\begin{center}
+\begin{tabular}{@ {}ll@ {}}
+@{thm[source]sym} & @{thm sym} \\
+@{thm[source]sym[OF append_self_conv]} & @{thm sym[OF append_self_conv]}\\
+@{thm[source]append_self_conv[THEN sym]} & @{thm append_self_conv[THEN sym]}
+\end{tabular}
+\end{center}
+*}
+
+(*<*)
+thm append_self_conv
+thm append_self_conv[of _ "[]"]
thm sym
-thm sym[OF rev_rev_ident]
-thm rev_rev_ident[THEN sym]
-
+thm sym[OF append_self_conv]
+thm append_self_conv[THEN sym]
+(*>*)
subsection{*Further Useful Methods*}
@@ -108,6 +177,7 @@
apply arith
done
+text{* And a cute example: *}
lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
\<forall>x y z. sqrt x * sqrt x = x \<and>
@@ -122,5 +192,7 @@
apply simp
done
*)
+(*<*)
oops
end
+(*>*)
--- a/doc-src/TutorialI/Overview/Sets.thy Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/Sets.thy Fri Jun 21 18:40:06 2002 +0200
@@ -1,32 +1,42 @@
+(*<*)
theory Sets = Main:
-
+(*>*)
section{*Sets, Functions and Relations*}
subsection{*Set Notation*}
-term "A \<union> B"
-term "A \<inter> B"
-term "A - B"
-term "a \<in> A"
-term "b \<notin> A"
-term "{a,b}"
-term "{x. P x}"
-term "{x+y+eps |x y. x < y}"
-term "\<Union> M"
-term "\<Union>a \<in> A. F a"
+text{*
+\begin{center}
+\begin{tabular}{ccc}
+@{term "A \<union> B"} & @{term "A \<inter> B"} & @{term "A - B"} \\
+@{term "a \<in> A"} & @{term "b \<notin> A"} \\
+@{term "{a,b}"} & @{text "{x. P x}"} \\
+@{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
+\end{tabular}
+\end{center}
+*}
+
+subsection{*Some Functions*}
-subsection{*Functions*}
-
+text{*
+\begin{tabular}{l}
+@{thm id_def}\\
+@{thm o_def[no_vars]}\\
+@{thm image_def[no_vars]}\\
+@{thm vimage_def[no_vars]}
+\end{tabular}
+*}
+(*<*)
thm id_def
-thm o_assoc
-thm image_Int
-thm vimage_Compl
+thm o_def[no_vars]
+thm image_def[no_vars]
+thm vimage_def[no_vars]
+(*>*)
-
-subsection{*Relations*}
+subsection{*Some Relations*}
thm Id_def
-thm converse_comp
+thm converse_def
thm Image_def
thm relpow.simps
thm rtrancl_idemp
@@ -117,7 +127,6 @@
@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
\end{exercise}
*}
-
+(*<*)
end
-
-
+(*>*)
--- a/doc-src/TutorialI/Overview/document/root.tex Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/document/root.tex Fri Jun 21 18:40:06 2002 +0200
@@ -10,11 +10,44 @@
\begin{document}
-\title{Overview}\maketitle
+\title{A Compact Overview of Isabelle/HOL}
+\author{Tobias Nipkow}
+\date{}
+\maketitle
+
+\noindent
+This document is a very compact introduction to the proof assistant
+Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283}
+where full explanations and a wealth of additional material can be found.
+
+While reading this document it is recommended to single-step through the
+corresponding theories using Isabelle/HOL to follow the proofs.
+
+\section{Functional Programming/Modelling}
+
+\subsection{An Introductory Theory}
+\input{FP0.tex}
-\input{session}
+\subsection{More Constructs}
+\input{FP1.tex}
+
+\input{RECDEF.tex}
+
+\input{Rules.tex}
+
+\input{Sets.tex}
+
+\input{Ind.tex}
-%\bibliographystyle{plain}
-%\bibliography{root}
+\input{Isar.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
+
+
+\bibliographystyle{plain}
+\bibliography{root}
\end{document}
--- a/doc-src/TutorialI/OverviewMakefile Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/OverviewMakefile Fri Jun 21 18:40:06 2002 +0200
@@ -1,4 +1,3 @@
-
## targets
default: Overview
@@ -13,7 +12,7 @@
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -i true -d dvi -D document
+USEDIR = $(ISATOOL) usedir -i true -d ps -D document -v true
## Overview
--- a/doc-src/TutorialI/free-copies Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/free-copies Fri Jun 21 18:40:06 2002 +0200
@@ -7,7 +7,7 @@
Gerwin Klein*
David von Oheimb*
Farhad Mehta*
-Stephan Merz
+Stephan Merz*
Leonor Prensa Nieto*
Cornelia Pusch
Bernhard Rumpe (wants a signed copy!)*