R12 - Historial de revisiones

Jalonso en 15:22 7 may 2020

2020-05-07T15:22:31Z

Mjoseh en 07:31 7 may 2020

2020-05-07T07:31:26Z

Mjoseh en 07:17 7 may 2020

2020-05-07T07:17:59Z

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

2020-05-07T06:39:53Z

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

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

2020-05-07T06:39:24Z

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

Página nueva

<source lang = "isabelle">
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)
----------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
›

― ‹Demostración declarativa:›

lemma sublistaMono_d:
assumes "sublista xs ys"
shows "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
---------------------------------------------------------------------›

― ‹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)
---------------------------------------------------------------------›

― ‹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
---------------------------------------------------------------------›

― ‹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 = []
---------------------------------------------------------------------›

― ‹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
---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
›

― ‹Demostración declarativa:›

lemma cogeTodos_d:
assumes "length xs ≤ n"
shows "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
---------------------------------------------------------------------›

― ‹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
---------------------------------------------------------------------›

― ‹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)
---------------------------------------------------------------------›

― ‹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
---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
›

― ‹Demostración declarativa:›

lemma estaEnCoge_d:
assumes "estaEn x (coge n xs)"
shows "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
---------------------------------------------------------------------›

― ‹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

</source>

← Revisión anterior		Revisión del 15:22 7 may 2020
Línea 1:		Línea 1:
−	<source lang = "isabelle"	+	<source lang = "isabelle">
	chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)›		chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)›

@@ Línea 1: / Línea 1: @@
-<source lang = "isabelle">
+<source lang = "isabelle"
 chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)›
@@ Línea 51: / Línea 51: @@
   ----------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 71: / Línea 74: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 89: / Línea 94: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 107: / Línea 114: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 142: / Línea 151: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 160: / Línea 171: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 179: / Línea 192: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 197: / Línea 212: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 215: / Línea 232: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 233: / Línea 252: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›
@@ Línea 253: / Línea 274: @@
    ---------------------------------------------------------------------›
- ― ‹Demostración en lenguaje natural:
+text ‹------------------------------------------------------------------
-›
+  Demostración en lenguaje natural:
 ― ‹Demostración declarativa:›

@@ Línea 57: / Línea 57: @@
 lemma sublistaMono_d:
-   assumes "sublista xs ys"
+   "sublista xs ys ⟶ sublista xs (y#ys)"
    oops
@@ Línea 167: / Línea 166: @@
 lemma cogeTodos_d:
-  assumes "length xs ≤ n"
+    "length xs ≤ n ⟶ coge n xs = xs"
    oops
@@ Línea 241: / Línea 239: @@
 lemma estaEnCoge_d:
-  assumes "estaEn x (coge n xs)"
+    "estaEn x (coge n xs) ⟶ estaEn x xs"
    oops
@@ Línea 270: / Línea 267: @@
 end
 </source>

← Revisión anterior	Revisión del 06:39 7 may 2020
(Sin diferencias)