Rel 9

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 (Bc True) b = Bc True"|
  "or b (Bc True) = Bc True"|
  "or (Bc False) b = b"|
  "or b (Bc False) = b"|
  "or b1 b2 = Not(And (Not(And (Not b1) b2))(Not(And b1 (Not b2))))"
  
text{* Comentario:
La definición no es correcta. Basta definirla como sigue:
" or b1 b2 = not (and (not b1) (not b2))"
*}

fun Le :: "aexp ⇒ aexp ⇒ bexp" where
 "Le a1 a2 = Not (Less a2 a1)"

fun Eq :: "aexp ⇒ aexp ⇒ bexp" where
  "Eq a1 a2 = And (Not (Less a1 a2)) (Not ((Less a2 a1)))"



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[simp]: "bval (Le a1 a2) s = (aval a1 s ≤ aval a2 s)"
apply (induct a1 a2 rule: Le.induct)
apply auto
done

lemma bval_Eq[simp]: "bval (Eq a1 a2) s = (aval a1 s = aval a2 s)"
apply (induct a1 a2 rule: Eq.induct)
apply auto
done

text{* Comentario:
No es necesario hacer la demostración por inducción.
*}

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 (Bc2 b) s = b" |
"ifval (If t a⇩1 a⇩2) s = (if (ifval t s) then (ifval a⇩1 s) else (ifval a⇩2 s))" |
"ifval (Less2 a⇩1 a⇩2) s = (aval a⇩1 s < aval a⇩2 s)"


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 (Bc b) = (Bc2 b)" |
  "b2ifexp (Not b) = (If (b2ifexp b) (Bc2 False) (Bc2 True))" |
  "b2ifexp (And a1 a2) = (If (b2ifexp a1) (b2ifexp a2) (Bc2 False))" |
  "b2ifexp (Less a1 a2) = (Less2 a1 a2)"


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 (Bc2 b) = (Bc b)" |
"if2bexp (If c a1 a2) = (Not (And (Not(And (if2bexp c) (if2bexp a1)))
                                  (Not(And (Not (if2bexp c)) (if2bexp a2)))))" |
"if2bexp (Less2 a1 a2) = (Less a1 a2)"
  
text{* Comentario:
La segunda ecuación de la definición no es correcta.
*}

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"
apply (induct e)
apply auto
done

lemma "ifval (b2ifexp e) s = bval e s"
apply (induct e)
apply auto
done


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 (VAR x) s = s x"|
"pbval (NOT b) s = (¬ pbval b s)"|
"pbval (AND a1 a2) s = conj (pbval a1 s)(pbval a2 s)"|
"pbval (OR a1 a2) s = disj (pbval a1 s)(pbval a2 s) "


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 (VAR x) = True" |
"is_nnf (NOT (VAR x)) = True" |
"is_nnf (NOT e) = False" |
"is_nnf (AND a1 a2) = conj(is_nnf a1)(is_nnf a2)" |
"is_nnf (OR a1 a2) = conj(is_nnf a1)(is_nnf a2)"


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 (VAR x) = (VAR x)" |
"nnf (NOT (VAR x)) = (NOT (VAR x))" |
"nnf (NOT (NOT e)) = nnf e" |
"nnf (AND a1 a2) = AND (nnf a1) (nnf a2)" |
"nnf (NOT (AND a1 a2)) = OR (nnf (NOT a1)) (nnf (NOT a2))" |
"nnf (OR a1 a2) = OR (nnf a1) (nnf a2)" |
"nnf (NOT (OR a1 a2)) = AND (nnf (NOT a1)) (nnf (NOT a2))"



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[simp]: "pbval (nnf b) s = pbval b s"
apply (induct b rule: nnf.induct)
apply simp_all
done

lemma is_nnf_nnf: "is_nnf (nnf b)"
apply (induct b rule: nnf.induct)
apply simp_all
done

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