Razonamiento automático (2016-17) Razonamiento automático (2016-17)

(* 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