header {* T11: Gramáticas libres de contexto *}
theory T11_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.
------------------------------------------------------------------ *}
lemma T_en_S:
assumes "w ∈ T"
shows "w ∈ S"
using assms
proof (induct rule: T.induct)
show "[] ∈ S" by (rule S1)
next
fix v w
assume "v ∈ T" and "v ∈ S" and "w ∈ T" and "w ∈ S"
have "[A] @ w @ [B] ∈ S" using `w ∈ S` by (rule S2)
with `v ∈ S` show "v @ [A] @ w @ [B] ∈ S" by (rule S3)
qed
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S está contenido en T.
------------------------------------------------------------------ *}
text {*
Se usarán dos lemas auxiliares:
· S_en_T_aux1: w ∈ T ⟹ [A] @ w @ [B] ∈ T
· S_en_T_aux2: v ∈ T ⟹ u ∈ T ⟹ u @ v ∈ T
*}
-- "La demostración estructurada del primer lema es"
lemma S_en_T_aux1:
assumes "w ∈ T"
shows "[A] @ w @ [B] ∈ T"
proof -
have "[] ∈ T" by (rule T1)
hence "[] @ [A] @ w @ [B] ∈ T" using assms by (rule T2)
thus "[A] @ w @ [B] ∈ T" by simp
qed
-- "La demostración automática del primer lema es"
lemma S_en_T_aux1b:
"w ∈ T ⟹ [A] @ w @ [B] ∈ T"
using T1 T2 [where v = "[]"] by simp
-- "La demostración estructurada del segundo lema es"
lemma S_en_T_aux2:
"v ∈ T ⟹ u ∈ T ⟹ u @ v ∈ T"
proof (induct rule: T.induct)
assume "u ∈ T"
thus "u @ [] ∈ T" by simp
next
fix w1 w2
assume "w1 ∈ T"
"u ∈ T ⟹ u @ w1 ∈ T"
"w2 ∈ T"
"u ∈ T ⟹ u @ w2 ∈ T"
"u ∈ T"
hence "u @ w1 ∈ T" by simp
hence "(u @ w1) @ [A] @ w2 @ [B] ∈ T" using `w2 ∈ T` by (rule T2)
thus "u @ w1 @ [A] @ w2 @ [B] ∈ T" by simp
qed
lemma S_en_T:
"w ∈ S ⟹ w ∈ T"
proof (induct rule: S.induct)
show "[] ∈ T" by (rule T1)
next
fix w
assume "w ∈ S" "w ∈ T"
show "[A] @ w @ [B] ∈ T" using `w ∈ T` by (rule S_en_T_aux1)
next
fix v w
assume "v ∈ S" "v ∈ T" "w ∈ S" "w ∈ T"
show "v @ w ∈ T" using `w ∈ T` `v ∈ T` by (rule S_en_T_aux2)
qed
text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar que S y T son iguales.
------------------------------------------------------------------ *}
lemma S_igual_T:
"S = T"
by (auto simp add: S_en_T T_en_S)
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.
------------------------------------------------------------------ *}
fun balanceada_aux :: "alfabeto list ⇒ nat ⇒ bool" where
"balanceada_aux [] 0 = True"
| "balanceada_aux (A#w) n = balanceada_aux w (Suc n)"
| "balanceada_aux (B#w) (Suc n) = balanceada_aux w n"
| "balanceada_aux w n = False"
fun balanceada :: "alfabeto list ⇒ bool" where
"balanceada w = balanceada_aux w 0"
value "balanceada [A,A,B,B]" -- "= True"
value "balanceada [A,B,A,B]" -- "= True"
value "balanceada [A,B,B,A]" -- "= False"
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que balanceada es un reconocedor correcto de la
gramática S; es decir,
w ∈ S ⟹ balanceada w
------------------------------------------------------------------ *}
text {*
Nota: En la demostración se usarán los siguientes lemas auxiliares:
· balanceada_correcto_aux_1:
balanceada_aux w n ⟹ balanceada_aux (w @ [B]) (Suc n)
· balanceada_correcto_aux_2:
⟦balanceada_aux v n;
balanceada_aux w 0⟧
⟹ balanceada_aux (v @ w) n
· balanceada_correcto_aux_3:
w ∈ S ⟹ balanceada_aux w 0 *}
-- "La demostración automática del primer lema auxiliar es"
lemma balanceada_correcto_aux_1:
"balanceada_aux w n ⟹ balanceada_aux (w @ [B]) (Suc n)"
by (induct w n rule: balanceada_aux.induct) simp_all
-- "La demostración estructurada del primer lema auxiliar es"
lemma balanceada_correcto_aux_1b:
assumes "balanceada_aux w n"
shows "balanceada_aux (w @ [B]) (Suc n)"
using assms
proof (induct w n rule: balanceada_aux.induct)
assume "balanceada_aux [] 0"
thus "balanceada_aux ([] @ [B]) (Suc 0)" by simp
next
fix w n
assume "balanceada_aux w (Suc n) ⟹ balanceada_aux (w @ [B]) (Suc (Suc n))"
"balanceada_aux (A # w) n"
thus "balanceada_aux ((A # w) @ [B]) (Suc n)" by simp
next
fix w n
assume "balanceada_aux w n ⟹ balanceada_aux (w @ [B]) (Suc n)"
"balanceada_aux (B # w) (Suc n)"
thus "balanceada_aux ((B # w) @ [B]) (Suc (Suc n))" by simp
next
fix v
assume "balanceada_aux (B # v) 0"
thus "balanceada_aux ((B # v) @ [B]) (Suc 0)" by simp
next
fix v
assume "balanceada_aux [] (Suc v)"
thus "balanceada_aux ([] @ [B]) (Suc (Suc v))" by simp
qed
-- "La demostración automática del segundo lema auxiliar es"
lemma balanceada_correcto_aux_2:
assumes "balanceada_aux v n"
"balanceada_aux w 0"
shows "balanceada_aux (v @ w) n"
using assms
by (induct v n rule: balanceada_aux.induct) simp_all
-- "La demostración automática del tercer lema auxiliar es"
lemma balanceada_correcto_aux_3:
"w ∈ S ⟹ balanceada_aux w 0"
by (induct rule: S.induct)
(auto simp add: balanceada_correcto_aux_1 balanceada_correcto_aux_2)
-- "La demostración estructurada del tercer lema auxiliar es"
lemma balanceada_correcto_aux_3b:
"w ∈ S ⟹ balanceada_aux w 0"
proof (induct rule: S.induct)
show "balanceada_aux [] 0" by simp
next
fix w
assume "w ∈ S"
"balanceada_aux w 0"
thus "balanceada_aux ([A] @ w @ [B]) 0"
by (simp add: balanceada_correcto_aux_1)
next
fix v w
assume "v ∈ S"
"balanceada_aux v 0"
"w ∈ S"
"balanceada_aux w 0"
thus "balanceada_aux (v @ w) 0"
by (simp add: balanceada_correcto_aux_2)
qed
-- "La demostración automática del tercer lema es"
lemma balanceada_correcto:
"w ∈ S ⟹ balanceada w"
by (simp add: balanceada_correcto_aux_3)
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que balanceada es un reconocedor completo de
la gramática S; es decir,
balanceada w ⟹ w ∈ S
------------------------------------------------------------------ *}
-- "La demostración automática del primer lema auxiliar es"
lemma balanceada_completo_aux_1:
"[A,B] ∈ S"
using S1 S2 [where w = "[]"] by simp
-- "La demostración estructurada del primer lema auxiliar es"
lemma balanceada_completo_aux_1b:
"[A,B] ∈ S"
proof -
have "[] ∈ S" using S1 by simp
hence "[A] @ [] @ [B] ∈ S" using S2 [where w = "[]"] by simp
thus "[A,B] ∈ S" by simp
qed
-- "La demostración estructurada del segundo lema auxiliar es"
lemma balanceada_completo_aux_2:
assumes "u ∈ S"
shows "⋀v w. u = v @ w ⟹ v @ A # B # w ∈ S"
using assms
proof (induct)
fix v w :: "alfabeto list"
assume "[] = v @ w"
thus "v @ A # B # w ∈ S" by (simp add: balanceada_completo_aux_1)
next
fix v u w :: "alfabeto list"
assume uS: "u ∈ S" and
HI: "⋀v w. u = v @ w ⟹ v @ A # B # w ∈ S" and
sup: "[A] @ u @ [B] = v @ w"
show "v @ A # B # w ∈ S"
proof (cases v)
case Nil
hence "w = A # u @ [B]" using sup by simp
hence "w ∈ S" using uS S2 by simp
hence "[A,B] @ w ∈ S" using balanceada_completo_aux_1 S3 by blast
thus ?thesis using Nil by simp
next
case (Cons x v')
show ?thesis
proof (cases w rule:rev_cases)
case Nil
have "A # u @ [B] ∈ S" using S2 uS by simp
hence "(A # u @ [B]) @ [A,B] ∈ S"
using balanceada_completo_aux_1 S3 by blast
thus ?thesis using Nil Cons sup by auto
next
case (snoc w' y)
hence u: "u = v' @ w'" and [simp]: "x = A ∧ y = B"
using Cons sup by auto
from u have "v' @ A # B # w' ∈ S" by (rule HI)
hence "A # (v' @ A # B # w') @ [B] ∈ S"
using S2 [where w = "v' @ A # B # w'"] by simp
thus ?thesis using Cons snoc by auto
qed
qed
next
fix v' w' v w
assume v'S: "v' ∈ S"
and HIv: "⋀v w. v' = v @ w ⟹ v @ A # B # w ∈ S"
and w'S: "w' ∈ S"
and HIw: "⋀v w. w' = v @ w ⟹ v @ A # B # w ∈ S"
and sup: "v' @ w' = v @ w"
then obtain r where "v' = v @ r ∧ r @ w' = w ∨ v' @ r = v ∧ w' = r @ w"
(is "?A ∨ ?B")
by (auto simp: append_eq_append_conv2)
thus "v @ A # B # w ∈ S"
proof
assume A: ?A
hence "v @ A # B # r ∈ S" using HIv by blast
hence "(v @ A # B # r) @ w' ∈ S" using w'S by (rule S3)
thus ?thesis using A by auto
next
assume B: ?B
hence "r @ A # B # w ∈ S" using HIw by blast
with v'S have "v' @ (r @ A # B # w) ∈ S" by (rule S3)
thus ?thesis using B by auto
qed
qed
-- "La demostración estructurada del tercer lema auxiliar es"
lemma balanceada_completo_aux_3:
"balanceada_aux w n ⟹ replicate n A @ w ∈ S"
proof (induct w n rule: balanceada_aux.induct)
assume "balanceada_aux [] 0"
thus "replicate 0 A @ [] ∈ S" using S1 by simp
next
fix w n
assume "balanceada_aux w (Suc n) ⟹ replicate (Suc n) A @ w ∈ S"
and "balanceada_aux (A # w) n"
thus "replicate n A @ A # w ∈ S"
by (simp add: replicate_app_Cons_same)
next
fix w n
assume "balanceada_aux w n ⟹ replicate n A @ w ∈ S"
and "balanceada_aux (B # w) (Suc n)"
thus "replicate (Suc n) A @ B # w ∈ S"
by (simp add: balanceada_completo_aux_2
replicate_app_Cons_same[symmetric])
next
fix v
assume "balanceada_aux (B # v) 0"
thus "replicate 0 A @ B # v ∈ S" by simp
next
fix v
assume "balanceada_aux [] (Suc v)"
thus "replicate (Suc v) A @ [] ∈ S" by simp
qed
-- "La demostración del lema es"
lemma balanceada_completo:
assumes "balanceada w"
shows " w ∈ S"
proof -
have "balanceada_aux w 0" using assms by simp
hence "replicate 0 A @ w ∈ S" by (rule balanceada_completo_aux_3)
thus "w ∈ S" by simp
qed
end
