# HG changeset patch
# User nipkow
# Date 1440425987 -7200
# Node ID 40a0a40771268733235e36b24782606f669a4c25
# Parent  018b0c996b543b614ba255f1ed4643694ec332ef
nex exercise

diff -r 018b0c996b54 -r 40a0a4077126 src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Aug 24 00:20:20 2015 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Aug 24 16:19:47 2015 +0200
@@ -1118,6 +1118,17 @@
 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}
+Extend Exercise~\ref{exe:cfg} with a function that checks if some
+\mbox{@{text "alpha list"}} is a balanced
+string of parentheses. More precisely, define a recursive function
+@{text "balanced :: nat \<Rightarrow> alpha list \<Rightarrow> bool"} such that @{term"balanced n w"}
+is true iff (informally) @{text"a\<^sup>n @ w \<in> S"}. Formally, prove
+@{prop "balanced n w \<longleftrightarrow> replicate n a @ w \<in> S"} where
+@{const replicate} @{text"::"} @{typ"nat \<Rightarrow> 'a \<Rightarrow> 'a list"} is predefined
+and @{term"replicate n x"} yields the list @{text"[x, \<dots>, x]"} of length @{text n}.
+\end{exercise}
 *}
 
 (*<*)
diff -r 018b0c996b54 -r 40a0a4077126 src/Doc/Prog_Prove/Logic.thy
--- a/src/Doc/Prog_Prove/Logic.thy	Mon Aug 24 00:20:20 2015 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy	Mon Aug 24 16:19:47 2015 +0200
@@ -826,7 +826,7 @@
 @{prop"star r x y \<Longrightarrow> iter r n x y"}.
 \end{exercise}
 
-\begin{exercise}
+\begin{exercise}\label{exe:cfg}
 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)$ means that $w$ is in the language generated by $A$.