--- a/doc-src/TutorialI/Overview/FP1.thy Fri Mar 30 16:12:57 2001 +0200
+++ b/doc-src/TutorialI/Overview/FP1.thy Fri Mar 30 18:12:26 2001 +0200
@@ -141,11 +141,9 @@
subsubsection{*Tracing*}
-ML "set trace_simp"
lemma "rev [a] = []"
apply(simp)
oops
-ML "reset trace_simp"
@@ -193,22 +191,9 @@
theorem "exec (comp e) s [] = [value e s]";
oops
-theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-oops
-
-lemma exec_app[simp]:
- "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
-apply(induct_tac xs)
-apply(simp)
-apply(simp split: instr.split)
-done
-
-theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-by(induct_tac e, auto)
-
-subsection{*Advanced Datatupes*}
+subsection{*Advanced Datatypes*}
subsubsection{*Mutual Recursion*}
@@ -279,8 +264,11 @@
apply simp_all
oops
-lemma "mirrors ts = rev(map mirror ts)"
-by(induct ts, simp_all)
+text{*
+\begin{exercise}
+Complete the above proof.
+\end{exercise}
+*}
subsubsection{*Datatypes Involving Functions*}
@@ -303,4 +291,10 @@
datatype lambda = C "lambda \<Rightarrow> lambda"
*)
+text{*
+\begin{exercise}
+Define a datatype of ordinals and the ordinal Gamma0.
+\end{exercise}
+*}
+
end
--- a/doc-src/TutorialI/Overview/RECDEF.thy Fri Mar 30 16:12:57 2001 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy Fri Mar 30 18:12:26 2001 +0200
@@ -75,4 +75,11 @@
apply(simp add:rev_map sym[OF map_compose] cong:map_cong)
done
+text{*
+\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/document/session.tex Fri Mar 30 16:12:57 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-\input{FP0.tex}
-
-\input{FP1.tex}
-
-\input{RECDEF.tex}
-
-\input{Rules.tex}
-
-\input{Sets.tex}
-
-\input{Ind.tex}
-
-\input{Isar.tex}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: