Razonamiento automático (2018-19) Razonamiento automático (2018-19)

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. 
  ------------------------------------------------------------------ *}

lemma T_en_S: 
  assumes "w ∈ T"  
  shows   "w ∈ S"
oops

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Demostrar que S está contenido en T. 
  ------------------------------------------------------------------ *}

lemma S_en_T: 
  "w ∈ S ⟹ w ∈ T"
oops  

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Demostrar que S y T son iguales. 
  ------------------------------------------------------------------ *}

lemma S_igual_T:
  "S = T"
oops

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 :: "alfabeto list ⇒ bool" where
  "balanceada w = undefined"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar que balanceada es un reconocedor correcto de la
  gramática S; es decir, 
     w ∈ S ⟹ balanceada w
  ------------------------------------------------------------------ *}

lemma balanceada_correcto:
  "w ∈ S ⟹ balanceada w"
oops

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar que balanceada es un reconocedor completo de 
  la gramática S; es decir, 
     balanceada w ⟹ w ∈ S 
  ------------------------------------------------------------------ *}

lemma balanceada_completo: 
  assumes "balanceada w"
  shows   "w ∈ S"
oops

end