Mjoseh en 07:23 4 may 2020

2020-05-04T07:23:47Z

Mjoseh: Protegió «R11» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-04-23T10:05:48Z

Protegió «R11» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)› theory R11 imports Main begin text ‹ -------------------------------…»

2020-04-23T10:05:30Z

Página creada con «<source lang = "isabelle"> chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)› theory R11 imports Main begin text ‹ -------------------------------…»

Página nueva

<source lang = "isabelle">
chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)›

theory R11
imports Main
begin

text ‹ ---------------------------------------------------------------
En toda la relación de ejercicios las demostraciones han de realizarse
de las formas siguientes:
+ automática
+ detallada (bien de forma declarativa o aplicativa)
------------------------------------------------------------------ ›

text ‹ ---------------------------------------------------------------
Ejercicio 1.1. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ ›

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = Suc n * factR n"

value "factR 4" ― ‹= 24›

text ‹ ---------------------------------------------------------------
Ejercicio 1.2. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- ›

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (x* (Suc n))"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

― ‹Demostración automática:›
lemma "factI' n x = x * factR n"
oops

― ‹Demostración detallada:›
lemma fact_d: "factI' n x = x * factR n"
oops

text ‹ ---------------------------------------------------------------
Ejercicio 1.3. Demostrar que
factI n = factR n
------------------------------------------------------------------- ›

corollary fact_equiv: "factI n = factR n"
oops

text ‹
---------------------------------------------------------------------
Ejercicio 2. Definir la función
estaEn :: 'a ⇒ 'a list ⇒ bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------
›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (x=a ∨ estaEn x xs)"

text ‹
---------------------------------------------------------------------
Ejercicio 3. Definir la función
sinDuplicados :: 'a list ⇒ bool
tal que (sinDuplicados xs) se verifica si la lista xs no contiene
duplicados. Por ejemplo,
sinDuplicados [1::nat,4,2] = True
sinDuplicados [1::nat,4,2,4] = False
---------------------------------------------------------------------
›

fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = True"
| "sinDuplicados (a#xs) = ((¬ estaEn a xs) ∧ sinDuplicados xs)"

text ‹
---------------------------------------------------------------------
Ejercicio 4. Definir la función
borraDuplicados :: 'a list ⇒ bool
tal que (borraDuplicados xs) es la lista obtenida eliminando los
elementos duplicados de la lista xs. Por ejemplo,
borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

Nota: La función borraDuplicados es equivalente a la predefinida
remdups.
---------------------------------------------------------------------
›

fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (a#xs) = (if estaEn a xs
then borraDuplicados xs
else (a#borraDuplicados xs))"

text ‹
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "length (borraDuplicados xs) ≤ length xs"
oops

― ‹Demostración detallada:›
lemma length_borraDuplicados_d:
"length (borraDuplicados xs) ≤ length xs"
oops

text ‹
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

― ‹Demostración detallada:›
lemma estaEn_borraDuplicados_d:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text ‹
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "sinDuplicados (borraDuplicados xs)"
oops

― ‹Demostración detallada:›
lemma sinDuplicados_borraDuplicados_d:
"sinDuplicados (borraDuplicados xs)"
oops

text ‹
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
›

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops

end

</source>

@@ Línea 11: / Línea 11: @@
     de las formas siguientes:
      + automática
-     + detallada (bien de forma declarativa o aplicativa)
+     + en el ejercicio 1.2, la prueba detallada usando "simp only:..."
    ------------------------------------------------------------------ ›

← Revisión anterior	Revisión del 10:05 23 abr 2020
(Sin diferencias)

R11 - Historial de revisiones

Mjoseh en 07:23 4 may 2020

Mjoseh: Protegió «R11» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)› theory R11 imports Main begin text ‹ -------------------------------…»