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