Relación 5

chapter {* R5: Eliminación de duplicados *}

theory R5_Eliminacion_de_duplicados
imports Main 
begin
        
text {*
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la funcion primitiva recursiva 
     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
  --------------------------------------------------------------------- 
*}

(* crigomgom rubgonmar bowma wilmorort pablucoto serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn _ [] = False"
| "estaEn x (a#xs) = ((a = x) ∨ (estaEn x xs))"

value "estaEn (2::nat) [3,2,4] = True"
value "estaEn (1::nat) [3,2,4] = False"

(* ivamenjim, ferrenseg *)
(* Igual que la anterior pero con x en lugar de _ en el caso base *)

fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn1 x [] = False" 
| "estaEn1 x (a#xs) = ((x=a) ∨ estaEn1 x xs)"

value "estaEn1 (2::nat) [3,2,4] = True"
value "estaEn1 (1::nat) [3,2,4] = False"

(* wilmorort *)
(* reutilizando  la funcion "algunos" de R4.thy*)
fun estaEn2  :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn2 a xs = algunos (λx. x = a) xs"

value "estaEn2 (2::nat) [3,2,4] = True"
value "estaEn2 (1::nat) [3,2,4] = False"


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función primitiva recursiva 
     sinDuplicados :: 'a list ⇒ bool
  tal que (sinDuplicados xs) se verifica si la lista xs no contiene
  duplicados. Por ejemplo,  
     sinDuplicados [1::nat,4,2]   = True
     sinDuplicados [1::nat,4,2,4] = False
  --------------------------------------------------------------------- 
*}

(* crigomgom rubgonmar ivamenjim  wilmorort bowma pablucoto serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1 ferrenseg *)
fun sinDuplicados :: "'a list ⇒ bool" where
  "sinDuplicados [] = True"
| "sinDuplicados (x#xs) = (¬ estaEn x xs ∧ sinDuplicados xs)"

value "sinDuplicados [1::nat,4,2]   = True"
value "sinDuplicados [1::nat,4,2,4] = False"

(* paupeddeg *)
(* Utilizando la función ∉ de Isabelle *)
fun sinDuplicados2 :: "'a list ⇒ bool" where
  "sinDuplicados2 [] = True"
| "sinDuplicados2 (a#xs) = ((a ∉ set xs) ∧  sinDuplicados2 xs ) "



text {* 
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir la función primitiva recursiva 
     borraDuplicados :: 'a list ⇒ bool
  tal que (borraDuplicados xs) es la lista obtenida eliminando los
  elementos duplicados de la lista xs. Por ejemplo, 
     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

  Nota: La función borraDuplicados es equivalente a la predefinida
  remdups.  
  --------------------------------------------------------------------- 
*}

(* crigomgom rubgonmar wilmorort bowma pablucoto serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1 ferrenseg*)
fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados [] = []"
| "borraDuplicados (x#xs) =( if estaEn x xs then borraDuplicados xs else x#borraDuplicados xs)"

value "borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]"

(* ivamenjim *)
(* Utilizando la negación primero *)

fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados [] = []"
| "borraDuplicados (x#xs) = (if ¬(estaEn x xs) then (x#(borraDuplicados xs)) else borraDuplicados xs)"


(* rubgonmar *)
(* Otra forma Sin usar if 
  Utilizando case aunque se le sacaría más partido con más de 2 casos *)
 
 fun borraDuplicados1 :: "'a list ⇒ 'a list" where
"borraDuplicados1 [] = []" |
"borraDuplicados1 (x#xs) = ( case estaEn x xs of False  => x#borraDuplicados1 xs | True => borraDuplicados1 xs )"


(* rubgonmar *)
(*Otra forma utilizando let*)
fun borraDuplicados2 :: "'a list ⇒ 'a list" where
"borraDuplicados2 [] = []" |
"borraDuplicados2 (x#xs) =  (let condicion = estaEn x xs::bool  in 
if  condicion then borraDuplicados2 xs else x # borraDuplicados2 xs)"

value "borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
(*crigomgom anaprarod ferrenseg*)
lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
by (induct xs, simp_all)

(* rubgonmar wilmorort pablucoto serrodcal migtermor paupeddeg fraortmoy marpoldia1*)
lemma length_borraDuplicados:
  "length ( borraDuplicados xs ) ≤ length xs"
by (induct xs) auto

(* ivamenjim *)
(* Demostrando objetivo a objetivo *)
lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
apply (induct xs)
apply simp 
apply auto
done

(* bowma  anaprarod *)
lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
apply (induct xs)
apply (simp, simp)  (* creo que es mejor poner aquí simp_all *)
done

(* ferrenseg *)

lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
by (induct xs) simp_all (* Creo que se puede poner simp_all fuera de parentesis *)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.2. Demostrar o refutar detalladamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

-- "La demostración estructurada es"
(* crigomgom *)
lemma length_borraDuplicados_2: 
  "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" by simp
next
  fix x xs
  assume HI: "length (borraDuplicados xs) ≤ length xs"
  show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"
  proof (cases)
    assume "estaEn x xs"
    then have "length (borraDuplicados (x#xs)) = length (borraDuplicados xs)" by simp
    also have "...  ≤ length xs" using HI by simp
    also have "... ≤ length (x#xs)" by simp
    finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)" by simp
  next
    assume "(¬ estaEn x xs)"
    then have "length (borraDuplicados (x#xs)) = length (x#borraDuplicados xs)" by simp
    also have "... = 1 +  length (borraDuplicados xs)" by simp
    also have "...  ≤ 1 + length xs" using HI by simp
    also have "... = length (x#xs)" by simp
    finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"  by simp
  qed
qed

(* ivamenjim  wilmorort ferrenseg *)
lemma length_borraDuplicados_2: 
  "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" by simp
next 
  fix a xs
  assume HI: "length (borraDuplicados xs) ≤ length xs"
  have "length (borraDuplicados (a # xs)) ≤ 1+length (borraDuplicados xs)" by simp
  also have "... ≤ 1+length xs" using HI by simp
  finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed

(* serrodcal anaprarod *)
lemma length_borraDuplicados_2: "length (borraDuplicados xs) ≤ length xs" (is "?P xs")
proof (induct xs)
  show "?P []" by simp
next 
  fix a xs
  assume HI: "?P xs"
  have "length (borraDuplicados (a # xs)) ≤ 1+length (borraDuplicados xs)" by simp
  also have "... ≤ 1+length xs" using HI by simp
  finally show "?P (a # xs)" by simp
qed

(* pablucoto *)
lemma length_borraDuplicados_2: 
  "length (borraDuplicados xs) ≤ length xs"  
proof(induct xs)
  show "length (borraDuplicados []) ≤ length [] " by simp
next 
  fix a xs
  assume HI: " length (borraDuplicados xs) ≤ length xs "
  have "length (borraDuplicados (a # xs)) ≤ 1 + length(borraDuplicados xs)"  by simp
  also have "... ≤ 1 + length xs" using HI by simp 
  also have "... ≤ length (a#xs)" by simp
  finally  show "length (borraDuplicados (a # xs)) ≤ length (a # xs) " by simp
qed

(* bowma *)
lemma length_borraDuplicados_3: 
  "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 "length (a#xs) = 1 + length xs" by simp 
    have "length(borraDuplicados (a#xs)) ≤ 1 + length(borraDuplicados xs)" by simp
    also have "... ≤ 1+length xs" using HI by simp
    also have "... ≤ length (a#xs)" by simp
  finally show "?p (a # xs)" by simp
qed

(* migtermor *)

lemma length_borraDuplicados_2: 
  "length (borraDuplicados xs) ≤ length xs" (is "?P xs")
proof (induct xs)
 show "?P []" by simp
next
 fix a xs
 assume HI: "?P xs"
 have "length (borraDuplicados (a#xs)) ≤ (length (a#xs))"
  proof (cases)
   assume "(estaEn a xs)"
   then have Aux: "length (borraDuplicados (a#xs)) = length (borraDuplicados xs)" by simp
   also have "… ≤ length (a#xs)" using HI by simp
   then show "length (borraDuplicados (a#xs)) ≤ (length (a#xs))" using Aux by simp
  next
   assume "¬ (estaEn a xs)"
   then have Aux: "length (borraDuplicados (a#xs)) = 1+ length (borraDuplicados xs)" by simp
   also have "… ≤ length (a#xs)" using HI by simp
   then show "length (borraDuplicados (a#xs)) ≤ (length (a#xs))" using Aux by simp
  qed
then show "?P (a#xs)" by simp
qed

(* paupeddeg marpoldia1*)
lemma length_borraDuplicados_4:
  "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" by simp
next
  fix a xs 
  assume HI: "length (borraDuplicados xs) ≤ length xs"
  have "length (borraDuplicados (a # xs)) ≤ length [a] + length (borraDuplicados xs) " by simp
  also have "... ≤ 1 + length (borraDuplicados xs)" by simp
  also have "... ≤ 1 + length xs" using HI by simp
  finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed

(* fraortmoy *)
(* muy parecida a alguna anterior, pero yo dí mas pasos *)
lemma length_borraDuplicados_2: 
  "length (borraDuplicados xs) ≤ length xs"
  proof (induct xs)
    show "length (borraDuplicados []) ≤ length []" by simp
  next
    fix a xs
    assume H1: "length (borraDuplicados xs) ≤ length xs"
    have "length (borraDuplicados (a # xs)) ≤ length(borraDuplicados [a])+length (borraDuplicados xs)" by simp
    also have "… ≤ 1 + length (borraDuplicados xs)" by simp
    also have "… ≤ 1 + length xs" using H1 by simp
    finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.1. Demostrar o refutar automáticamente
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
*}

-- "La demostración automática es"
(* crigomgom rubgonmar  wilmorort pablucoto serrodcal bowma migtermor fraortmoy marpoldia1 *)
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto

(* ivamenjim *)
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs) 
apply auto
done

(* anaprarod *)
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs, simp_all, blast)


(* anaprarod *)
lemma estaEn_borraDuplicados': 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply (cases "estaEn x xs")
apply (simp_all)
apply blast
done

(* bowma *)
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply simp
apply (simp, blast)
done
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.2. Demostrar o refutar detalladamente
     estaEn a (borraDuplicados xs) = estaEn a xs
  Nota: Para la demostración de la equivalencia se puede usar
     proof (rule iffI)
  La regla iffI es
     ⟦P ⟹ Q ; Q ⟹ P⟧ ⟹ P = Q
  --------------------------------------------------------------------- 
*}

-- "La demostración estructurada es"

(* wilmorort *)

lemma estaEn_borraDuplicados_2: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
  show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
  fix b xs
  assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
  show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)"
  proof (rule iffI)
    assume H1: "estaEn a (borraDuplicados (b#xs))"
    show "estaEn a (b#xs)"
    proof (cases)
      assume "estaEn b xs"
      then have "estaEn a (borraDuplicados xs)" using  H1 by  simp
      then have "estaEn a xs" using HI by simp
      then show  "estaEn a (b#xs)" by simp
    next
      assume "¬ estaEn b xs"
      then have "estaEn a (b#(borraDuplicados xs))" using H1 by simp
      then have "a=b ∨ (estaEn a (borraDuplicados xs))" by simp
      then have " a=b ∨ (estaEn a xs)" using HI by simp
      then show "estaEn a (b#xs)" by simp
    qed
  next
    assume H2: "estaEn a (b#xs)"
    show "estaEn a (borraDuplicados (b#xs))"
    proof (cases)
      assume "a=b"
      then have "estaEn b (borraDuplicados xs) = estaEn b xs" using HI by simp
      then have "(estaEn b xs ⟶ estaEn b (borraDuplicados xs)) ∧
           (¬ estaEn b xs ⟶ estaEn b (b # borraDuplicados xs))" by simp      
       then have "estaEn b (borraDuplicados (b#xs))" by simp
      then show "estaEn a (borraDuplicados (b#xs))" using `a=b` by simp
     next
      assume "a≠b"
      then have "estaEn a (b#xs)" using H2 by simp
      then have "a = b ∨ estaEn a xs" by simp
      then have "False ∨ estaEn a xs " using `a≠b` by simp
      then have "estaEn a xs" by simp
      then have "estaEn a (borraDuplicados xs)" using HI by simp
      then show "estaEn a (borraDuplicados (b#xs))" using `a≠b` by simp
    qed
  qed
qed


(* anaprarod marpoldia1 *)
lemma estaEn_borraDuplicados_2:
 "estaEn a (borraDuplicados xs) = estaEn a xs" (is "?P xs")
proof (induct xs)
 show "?P []" by simp
next
 fix x xs
 assume HI: "?P xs"
 show "?P (x#xs)"
 proof (cases)
  assume "estaEn x xs"
  then have "estaEn a (borraDuplicados (x#xs)) = estaEn a (borraDuplicados xs)" by simp
  also have "...= estaEn a xs" using HI by simp
  finally show "?P (x#xs)" by auto
 next
  assume "¬estaEn x xs"
  then have "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#borraDuplicados xs)" by simp
  also have "...= (x = a ∨ estaEn a (borraDuplicados xs))" by simp
  finally show  "?P (x#xs)" using HI by simp
 qed
qed


(* migtermor *)

lemma estaEn_borraDuplicados_2: 
  "estaEn a (borraDuplicados xs) = estaEn a xs" (is "?P xs")
proof (induct xs)
 show "?P []" by simp
next 
 fix aa xs
 assume HI: "?P xs"
 have P1: "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)"
  proof (cases)
   assume C1: "(estaEn aa xs)"
    have "estaEn a (borraDuplicados (aa#xs)) = estaEn a (borraDuplicados xs)" 
             using C1 by simp
    also have P3: "… = estaEn a xs" using HI by simp
    also have "… = estaEn a (aa#xs)"  
    proof (cases)
     assume "(a=aa)"
     then show "estaEn a xs = estaEn a (aa#xs)" using C1 by simp
    next
     assume "¬(a=aa)"
     then show "estaEn a xs = estaEn a (aa#xs)" by simp
    qed
    then show "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)" using P3 by simp
  next
   assume C2: "¬(estaEn aa xs)"
    then show "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)" using HI by simp
  qed
 also have Conc: "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)" using P1 by simp
 finally show "?P (aa#xs)" using Conc by simp
qed

(* crigomgom *)
-- "La demostración estructurada es"
lemma estaEn_borraDuplicados_2: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
  show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
  fix x xs
  assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
  show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)"
  proof (rule iffI)
    assume a1: "estaEn a (borraDuplicados (x#xs))"
    show "estaEn a (x#xs)"
    proof (cases)
      assume "estaEn x xs"
      then have "estaEn a (borraDuplicados xs)" using  a1 by  simp
      then have "estaEn a xs" using HI by simp
      then show  "estaEn a (x#xs)" by simp
    next
      assume "¬ estaEn x xs"
      then have "estaEn a (x#(borraDuplicados xs))" using a1 by simp
      then have " x=a ∨ (estaEn a (borraDuplicados xs))" by simp
      then have " x=a ∨ (estaEn a xs)" using HI by simp
      then show "estaEn a (x#xs)" by simp
    qed
  next
    assume a2: "estaEn a (x#xs)"
    show "estaEn a (borraDuplicados (x#xs))"
    proof (cases)
      assume "a=x"
      then  show "estaEn a (borraDuplicados (x#xs))" using HI by simp
    next
      assume b1: "a≠x"
      then have "estaEn a (x#xs)" using a2 by simp
      then have "x = a ∨ estaEn a xs" by simp
      then have "estaEn a xs " using b1  by simp
      then have "estaEn a (borraDuplicados xs)" using HI by simp
      then show "estaEn a (borraDuplicados (x#xs))" using b1 by simp
    qed
  qed
qed


(* rubgonmar *)
lemma estaEn_borraDuplicados_2: 
  "estaEn a  ( borraDuplicados xs ) = estaEn a xs"
proof (induct xs)
   show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
   fix x
   fix xs
   assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
   show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)"
   proof (rule iffI) (* usamos proof de la regla dada iffI*)
     assume cprim: "estaEn a (borraDuplicados (x#xs))"
     show "estaEn a (x#xs)"
     proof (cases)
       assume "estaEn x xs"
       then show "estaEn a (x#xs)" using cprim HI by simp
     next
       assume "¬ estaEn x xs"
       then show "estaEn a (x#xs)" using cprim HI by simp
     qed
   next
     assume cseg: "estaEn a (x#xs)"
     show "estaEn a (borraDuplicados (x#xs))"
     proof (cases)
       assume "a=x"
       then show "estaEn a (borraDuplicados (x#xs))" using HI by auto
     next
       assume "a≠x"
       thus "estaEn a (borraDuplicados (x#xs))" using `a≠x` cseg HI by simp
     qed
   qed
qed

(* 
Aplico la regla iffI:
     ⟦P ⟹ Q ; Q ⟹ P⟧ ⟹ P = Q
Así:
 [estaEn a (borraDuplicados (x # xs)) ⟹ estaEn a (x # xs); estaEn a (x # xs) ⟹ estaEn a (borraDuplicados (x # xs))] 
⟹ estaEn a (borraDuplicados (x # xs)) = estaEn a (x # xs)
*)


(* bowma *)
lemma estaEn_borraDuplicados_2: 
  "estaEn a (borraDuplicados xs) = estaEn a xs" (is "?p xs")
proof (induct xs)
show "?p []" by simp
next 
fix x xs
assume HI: "?p xs"
show "?p (x#xs)"
  proof (cases)
  assume H1:"estaEn x xs"
  then have "estaEn a (borraDuplicados (x#xs)) = estaEn a (borraDuplicados xs)" by simp
  also have "... = estaEn a xs" using HI by simp
  also have "... = estaEn a (x#xs)" 
    proof(cases)
    assume "x=a"
    then show "estaEn a xs = estaEn a (x#xs)" using H1 by simp
    next
    assume "x≠a"
    then show "estaEn a xs = estaEn a (x#xs)" by simp
    qed
  finally show "?p (x#xs)" by simp
  next
  assume H2:"¬estaEn x xs"
  then have "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#borraDuplicados xs)" by simp
  also have "... = ((x=a) ∨ estaEn a (borraDuplicados xs))" by simp
  also have "... = ((x=a) ∨ estaEn a xs)" using HI by simp
  also have "... = estaEn a (x#xs)" by simp
  finally show "?p (x#xs)" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6.1. Demostrar o refutar automáticamente
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

-- "La demostración automática"

(* ivamenjim wilmorort serrodcal crigomgom anaprarod fraortmoy marpoldia1*)
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)

(* migtermor *)
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
by (induct xs, simp_all add: estaEn_borraDuplicados_2)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6.2. Demostrar o refutar detalladamente
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

(*wilmorort*)

-- "La demostración estructurada es"
lemma sinDuplicados_borraDuplicados_2:
  "sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show " sinDuplicados (borraDuplicados [])" by simp
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados xs)"
show "sinDuplicados (borraDuplicados (a # xs))"
proof (cases)
assume "estaEn a xs"
then show "sinDuplicados (borraDuplicados (a#xs))" using HI by simp
next
assume"¬ estaEn a xs"
then have "¬ (estaEn a xs) ∧ sinDuplicados (borraDuplicados xs)" using HI by simp
then have "¬ estaEn a (borraDuplicados xs) ∧  sinDuplicados (borraDuplicados xs)" 
      by (simp add: estaEn_borraDuplicados)
then have " sinDuplicados (a#borraDuplicados xs)" by simp
then show " sinDuplicados (borraDuplicados(a #xs))" by simp
qed
qed

(* ivamenjim migtermor crigomgom rubgonmar fraortmoy *)

lemma sinDuplicados_borraDuplicados_2:
  "sinDuplicados (borraDuplicados xs)"
proof (induct xs)
  show "sinDuplicados (borraDuplicados [])" by simp
next
  fix a xs
  assume HI: "sinDuplicados (borraDuplicados xs)"
  show "sinDuplicados (borraDuplicados (a # xs))" 
  proof (cases)
    assume "estaEn a xs" 
    then show "sinDuplicados (borraDuplicados (a # xs))" using HI by simp
  next
    assume "¬(estaEn a xs)"
    then show "sinDuplicados (borraDuplicados (a # xs))" using HI by (simp add: estaEn_borraDuplicados)
  qed
qed

(* anaprarod *)
lemma sinDuplicados_borraDuplicados_2:
  "sinDuplicados (borraDuplicados xs)" (is "?P xs")
proof (induct xs)
  show  "?P []" by simp
  next
  fix x xs
  assume HI: "?P xs"
  show "?P (x#xs)"
   proof (cases)
   assume c1: "estaEn x xs"
   then show "sinDuplicados (borraDuplicados (x#xs))" using HI by simp
   next
   assume c2: "¬ estaEn x xs"
   then have "sinDuplicados (borraDuplicados (x#xs)) =sinDuplicados (x#borraDuplicados xs)" by simp
   also have "…= (¬estaEn x (borraDuplicados xs) ∧ sinDuplicados (borraDuplicados xs))" by simp
   also have "… = (¬estaEn x (borraDuplicados xs))" using HI by simp
   also have "… = (¬(estaEn x xs))" by (simp add:estaEn_borraDuplicados)
   also have "… = True" using c2 by simp
   finally show "?P (x#xs)" by simp
 qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
*}

(*crigomgom rubgonmar ivamenjim wilmorort pablucoto migtermor anaprarod fraortmoy *)
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
quickcheck
oops

(* ivamenjim: Quickcheck encuentra el siguiente contraejemplo: 
   xs = [a1, a2, a1]
   Por lo que:
   · "borraDuplicados (rev xs) = [a2, a1]"
   · "rev (borraDuplicados xs) = [a1, a2]" *)

end