author nipkow Thu, 31 Oct 2013 11:48:45 +0100 changeset 54218 07c0c121a8dc parent 54217 2fa338fd0a28 child 54219 63fe59f64578
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	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