Theory AnBn_Not_Regular
section ‹‹a⇧nb⇧n› is Not Regular›
theory AnBn_Not_Regular
imports Pumping_Lemma_Regular
begin
lemma pow_list_set_if: "set (w ^^ k) = (if k=0 then {} else set w)"
using pow_list_set[of _ w] by (auto dest: gr0_implies_Suc)
lemma in_pow_list_set[simp]: "x ∈ set (ys ^^ m) ⟷ x ∈ set ys ∧ m ≠ 0"
by (simp add: pow_list_set_if)
lemma pow_list_eq_appends_iff:
"n ≥ m ⟹ x^^n @ y = x^^m @ z ⟷ z = x^^(n-m) @ y"
using pow_list_add[of m "n-m" x] by auto
lemma append_eq_append_conv_if_disj:
"(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}
⟹ xs @ ys = xs' @ ys' ⟷ xs = xs' ∧ ys = ys'"
by (auto simp: all_conj_distrib disjoint_iff append_eq_append_conv2)
lemma pow_list_eq_single_appends_iff[simp]:
"⟦ x ∉ set ys; x ∉ set zs ⟧ ⟹ [x]^^m @ ys = [x]^^n @ zs ⟷ m = n ∧ ys = zs"
using append_eq_append_conv_if_disj[of "[x]^^m" "[x]^^n" "ys" "zs"]
by (auto simp: disjoint_iff pow_list_single)
text
‹The following theorem proves that the language ‹a^nb^n› cannot be produced by a right linear production set, using the contrapositive form
of the pumping lemma›
theorem not_rlin2_ab:
assumes "a ≠ b"
and "Lang P A = (⋃n. {[a]^^n @ [b]^^n})" (is "_ = ?AnBn")
and "finite P"
shows "¬rlin2 P"
proof -
have "∃w ∈ Lang P A. length w ≥ n ∧ (∀x y z. w = x@y@z ∧ length y ≥ 1 ∧ length (x@y) ≤ n ⟶ (∃i. x@(y^^i)@z ∉ Lang P A))" for n
proof -
let ?anbn = "[a]^^n @ [b]^^n"
show ?thesis
proof
have **: "(∃i. x @ (y^^i) @ z ∉ Lang P A)"
if asm: "?anbn = x @ y @ z ∧ 1 ≤ length y ∧ length (x @ y) ≤ n" for x y z
proof
from asm have asm1: "[a]^^n @ [b]^^n = x @ y @ z" by blast
from asm have asm2: "1 ≤ length y" by blast
from asm have asm3: "length (x @ y) ≤ n" by blast
let ?kx = "length x" let ?ky = "length y"
have splitted: "x = [a]^^?kx ∧ y = [a]^^?ky ∧ z = [a]^^(n - ?kx - ?ky) @ [b]^^n"
proof -
have "∀i < n. ([a]^^n @ [b]^^n)!i = a"
by (simp add: nth_append nth_pow_list_single)
with asm1 have xyz_tma: "∀i < n. (x@y@z)!i = a" by metis
with asm3 have xy_tma: "∀i < length(x@y). (x@y)!i = a"
by (metis append_assoc nth_append order_less_le_trans)
from xy_tma have "∀i < ?kx. x!i = a"
by (metis le_add1 length_append nth_append order_less_le_trans)
hence *: "x = [a]^^?kx"
by (simp add: list_eq_iff_nth_eq nth_pow_list_single)
from xy_tma have "∀i < ?ky. y!i = a"
by (metis length_append nat_add_left_cancel_less nth_append_length_plus)
hence **: "y = [a]^^?ky"
by (simp add: nth_equalityI pow_list_single)
from * ** asm1 have "[a]^^n @ [b]^^n = [a]^^?kx @ [a]^^?ky @ z" by simp
hence z_rest: "[a]^^n @ [b]^^n = [a]^^(?kx+?ky) @ z"
by (simp add: pow_list_add)
from asm3 have ***: "z = [a]^^(n-?kx-?ky) @ [b]^^n"
using pow_list_eq_appends_iff[THEN iffD1, OF _ z_rest] by simp
from * ** *** show ?thesis by blast
qed
from splitted have "x @ y^^2 @ z = [a]^^?kx @ ([a]^^?ky)^^2 @ [a]^^(n - ?kx - ?ky) @ [b]^^n" by simp
also have "... = [a]^^?kx @ [a]^^(?ky*2) @ [a]^^(n - ?kx - ?ky) @ [b]^^n"
by (simp add: pow_list_mult)
also have "... = [a]^^(?kx + ?ky*2 + (n - ?kx - ?ky)) @ [b]^^n"
by (simp add: pow_list_add)
also from asm3 have "... = [a]^^(n+?ky) @ [b]^^n"
by (simp add: add.commute)
finally have wit: "x @ y^^2 @ z = [a]^^(n+?ky) @ [b]^^n" .
from asm2 have "[a]^^(n + ?ky) @ [b]^^n ∉ ?AnBn"
using ‹a≠b› by auto
with wit have "x @ y^^2 @ z ∉ ?AnBn" by simp
thus "x @ y^^2 @ z ∉ Lang P A" using assms(2) by blast
qed
from ** show "n ≤ length ?anbn ∧ (∀x y z. ?anbn = x @ y @ z ∧ 1 ≤ length y ∧ length (x @ y) ≤ n ⟶ (∃i. x @ (y^^i) @ z ∉ Lang P A))" by simp
next
have "?anbn ∈ ?AnBn" by blast
thus "?anbn ∈ Lang P A"
by (simp add: assms(2))
qed
qed
thus ?thesis
using pumping_lemma_regular_contr[OF assms(3)] by blast
qed
end