author nipkow Fri, 30 Mar 2001 18:12:26 +0200 changeset 11236 17403c5a9eb1 parent 11235 860c65c7388a child 11237 0ef5ecc1fd4d
*** empty log message ***
 doc-src/TutorialI/Overview/FP1.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/RECDEF.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Overview/document/session.tex file | annotate | diff | comparison | revisions
--- 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)

-

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 @@
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: