Relación 8

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