author nipkow Fri, 08 Nov 2013 21:40:07 +0100 changeset 54292 ce4a17b2e373 parent 54291 709a2bbd7638 child 54293 cd896760fa0f
more exercises
 src/Doc/ProgProve/Isar.thy file | annotate | diff | comparison | revisions src/Doc/ProgProve/Logic.thy file | annotate | diff | comparison | revisions
--- a/src/Doc/ProgProve/Isar.thy	Fri Nov 08 19:03:14 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Fri Nov 08 21:40:07 2013 +0100
@@ -1081,8 +1081,7 @@

\exercise
-Give a structured proof of @{prop "ev(Suc(Suc n)) \<Longrightarrow> ev n"}
-by rule inversion:
+Give a structured proof by rule inversion:
*}

lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
@@ -1098,6 +1097,13 @@
\end{exercise}

\begin{exercise}
+Recall predicate @{text star} from \autoref{sec:star} and @{text iter}
+from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \<Longrightarrow> star r x y"}
+in a structured style, do not just sledgehammer each case of the
+required induction.
+\end{exercise}
+
+\begin{exercise}
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
\end{exercise}
--- a/src/Doc/ProgProve/Logic.thy	Fri Nov 08 19:03:14 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Fri Nov 08 21:40:07 2013 +0100
@@ -816,7 +816,7 @@
if the assumption about the inductive predicate is not the first assumption.
\endexercise

-\begin{exercise}
+\begin{exercise}\label{exe:iter}
Analogous to @{const star}, give an inductive definition of the @{text n}-fold iteration
of a relation @{text r}: @{term "iter r n x y"} should hold if there are @{text x\<^sub>0}, \dots, @{text x\<^sub>n}
such that @{prop"x = x\<^sub>0"}, @{prop"x\<^sub>n = y"} and @{text"r x\<^bsub>i\<^esub> x\<^bsub>i+1\<^esub>"} for