header {* 6ª relación de ejercicios *}
theory Relacion_6
imports Main
begin
section {* Número de elementos válidos *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (cuentaP Q xs) es el número de elementos de la lista xs que
satisfacen el predicado Q. Por ejemplo,
cuentaP (λx. 2<x) [1,3,4,0,5] = 3
---------------------------------------------------------------------
*}
primrec cuentaP :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
"cuentaP Q [] = 0"
| "cuentaP Q (x#xs) = (if Q x then 1 + cuentaP Q xs else cuentaP Q xs)"
text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys*
---------------------------------------------------------------------
*}
text {*
Se puede demostrar tal como se indica a continuación
*}
lemma "cuentaP P (xs @ ys) = cuentaP P xs + cuentaP P ys"
by (induct xs arbitrary: ys) auto
text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar que el número de elementos de una lista que
cumplen una determinada propiedad es el mismo que el de esa lista
invertida.
---------------------------------------------------------------------
*}
text {*
Para demostrar el resultado propuesto en este ejercicio
he necesitado formular y demostrar un lema auxiliar.
*}
lemma cuentaP_almoh_snoc: "cuentaP Q (x#xs)= cuentaP Q (snoc xs x)"(is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
thus "?P (x#xs)"
proof (cases "Q x")
case True thus "?thesis" using HI by auto
next
case False thus "?thesis" using HI by auto
qed
qed
text {*
En la demostración de este resultado, además del lema
auxiliar anterior, he debido introducir en las líneas
2 y 10 una proposición teoremática adicional sin la
cual el sistema no me aceptaba el razonamiento indicado.
*}
lemma "cuentaP Q xs = cuentaP Q (inversa xs)" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume 1: "?P xs"
thus "?P (x#xs)"
proof (cases "Q x")
case True thus "?thesis"
proof -
have 2: "snoc (inversa xs) x = (inversa xs) @ [x]" by (rule snoc_append)
from True have 3: "cuentaP Q (x#xs) = 1 + cuentaP Q xs" by auto
also have 4: "... = 1 + cuentaP Q (inversa xs)" using 1 by auto
also have 5: "... = cuentaP Q (x#(inversa xs))" using 1 and True by auto
also have 6: "... = cuentaP Q (snoc (inversa xs) x)" by (rule cuentaP_almoh_snoc)
also have 7: "... = cuentaP Q ((inversa xs) @ [x])" using 2 by auto
also have 8: "... = cuentaP Q (inversa (x#xs))" by auto
finally show 9: "cuentaP Q (x#xs) = cuentaP Q (inversa (x#xs))" by auto
qed
next
case False thus "?thesis"
proof -
have 10: "snoc (inversa xs) x = (inversa xs) @ [x]" by (rule snoc_append)
from False have 11: "cuentaP Q (x#xs) =cuentaP Q xs" by auto
also have 12: "... = cuentaP Q (inversa xs)" using 1 by auto
also have 13: "... = cuentaP Q (x#(inversa xs))" using 1 and False by auto
also have 14: "... = cuentaP Q (snoc (inversa xs) x)" by (rule cuentaP_almoh_snoc)
also have 15: "... = cuentaP Q ((inversa xs) @ [x])" using 10 by auto
also have 16: "... = cuentaP Q (inversa (x#xs))" by auto
finally show 16: "cuentaP Q (x#xs) = cuentaP Q (inversa (x#xs))" by auto
qed
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 4. Encontrar y demostrar una relación entre las funciones
filter y cuentaP.
---------------------------------------------------------------------
*}
text {*
Relación: El número de elementos de xs que cumplen la propiedad P será el número de elementos
que contendrá la lista resultante de aplicar el filtro P sobre xs.
*}
lemma "cuentaP P xs = length (filter P xs)"
by (induct xs) auto
end
