# HG changeset patch
# User nipkow
# Date 1024677606 -7200
# Node ID a6cb18a25cbb19fcbce1fa77b8ff4f375beee469
# Parent  493d61afa73106686f78aad2285fa74f444f4753
*** empty log message ***

diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/FP0.thy
--- 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{*
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/FP1.thy
--- 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
+(*>*)
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/RECDEF.thy
--- 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
+(*>*)
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/Rules.thy
--- 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
+(*>*)
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/Sets.thy
--- 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
-
-
+(*>*)
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/Overview/document/root.tex
--- 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}
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/OverviewMakefile
--- 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
diff -r 493d61afa731 -r a6cb18a25cbb doc-src/TutorialI/free-copies
--- 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!)*