Diferencia entre revisiones de «R12»
De Lógica matemática y fundamentos [Curso 2019-20]
(Página creada con «<source lang = "isabelle"> chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)› theory R12 imports Main begin text ‹--------------------------------…») |
|||
(No se muestran 3 ediciones intermedias de otro usuario) | |||
Línea 51: | Línea 51: | ||
----------------------------------------------------------------------› | ----------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
+ | |||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
lemma sublistaMono_d: | lemma sublistaMono_d: | ||
− | + | "sublista xs ys ⟶ sublista xs (y#ys)" | |
− | |||
oops | oops | ||
Línea 72: | Línea 74: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 90: | Línea 94: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 108: | Línea 114: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 143: | Línea 151: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 161: | Línea 171: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
lemma cogeTodos_d: | lemma cogeTodos_d: | ||
− | + | "length xs ≤ n ⟶ coge n xs = xs" | |
− | |||
oops | oops | ||
Línea 181: | Línea 192: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 199: | Línea 212: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 217: | Línea 232: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 235: | Línea 252: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
lemma estaEnCoge_d: | lemma estaEnCoge_d: | ||
− | + | "estaEn x (coge n xs) ⟶ estaEn x xs" | |
− | |||
oops | oops | ||
Línea 256: | Línea 274: | ||
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
− | + | text ‹------------------------------------------------------------------ | |
− | › | + | Demostración en lenguaje natural: |
+ | |||
+ | ----------------------------------------------------------------------› | ||
― ‹Demostración declarativa:› | ― ‹Demostración declarativa:› | ||
Línea 270: | Línea 290: | ||
end | end | ||
− | |||
</source> | </source> |
Revisión actual del 17:22 7 may 2020
chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)›
theory R12
imports Main
begin
text ‹------------------------------------------------------------------
En toda la relación de ejercicios las demostraciones han de realizarse
de las formas siguientes:
+ en lenguaje natural
+ aplicativa o declarativa usando "simp"
+ aplicativa o declarativa usando "simp only: ..."
+ automática
Además, se recomienda el uso de lemas auxiliares (nuevos o de los
ejercicios anteriores) para que las demostraciones sean más cortas y
claras.
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Ejercicio 1. 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) = (a=x ∨ estaEn x xs)"
text ‹------------------------------------------------------------------
Ejercicio 2. Definir la función
sublista :: "'a list ⇒ 'a list ⇒ bool
tal que (sublista xs ys) se verifica si todos los elementos de la
lista xs están en la lista ys. Por ejemplo,
sublista [(1::nat),2,3] [3,2,1,2] = True
sublista [(1::nat),2,3] [2,1,2] = False
----------------------------------------------------------------------›
fun sublista :: "'a list ⇒ 'a list ⇒ bool" where
"sublista [] ys = True"
| "sublista (x#xs) ys = (estaEn x ys ∧ sublista xs ys )"
text ‹------------------------------------------------------------------
Ejercicio 3. Demostrar la siguiente propiedad: si xs es sublista de
ys, entonces xs también es sublista de la lista (y#ys). Es decir,
sublista xs ys ⟹ sublista xs (y#ys)
----------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma sublistaMono_d:
"sublista xs ys ⟶ sublista xs (y#ys)"
oops
― ‹Demostración aplicativa:›
lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y#ys)"
oops
text ‹------------------------------------------------------------------
Ejercicio 4. Demostrar que la relación sublista es reflexiva. Es
decir,
sublista xs xs
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma sublistaReflexiva_d: "sublista xs xs"
oops
― ‹Demostración aplicativa:›
lemma sublistaReflexiva: "sublista xs xs"
oops
text ‹------------------------------------------------------------------
Ejercicio 5. Probar, como corolario, que
sublista xs (x#xs)
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
corollary sublistaInc_d: "sublista xs (x#xs)"
oops
― ‹Demostración aplicativa:›
corollary sublistaInc: "sublista xs (x#xs)"
oops
text ‹------------------------------------------------------------------
Ejercicio 6. Probar que la relación sublista es transitiva. Es decir,
sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma sublistaTransitiva_d:
"sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
oops
― ‹Demostración aplicativa:›
lemma sublistaTransitiva:
"sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
oops
text ‹------------------------------------------------------------------
Ejercicio 7. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ ›
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"
value "coge 2 [a,c,d,b,e] = [a,c]"
text ‹------------------------------------------------------------------
Ejercicio 8. Probar que
coge 0 xs = []
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma coge0_d: "coge 0 xs = []"
oops
― ‹Demostración aplicativa:›
lemma coge0: "coge 0 xs = []"
oops
text ‹------------------------------------------------------------------
Ejercicio 9. Probar que
length xs ≤ n ⟹ coge n xs = xs
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma cogeTodos_d:
"length xs ≤ n ⟶ coge n xs = xs"
oops
― ‹Demostración aplicativa:›
lemma cogeTodos: "length xs ≤ n ⟹ coge n xs = xs"
oops
text ‹------------------------------------------------------------------
Ejercicio 10. Probar que
length (coge n xs) ≤ n
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma cogeLongN_d: "length (coge n xs) ≤ n"
oops
― ‹Demostración aplicativa:›
lemma cogeLongN: "length (coge n xs) ≤ n"
oops
text ‹------------------------------------------------------------------
Ejercicio 11. Probar que
length (coge n xs) ≤ length xs
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma cogeLongL_d: "length (coge n xs) ≤ length xs"
oops
― ‹Demostración aplicativa:›
lemma cogeLongL: "length (coge n xs) ≤ length xs"
oops
text ‹------------------------------------------------------------------
Ejercicio 12. Probar que
length (coge n xs) = min n (length xs)
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma lengthCogeMin_d:"length (coge n xs) = min n (length xs)"
oops
― ‹Demostración aplicativa:›
lemma lengthCogeMin: "length (coge n xs) = min n (length xs)"
oops
text ‹------------------------------------------------------------------
Ejercicio 13. Probar que
estaEn x (coge n xs) ⟹ estaEn x xs
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma estaEnCoge_d:
"estaEn x (coge n xs) ⟶ estaEn x xs"
oops
― ‹Demostración aplicativa:›
lemma estaEnCoge:
"estaEn x (coge n xs) ⟹ estaEn x xs"
oops
text ‹------------------------------------------------------------------
Ejercicio 14. Probar que
sublista (coge n xs) xs
---------------------------------------------------------------------›
text ‹------------------------------------------------------------------
Demostración en lenguaje natural:
----------------------------------------------------------------------›
― ‹Demostración declarativa:›
lemma sublistaCoge_d: "sublista (coge n xs) xs"
oops
― ‹Demostración aplicativa:›
lemma sublistaCoge: "sublista (coge n xs) xs"
oops
end