# HG changeset patch
# User nipkow
# Date 1025884085 -7200
# Node ID f88d0c3635821a704ebac6ae231104ffefe626c9
# Parent  43ef6c6dd9065d7fc27c61e955cb3671421bc71a
*** empty log message ***

diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/IsaMakefile
--- 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
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- 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(*>*)
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/Misc/Plus.thy
--- /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
+(*>*)
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/Misc/ROOT.ML
--- 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";
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/Misc/Tree2.thy
--- 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"
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/Misc/document/Plus.tex
--- /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:
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/Misc/document/Tree2.tex
--- 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}%
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/fp.tex
--- 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}
diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/tutorial.ind
--- 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}