--- a/doc-src/TutorialI/IsaMakefile Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/IsaMakefile Fri Jul 05 17:48:05 2002 +0200
@@ -168,8 +168,8 @@
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
- Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \
- Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
+ Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \
+ Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
$(USEDIR) Misc
@rm -f tutorial.dvi
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Fri Jul 05 17:48:05 2002 +0200
@@ -471,4 +471,114 @@
text{*\noindent You may need to resort to this technique if an automatic step
fails to prove the desired proposition. *}
+
+section{*Induction*}
+
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+by (induct n, simp_all)
+
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n")
+proof (induct n)
+ show "?P 0" by simp
+next
+ fix n assume "?P n"
+ thus "?P(Suc n)" by simp
+qed
+
+(* Could refine further, but not necessary *)
+
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case Suc thus ?case by simp
+qed
+
+
+
+
+consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+primrec
+"itrev [] ys = ys"
+"itrev (x#xs) ys = itrev xs (x#ys)"
+
+lemma "\<And>ys. itrev xs ys = rev xs @ ys"
+by (induct xs, simp_all)
+
+(* The !! just disappears. Even more pronounced for \<Longrightarrow> *)
+
+lemma r: assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
+ shows "\<And>m. m < n \<Longrightarrow> P(m::nat)"
+proof (induct n)
+ case 0 hence False by simp thus ?case ..
+next
+ case (Suc n m)
+ show ?case
+ proof (cases)
+ assume eq: "m = n"
+ have "P n" sorry
+ with eq show "P m" by simp
+ next
+ assume neq: "m \<noteq> n"
+ with Suc have "m < n" by simp
+ with Suc show "P m" by blast
+ qed
+
+
+
+thm r
+thm r[of _ n "Suc n", simplified]
+
+lemma "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n) \<Longrightarrow> P n"
+
+lemma assumes P0: "P 0" and P1: "P(Suc 0)"
+ and P2: "\<And>k. P k \<Longrightarrow> P(Suc (Suc k))" shows "P n"
+proof (induct n rule: nat_less_induct)
+thm nat_less_induct
+ fix n assume "\<forall>m. m < n \<longrightarrow> P m"
+ show "P n"
+ proof (cases n)
+ assume "n=0" thus "P n" by simp
+ next
+ fix m assume n: "n = Suc m"
+ show "P n"
+ proof (cases m)
+ assume "m=0" with n show "P n" by simp
+ next
+ fix l assume "m = Suc l"
+ with n show "P n" apply simp
+
+by (case_tac "n" 1);
+by (case_tac "nat" 2);
+by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
+qed "nat_induct2";
+
+consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
+inductive "r*"
+intros
+rtc_refl[iff]: "(x,x) \<in> r*"
+rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+
+lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
+by(blast intro: rtc_step);
+
+lemma assumes A:"(x,y) \<in> r*" and B:"(y,z) \<in> r*" shows "(x,z) \<in> r*"
+proof -
+ from A B show ?thesis
+ proof (induct)
+ fix x assume "(x,z) \<in> r*" thus "(x,z) \<in> r*" .
+ next
+ fix x y
+qed
+
+text{*
+\begin{exercise}
+Show that the converse of @{thm[source]rtc_step} also holds:
+@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
+\end{exercise}*}
+
+
+
+text{*As always, the different cases can be tackled in any order.*}
+
(*<*)end(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Plus.thy Fri Jul 05 17:48:05 2002 +0200
@@ -0,0 +1,23 @@
+(*<*)
+theory Plus = Main:
+(*>*)
+
+text{*\noindent Define the following addition function *}
+
+consts plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+primrec
+"plus m 0 = m"
+"plus m (Suc n) = plus (Suc m) n"
+
+text{*\noindent and prove*}
+(*<*)
+lemma [simp]: "!m. plus m n = m+n"
+apply(induct_tac n)
+by(auto)
+(*>*)
+lemma "plus m n = m+n"
+(*<*)
+by(simp)
+
+end
+(*>*)
--- a/doc-src/TutorialI/Misc/ROOT.ML Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML Fri Jul 05 17:48:05 2002 +0200
@@ -1,6 +1,7 @@
use "../settings.ML";
use_thy "Tree";
use_thy "Tree2";
+use_thy "Plus";
use_thy "case_exprs";
use_thy "fakenat";
use_thy "natsum";
--- a/doc-src/TutorialI/Misc/Tree2.thy Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/Misc/Tree2.thy Fri Jul 05 17:48:05 2002 +0200
@@ -8,7 +8,7 @@
quadratic. A linear time version of @{term"flatten"} again reqires an extra
argument, the accumulator: *}
-consts flatten2 :: "'a tree => 'a list => 'a list"
+consts flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
(*<*)
primrec
"flatten2 Tip xs = xs"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Fri Jul 05 17:48:05 2002 +0200
@@ -0,0 +1,30 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Plus}%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Define the following addition function%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{primrec}\isanewline
+{\isachardoublequote}plus\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
+{\isachardoublequote}plus\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ plus\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent and prove%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Fri Jul 05 17:48:05 2002 +0200
@@ -11,7 +11,7 @@
argument, the accumulator:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/fp.tex Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/fp.tex Fri Jul 05 17:48:05 2002 +0200
@@ -377,7 +377,9 @@
\index{simplification|)}
\input{Misc/document/Itrev.tex}
-
+\begin{exercise}
+\input{Misc/document/Plus.tex}%
+\end{exercise}
\begin{exercise}
\input{Misc/document/Tree2.tex}%
\end{exercise}
--- a/doc-src/TutorialI/tutorial.ind Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/tutorial.ind Fri Jul 05 17:48:05 2002 +0200
@@ -137,7 +137,7 @@
\indexspace
- \item \isacommand {datatype} (command), 9, 38--43
+ \item \isacommand {datatype} (command), 9, 38--44
\item datatypes, 17--22
\subitem and nested recursion, 40, 44
\subitem mutually recursive, 38
@@ -226,7 +226,7 @@
\item function types, 5
\item functions, 109--111
\subitem partial, 182
- \subitem total, 11, 46--52
+ \subitem total, 11, 47--52
\subitem underdefined, 183
\indexspace
@@ -246,7 +246,7 @@
\item \isacommand {header} (command), 59
\item Hilbert's $\varepsilon$-operator, 86
\item \isacommand {hints} (command), 49, 180, 182
- \item HOLCF, 43
+ \item HOLCF, 44
\item Hopcroft, J. E., 145
\item \isa {hypreal} (type), 155
@@ -260,7 +260,7 @@
\item identity relation, \bold{112}
\item \isa {if} expressions, 5, 6
\subitem simplification of, 33
- \subitem splitting of, 31, 49
+ \subitem splitting of, 31, 50
\item if-and-only-if, 6
\item \isa {iff} (attribute), 90, 102, 130
\item \isa {iffD1} (theorem), \bold{94}
@@ -330,7 +330,7 @@
\indexspace
\item $\lambda$ expressions, 5
- \item LCF, 43
+ \item LCF, 44
\item \isa {LEAST} (symbol), 23, 85
\item least number operator, \see{\protect\isa{LEAST}}{85}
\item Leibniz, Gottfried Wilhelm, 53
@@ -423,7 +423,7 @@
\item pairs and tuples, 24, 155--158
\item parent theories, \bold{4}
\item pattern matching
- \subitem and \isacommand{recdef}, 47
+ \subitem and \isacommand{recdef}, 48
\item patterns
\subitem higher-order, \bold{177}
\item PDL, 118--120
@@ -431,7 +431,7 @@
\item \isacommand {prefer} (command), 16, 100
\item prefix annotation, 55
\item primitive recursion, \see{recursion, primitive}{1}
- \item \isacommand {primrec} (command), 10, 18, 38--43
+ \item \isacommand {primrec} (command), 10, 18, 38--44
\item print mode, \bold{55}
\item product type, \see{pairs and tuples}{1}
\item Proof General, \bold{7}
@@ -463,7 +463,7 @@
\item \isa {Real} (theory), 155
\item \isa {real} (type), 154--155
\item real numbers, 154--155
- \item \isacommand {recdef} (command), 46--52, 114, 178--186
+ \item \isacommand {recdef} (command), 47--52, 114, 178--186
\subitem and numeric literals, 150
\item \isa {recdef_cong} (attribute), 182
\item \isa {recdef_simp} (attribute), 49
@@ -597,7 +597,7 @@
\item \isa {trancl_trans} (theorem), \bold{113}
\item transition systems, 117
\item \isacommand {translations} (command), 56
- \item tries, 44--46
+ \item tries, 44--47
\item \isa {True} (constant), 5
\item \isa {truncate} (constant), 163
\item tuples, \see{pairs and tuples}{1}