Diferencia entre revisiones de «Relación 5»
De Razonamiento automático (2016-17)
(Página creada con '(* bowma *) lemma length_borraDuplicados_2f: "length (borraDuplicados xs) ≤ length xs" (is "?p xs") proof (induct xs) show "length (borraDuplicados []) ≤ length []" by ...') |
m |
||
| (No se muestran 2 ediciones intermedias del mismo usuario) | |||
| Línea 18: | Línea 18: | ||
(* respuesta : danrodcha *) | (* respuesta : danrodcha *) | ||
| + | (* 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") | ||
| Línea 32: | Línea 33: | ||
using c1 by simp *) | using c1 by simp *) | ||
finally show "?p (a#xs)" by simp | finally show "?p (a#xs)" by simp | ||
| − | |||
| − | |||
qed | qed | ||
Revisión actual del 16:07 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
qed