Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

header "Ejercicios sobre expresiones booleanas" 

theory BExp_ejercicios

imports AExp_b BExp_b

begin

text{*
Ejercicios


text{*
  Ejercicio 1.1.
Definir las siguientes funciones sobre expresiones booleanas:
- una función "or" para representar la disyunción de expresiones
  booleanas
- una función "Le" tal que "Le a1 a2" represente que la expresión 
  aritmética a1 es menor o igual que a2.
- una función "Eq" que represente que la igualdad entre expresiones
  aritméticas.
*}

fun "or"::"bexp ⇒ bexp ⇒ bexp" where
  "or b1 b2 = undefined"

fun Le :: "aexp ⇒ aexp ⇒ bexp" where
 "Le a1 a2 = undefined"

fun Eq :: "aexp ⇒ aexp ⇒ bexp" where
  "Eq a1 a2 = undefined"


text{* Ejercicio 1.2.
Probar que las funciones "or", "Le" y "Eq" son correctas.
*}

lemma or_bval: "bval (or b1 b2) s = ((bval b1 s) ∨ (bval b2 s))"
oops

lemma bval_Le: "bval (Le a1 a2) s = (aval a1 s ≤ aval a2 s)"
oops

lemma bval_Eq: "bval (Eq a1 a2) s = (aval a1 s = aval a2 s)"
oops

text{*
  Ejercicio 2.
Consideremos el siguiente tipo de expresiones booleanas, formadas por
  - constantes booleanas,
  - expresiones condicionales, o
  - comparación de expresiones aritméticas.
*}

datatype ifexp = Bc2 bool | If ifexp ifexp ifexp | Less2 aexp aexp

text {*  Ejercicio 2.1.
Definir una función que calcule el valor una expresión "ifexp" en 
un estado. Por ejemplo,

value "ifval (If (Less2 (N 3) (V ''x'')) (Bc2 true) (Bc2 false))
             <''x'':= 1> == true"

value "ifval (If (Less2 (N 3) (V ''x'')) (Bc2 true) (Bc2 false))
             <''x'':= 5> == false"
*}

fun ifval :: "ifexp ⇒ state ⇒ bool" where
  "ifval e s = undefined"


value "ifval (If (Less2 (N 3) (V ''x'')) (Bc2 true) (Bc2 false))
             <''x'':= 1>"

value "ifval (If (Less2 (N 3) (V ''x'')) (Bc2 true) (Bc2 false))
             <''x'':= 5>"

text{* Ejercicio 2.2. 
Definir dos funciones de traducción:
- una función b2ifexp que transforme una expresión booleana "bexp"
  en una expresión "ifexp"
- una función "if2exp" que realice la transformación inversa.

Por ejemplo:
 
value "b2ifexp (Less (N 2) (V '' x'')) = Less2 (N 2) (V '' x'')"

value "b2ifexp (And (Less (N 2) (V '' x''))
                    (Not (Bc true))) =
       ifexp.If (Less2 (N 2) (V '' x''))
                (ifexp.If (ifexp.If (Bc2 true) 
                                    (Bc2 False) 
                                    (Bc2 True)) 
                           (Bc2 True) 
                           (Bc2 False)) 
                 (Bc2 False)"

value "if2bexp (If (Less2 (N 3) (V ''x'')) 
                   (Bc2 true) 
                   (Bc2 false)) =
       And (not (and (bexp.Not (bexp.Not (Less (N 3) (V ''x'')))) 
                     (not (Bc true))))
           (not (and (bexp.Not (Less (N 3) (V ''x''))) 
                     (not (Bc false))))"

value "if2bexp (Bc2 true) == Bc true"

 *}

fun b2ifexp :: "bexp ⇒ ifexp" where
  "b2ifexp e = undefined"

value "b2ifexp (Less (N 2) (V '' x''))"
value "b2ifexp (And (Less (N 2) (V '' x''))
                    (Not (Bc true)))"

value "b2ifexp (Bc true) == Bc2 true"

fun if2bexp :: "ifexp ⇒ bexp" where
  "if2bexp e = undefined"

value "if2bexp (If (Less2 (N 3) (V ''x'')) (Bc2 true) (Bc2 false))"
value "if2bexp (Bc2 true) == Bc true"

text{* Ejercicio 2.3. 
Probar que ambas funciones son correctas. Es decir, que el valor
de una expresión en un estado no varía mediante la transformación. 
*}

lemma "bval (if2bexp e) s = ifval e s"
oops

lemma "ifval (b2ifexp e) s = bval e s"
oops


text{*
  Ejercicio 3.
Definimos el siguiente tipo de expresiones booleanas: una expresión
booleana pura es:
   - una variable
   - la negación de una expresión booleana pura, 
   - la conjunción de expresiones booleanas puras, o
   - la disyunción de expresiones booleanas puras.

donde el valor de las variables es un valor booleano.
*}

datatype pbexp =
  VAR vname | NOT pbexp | AND pbexp pbexp | OR pbexp pbexp

text{* Ejercico 3.1.
Definir una función "pbexp" que calcule el valor de una expresión
booleana pura en un estado. Por ejemplo,

value "pbval (AND (VAR ''x'') (NOT (VAR ''y''))) 
             (λx. true) = 
       true ∧ ¬ true" 
*}

fun pbval :: "pbexp ⇒ (vname ⇒ bool) ⇒ bool" where
"pbval e s = undefined" 

value "pbval (AND (VAR ''x'') (NOT (VAR ''y''))) 
             (λx. true)"

text {* Ejercicio 3.2.
Definir una función "is_nnf" que compruebe si una expresión booleana
pura está en forma normal negativa, es decir, el constructor NOT sólo
se aplica directamente a las variables. Por ejemplo,

value "is_nnf (VAR ''x'') == True"
value "is_nnf (NOT (VAR ''x'')) == True"
value "is_nnf (NOT (AND (VAR ''x'') (VAR ''y''))) == False"
*}

fun is_nnf :: "pbexp ⇒ bool" where
  "is_nnf e = undefined"

value "is_nnf (VAR ''x'')"
value "is_nnf (NOT (VAR ''x''))"
value "is_nnf (NOT (AND (VAR ''x'') (VAR ''y'')))"


text{* Ejercicio 3.3.
Definir una función "nnf" transforme una expresión booleana pura
en su forma normal negativa, introduciendo la nagación tanto como
sea posible. Por ejemplo,

value " nnf (AND (VAR ''x'') (NOT (VAR ''y''))) = 
             AND (VAR ''x'') (NOT (VAR ''y''))"

value " nnf (NOT (AND (VAR ''x'') (VAR ''y''))) = 
            OR (NOT (VAR ''x'')) (NOT (VAR ''y''))"
*}

fun nnf :: "pbexp ⇒ pbexp" where
  "nnf e = undefined"

value " nnf (AND (VAR ''x'') (NOT (VAR ''y'')))"
value " nnf (NOT (AND (VAR ''x'') (VAR ''y'')))"

text{* Ejercicio 3.3.
Probar que la función "nnf" es correcta. Es decir, "nnf e"
calcula una forma normal negativa de la expresión "e".
*}


lemma pbval_nnf: "pbval (nnf b) s = pbval b s"
oops

lemma is_nnf_nnf: "is_nnf (nnf b)"
oops

text{* Ejericio 4.
Una expresión booleana está en forma normal disyuntiva (DNF)
si está en forma normal negativa y ningún constructor "OR" 
ocurre dentro de un constructor "AND". Por ejemplo,

- (AND (OR (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x''))) no está en DNF

- (OR (AND (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x''))) está en DNF

- (AND (NOT (OR (VAR ''x'') (VAR ''y''))) (VAR ''x'')) no está en DNF
*}

text{* Ejercico 4.1.
Definir una función "is_dnf" que compruebe si una expresión booleana
pura está en forma normal disyuntiva. Por ejemplo,

value "is_dnf (AND (OR (VAR ''x'') (VAR ''y''))
                   (NOT (VAR ''x''))) == False"

value "is_dnf (OR (AND (VAR ''x'') (VAR ''y''))
                   (NOT (VAR ''x''))) == True"

value "is_dnf (AND (NOT (OR (VAR ''x'') (VAR ''y'')))
                   (VAR ''x'')) == False"
*}

fun is_dnf :: "pbexp ⇒ bool" where
  "is_dnf e = undefined"

value "is_dnf (AND (OR (VAR ''x'') (VAR ''y''))
                   (NOT (VAR ''x''))) == False"

value "is_dnf (OR (AND (VAR ''x'') (VAR ''y''))
                   (NOT (VAR ''x''))) == True"

value "is_dnf (AND (NOT (OR (VAR ''x'') (VAR ''y'')))
                   (VAR ''x'')) == False"


text {* 
Una expresión en forma normal negativa (NNF) se puede transformar en 
una expresión en forma normal disyuntiva, aplicando distribitividad
en cada expresión de la forma "AND (OR a1 a2) (b1 b2)".

Ejercico 4.2.
Definir una función "dist_AND" que aplique la propiedad
distributiva a las componentes de una expresión conjuntiva.
Por ejemplo,

value "dist_AND (OR (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x'')) =
      "OR (AND (VAR ''x'') (NOT (VAR ''x''))) 
         (AND (VAR ''y'') (NOT (VAR ''x'')))

value "dist_AND (VAR ''x'') (OR (VAR ''y'') (NOT (VAR ''x''))) =
      OR (AND (VAR ''x'') (VAR ''y'')) 
         (AND (VAR ''x'') (NOT (VAR ''x'')))"

value "dist_AND (AND (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x'')) =
      AND (AND (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x''))"
*}


fun dist_AND :: "pbexp ⇒ pbexp ⇒ pbexp" where
  "dist_AND e1 e2 = undefined"

value "dist_AND (OR (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x''))"
value "dist_AND (VAR ''x'') (OR (VAR ''y'') (NOT (VAR ''x'')))"
value "dist_AND (AND (VAR ''x'') (VAR ''y'')) (NOT (VAR ''x''))"


text {* Ejercicio 4.3 
Probar que se verifican las siguientes propiedades.
*}

lemma pbval_dist1: 
  "pbval (AND b1 (OR b2 b3)) s 
  = pbval (OR (AND b1 b2) (AND b1 b3)) s"
oops

lemma pbval_dist2: 
  "pbval (AND (OR b1 b2) b3) s 
  = pbval (OR (AND b1 b3) (AND b2 b3)) s"
oops

lemma pbval_dist: "pbval (dist_AND b1 b2) s = pbval (AND b1 b2) s" 
oops

lemma is_dnf_nnf: "is_dnf b ⟹ is_nnf b" 
oops

lemma is_dnf_or: "is_dnf b1 ⟹ is_dnf b2 ⟹ is_dnf (OR b1 b2)"
oops

lemma is_dnf_or2: "is_nnf (OR e1 e2) ⟹ is_nnf e1 ∧ is_nnf e2"
oops

lemma is_dnf_and: "is_nnf (AND e1 e2) ⟹ is_nnf e1 ∧ is_nnf e2"
oops

lemma dist_AND_nnf: 
  "is_nnf b1 ⟹ is_nnf b2 ⟹ is_nnf (dist_AND b1 b2)" 
oops


text {* Ejercicio 4.4.
Usando la función "dist_AND", definir una función "dnf_of_nnf" que
transforme una expresión en forma normal negativa en una expresión
equivalente, en forma normal disyuntiva. Por ejemplo,

value "dnf_of_nnf (AND (VAR ''x'') (VAR ''y'')) =
      AND (VAR ''x'') (VAR ''y'')"

value "dnf_of_nnf (AND (NOT (VAR ''x'')) (OR (VAR ''y'') (VAR ''x''))) =
      OR (AND (NOT (VAR ''x'')) (VAR ''y'')) 
         (AND (NOT (VAR ''x'')) (VAR ''x''))"

*}

fun dnf_of_nnf :: "pbexp ⇒ pbexp" where
  "dnf_of_nnf e = undefined"

value "dnf_of_nnf (AND (VAR ''x'') (VAR ''y''))"
value "dnf_of_nnf (AND (NOT (VAR ''x'')) (OR (VAR ''y'') (VAR ''x'')))"

text {* Ejercicio 4.5.
Probar que dicha función es correcta.

*}

lemma "pbval (dnf_of_nnf b) s = pbval b s"
oops

lemma "is_nnf b ⟹ is_dnf (dnf_of_nnf b)"
oops

end