chapter {* R8: Gramáticas libres de contexto *}
theory R8_Gramaticas_libre_de_contexto
imports Main
begin
text {*
En esta relación se definen dos gramáticas libres de contexto y se
demuestra que son equivalentes. Además, se define por recursión una
función para reconocer las palabras de la gramática y se demuestra que
es correcta y completa. *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Una gramática libre de contexto para las expresiones
parentizadas es
S ⟶ ε | '(' S ')' | SS
definir inductivamente la gramática S usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}
datatype alfabeto = A | B
inductive_set S :: "alfabeto list set" where
S1: "[] ∈ S"
| S2: "w ∈ S ⟹ [A] @ w @ [B] ∈ S"
| S3: "v ∈ S ⟹ w ∈ S ⟹ v @ w ∈ S"
text {*
---------------------------------------------------------------------
Ejercicio 2. Otra gramática libre de contexto para las expresiones
parentizadas es
T ⟶ ε | T '(' T ')'
definir inductivamente la gramática T usando A y B para '(' y ')',
respectivamente.
------------------------------------------------------------------ *}
inductive_set T :: "alfabeto list set" where
T1: "[] ∈ T"
| T2: "v ∈ T ⟹ w ∈ T ⟹ v @ [A] @ w @ [B] ∈ T"
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que T está contenido en S.
------------------------------------------------------------------ *}
(* benber alfmarcua antramhur josgomrom4 juacanrod giafus1 gleherlop *)
lemma T_en_S:
assumes "w ∈ T"
shows "w ∈ S"
proof -
have "w ∈ T ⟹ w ∈ S"
proof (induction rule: T.induct)
show "[] ∈ S" by (rule S1)
next
fix v w
assume "w ∈ S"
hence "[A] @ w @ [B] ∈ S" by (rule S2)
moreover assume "v ∈ S"
ultimately show "v @ [A] @ w @ [B] ∈ S" using S3 by simp
qed
thus ?thesis using assms .
qed
(* cammonagu *)
declare S1 [iff] S2[intro!,simp]
(* cammonagu *)
declare T1 [iff]
(* cammonagu *)
lemma T2ImpS: "w ∈ T ⟹ w ∈ S"
apply (erule T.induct)
apply simp
apply (blast intro: S3)
done
(* cammonagu *)
lemma T_en_S1:
assumes "w ∈ T"
shows "w ∈ S"
proof -
have "w ∈ T ⟹ w ∈ S" using assms by (rule T2ImpS)
thus ?thesis using assms .
qed
(* pabalagon marfruman1 pabbergue *)
lemma T_en_S2:
assumes "w ∈ T"
shows "w ∈ S"
using assms(1) apply (induction rule: T.induct) apply (rule S1) proof -
fix v w
assume HI1: "v ∈ S" and HI2: "w ∈ S"
have "[A] @ w @ [B] ∈ S" using HI2 by (rule S2)
thus "v @ [A] @ w @ [B] ∈ S" using HI1 S3 by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S está contenido en T.
------------------------------------------------------------------ *}
(* benber *)
lemma S_en_T:
"w ∈ S ⟹ w ∈ T"
proof (induction rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w
have "[] ∈ T" by (rule T1)
moreover assume "w ∈ T"
ultimately have "[] @ [A] @ w @ [B] ∈ T" by (rule T2)
thus "[A] @ w @ [B] ∈ T" by simp
next
fix v w
assume "v ∈ T"
moreover assume "w ∈ T"
moreover have "⟦v ∈ T; w ∈ T⟧ ⟹ v @ w ∈ T" for v w
proof (induction "length w + length v"
arbitrary: w v
rule: less_induct)
case IH: less
show "v @ w ∈ T"
proof (cases w rule: T.cases)
show "w ∈ T" using `w ∈ T`.
next
assume "w = []"
thus "v @ w ∈ T" using `v ∈ T` by simp
next
fix w1 w2
assume "w1 ∈ T" and "w2 ∈ T"
assume "w = w1 @ [A] @ w2 @ [B]"
hence 1: "v @ w = v @ w1 @ [A] @ w2 @ [B]" by simp
have "length w1 < length w" using `w = w1 @ [A] @ w2 @ [B]`
by simp
hence "length v + length w1 < length v + length w" by simp
moreover note `v ∈ T`
moreover note `w1 ∈ T`
ultimately have "v @ w1 ∈ T" using IH by simp
moreover note `w2 ∈ T`
ultimately have "(v @ w1) @ [A] @ w2 @ [B] ∈ T" by (rule T2)
thus "v @ w ∈ T" using 1 by simp
qed
qed
ultimately show "v @ w ∈ T" by simp
qed
(* alfmarcua antramhur josgomrom4 juacanrod gleherlop *)
lemma S_en_T_2:
"w ∈ S ⟹ w ∈ T"
proof (induction rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w
assume "w ∈ T"
have "[] @ [A] @ w @ [B] ∈ T" using T1 `w ∈ T` by (rule T2)
then show "[A] @ w @ [B] ∈ T" by (simp only: List.append.append_Nil)
next
fix w v
assume "v ∈ T"
show "w ∈ T ⟹ v @ w ∈ T"
proof (induction rule: T.induct)
show "v @ [] ∈ T" using `v ∈ T`
by (simp only: List.append.right_neutral)
next
fix va w
have "v @ va ∈ T ⟹ w ∈ T ⟹ (v @ va) @ [A] @ w @ [B] ∈ T "
by (rule T2)
then show "v @ va ∈ T ⟹ w ∈ T ⟹ v @ va @ [A] @ w @ [B] ∈ T "
by (simp only: List.append_assoc)
qed
qed
(* pabalagon giafus1 marfruman1 pabbergue *)
lemma S_en_T3:
"w ∈ S ⟹ w ∈ T"
apply (induction rule: S.induct) apply (rule T1) proof -
fix w
assume "w ∈ T"
with T1 have "[] @ [A] @ w @ [B] ∈ T" by (rule T2)
thus "[A] @ w @ [B] ∈ T" by simp
next
fix v w
assume HI1: "v ∈ T" and HI2: "w ∈ T"
show "w ∈ T ⟹ v @ w ∈ T" apply (induction rule: T.induct) apply (simp add: HI1)
proof -
fix va wa
assume "v @ va ∈ T"
moreover assume "wa ∈ T"
ultimately have "(v @ va) @ [A] @ wa @ [B] ∈ T" by (rule T2)
thus "v @ va @ [A] @ wa @ [B] ∈ T" by simp
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S y T son iguales.
------------------------------------------------------------------ *}
(* benber cammonagu antramhur josgomrom4 pabbergue *)
lemma S_igual_T:
"S = T"
using T_en_S S_en_T by auto
(* alfmarcua pabalagon giafus1 gleherlop marfruman1*)
lemma S_igual_T_2:
"S = T"
proof (rule equalityI)
show "S ⊆ T" using S_en_T by (rule subsetI)
next
show "T ⊆ S" using T_en_S by (rule subsetI)
qed
text {*
---------------------------------------------------------------------
Ejercicio 5. En lugar de una gramática, se puede usar el siguiente
procedimiento para determinar si la cadena es una sucesión de
paréntesis bien balanceada: se recorre la cadena de izquierda a
derecha contando cuántos paréntesis de necesitan para que esté bien
balanceada. Si el contador al final de la cadena es 0, la cadena está
bien balanceada.
Definir la función
balanceada :: alfabeto list ⇒ bool
tal que (balanceada w) se verifica si w está bien balanceada. Por
ejemplo,
balanceada [A,A,B,B] = True
balanceada [A,B,A,B] = True
balanceada [A,B,B,A] = False
Indicación: Definir balanceada usando la función auxiliar
balanceada_aux :: alfabeto list ⇒ nat ⇒ bool
tal que (balanceada_aux w 0) se verifica si w está bien balanceada.
------------------------------------------------------------------ *}
(* benber alfmarcua antramhur josgomrom4 pabalagon gleherlop giafus1 marfruman1 pabbergue *)
(* balanceada_aux w n = True si y solo si ([A]*n) @ w es balanceada *)
fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where
"balanceada_aux [] 0 = True"
| "balanceada_aux [] (Suc n) = False"
| "balanceada_aux (B#w) 0 = False"
| "balanceada_aux (B#w) (Suc n) = balanceada_aux w n"
| "balanceada_aux (A#w) n = balanceada_aux w (Suc n)"
fun balanceada :: "alfabeto list ⇒ bool" where
"balanceada w = balanceada_aux w 0"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que balanceada es un reconocedor correcto de la
gramática S; es decir,
w ∈ S ⟹ balanceada w
------------------------------------------------------------------ *}
(* benber *)
lemma balanceada_correcto_aux1:
"balanceada_aux w n ⟹ balanceada_aux (w @ [B]) (Suc n)"
proof (induction w arbitrary: n)
case Nil
assume "balanceada_aux [] n"
thus ?case by simp
next
case IS: (Cons x w)
show ?case
proof (cases x)
case A
note `balanceada_aux (x#w) n`
hence "balanceada_aux (A#w) n" using `x = A` by simp
hence "balanceada_aux w (Suc n)" by simp
hence "balanceada_aux (w@[B]) (Suc (Suc n))" using IS.IH by simp
hence "balanceada_aux ((A#w)@[B]) (Suc n)" by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B#w) n" using IS.prems by simp
show ?thesis
proof (cases n)
case 0
hence "balanceada_aux (B#w) 0" using 1 by simp
hence "False" by simp
thus ?thesis ..
next
case (Suc m)
hence "balanceada_aux (B#w) (Suc m)" using 1 by simp
hence "balanceada_aux w m" by simp
hence "balanceada_aux (w@[B]) (Suc m)" using IS.IH by simp
hence "balanceada_aux (w@[B]) n" using `n = Suc m` by simp
hence "balanceada_aux (B#(w@[B])) (Suc n)" by simp
thus ?thesis using `x = B` by simp
qed
qed
qed
lemma balanceada_correcto_aux2:
assumes "balanceada v"
shows "balanceada_aux w n ⟹ balanceada_aux (w @ v) n"
proof (induction w arbitrary: n)
case Nil
hence "n = 0" using balanceada_aux.elims by auto
thus ?case using assms by simp
next
case IS: (Cons x w)
show "balanceada_aux ((x#w)@v) n"
proof (cases x)
case A
hence "balanceada_aux (A#w) n" using IS.prems by simp
hence "balanceada_aux w (Suc n)" by simp
hence "balanceada_aux (w@v) (Suc n)" using IS.IH by simp
hence "balanceada_aux (A#(w@v)) n" by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B#w) n" using IS.prems by simp
show ?thesis
proof (cases n)
case 0
hence "balanceada_aux (B#w) 0" using 1 by simp
hence "False" by simp
thus ?thesis ..
next
case (Suc m)
hence "balanceada_aux (B#w) (Suc m)" using 1 by simp
hence "balanceada_aux w m" by simp
hence "balanceada_aux (w@v) m" using IS.IH by simp
hence "balanceada_aux (B#(w@v)) (Suc m)" by simp
thus ?thesis using `x = B` `n = Suc m` by simp
qed
qed
qed
lemma balanceada_correcto:
"w ∈ S ⟹ balanceada w"
proof (induction rule: S.induct)
case S1
have "balanceada [] = balanceada_aux [] 0" by simp
also have "..." by simp
finally show ?case.
next
case S2
fix w
assume "balanceada w"
hence "balanceada_aux w 0" by simp
hence "balanceada_aux (w@[B]) 1" using balanceada_correcto_aux1
by simp
hence "balanceada_aux ([A] @ w @ [B]) 0" by simp
thus "balanceada ([A] @ w @ [B])" by simp
next
case S3
thus ?case using balanceada_correcto_aux2 by auto
qed
(* alfmarcua antramhur josgomrom4 giafus1 pabbergue *)
lemma balanceada_correcto_aux3:
shows "balanceada_aux v m ⟹
balanceada_aux w n ⟹
balanceada_aux (v @ w) (m+n)"
proof (induction v arbitrary: n m)
case Nil
then show ?case
proof (cases m)
case 0
then have "balanceada_aux w (m + n)" using Nil.prems(2)
by (simp only:Groups.monoid_add_class.add.left_neutral)
then show ?thesis by (simp only:List.append.append_Nil)
next
case (Suc mm)
then have "False" using Nil.prems(1)
by (simp only: balanceada_aux.simps(2))
then show ?thesis ..
qed
next
case IS:(Cons a v)
show "balanceada_aux ((a # v) @ w) (m + n)"
proof (cases a)
define k :: nat where "k = m + 1"
case A
then have "balanceada_aux v k" using `k = m + 1` IS.prems(1)
by simp
then have "balanceada_aux (v @ w) (k + n)" using IS.prems(2)
by (rule IS.IH)
then have "balanceada_aux (v @ w) (Suc(m + n))" using `k = m + 1`
by simp
then have "balanceada_aux (A # (v @ w)) (m + n)"
by (simp only: balanceada_aux.simps(5))
then show ?thesis using `a = A`
by (simp only:List.append.append_Cons)
next
case B
then show ?thesis
proof (cases m)
case 0
then have "False" using IS.prems(1) `a = B`
by (simp only: balanceada_aux.simps(3))
then show ?thesis ..
next
case (Suc mm)
hence "balanceada_aux v mm" using IS.prems(1) `a = B`
by (simp only: balanceada_aux.simps(4))
then have "balanceada_aux (v @ w) (mm + n)" using IS.prems(2)
by (rule IS.IH)
then have "balanceada_aux (B # (v @ w)) (Suc (mm + n))"
by (simp only: balanceada_aux.simps(4))
then have "balanceada_aux (B # (v @ w)) (m + n)"
using `m = Suc mm` by (simp only: Nat.plus_nat.add_Suc)
then show ?thesis using `a=B`
by (simp only:List.append.append_Cons)
qed
qed
qed
lemma balanceada_correcto_2:
"w ∈ S ⟹ balanceada w"
proof (induction rule: S.induct)
case S1
have "balanceada_aux [] 0" by (simp only: balanceada_aux.simps(1))
then show ?case by (simp only: balanceada.simps)
next
case (S2 w)
then have 1:"balanceada_aux w 0" by (simp only: balanceada.simps)
have "balanceada_aux [] 0" by (simp only: balanceada_aux.simps(1))
then have 2:"balanceada_aux (B#[]) (Suc 0)"
by (simp only: balanceada_aux.simps(4))
have "balanceada_aux w 0 ⟹
balanceada_aux [B] (Suc 0) ⟹
balanceada_aux (w @ [B]) (0+Suc 0)"
by (rule balanceada_correcto_aux3)
then have "balanceada_aux (w @ [B]) (Suc 0)" using 1 2
by (simp only:Groups.monoid_add_class.add.left_neutral)
then have "balanceada_aux (A # (w @ [B])) 0"
by (simp only: balanceada_aux.simps(5))
then have "balanceada_aux ([A] @ w @ [B]) 0"
by (simp only: List.append_Cons List.append_Nil)
then show ?case by (simp only: balanceada.simps)
next
case (S3 v w)
then have 1:"balanceada_aux w 0" by (simp only: balanceada.simps)
have 2:"balanceada_aux v 0" using S3(3)
by (simp only: balanceada.simps)
have "balanceada_aux v 0 ⟹
balanceada_aux w 0 ⟹
balanceada_aux (v @ w) (0+0)"
by (rule balanceada_correcto_aux3)
then have "balanceada_aux (v @ w) 0" using 1 2
by (simp only:Groups.monoid_add_class.add.right_neutral)
then show ?case by (simp only: balanceada.simps)
qed
(* pabalagon *)
lemma balanceada_correcto_aux4:
"⟦balanceada_aux v m; balanceada_aux w n⟧ ⟹ balanceada_aux (v@w) (m+n)"
proof (induction v arbitrary: m n)
fix m n
case Nil
hence "m = 0" proof (induct m)
case 0 thus ?case by simp
next
case Suc hence False using Nil(1) by simp thus ?case by (rule FalseE)
qed
have "balanceada_aux ([] @ w) n" using Nil(2) by simp
thus "balanceada_aux ([] @ w) (m + n)" using `m=0` by simp
next
fix m n
case (Cons a v)
show "balanceada_aux ((a#v)@w) (m+n)" using Cons(2) Cons(3)
proof (cases a)
define k where "k = Suc m"
case A
hence "balanceada_aux (A#v) m" using Cons(2) by simp
hence "balanceada_aux v k" using k_def by simp
hence "balanceada_aux (v@w) (k + n)" using Cons(1,3) by simp
hence "balanceada_aux (A # (v@w)) (m+n)" using k_def by simp
thus ?thesis using A by simp
next
case B thus ?thesis proof (cases m)
case 0
hence False using Cons(2) B by simp
thus ?thesis by (rule FalseE)
next
case (Suc mm)
hence "balanceada_aux (B#v) (Suc mm)" using Cons(2) B by simp
hence "balanceada_aux v mm" by simp
hence "balanceada_aux (v@w) (mm + n)" using Cons(1, 3) by simp
hence "balanceada_aux (B#v@w) (Suc (mm+n))" by simp
thus ?thesis using B Suc by simp
qed
qed
qed
lemma balanceada_correcto3:
"w ∈ S ⟹ balanceada w"
apply (induction rule: S.induct) apply simp proof -
fix w n
assume HI: "balanceada w"
hence "balanceada_aux w 0" by simp
moreover have "balanceada_aux [B] 1" by simp
ultimately have "balanceada_aux (w@[B]) (0+1)" by (rule balanceada_correcto_aux4)
thus "balanceada ([A] @ w @ [B])" by simp
next
fix v w
assume "balanceada v"
hence 1: "balanceada_aux v 0" by simp
assume "balanceada w"
hence "balanceada_aux w 0" by simp
with 1 have "balanceada_aux (v@w) (0+0)" by (rule balanceada_correcto_aux4)
thus "balanceada (v@w)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que balanceada es un reconocedor completo de
la gramática S; es decir,
balanceada w ⟹ w ∈ S
------------------------------------------------------------------ *}
(* benber antramhur pabalagon pabbergue *)
lemma balanceada_aux_unico:
"⟦balanceada_aux w k; balanceada_aux w l⟧ ⟹ k = l" for w k l
proof (induction w arbitrary: k l)
case Nil
hence "k = 0 ∧ l = 0" using balanceada_aux.elims by auto
thus ?case by simp
next
case IS: (Cons x w')
show ?case
proof (cases x)
case A
thus ?thesis using IS by auto
next
case B
show ?thesis
proof (cases k)
case 0
hence "False" using IS.prems `x = B` by simp
thus ?thesis ..
next
case (Suc k')
hence "balanceada_aux w' k'" using IS.prems `x = B` by simp
show ?thesis
proof (cases l)
case 0
hence "False" using IS.prems `x = B` by simp
thus ?thesis ..
next
case (Suc l')
hence "balanceada_aux w' l'" using IS.prems `x = B` by simp
thus ?thesis
using `balanceada_aux w' k'` IS.IH `k = Suc k'` `l = Suc l'`
by auto
qed
qed
qed
qed
lemma balanceada_completo_aux1:
"⟦balanceada (x # w @ [y]);
⋀u v. u ≠ [] ∧ v ≠ [] ∧ u @ v = x # w @ [y] ⟶ ¬ (balanceada v)⟧
⟹ x = A ∧ y = B ∧ balanceada w"
proof -
assume "balanceada (x # w @ [y])"
hence bal: "balanceada_aux ( x # w @ [y] ) 0" by simp
assume postfix_con: "⋀u v. u ≠ [] ∧ v ≠ [] ∧ u @ v = x # w @ [y] ⟶
¬ (balanceada v)"
have "x = A"
proof (rule ccontr)
assume "x ≠ A"
hence "x = B" using alfabeto.exhaust by blast
thus "False" using bal by simp
qed
have hl1: "balanceada_aux (w @ [y]) n ⟹ y = B" for w y n
proof (induction w arbitrary: n)
case IB: Nil
show "y = B"
proof (rule ccontr)
assume "y ≠ B"
hence "y = A" using alfabeto.exhaust by blast
thus "False" using IB by simp
qed
next
case IS: (Cons x w)
hence "balanceada_aux (x # w @ [y]) n" by simp
hence "∃m. balanceada_aux (w @ [y]) m" using balanceada_aux.elims(2)
by blast (* SH'd *)
thus "y = B" using IS.IH by auto
qed
have "y = B" using bal hl1[of "(x#w)"] by simp
hence "balanceada_aux (w @ [B]) 1" using bal `x = A` by simp
have hl2: "balanceada_aux (x#w) n ⟹ ∃m. balanceada_aux w m"
for x w n
proof (cases x)
case A
moreover assume "balanceada_aux (x#w) n"
ultimately show ?thesis by auto
next
case B
moreover assume "balanceada_aux (x#w) n"
ultimately have "balanceada_aux (B#w) n" by simp
thus ?thesis by (cases n) auto
qed
have "⟦balanceada_aux w n; u @ v = w⟧ ⟹ ∃ m. balanceada_aux v m"
for u v w n
proof (induction w arbitrary: u v n)
case Nil
hence "v = []" by simp
hence "balanceada_aux v 0" by simp
thus ?case ..
next
case IS: (Cons x w')
then obtain m where mDef: "balanceada_aux w' m" using hl2 by blast
show ?case
proof (cases u)
case Nil
hence "balanceada_aux v n" using IS by simp
thus ?thesis ..
next
case (Cons y u')
hence "w' = u' @ v" using IS.prems by simp
thus ?thesis using IS.IH mDef by simp
qed
qed
moreover have "balanceada_aux (w @ [B]) 1" using bal `x = A` `y = B`
by simp
ultimately have "u @ v = (w @ [B]) ⟹ ∃m. balanceada_aux v m"
for u v by auto
moreover {
fix u v
have 1: "⟦u' ≠ []; v ≠ []; u' @ v = (x # w @ [y])⟧ ⟹
¬(balanceada v)" for u'
using postfix_con by auto
have "⟦v ≠ []; (x#u) @ v = (x # w @ [y])⟧ ⟹ ¬(balanceada v)"
using 1[of "x#u"] by simp
hence "⟦v ≠ []; u @ v = (w @ [B])⟧ ⟹ ¬(balanceada_aux v 0)"
using `y = B` by simp
}
ultimately have hl3: "⟦v ≠ []; u @ v = (w @ [B])⟧ ⟹
∃m. balanceada_aux v (Suc m)" for u v
by (metis zero_induct) (* SH'd *)
have hl4: "⟦balanceada_aux (v @ [B]) (Suc n); ⋀s t. v = s @ t ⟹
∃m. balanceada_aux (t @ [B]) (Suc m)⟧
⟹ balanceada_aux v n" for v n
proof (induction v arbitrary: n)
case Nil
hence "balanceada_aux [B] (Suc n)" by simp
thus "balanceada_aux [] n" by simp
next
case IS: (Cons x v')
have "x#v' = [x] @ v'" by simp
then obtain m where mDef: "balanceada_aux (v' @ [B]) (Suc m)"
using IS.prems by blast
moreover have v'Postf: "⋀s t. v' = s @ t ⟹
∃m. balanceada_aux (t @ [B]) (Suc m)"
using IS.prems by auto
ultimately have "balanceada_aux v' m" using IS.IH by simp
show ?case
proof (cases x)
case A
hence "balanceada_aux ((A # v') @ [B]) (Suc n)" using IS.prems
by simp
hence "balanceada_aux (v' @ [B]) (Suc (Suc n))" by simp
hence "balanceada_aux v' (Suc n)" using IS.IH v'Postf by simp
thus ?thesis using `x = A` by simp
next
case B
hence "balanceada_aux ((B # v') @ [B]) (Suc n)" using IS.prems
by simp
hence 1: "balanceada_aux ( v' @ [B]) n" using IS.prems by simp
have "n = Suc m" using 1 mDef balanceada_aux_unico by simp
thus "balanceada_aux (x # v') n"
using `balanceada_aux v' m` `x = B` by simp
qed
qed
moreover note `balanceada_aux (w @ [B]) 1`
moreover have "w = s @ t ⟹ ∃m. balanceada_aux (t @ [B]) (Suc m)"
for s t using hl3 by simp
ultimately have "balanceada_aux w 0" by simp
thus "x = A ∧ y = B ∧ balanceada w" using `x = A` `y = B`by simp
qed
lemma balanceada_completo_aux2:
assumes "balanceada (u @ v)" and "¬ balanceada u"
shows "¬ balanceada v"
proof -
have "⟦balanceada_aux (u @ v) n; balanceada v⟧ ⟹ balanceada_aux u n"
for n
proof (induction u arbitrary: n)
case Nil
hence "n = 0" using balanceada_aux_unico by simp
thus ?case by simp
next
case IS: (Cons x u')
show ?case
proof (cases x)
case A
hence "balanceada_aux (A # u' @ v) n" using IS.prems by simp
hence "balanceada_aux (u' @ v) (Suc n)" by simp
hence "balanceada_aux u' (Suc n)" using `balanceada v` IS.IH
by simp
thus ?thesis using `x = A` by simp
next
case B
hence 1: "balanceada_aux (B # u' @ v) n" using IS.prems by simp
then obtain m where "Suc m = n" by (cases n) auto
hence "balanceada_aux (B # u' @ v) (Suc m)" using 1 by simp
hence "balanceada_aux u' m" using `balanceada v` IS.IH by simp
hence "balanceada_aux (B # u') n" using `Suc m = n` by auto
thus ?thesis using `x = B` by simp
qed
qed
thus ?thesis using assms by auto
qed
lemma balanceada_completo:
assumes "balanceada w"
shows "w ∈ S"
proof -
have "balanceada w ⟹ w ∈ S"
proof (induction "length w" arbitrary: w rule: less_induct)
case IS: less
show ?case
proof (cases w)
case Nil
thus ?thesis using S1 by simp
next
case (Cons x w')
show ?thesis
proof (cases w')
case Nil
hence "¬ balanceada (x#w')" by (cases x) auto
hence "False" using `w = x # w'`IS.prems by simp
thus ?thesis ..
next
case (Cons y w'')
show ?thesis
proof cases
assume "∃u v. w = u @ v ∧ u ≠ [] ∧ v ≠ [] ∧
balanceada u ∧ balanceada v"
then obtain u v where "w = u @ v" and
"u ≠ []" and
"v ≠ []" and
"balanceada u"
and "balanceada v" by blast
have "u ∈ S" using `w = u @ v` `v ≠ []` `balanceada u` IS
by simp
moreover have "v ∈ S"
using `w = u @ v` `u ≠ []` `balanceada v` IS by simp
ultimately show "w ∈ S" using S3 `w = u @ v` by simp
next
assume "∄u v. w = u @ v ∧ u ≠ [] ∧ v ≠ [] ∧
balanceada u ∧ balanceada v"
hence 1: "⟦u @ v = w; u ≠ []; v ≠ []; balanceada u⟧ ⟹
¬ balanceada v" for u v by auto
have "w = x # y # w''" using `w = x # w'` `w' = y # w''`
by simp
moreover have "∃ u z. y # w'' = u @ [z]"
proof -
have "∃ u y. (x :: alfabeto) # v = u @ [y]" for x v
proof (induction v arbitrary: x)
case Nil
have "x # [] = [] @ [x]" by simp
thus ?case by simp
next
case IS: (Cons z v')
then obtain u' y' where "z # v' = u' @ [y']" by blast
hence "x # z # v' = x # u' @ [y']" using IS by simp
thus ?case by simp
qed
thus ?thesis by simp
qed
ultimately have "∃ u z. w = x # u @ [z]" by auto
then obtain u z where "w = x # u @ [z]" by blast
hence "balanceada (x # u @ [z])" using `balanceada w` by simp
moreover have "⟦s ≠ []; t ≠ []; s @ t = x # u @ [z]⟧ ⟹
¬ balanceada t" for s t
proof (cases "balanceada s")
case True
moreover assume "s ≠ []"
moreover assume "t ≠ []"
moreover assume "s @ t = x # u @ [z]"
ultimately show ?thesis using 1 `w = x # u @ [z]` by auto
next
case False
assume "s @ t = x # u @ [z]"
hence "x # u @ [z] = s @ t" ..
thus ?thesis
using balanceada_completo_aux2
`balanceada w`
`¬ balanceada s`
`w = x # u @ [z]`
by simp
qed
ultimately have "x = A" and "z = B" and "balanceada u"
using balanceada_completo_aux1[of x u z] by auto
moreover have "u ∈ S"
using `w = x # u @ [z]` IS `balanceada u` by simp
hence "x # u @ [z] ∈ S" using S2 `u ∈ S` `x = A` `z = B`
by simp
thus "w ∈ S" using `w = x # u @ [z]` by simp
qed
qed
qed
qed
thus ?thesis using assms .
qed
end
