Rel 8

header "Ejercicios sobre expresiones aritméticas" 

theory AExp_ejercicios

imports AExp_b

begin

text{*
Ejercicios

Ejercicio 1.1.
Para probar que la función asimp_const efectivamente simplifica todas
las subexpresiones de la forma "Plus (N i) (N j)", definir una función
optimal, tal que (optimal a) compruebe que la expresión aritmética a
no contiene ninguna subexpresión de la forma  "Plus (N i) (N j)".
Por ejemplo,
  value "optimal_b (Plus (N 2) (Plus (N 3) (N 4))) = False"

Nota: En la definición usar la expresión case.
*}

fun optimal :: "aexp ⇒ bool" where
  "optimal (N n) = True"|
  "optimal (V x) = True"|
  "optimal (Plus (N n1) (N n2)) = False"|
  "optimal (Plus b1 b2) = conj (optimal b1) (optimal b2) "
  

text{*
Ejercicio 1.2.
Probar que, para toda expresión aritmética a, la expresión
(asimp_const a) es optimal.
*}

lemma "optimal (asimp_const a)"
apply (induction a)
apply (auto split: aexp.split)
done

text{* Nota: 
Esta prueba necesita la ayuda split, lo que puede dar lugar
a que el proceso de simplificación automática de la prueba no
termine. Por tanto, definimos nuevamente la función optimal,
mediante equiparación de patrones.
*}

text{* Definir la función optimal mediante equiparación de patrones.
*}

fun optimal_b :: "aexp ⇒ bool" where
  "optimal_b (N i) = True"
  |"optimal_b (V x) = True"
  |"optimal_b (Plus a1 a2) = 
  (case (a1, a2) of 
  (N n1, N n2) ⇒ False
  |( b1, b2) ⇒ conj (optimal_b b1)(optimal_b b2) )"


(* value "optimal_b (Plus (N 2) (Plus (N 3) (N 4))) = False" *)

text{*
Ejercicio 1.4.
Probar que, para toda expresión aritmética a, la expresión
(asimp_const a) es optimal, con la nueva definición de la función
optimal.
*}

lemma "optimal_b (asimp_const a)"
oops


text{*
  Ejercicio 2. En este ejercicio simplificamos una expresión
aritmética, sumando todas las constantes, incluso si no son
consecutivas. Y probamos que la simplificación es correcta.


  Ejercicio 2.1 
Definir una función sumN que devuelva la suma de todas las 
constantes de una expresión aritmética. Por ejemplo,

value "sumN (Plus (N 1) (Plus (V x) (N 2))) == 3"

*}


fun sumN :: "aexp ⇒ int" where
  "sumN (N n) = n" |
  "sumN (V x) = 0" |
  "sumN (Plus a⇩1 a⇩2) = sumN a⇩1 + sumN a⇩2"  
 

(* value "sumN (Plus (N 1) (Plus (V x) (N 2))) == 3" *)

text{* Ejercicio 2.2
Definir una función zeroN que sustituya todas las constantes de una
expresión aritmética por ceros. Por ejemplo,

value "zeroN (Plus (N 1) (Plus (V x) (N 2))) == 
              Plus (N 0) (Plus (V x) (N 0))"
*}

fun zeroN :: "aexp ⇒ aexp" where
  "zeroN (N c) = (N 0)" |  
  "zeroN (V x) = (V x)" |
  "zeroN (Plus a⇩1 a⇩2) = Plus (zeroN a⇩1) (zeroN a⇩2)"


(* value "zeroN (Plus (N 1) (Plus (V x) (N 2))) ==  *)
(*               Plus (N 0) (Plus (V x) (N 0))" *)

text {* Ejercicio 2.3
Definir una función sepN que, dada una expresión aritmética e,
construya la expresión aritmética que resulta de añadir a la 
expresión (zeroN e) la constante (sumN e). Por ejemplo,

value "sepN (Plus (N 1) (Plus (V x) (N 2))) ==
             Plus (Plus (N 0) (Plus (V x) (N 0))) (N 3)"

*}

fun sepN :: "aexp ⇒ aexp" where
"sepN e = Plus (N (sumN e)) (zeroN e)"
 

(* value "sepN (Plus (N 1) (Plus (V x) (N 2))) == *)
(*              Plus (Plus (N 0) (Plus (V x) (N 0))) (N 3)" *)

text{* Ejercicio 2.4.
Probar que la función sepN conserva el valor de la expresión 
aritmética.
*}


lemma aval_sepN: "aval (sepN t) s = aval t s"
apply (induction t)
apply auto
done


text {* Ejercicio 2.5.
Definir una función full_asimp que utilice la función asimp
para eliminar los ceros después de aplicar la función sepN.
Por ejemplo,
value "full_asimp (Plus (N 1) (Plus (V x) (N 2))) = 
                   Plus (V x) (N 3)"

value "asimp (Plus (N 1) (Plus (V x) (N 2))) == 
              Plus (N 1) (Plus (V x) (N 2))"

*}

fun full_asimp :: "aexp ⇒ aexp" where
   "full_asimp t = asimp (sepN t)"


(* value "full_asimp (Plus (N 1) (Plus (V x) (N 2))) == *)
(*                   Plus (V x) (N 3)" *)

(* value "asimp (Plus (N 1) (Plus (V x) (N 2))) == *)
(*               Plus (N 1) (Plus (V x) (N 2))" *)

text{* Ejercicio 2.6.
Probar que la función full_asimp conserva el valor de la 
expresión aritmética.

Nota: Establecer los lemas necesarios.
*}

(* lema auxiliar *)

lemma aval_zeroN_sumN[simp]:" sumN t + aval(zeroN t)s = aval t s"
apply (induct t)
apply auto
done


lemma aval_full_asimp[simp]: "aval (full_asimp t) s = aval t s"
oops

text{* Ejercico 3. 
Una sustitución consiste en reemplazar una variable de una expresión
aritmética por otra expresión.

  Ejercicio 3.1. 
Definir una función subst tal que (subst x e1 e2) reemplace
cada ocurrencia de la variable x en la expresión e2 por la 
expresión e1. Por ejemplo,

"subst ''x'' (N 3) (Plus (V ''x'') (V ''y'')) = 
                    Plus (N 3) (V ''y'')"
*}

fun subst :: "vname ⇒ aexp ⇒ aexp ⇒ aexp" where
"subst x e (N c) = (N c)" |
"subst x e (V x') = (if x = x' then e else (V x'))" |
"subst x e (Plus a1 a2) = Plus (subst x e a1) (subst x e a2)"


(* value "subst ''x'' (N 3) (Plus (V ''x'') (V ''y'')) = *)
(*                           Plus (N 3) (V ''y'')" *)

text{* Ejercicio 3.2.
Probar el siguiente lema de sustitución: el valor de la 
expresión (subst x e1 e2) en un estado s, coincide con
el valor de la expresión e2 en el estado s, actualizado 
mediante "x := aval e1 s". Es decir, podemos sustituir
primero y evaluar después, o bien evaluar con el estado
actualizado.
*}


lemma subst_lemma: "aval (subst x a e) s = aval e (s(x := aval a s))"
apply (induction e)
apply auto
done

text {*
  Ejercicio 3.3.
Probar que las expresiones a1 y a2 tienen el mismo valor en un 
estado s, entonces el valor de sustituir por a1 es el mismo que 
el valor de sustituir por a2.
*}

lemma "aval a1 s = aval a2 s
  ⟹ aval (subst x a1 e) s = aval (subst x a2 e) s"
apply (induction e)
apply simp_all
done

text{* Ejercicio 4 (en un fichero aparte AExp2.thy)
Considerar una "copia" de la teoría AExp_b y modificarla como
sigue:
- Extender el tipo con un constructor binario Times, que 
  represente la multiplicación.
- Modificar las funciones aval y asimp, de acuerco con el 
  nuevo tipo. La función asimp debe eliminar 0 y 1 de las
  multiplicaciones y evaluar las subexpresiones constantes.
- Actualizar las pruebas de los lemas y teoremas.
*}

text{* Ejercicio 5.
El siguiente tipo añade el constructor LET a una expresión
aritmética:
*}

datatype lexp = 
  Nl int | Vl vname | Plusl lexp lexp | LET vname lexp lexp

text{* El constructor LET introduce una variable local:
el valor de "LET x e1 e2" es el valor de e2 en el estado,
en el que a la variable x se le ha asignado el valor de e1
en el estado original.
*}

text{* Ejercico 5.1.
Definir una función lval::"lexp ⇒ state ⇒ int 
que evalúe las expresiones lexp. 

Nota: recordar la forma s(x := i).

*}


fun lval::"lexp ⇒ state ⇒ int" where
  "lval (Nl n) s = n" |
  "lval (Vl x) s = s x" |
  "lval (Plusl a⇩1 a⇩2) s = (lval a⇩1 s) + (lval a⇩2 s)" |
  "lval (LET x e⇩1 e⇩2) s = lval e⇩2 (s(x := lval e⇩1 s))"


text{*
  Ejercicio 5.2.
Definir la función de conversión inline::"lexp ⇒ aexp"
tal que la expresión "LET x e⇩1 e⇩2" es la expresión aritmética
que resulta de sustituir la variable x por la conversión de e1
en la conversión de e2.
*}


fun inline:: "lexp ⇒ aexp" where
  "inline (Nl n) = (N n)" |
  "inline (Vl x) = (V x)" |
  "inline (Plusl a⇩1 a⇩2) = Plus (inline a⇩1) (inline a⇩2)" |
  "inline (LET x e⇩1 e⇩2) = subst x (inline e⇩1) (inline e⇩2)"


text{* Ejercicio 5.3
Probar que la función inline es correcta con respecto a la evaluación.
*}

lemma "aval (inline e) s = lval e s"
oops

end