(*<*)
theory hwsol_04
imports Main
begin
(*>*)
text {* \ExerciseSheet{4}{3.~11.~2015} *}
text {*\NumHomework{Counting Elements}{November 10} *}
text {* {\bf Give all your proofs in Isar, not apply style}*}
text \Recall the count function, that counts how often a specified element
occurs in a list:\
fun count :: "'a \ 'a list \ nat" where
"count x [] = 0"
| "count x (y#ys) = (if x=y then Suc (count x ys) else count x ys)"
text \Show that, if an element occurs in the list (its count is positive),
the list can be split into a prefix not containing the element, the element itself,
and a suffix containing the element one times less\
lemma "count x xs = Suc n \ \p s. xs = p@x#s \ count x p = 0 \ count x s = n"
(*<*)
proof (induction xs arbitrary: n)
case Nil thus ?case by auto
next
case (Cons y ys)
show ?case proof (cases "x=y")
case True[simp]
from \count x (y # ys) = Suc n\ have "count x ys = n" by simp
moreover have "y#ys = []@x#ys" by simp
moreover have "count x [] = 0" by simp
ultimately show ?thesis by blast
next
case False[simp]
from Cons.prems have "count x ys = Suc n" by simp
from Cons.IH[OF this] obtain p s where "y#ys = (y#p) @ x # s" "count x (y#p) = 0" "count x s = n"
by auto
thus ?thesis by blast
qed
qed
(*>*)
text {*\NumHomework{Counting Elements II}{November 10} *}
text {* {\bf Use Isar where appropriate }*}
text \
Use an inductive definition to specify the words accepted by the following context free grammar:
@{text "S \ aSbS | bSaS | \"}
\
datatype character = a | b
inductive S :: "character list \ bool"
(*<*)
where
"S []"
| "S x1 \ S x2 \ S (a#x1@b#x2)"
| "S x1 \ S x2 \ S (b#x1@a#x2)"
(*>*)
(*<*)
lemma [simp]: "count x (xs@ys) = count x xs + count x ys"
by (induction xs) auto
(*>*)
text \
Show that every word accepted by the grammar has the same number of $a$s and $b$s.
\
lemma S_same_number:
assumes "S xs"
shows "count a xs = count b xs"
(*<*)
using assms
by (induction) auto
(*>*)
text \
The crucial lemma for the other direction, i.e., that every word with the
same number of $a$s and $b$s is accepted by the grammar, states that,
in a sequence of numbers, such that the next number
is one less or one more than the previous number, the first number is $0$,
and the last number is $1$, we must find a $0$ to $1$ transition.
We first fix the situation described above in a context:
\
context
fixes d :: "nat \ int" -- \The sequence as a function\
fixes n :: nat -- \The maximum index into the sequence (length - 1)\
assumes DIFF: "\iThe difference between adjacent elements is $-1$ or $1$\
assumes START: "d 0 = 0" -- \The first element is $0$\
assumes END: "d n = 1" -- \The last element is $1$\
begin
(*<*)
lemma find_step_aux:
assumes "j\n"
assumes "d j \ 0"
shows "\i d (i+1) = 1"
using assms
(*apply (induction rule: inc_induct)
using DIFF START END
apply auto
apply force*)
proof (induction rule: inc_induct)
case base with END show ?case by auto
next
case (step i)
show ?case proof (cases "d (Suc i) \ 0")
case True from step.IH[OF this] show ?thesis by blast
next
case False with DIFF \i \d i \ 0\ have "d i = 0 \ d (Suc i) = 1"
by auto
thus ?thesis using \i by auto
qed
qed
(*>*)
text \Your task is to prove the following theorem.
You will need to generalize the theorem to allow
arbitrary indexes with values $\le 0$ as starting point.
Then, you may use the induction rule @{text "inc_induct"}.
Hint: If you have problems finding a proof, sketch the proof on paper first,
and then try to translate your proof sketch to Isar!
\
theorem find_step: "\i d (i+1) = 1"
(*<*)
using find_step_aux[of 0] START by simp
(*>*)
end
(*<*)
definition "delta l i = int (count a (take i l)) - int (count b (take i l))"
definition "delta' l i = int (count b (take i l)) - int (count a (take i l))"
lemma [simp]: "a\x \ x=b" by (cases x) auto
lemma same_number_S:
assumes "count a l = count b l"
shows "S l"
using assms
proof (induction l rule: length_induct)
case (1 xl)
note A = "1.prems"
note IH = "1.IH"[rule_format]
show ?case
proof (cases xl)
case Nil thus ?thesis by (auto intro: S.intros)
next
case (Cons x l) [simp]
show ?thesis proof (cases x)
case a[simp]
{ fix i
assume "idelta' l i - delta' l (i + 1)\ = 1"
by (auto simp: delta'_def take_Suc_conv_app_nth)
} hence 1: "\idelta' l i - delta' l (i + 1)\ = 1" by auto
have [simp]: "delta' l 0 = 0" by (auto simp: delta'_def)
from A have END: "delta' l (length l) = 1" unfolding delta'_def by auto
from find_step[where d="delta' l" and n="length l", OF 1 _ END]
obtain i where 2: "i"take i l"
def s \"drop (Suc i) l"
have LP: "length p < length xl" by (simp add: p_def)
have LS: "length s < length xl" by (simp add: s_def)
from 2 have CE: "count a p = count b p" by (auto simp: delta'_def p_def)
from IH[OF LP CE] have "S p" .
from 2 have IB: "l!i = b"
unfolding delta'_def
by (simp add: take_Suc_conv_app_nth split: split_if_asm)
note LF[simp] = id_take_nth_drop[OF \i, folded p_def s_def, unfolded IB]
from CE IB LF END have C2EQ: "count a s = count b s"
by (auto simp: delta'_def)
from IH[OF LS this] have "S s" .
from S.intros(2)[OF \S p\ \S s\] show "S xl" by simp
next
case b[simp]
{ fix i
assume "idelta l i - delta l (i + 1)\ = 1"
by (auto simp: delta_def take_Suc_conv_app_nth)
} hence 1: "\idelta l i - delta l (i + 1)\ = 1" by auto
have [simp]: "delta l 0 = 0" by (auto simp: delta_def)
from A have END: "delta l (length l) = 1" unfolding delta_def by auto
from find_step[where d="delta l" and n="length l", OF 1 _ END]
obtain i where 2: "i"take i l"
def s \"drop (Suc i) l"
have LP: "length p < length xl" by (simp add: p_def)
have LS: "length s < length xl" by (simp add: s_def)
from 2 have CE: "count a p = count b p" by (auto simp: delta_def p_def)
from IH[OF LP CE] have "S p" .
from 2 have IB: "l!i = a"
unfolding delta_def
by (simp add: take_Suc_conv_app_nth split: split_if_asm)
note LF[simp] = id_take_nth_drop[OF \i, folded p_def s_def, unfolded IB]
from CE IB LF END have C2EQ: "count a s = count b s"
by (auto simp: delta_def)
from IH[OF LS this] have "S s" .
from S.intros(3)[OF \S p\ \S s\] show "S xl" by simp
qed
qed
qed
(*>*)
text \
For {\bf 5 bonus points}, finish the proof of the other direction, i.e., prove:
\
theorem "S l \ count a l = count b l"
(*<*)
using S_same_number same_number_S by blast
(*>*)
text \{\bf Warning:} This proof is hard. Do not attempt it unless you
finished the rest of this homework. To succeed with this proof,
you are strongly advised to sketch it on paper first, and then
translate it to Isar.\
(*<*)
end
(*>*)