# HG changeset patch
# User nipkow
# Date 1383216525 -3600
# Node ID 07c0c121a8dce2cb99f86590e3e88089b4eec583
# Parent  2fa338fd0a280d82bbcf68d51ef682e96f716b2a
more exercises

diff -r 2fa338fd0a28 -r 07c0c121a8dc src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Wed Oct 30 17:20:59 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Thu Oct 31 11:48:45 2013 +0100
@@ -595,10 +595,10 @@
 \exercise
 Give a readable, structured proof of the following lemma:
 *}
-lemma assumes T: "\<forall> x y. T x y \<or> T y x"
-  and A: "\<forall> x y. A x y \<and> A y x \<longrightarrow> x = y"
-  and TA: "\<forall> x y. T x y \<longrightarrow> A x y" and "A x y"
-shows "T x y"
+lemma assumes T: "\<forall>x y. T x y \<or> T y x"
+  and A: "\<forall>x y. A x y \<and> A y x \<longrightarrow> x = y"
+  and TA: "\<forall>x y. T x y \<longrightarrow> A x y" and "A x y"
+  shows "T x y"
 (*<*)oops(*>*)
 text{*
 \endexercise
@@ -612,10 +612,11 @@
 text{*
 Hint: There are predefined functions @{const_typ take} and @{const_typ drop}
 such that @{text"take k [x\<^sub>1,\<dots>] = [x\<^sub>1,\<dots>,x\<^sub>k]"} and
-@{text"drop k [x\<^sub>1,\<dots>] = [x\<^bsub>k+1\<^esub>,\<dots>]"}. Let @{text simp} and especially
-sledgehammer find and apply the relevant @{const take} and @{const drop} lemmas for you.
+@{text"drop k [x\<^sub>1,\<dots>] = [x\<^bsub>k+1\<^esub>,\<dots>]"}. Let sledgehammer find and apply
+the relevant @{const take} and @{const drop} lemmas for you.
 \endexercise
 
+
 \section{Case Analysis and Induction}
 
 \subsection{Datatype Case Analysis}
@@ -1075,45 +1076,20 @@
 @{text induct} method.
 \end{warn}
 
+
 \subsection{Exercises}
 
 \begin{exercise}
+Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"}.
+Rule inversion is sufficient. If there are no cases to be proved you can close
+a proof immediateley with \isacom{qed}.
+\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}
-
-\begin{exercise}
-A context-free grammar can be seen as an inductive definition where each
-nonterminal $A$ is an inductively defined predicate on lists of terminal
-symbols: $A(w)$ mans
-that $w$ is in the language generated by $A$. For example, the production $S
-\to a S b$ can be viewed as the implication @{prop"S w \<Longrightarrow> S (a # w @ [b])"}
-where @{text a} and @{text b} are constructors of some datatype of terminal
-symbols: \isacom{datatype} @{text"tsymbs = a | b | \<dots>"}
-
-Define the two grammars
-\[
-\begin{array}{r@ {\quad}c@ {\quad}l}
-S &\to& \varepsilon \quad\mid\quad a~S~b \quad\mid\quad S~S \\
-T &\to& \varepsilon \quad\mid\quad T~a~T~b
-\end{array}
-\]
-($\varepsilon$ is the empty word)
-as two inductive predicates and prove @{prop"S w \<longleftrightarrow> T w"}.
-\end{exercise}
-
 *}
-(*
-lemma "\<not> ev(Suc(Suc(Suc 0)))"
-proof
-  assume "ev(Suc(Suc(Suc 0)))"
-  then show False
-  proof cases
-    case evSS
-    from `ev(Suc 0)` show False by cases
-  qed
-qed
-*)
 
 (*<*)
 end
diff -r 2fa338fd0a28 -r 07c0c121a8dc src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Wed Oct 30 17:20:59 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Thu Oct 31 11:48:45 2013 +0100
@@ -805,6 +805,29 @@
 if the assumption about the inductive predicate is not the first assumption.
 \endexercise
 
+\begin{exercise}
+A context-free grammar can be seen as an inductive definition where each
+nonterminal $A$ is an inductively defined predicate on lists of terminal
+symbols: $A(w)$ mans that $w$ is in the language generated by $A$.
+For example, the production $S \to a S b$ can be viewed as the implication
+@{prop"S w \<Longrightarrow> S (a # w @ [b])"} where @{text a} and @{text b} are terminal symbols,
+i.e., elements of some alphabet. The alphabet can be defined like this:
+\isacom{datatype} @{text"alpha = a | b | \<dots>"}
+
+Define the two grammars (where $\varepsilon$ is the empty word)
+\[
+\begin{array}{r@ {\quad}c@ {\quad}l}
+S &\to& \varepsilon \quad\mid\quad aSb \quad\mid\quad SS \\
+T &\to& \varepsilon \quad\mid\quad TaTb
+\end{array}
+\]
+as two inductive predicates.
+If you think of @{text a} and @{text b} as ``@{text "("}'' and  ``@{text ")"}'',
+the grammars defines strings of balanced parentheses.
+Prove @{prop"T w \<Longrightarrow> S w"} and @{prop "S w \<Longrightarrow> T w"} separately and conclude
+@{prop "S w = T w"}.
+\end{exercise}
+
 \ifsem
 \begin{exercise}
 In \autoref{sec:AExp} we defined a recursive evaluation function