Rel 11

theory Hoare_ejercicios_1

imports "Hoare_b_ejemplos" "Hoare_Sound_Complete_b"

begin

text{* Ejercicio 1:
Definir una función bsubst 
fun bsubst :: "bexp ⇒ vname ⇒ aexp ⇒ bexp"

y probar el siguiente lema de sustitución:

lemma bsubstitution: "bval (bsubst b x a) s = bval b (s[a/x])"

*}


fun bsubst :: "bexp ⇒ vname ⇒ aexp ⇒ bexp" where
"bsubst b x a       = undefined" 

lemma bsubstitution: "bval (bsubst b x a) s = bval b (s[a/x])"
oops

text{* Ejercicio 2:
Dada la siguiente operación de igualdad para expresiones aritméticas

fun Eq :: "aexp ⇒ aexp ⇒ bexp" where
  "Eq a1 a2 = And (Not (Less a1 a2)) (Not (Less a2 a1))"

probar las siguientes propiedades:
*}

fun Eq :: "aexp ⇒ aexp ⇒ bexp" where
  "Eq a1 a2 = And (Not (Less a1 a2)) (Not (Less a2 a1))"

lemma bval_Eq[simp]: "bval (Eq a1 a2) s = (aval a1 s = aval a2 s)"
oops

lemma bval_NotEq[simp]: "bval (Not (Eq a1 a2)) s = (aval a1 s ≠ aval a2 s)"
oops

lemma notEq: "¬ bval (bexp.Not (Eq (V ''r'') (N i))) s ⟶ s ''r'' = i"
oops

lemmas Seq_bwd = Seq[rotated]

text{* Ejercicio 3:
Probar la corrección parcial de la siguiente variante del programa 
para sumar los números de 1 a n.

lemma
  "⊢ {λs. s ''x'' = i ∧ 0 ≤ i}
     ''y'' ::= N 0;;
     WHILE Not(Eq (V ''x'') (N 0))
     DO (''y'' ::= Plus (V ''y'') (V ''x'');;
          ''x'' ::= Plus (V ''x'') (N -1))
     {λs. s ''y'' = sum i}"

Nota: establecer los lemas auxiliares necesarios.
*}


lemma
  "⊢ {λs. s ''x'' = i ∧ 0 ≤ i}
     ''y'' ::= N 0;;
     WHILE Not(Eq (V ''x'') (N 0))
     DO (''y'' ::= Plus (V ''y'') (V ''x'');;
          ''x'' ::= Plus (V ''x'') (N -1))
     {λs. s ''y'' = sum i}"
oops

text{* Ejercicio 4:
Probar que el siguiente programa calcula una aproximación entera 
de la raiz cuadrada de x.

Nota: Usar las reglas de simplificación algebra_simps y 
power2_eq_square.
*}

lemma
  "⊢ { λs. 0 ≤ s ''x'' }
     ''r'' ::= N 0;; ''t'' ::= N 1;;
     WHILE (Not (Less (V ''x'') (V ''t'')))
     DO (''r'' ::= Plus (V ''r'') (N 1);;
         ''t'' ::= Plus (V ''t'') 
                        (Plus (Plus (V ''r'') (V ''r'')) 
                              (N 1)))
     {λs. (s ''r'')^2 ≤ s ''x'' ∧ s ''x'' < (s ''r'' + 1)^2}"
oops

text{* Ejercicio 5:
Probar que el siguiente programa calcula la diferencia y - x.

*}

abbreviation "diferencia n m ==
    ''r'' ::= N m;;
    ''t'' ::= N n;;
     WHILE (Less (N 0) (V ''r''))
     DO (''r'' ::= Plus (V ''r'') (N -1);; 
         ''t'' ::= Plus (V ''t'') (N -1))"

lemma
  "⊢ {λs. s ''x'' = m ∧ s ''y'' = n ∧ 0 ≤ m}
    ''r'' ::= N m;;
    ''t'' ::= N n;;
     WHILE (Less (N 0) (V ''r''))
     DO (''r'' ::= Plus (V ''r'') (N -1);; 
         ''t'' ::= Plus (V ''t'') (N -1))
     {λs. s ''t'' = n - m}"
oops

text{* Ejercicio 6: 
Probar que el siguiente programa calcula la potencia n-sima
de 2
*}

fun pot2 :: "int ⇒ int" where
"pot2 i = (if i ≤ 0 then 1 else pot2 (i - 1) * 2)"

text{* Establecemos las siguientes reglas de simplificación, que
sustituyen a las reglas de simplificación generadas por la 
definición.
*}

lemma pot2_simps[simp]:
  "0 < i ⟹ pot2 i = pot2 (i - 1) * 2"
  "i ≤ 0 ⟹ pot2 i = 1"
by(simp_all)

declare pot2.simps[simp del]

lemma
  "⊢ {λs. s ''x'' = i ∧ 0 ≤ i}
     ''r'' ::= N 0;;
     ''t'' ::= N 1;;
     WHILE Not(Eq (V ''r'') (N i))
     DO (''r'' ::= Plus (V ''r'') (N 1);;
         ''t'' ::= Plus (V ''t'') (V ''t''))
     {λs. s ''t'' = pot2 i}"
oops

text{* Ejercicio 7:
Probar que el siguiente programa calcula el cociente y el resto
de la división euclídea.
*}

lemma
  "⊢ {λs. s ''x'' = a ∧ s ''y'' = b ∧ 0 ≤ a ∧ 0 < b}
    ''c'' ::= N 0;;
    ''r'' ::= N a;;
     WHILE (Not (Less (V ''r'') (N b)))
     DO (''c'' ::= Plus (V ''c'') (N 1);; 
         ''r'' ::= Plus (V ''r'') (N (-b)))
     {λs. a = b*(s ''c'') + (s ''r'') ∧ (s ''r'' < b) }"
oops

text{* Ejercicio 8: 
Probar la siguiente propiedad:

lemma postCondicion_dem: "⊢ {P} c {λs. True}"

*}


lemma postCondicion_dem: "⊢ {P} c {λs. True}"
oops

end
De Demostración automática de teoremas (2014-15)
