|
|
| Línea 1: |
Línea 1: |
| | <source lang = "isar"> | | <source lang = "isar"> |
| − | 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, o 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 {* El mismo estado, expresado de forma más concisa:
| |
| − | Se puede utilizar la notación f(a:=b) para representar 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>
| |
| − |
| |
| − | Establecemos 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 subespresiones 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
| |
| | </source> | | </source> |
