header "Expresiones aritméticas"
theory AExp_b imports Main begin
subsection "Expresiones aritméticas"
text{*
En primer lugar, definimos los tipos para representar los
- nombres de variables como cadenas
- valores como enteros
*}
type_synonym vname = string
type_synonym val = int
text{* Sintaxis:
Una expresión aritmética es un número entero, una variable,
o la suma de dos expresiones aritméticas.
Una expresión aritmética se representa mediante el tipo aexp,
definido por
datatype aexp = N int | V vname | Plus aexp aexp
*}
datatype aexp = N int | V vname | Plus aexp aexp
text{* Semántica:
El valor de una expresión aritmética depende del valor que tomen
las variables. Definimos un estado como una aplicación que asigna
un valor a cada nombre de variable.
type_synonym state = "vname ⇒ val"
*}
type_synonym state = "vname ⇒ val"
text{* El valor de una expresión aritmética e en un estado s,
se define por recursión en la estructura de la expresión, como
sigue:
- el valor de un número es él mismo
- el valor de una variable es su valor en el estado
- el valor de una suma se calcula de forma recursiva
*}
fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Plus a⇩1 a⇩2) s = aval a⇩1 s + aval a⇩2 s"
value "aval (Plus (V ''x'') (N 5)) (λx. if x = ''x'' then 7 else 0)"
value "aval (Plus (V ''x'') (N 5)) (λx. 0)"
text {* Para representar un estado de forma más concisa,
se puede utilizar la notación f(a:=b) que denota la
función que toma los mismos valores que f, excepto para a,
cuyo valor es b.
Es decir,
f(a:=b) = (λx. if x = a then b else f x)
*}
value "aval (Plus (V ''x'') (N 5)) ((λx. 0) (''x'':= 7))"
text{* Por ejemplo, ((λx. 0) (''x'':= 7))(''y'':=3)
transforma ''x'' en 7, ''y'' en 3, y todos los demás nombres
de variables en 0.
Se puede usar una notación más compacta:
<''x'':= 7, ''y'' := 3>
para lo que se establece la notación siguiente:
*}
definition null_state ("<>") where
"null_state ≡ λx. 0"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
text {* Ejemplo:
*}
lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))"
by (rule refl)
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
subsection "Simplicación de constantes"
text{* La función asimp_const reemplaza cada subexpresión cuyo valor
sea una constante por dicha constante. Por ejemplo, la expresión
Plus (V ''x'') (Plus (N 3) (N 1)) por la expresión Plus (V ''x'') (N 4) *}
fun asimp_const :: "aexp ⇒ aexp" where
"asimp_const (N n) = N n" |
"asimp_const (V x) = V x" |
"asimp_const (Plus a⇩1 a⇩2) =
(case (asimp_const a⇩1, asimp_const a⇩2) of
(N n⇩1, N n⇩2) ⇒ N(n⇩1+n⇩2) |
(b⇩1,b⇩2) ⇒ Plus b⇩1 b⇩2)"
text{* La simplificación es correcta. Es decir, no cambia el valor
de la expresión aritmética.
*}
thm aexp.split
theorem aval_asimp_const:
"aval (asimp_const a) s = aval a s"
apply(induction a)
apply (auto split: aexp.split)
done
text{* La prueba se realiza por inducción en la expresión a. Si a es
un número o una variable, es trivial. Y, si a es de la forma
Plus a1 a2, se distiguen dos casos, según que a1 y a2 sean o no
expresiones numéricas.
En la prueba automática, split proporciona la ayuda para que se
realice la distinción de casos cuando una expresión case se aplica
sobre un dato aexp.
*}
text{* Realizamos una segunda simplificación, eliminando los ceros
en las sumas. Para ello, definimos la siguiente función
*}
fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i⇩1) (N i⇩2) = N(i⇩1+i⇩2)" |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
"plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"
text{* Lema: la función plus se comporta como Plus, mediante la
evaluación.
*}
text{* Demostración aplicativa: *}
lemma aval_plus[simp]:
"aval (plus a1 a2) s = aval a1 s + aval a2 s"
apply(induction a1 a2 rule: plus.induct)
apply simp_all
done
text{* Demostración automática: *}
lemma "aval (plus a1 a2) s = aval a1 s + aval a2 s"
by (induct a1 a2 rule: plus.induct) simp_all
text{* La función asimp simplifica una expresión aritmética,
eliminando los ceros de las sumas y efectuando las sumas
de las subexpresiones numéricas.
*}
fun asimp :: "aexp ⇒ aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a⇩1 a⇩2) = plus (asimp a⇩1) (asimp a⇩2)"
value "asimp (Plus (V ''x'')
(Plus (Plus (N 3) (N 1))
(Plus (V ''y'') (N 0))))"
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
text{* La función asimp es correcta: el valor de la expresión aritmética
no varía.
*}
text{* Demostración aplicativa: *}
theorem aval_asimp[simp]:
"aval (asimp a) s = aval a s"
apply(induction a)
apply simp_all
done
text{* Demostración automática: *}
theorem "aval (asimp a) s = aval a s"
by (induct a) simp_all
text{* La demostración es por inducción estructurada en la expresión a.
*}
text{* Nota: Los teoremas aval_plus y aval_asimp se incormporan
como reglas de simplificación.
*}
end