Diferencia entre revisiones de «Relación 5»
De Razonamiento automático (2016-17)
m |
|||
| Línea 18: | Línea 18: | ||
(* respuesta : danrodcha *) | (* respuesta : danrodcha *) | ||
| − | (* mirar en editar xq aqui | + | (* mirar en editar xq aqui no se entiende *) |
lemma length_borraDuplicados_2f: | lemma length_borraDuplicados_2f: | ||
"length (borraDuplicados xs) ≤ length xs" (is "?p xs") | "length (borraDuplicados xs) ≤ length xs" (is "?p xs") | ||
Revisión del 16:06 1 dic 2016
(* bowma *) lemma length_borraDuplicados_2f:
"length (borraDuplicados xs) ≤ length xs" (is "?p xs")
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "?p xs"
have c1: "1+length xs = length (a#xs)" by simp
also have "length(borraDuplicados (a#xs)) ≤
1 + length(borraDuplicados xs)" by simp
also have "... ≤ 1+length xs" using HI by simp
then show "length(borraDuplicados (a#xs)) ≤ length (a#xs)"
using c1 by simp
(* ¿Aquí porqué no puedo usar "finally show "?p (a # xs)" using c1 by simp?
Y porque no puedo añadir "finally show "?p (a # xs)" by simp al final? *)
qed
(* respuesta : danrodcha *) (* mirar en editar xq aqui no se entiende *) lemma length_borraDuplicados_2f:
"length (borraDuplicados xs) ≤ length xs" (is "?p xs")
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp (* <----yo aprovecharia los patrones "?p []" *)
next
fix a xs assume HI: "?p xs"
(* have c1: "1+length xs = length (a#xs)" by simp *) (* <------ esto no hace falta *) (* also *) have "length(borraDuplicados (a#xs)) ≤
1 + length(borraDuplicados xs)" by simp
also have "... ≤ 1+length xs" using HI by simp
(* then show "length(borraDuplicados (a#xs)) ≤ length (a#xs)"
using c1 by simp *)
finally show "?p (a#xs)" by simp
(* ¿Aquí porqué no puedo usar "finally show "?p (a # xs)" using c1 by simp?
Y porque no puedo añadir "finally show "?p (a # xs)" by simp al final? *)
qed