theory Big_Step_b imports Com_b begin
subsection "Semántica de paso largo."
text{*
En esta sección definimos una semántica operacional para dar
significado a las instrucciones del lenguaje IMP. La idea es
que la semántica describa el proceso de ejecución de un programa.
La semántica de paso largo establece una relación entre el programa,
el estado inicial y el estado final. Los estados intermedios no se
tienen en cuenta en dicha relación. Aunque a través de las reglas
inductivas que van a definir la semántica se puede ver cómo es la
ejecución del programa, la relación propiamente dicha sólo muestra
como si el programa se ejecutara en un único paso (paso largo).
*}
text {*
Formalizamos la semántica mediante un predicado ternario big_step,
tal que (big_step c s t) significa que la ejecución de la instrucción
c, empezando em el estado s, termina en el estado t.
Usaremos la notación (c,s) ⇒ t, en vez de (big_step c s t).
*}
inductive
big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP,s) ⇒ s"
| Assign: "(x ::= a,s) ⇒ s(x := aval a s)"
| Seq: "⟦ (c⇩1,s⇩1) ⇒ s⇩2; (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3"
| IfTrue: "⟦ bval b s; (c⇩1,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t"
| IfFalse: "⟦ ¬bval b s; (c⇩2,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t"
| WhileFalse: "¬bval b s ⟹ (WHILE b DO c,s) ⇒ s"
| WhileTrue: "⟦ bval b s⇩1; (c,s⇩1) ⇒ s⇩2; (WHILE b DO c, s⇩2) ⇒ s⇩3 ⟧
⟹ (WHILE b DO c, s⇩1) ⇒ s⇩3"
text{*
Descripción de la semántica de cada instrucción:
- Si la instrucción es SKIP, el estado inicial y el final
han de ser el mismo.
- Si la instrucción es x::= a y el estado inicial es s, entonces
el estado final es el estado s, en el que el valor de la variable
x es el valor de a en s.
- Si la instrucción es c1;;c2 y el estado inicial es s1, entonces
el estado final es s3 si existe un estado intermedio s2 tal que
c1 termina en s2 empezando en s1, y c2 termina en s3 empezando
en s2.
- La instrucción condicional (if b c1 c2) tiene dos reglas, dependiendo
del valor de b en el estado inicial s:
- Si es True, entonces el estado final es el estado final de ejecutar
c1 empezando en s.
- Si es False, entonces el estado final es el estado final de ejecutar
c2 empezando en s.
- La instrucción (While b c) tiene dos reglas, dependiendo del valor de b
en el estado inicial s:
- Si es False, entonces el estado final es s.
- Si es True en un estado inicial s1, entonces el estado final será un
estado s3 si existe un estado intermedio s2 tal que:
- la instrucción c termina en s2 empezando en s1, y
- el bucle (While b c) termina en s3, empezando en s2.
*}
text{*
Ejemplo:
Consideremos el programa P = ''x''::= N 5 ;; ''y::= V ''x''.
Si ejecutamos P en un estado inicial s, el estado final será
el mismo estado s, en el que x e y valen 5.
Veamos cómo usar Isabelle para seguir la ejecución del programa.
*}
schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) ⇒ ?t"
apply(rule Seq)
apply(rule Assign)
apply simp
apply(rule Assign)
done
text{*
Una vez finalizada la prueba, Isabelle instancia el lema y, después
de simplificarlo, se obtiene
(''x'' ::= N 5;; ''y'' ::= V ''x'', ?s) ⇒ ?s(''x'' := 5, ''y'' := 5)
*}
thm ex[simplified]
text{*
Otra forma mejor de ejecutar simbólicamente los programas IMP
usando el generador de código de Isabelle code_pred, y usando
el comando values, análogo a value pero que se puede aplicar
a definiciones inductivas.
*}
code_pred big_step .
values "{t. (SKIP, λ_. 0) ⇒ t}"
text{* El código generado se puede ver mediante:
*}
thm big_step.equation
text{*
En los siguientes ejemplos, calculamos el valor de una
lista de variables en el estado final de la ejecución
de un programa.
*}
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) ⇒ t}"
values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) ⇒ t}"
values "{map t [''x'',''y''] |t.
(WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)),
<''x'' := 0, ''y'' := 13>) ⇒ t}"
text{* Automatización de las demostraciones: *}
text {*
Declaramos las reglas big_step.intros como reglas de introducción,
con objeto de automatizar la ejecución de programas pequeños.
*}
thm big_step.intros
declare big_step.intros [intro]
text{*
Nota: como la definición de big_step es inductiva, las
demostraciones suelen hacerse por inducción en la estructura
de la definición. Es decir, mediante el siguiente esquema de
inducción:
*}
thm big_step.induct
text{*
?x1.0 ⇒ ?x2.0 ⟹
(⋀s. ?P (SKIP, s) s) ⟹
(⋀x a s. ?P (x ::= a, s) (s(x := aval a s))) ⟹
(⋀c⇩1 s⇩1 s⇩2 c⇩2 s⇩3.
(c⇩1, s⇩1) ⇒ s⇩2 ⟹
?P (c⇩1, s⇩1) s⇩2 ⟹
(c⇩2, s⇩2) ⇒ s⇩3 ⟹ ?P (c⇩2, s⇩2) s⇩3 ⟹ ?P (c⇩1;; c⇩2, s⇩1) s⇩3) ⟹
(⋀b s c⇩1 t c⇩2.
bval b s ⟹ (c⇩1, s) ⇒ t ⟹ ?P (c⇩1, s) t ⟹ ?P (IF b THEN c⇩1 ELSE c⇩2, s) t) ⟹
(⋀b s c⇩2 t c⇩1.
¬ bval b s ⟹ (c⇩2, s) ⇒ t ⟹ ?P (c⇩2, s) t ⟹ ?P (IF b THEN c⇩1 ELSE c⇩2, s) t) ⟹
(⋀b s c. ¬ bval b s ⟹ ?P (WHILE b DO c, s) s) ⟹
(⋀b s⇩1 c s⇩2 s⇩3.
bval b s⇩1 ⟹
(c, s⇩1) ⇒ s⇩2 ⟹
?P (c, s⇩1) s⇩2 ⟹
(WHILE b DO c, s⇩2) ⇒ s⇩3 ⟹ ?P (WHILE b DO c, s⇩2) s⇩3 ⟹ ?P (WHILE b DO c, s⇩1) s⇩3)
⟹
?P ?x1.0 ?x2.0
*}
text{*
Onservación: el esquema de inducción tiene dos variables
(?x1.0 para representar la instrucción y ?x2.0 para el estado
inicial), en vez de los tres que aparecerán en las pruebas:
s, c y t. Con objeto de modificar la forma del esquema de
inducción, introducimos el siguiente lema:
*}
lemmas big_step_induct = big_step.induct[split_format(complete)]
text{*
Y observamos la nueva forma del esquema de inducción, ahora con
las tres variables, que representan la instrucción, el estado
inicialy el estado final.
*}
thm big_step_induct
text {*
Esquema de inducción:
(?x1a, ?x1b) ⇒ ?x2a ⟹
(⋀s. ?P SKIP s s) ⟹
(⋀x a s. ?P (x ::= a) s (s(x := aval a s))) ⟹
(⋀c⇩1 s⇩1 s⇩2 c⇩2 s⇩3.
(c⇩1, s⇩1) ⇒ s⇩2 ⟹
?P c⇩1 s⇩1 s⇩2 ⟹ (c⇩2, s⇩2) ⇒ s⇩3 ⟹ ?P c⇩2 s⇩2 s⇩3 ⟹ ?P (c⇩1;; c⇩2) s⇩1 s⇩3) ⟹
(⋀b s c⇩1 t c⇩2.
bval b s ⟹ (c⇩1, s) ⇒ t ⟹ ?P c⇩1 s t ⟹ ?P (IF b THEN c⇩1 ELSE c⇩2) s t) ⟹
(⋀b s c⇩2 t c⇩1.
¬ bval b s ⟹ (c⇩2, s) ⇒ t ⟹ ?P c⇩2 s t ⟹ ?P (IF b THEN c⇩1 ELSE c⇩2) s t) ⟹
(⋀b s c. ¬ bval b s ⟹ ?P (WHILE b DO c) s s) ⟹
(⋀b s⇩1 c s⇩2 s⇩3.
bval b s⇩1 ⟹
(c, s⇩1) ⇒ s⇩2 ⟹
?P c s⇩1 s⇩2 ⟹
(WHILE b DO c, s⇩2) ⇒ s⇩3 ⟹ ?P (WHILE b DO c) s⇩2 s⇩3 ⟹
?P (WHILE b DO c) s⇩1 s⇩3)
⟹
?P ?x1a ?x1b ?x2a
*}
subsection "Regla de inversión"
text{*
Las reglas de inversión asociadas a la definición inductiva
del predicado big_step determinan qué es lo que se puede inferir
a partir de (c,s) ⇒ t. Por ejemplo, si tenemos (SKIP,s) ⇒ t?,
está claro que podemos inferir que t = s.
Para cada una de las reglas, tenemos lo siguiente:
(SKIP, s) ⇒ t ⟹ t = s
(x::=a, s) ⇒ t ⟹ t = s(x:= aval a s)
(c1;;c2, s) ⇒ t ⟹ ∃ s'. (c1,s) ⇒ s' ∧ (c2,s')⇒ t
(IF b THEN c1 ELSE c2, s) ⇒ t ⟹
(bval b s ∧ (c1,s) ⇒ t) ∨ (¬ bval b s ∧ (c2,s) ⇒ t)
(WHILE b DO c, s) ⇒ t ⟹
(¬bval b s ∧ t = s) ∨
(∃s'. (c,s) ⇒ s' ∧ (WHILE b DO c, s') ⇒ t)
*}
text{*
Podemos decirle a Isabelle que genere de forma automática
reglas de inversión para cada conclusión, usando el comando
inductive_cases.
Además, todas ellas se pueden usar en el demostrador como
reglas de eliminación, de forma segura. Por ello, las
etiquetamos con el atributo elim!, con objeto de que
se puedan usar de forma automática mediante auto y blast.
Y que se apliquen de forma impaciente.
*}
inductive_cases SkipE[elim!]: "(SKIP,s) ⇒ t"
thm SkipE
inductive_cases AssignE[elim!]: "(x ::= a,s) ⇒ t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) ⇒ s3"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) ⇒ t"
thm IfE
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"
thm WhileE
text{*
Observación: en este caso sólo lo etiquetamos con el
atributo elim, pues elim! podría no terminar.
*}
text{* Ejemplo de prueba automática, usando las
reglas de eliminación.
*}
lemma "(IF b THEN SKIP ELSE SKIP, s) ⇒ t ⟹ t = s"
by blast
text{* La misma prueba "a mano", mediante la distinción
de casos.
*}
thm IfTrue
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) ⇒ t"
shows "t = s"
proof-
from assms show ?thesis
proof cases
case IfTrue
thus ?thesis by (blast intro: IfTrue)
next
case IfFalse thus ?thesis by blast
qed
qed
text{*
Ejemplos: uso de reglas de inversión para probar reglas de
simplificación. Con ello, cada una de las reglas de inversión
previas son equivalencias.
*}
lemma assign_simp:
"(x ::= a,s) ⇒ s' ⟷ (s' = s(x := aval a s))"
by auto
lemma
"(IF b THEN c1 ELSE c2, s) ⇒ t ⟷
(bval b s ∧ (c1,s) ⇒ t) ∨ (¬ bval b s ∧ (c2,s) ⇒ t)"
by auto
text {*
En la prueba siguiente se combina el uso de regla de inversión
y derivación.
*}
lemma Seq_assoc:
"(c1;; c2;; c3, s) ⇒ s' ⟷ (c1;; (c2;; c3), s) ⇒ s'"
proof
assume "(c1;; c2;; c3, s) ⇒ s'"
then obtain s1 s2 where
c1: "(c1, s) ⇒ s1" and
c2: "(c2, s1) ⇒ s2" and
c3: "(c3, s2) ⇒ s'" by auto
from c2 c3
have "(c2;; c3, s1) ⇒ s'" by (rule Seq)
with c1
show "(c1;; (c2;; c3), s) ⇒ s'" by (rule Seq)
next
-- "Análogamente, la otra implicación"
assume "(c1;; (c2;; c3), s) ⇒ s'"
thus "(c1;; c2;; c3, s) ⇒ s'" by auto
qed
subsection "Equivalencia de instrucciones"
text {*
Decimos que dos instrucciones c y c' son equivalentes con
respecto a la semántica de paso largo si para cualesquiera
estados s y t se verifica lo siguiente:
c empezando en s termina en t syss c' empezando en s termina en t
La definición formal en Isabelle es:
*}
abbreviation
equiv_c :: "com ⇒ com ⇒ bool" (infix "∼" 50) where
"c ∼ c' ≡ (∀s t. (c,s) ⇒ t = (c',s) ⇒ t)"
text {*
Ejemplo: desplegado de la instrucción WHILE
*}
text{* Prueba detallada *}
lemma unfold_while:
"(WHILE b DO c) ∼ (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w ∼ ?iw")
proof -
-- "para probar la equivalencia, desarrollamos el árbol de "
-- "computación de un lado y, a partir de él, construimos"
-- "el árbol de computación del otro"
{ fix s t assume "(?w, s) ⇒ t"
-- "en primer lugar, hay que tener en cuenta que si b es falso"
-- "en el estado s, ambas instrucciones no hacen nada"
{ assume "¬bval b s"
hence "t = s" using `(?w,s) ⇒ t` by blast
hence "(?iw, s) ⇒ t" using `¬bval b s` by blast
}
moreover
-- "por otra parte, si b es cierto en el estado s, entonces"
-- "sólo se puede usar la regla WhileTrue para computar"
-- "(?w, s) ⇒ t"
{ assume "bval b s"
with `(?w, s) ⇒ t` obtain s' where
"(c, s) ⇒ s'" and "(?w, s') ⇒ t" by auto
-- "ahora podemos construir el árbol de computación para"
-- "la rama verdadera de IF"
hence "(c;; ?w, s) ⇒ t" by (rule Seq)
-- "por tanto"
with `bval b s` have "(?iw, s) ⇒ t" by (rule IfTrue)
}
ultimately
-- "finalmente, con ambos casos"
have "(?iw, s) ⇒ t" by blast
}
moreover
-- "ahora, en la otra dirección"
{ fix s t assume "(?iw, s) ⇒ t"
-- "de nuevo, si b es falso en el estado s, se ejecuta"
-- "la rama falsa de IF; ambas instrucciones no hacen nada:"
{ assume "¬bval b s"
hence "s = t" using `(?iw, s) ⇒ t` by blast
hence "(?w, s) ⇒ t" using `¬bval b s` by blast
}
moreover
-- "por otra parte, si b es cierta en el estado s, entonces"
-- "sólo se puede aplicar IfTrue"
{ assume "bval b s"
with `(?iw, s) ⇒ t` have "(c;; ?w, s) ⇒ t" by auto
-- "y por tanto, sólo se aplica la regla Seq"
then obtain s' where
"(c, s) ⇒ s'" and "(?w, s') ⇒ t" by auto
-- "con esta información, podemos construir un árbol"
-- "de computación para WHILE"
with `bval b s`
have "(?w, s) ⇒ t" by (rule WhileTrue)
}
ultimately
-- "por último, de ambos casos:"
have "(?w, s) ⇒ t" by blast
}
ultimately
show ?thesis by blast
qed
text {* Prueba automática. *}
lemma while_unfold:
"(WHILE b DO c) ∼ (IF b THEN c;; WHILE b DO c ELSE SKIP)"
by blast
text {* Propiedades *}
lemma triv_if:
"(IF b THEN c ELSE c) ∼ c"
by blast
lemma commute_if:
"(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)
∼
(IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
by blast
lemma sim_while_cong_aux:
"(WHILE b DO c,s) ⇒ t ⟹ c ∼ c' ⟹ (WHILE b DO c',s) ⇒ t"
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct)
apply blast
apply blast
done
lemma sim_while_cong: "c ∼ c' ⟹ WHILE b DO c ∼ WHILE b DO c'"
by (metis sim_while_cong_aux) (* uso de Sledgehammer *)
text {*
La equivalencia de instrucciones es una relación de equivalencia:
reflexiva, simétrica y transitiva.
Isabelle realiza las pruebas de forma automática.
*}
lemma sim_refl: "c ∼ c" by simp
lemma sim_sym: "(c ∼ c') = (c' ∼ c)" by auto
lemma sim_trans: "c ∼ c' ⟹ c' ∼ c'' ⟹ c ∼ c''" by auto
subsection "IMP es determinista."
text{*
Un lenguaje es determinista si dos ejecuciones de las mismas
instrucciones sobre el mismo estado inicial siempre produce
el mismo estado final.
*}
text {* Prueba automática, por inducción en la estructura de
big_step, con t' arbitrario. *}
theorem big_step_determ: "⟦ (c,s) ⇒ t; (c,s) ⇒ t' ⟧ ⟹ t' = t"
apply (induction arbitrary: t' rule: big_step.induct)
apply blast+
done
(* by (induction arbitrary: t' rule: big_step.induct) blast+ *)
text {*
En la siguiente demostración, sólo detallamos los casos
significativos, dejando los demás de forma automática.
*}
theorem
"(c,s) ⇒ t ⟹ (c,s) ⇒ t' ⟹ t' = t"
proof (induction arbitrary: t' rule: big_step.induct)
-- "el único caso interesante es WhileTrue:"
fix b c s s⇩1 t t'
-- "las hipótesis de la regla:"
assume "bval b s" and "(c,s) ⇒ s⇩1" and "(WHILE b DO c,s⇩1) ⇒ t"
-- {* H.I.: nótese ⋀ por el uso de arbitrary: *}
assume IHc: "⋀t'. (c,s) ⇒ t' ⟹ t' = s⇩1"
assume IHw: "⋀t'. (WHILE b DO c,s⇩1) ⇒ t' ⟹ t' = t"
-- "premisa de la implicación:"
assume "(WHILE b DO c,s) ⇒ t'"
with `bval b s` obtain s⇩1' where
c: "(c,s) ⇒ s⇩1'" and
w: "(WHILE b DO c,s⇩1') ⇒ t'"
by auto
from c IHc have "s⇩1' = s⇩1" by blast
with w IHw show "t' = t" by blast
qed blast+ -- "el resto se prueba de forma automática"
end