Rel 10 (e)

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 c = undefined"

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 c = undefined"

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 c = undefined"


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