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 a = undefined"
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)"
oops
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 e = undefined"
(* 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 = undefined"
(* 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 e = undefined"
(* 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 = undefined"
(* 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"
oops
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 = undefined"
(* 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.
*}
lemma aval_full_asimp: "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 = undefined"
(* 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))"
oops
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"
oops
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 e = undefined"
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 e = undefined"
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
