equal
deleted
inserted
replaced
1116 |
1116 |
1117 \begin{exercise} |
1117 \begin{exercise} |
1118 Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"} |
1118 Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"} |
1119 and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}. |
1119 and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}. |
1120 \end{exercise} |
1120 \end{exercise} |
|
1121 |
|
1122 \begin{exercise} |
|
1123 Extend Exercise~\ref{exe:cfg} with a function that checks if some |
|
1124 \mbox{@{text "alpha list"}} is a balanced |
|
1125 string of parentheses. More precisely, define a recursive function |
|
1126 @{text "balanced :: nat \<Rightarrow> alpha list \<Rightarrow> bool"} such that @{term"balanced n w"} |
|
1127 is true iff (informally) @{text"a\<^sup>n @ w \<in> S"}. Formally, prove |
|
1128 @{prop "balanced n w \<longleftrightarrow> replicate n a @ w \<in> S"} where |
|
1129 @{const replicate} @{text"::"} @{typ"nat \<Rightarrow> 'a \<Rightarrow> 'a list"} is predefined |
|
1130 and @{term"replicate n x"} yields the list @{text"[x, \<dots>, x]"} of length @{text n}. |
|
1131 \end{exercise} |
1121 *} |
1132 *} |
1122 |
1133 |
1123 (*<*) |
1134 (*<*) |
1124 end |
1135 end |
1125 (*>*) |
1136 (*>*) |