Ver el código de «Tema 11: Gramáticas libre de contexto» - Razonamiento automático (2014-15)

<source lang="isabelle">
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
</source>