theory Big_Step_ejercicios
imports Big_Step_b
begin
text{* Ejercicios
*}
text{* Ejercicio 1.1
Definir una función
fun assigned :: "com ⇒ vname set"
que obtenga el conjunto de las variables asignadas en un programa c.
*}
fun assigned :: "com ⇒ vname set" where
"assigned (SKIP) = {}"|
"assigned (Assign v a) = {v}"|
"assigned (Seq c1 c2) = (assigned c1)∪(assigned c2)"|
"assigned (If a c1 c2) = (assigned c1)∪(assigned c2)"|
"assigned (While b c) = (assigned c)"
text{* Ejercicio 1.2.
Probar que si una variable no está asignada en un programa c,
dicha variable nunca se modifica mediante c
*}
lemma "⟦ (c, s) ⇒ t; x ∉ assigned c ⟧ ⟹ s x = t x"
oops
text {* Ejercicio 2.
Definir una función recursiva
fun skip :: "com ⇒ bool"
que compruebe que el programa c realiza lo mismo que la
instrucción SKIP.
*}
fun skip :: "com ⇒ bool" where
"skip (SKIP) = True"|
"skip (Assign v a) = False"|
"skip (Seq c1 c2) = conj(skip c1)(skip c2)"|
"skip (If a c1 c2) = conj(skip c1)(skip c2)"|
"skip (While b c) = skip c"
text{* Ejercicio 2.2.
Probar que la función skip es correcta, estableciendo lemas
auxiliares si es necesario.
*}
lemma "skip c ⟹ c ∼ SKIP"
oops
text{* Ejercicio 3.1.
Definir una función
fun deskip :: "com ⇒ com"
que elimine de un programa c todas las instruciones SKIP posibles.
Por ejemplo,
value "deskip (SKIP;; WHILE b DO (x::=a;; SKIP)) = WHILE b DO x::=a"
*}
fun deskip :: "com ⇒ com" where
"deskip (Seq c1 c2) =
(if c1=SKIP then deskip c2 else if c2=SKIP then deskip c1 else Seq c1 c2)" |
"deskip (If b c1 c2) =
(if conj(c1=SKIP)(c2=SKIP) then SKIP else If b (deskip c1)(deskip c2))" |
"deskip (While b c) = (While b (deskip c))" |
"deskip c = c"
text{* Ejercicio 3.2.
Probar que la función deskip es correcta. Es decir, que
c ∼ (deskip c).
Nota: Establecer los lemas necesarios y usar el teorema
sim_while_cong para el caso WHILE.
*}
text{* Esquema de la prueba, detallando los casos de interés:
*}
lemma deskipD:"c ∼ (deskip c)"
oops
lemma "deskip c ∼ c"
oops
text{* Ejercicio 4.
Demostrar o refutar mediante un contraejemplo las propiedades
siguientes:
*}
lemma "IF And b1 b2 THEN c1 ELSE c2 ∼
IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2" (is "?w ∼ ?iw")
oops
lemma "(c,s) ⇒ s ⟹ (WHILE b DO c, s) ⇒ s"
oops
lemma "(WHILE And b1 b2 DO c,s) ⇒ t ⟹
(WHILE b1 DO WHILE b2 DO c,s) ⇒t"
oops
lemma "WHILE And b1 b2 DO c ∼ WHILE b1 DO WHILE b2 DO c" (is "?w ∼ ?iw")
oops
text{* Ejercicio 5.
Definimos una nueva instrucción Or como sigue:
*}
definition Or :: "bexp ⇒ bexp ⇒ bexp" where
"Or b⇩1 b⇩2 = Not (And (Not b⇩1) (Not b⇩2))"
text{* Probar los siguientes lemas:
*}
lemma While_end: "(WHILE b DO c, s) ⇒ t ⟹ ¬bval b t"
oops
lemma "WHILE Or b1 b2 DO c ∼
WHILE Or b1 b2 DO c;; WHILE b1 DO c"
oops
text{* Ejercicio 6.
Definir una nueva instrucción (DO c WHILE b) tal que la
instrucción c se ejecuta una vez antes de comprobar si la
expresión b es cierta en un estado
*}
fun Do :: "com ⇒ bexp ⇒ com" ("DO _ WHILE _" [0, 61] 61) where
"Do c b = undefined"
text{* Ejercicio 7.1.
Definir una función
fun dewhile :: "com ⇒ com"
tal que realice una traducción de las instrucciones, reemplazando
las instrucciones de la forma (WHOILE b DO c) por instrucciones
de la forma (DO c WHILE b), manteniendo la semántica.
*}
fun dewhile :: "com ⇒ com" where
"dewhile c = undefined"
text{* Ejercicio 7.2.
Probar que la traducción conserva la semántica.
Nota: establecer los lemas auxiliares necesarios.
*}
lemma "dewhile c ∼ c"
oops
end