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



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*)
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)"

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*)
lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
by (induct xs, simp_all)

(* rubgonmar wilmorort *)
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

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

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

 
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"
lemma estaEn_borraDuplicados_2: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
oops




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

-- "La demostración automática"

(* ivamenjim wilmorort *)
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)


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

-- "La demostración estructurada es"
lemma sinDuplicados_borraDuplicados_2:
  "sinDuplicados (borraDuplicados xs)"
oops

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

(*crigomgom rubgonmar ivamenjim wilmorort *)
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