Acciones

Diferencia entre revisiones de «Relación 5»

De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle»)
 
(No se muestran 158 ediciones intermedias de 25 usuarios)
Línea 1: Línea 1:
−
<source lang="isar">
+
<source lang="isabelle">
 
chapter {* R5: Eliminación de duplicados *}
 
chapter {* R5: Eliminación de duplicados *}
  
Línea 17: Línea 17:
 
*}
 
*}
  
−
(* crigomgom rubgonmar bowma *)
+
(* crigomgom rubgonmar bowma wilmorort pablucoto serrodcal
 +
  anaprarod migtermor paupeddeg fraortmoy marpoldia1
 +
  danrodcha manmorjim1 jeamacpov marcarmor13*)
 
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
 
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
−
   "estaEn _ [] = False"
+
   "estaEn _ []     = False"
 
| "estaEn x (a#xs) = ((a = x) ∨ (estaEn x xs))"
 
| "estaEn x (a#xs) = ((a = x) ∨ (estaEn x xs))"
  
Línea 25: Línea 27:
 
value "estaEn (1::nat) [3,2,4] = False"
 
value "estaEn (1::nat) [3,2,4] = False"
  
−
(* ivamenjim *)
+
(* ivamenjim ferrenseg josgarsan juacabsou dancorgar pabrodmac lucnovdos
 +
  fracorjim1 antsancab1 *)  
 
(* Igual que la anterior pero con x en lugar de _ en el caso base *)
 
(* Igual que la anterior pero con x en lugar de _ en el caso base *)
−
 
 
fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
 
fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
−
   "estaEn1 x [] = False"  
+
   "estaEn1 x []     = False"  
 
| "estaEn1 x (a#xs) = ((x=a) ∨ estaEn1 x xs)"
 
| "estaEn1 x (a#xs) = ((x=a) ∨ estaEn1 x xs)"
  
 
value "estaEn1 (2::nat) [3,2,4] = True"
 
value "estaEn1 (2::nat) [3,2,4] = True"
 
value "estaEn1 (1::nat) [3,2,4] = False"
 
value "estaEn1 (1::nat) [3,2,4] = False"
 +
 +
(* wilmorort *)
 +
(* reutilizando  la funcion "algunos" de R4.thy*)
 +
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
 +
  "algunos p []    = False"
 +
| "algunos p (x#xs) = (p x ∨ algunos p xs)"
 +
 +
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 {*  
 
text {*  
Línea 46: Línea 61:
 
*}
 
*}
  
−
(* crigomgom rubgonmar ivamenjim *)
+
(* crigomgom rubgonmar ivamenjim wilmorort bowma pablucoto
 +
  serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1
 +
  ferrenseg josgarsan danrodcha manmorjim1 juacabsou dancorgar
 +
  pabrodmac lucnovdos jeamacpov marcarmor13 antsancab1 *)  
 
fun sinDuplicados :: "'a list ⇒ bool" where
 
fun sinDuplicados :: "'a list ⇒ bool" where
−
   "sinDuplicados [] = True"
+
   "sinDuplicados []     = True"
 
| "sinDuplicados (x#xs) = (¬ estaEn x xs ∧ sinDuplicados xs)"
 
| "sinDuplicados (x#xs) = (¬ estaEn x xs ∧ sinDuplicados xs)"
  
Línea 54: Línea 72:
 
value "sinDuplicados [1::nat,4,2,4] = False"
 
value "sinDuplicados [1::nat,4,2,4] = False"
  
 +
(* fracorjim1 - La versión anterior no prueba el segundo enunciado. La
 +
  que propongo demuestra ambos. *)
 +
fun sinDuplicados1 :: "'a list ⇒ bool" where
 +
  "sinDuplicados1 [] = True"
 +
| "sinDuplicados1 (x#xs) = (¬(estaEn x xs ∧ sinDuplicados xs))"
  
 +
value "sinDuplicados1 [1::nat,4,2]  = True"
 +
value "sinDuplicados1 [1::nat,4,2,4] = False"
 +
 +
(* Comentario: La definición sinDuplicados1 no cumple el segundo
 +
  ejemplo. *)
 +
 +
(* paupeddeg *)
 +
(* Utilizando la función ∉ de Isabelle *)
 +
fun sinDuplicados2 :: "'a list ⇒ bool" where
 +
  "sinDuplicados2 [] = True"
 +
| "sinDuplicados2 (a#xs) = ((a ∉ set xs) ∧  sinDuplicados2 xs ) "
 +
 +
(* Comentario: Uso de ∉ y set *)
  
 
text {*  
 
text {*  
Línea 69: Línea 105:
 
*}
 
*}
  
−
(* crigomgom rubgonmar *)
+
(* crigomgom rubgonmar wilmorort bowma pablucoto serrodcal
 +
  anaprarod migtermor paupeddeg fraortmoy marpoldia1 ferrenseg
 +
  josgarsan danrodcha juacabsou dancorgar manmorjim1 pabrodmac
 +
  lucnovdos jeamacpov marcarmor13 antsancab1 *)  
 
fun borraDuplicados :: "'a list ⇒ 'a list" where
 
fun borraDuplicados :: "'a list ⇒ 'a list" where
−
   "borraDuplicados [] = []"
+
   "borraDuplicados []     = []"
−
| "borraDuplicados (x#xs) =( if estaEn x xs then borraDuplicados xs else x#borraDuplicados xs)"
+
| "borraDuplicados (x#xs) = (if estaEn x xs  
 +
                            then borraDuplicados xs  
 +
                            else x#borraDuplicados xs)"
 +
 
 +
value "borraDuplicados0 [1::nat,2,4,2,3] = [1,4,2,3]"
 +
 
 +
(* 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 )"
 +
 
 +
value "borraDuplicados1 [1::nat,2,4,2,3] = [1,4,2,3]"
 +
 
 +
(* 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]"
+
value "borraDuplicados2 [1::nat,2,4,2,3] = [1,4,2,3]"
  
 
(* ivamenjim *)
 
(* ivamenjim *)
 
(* Utilizando la negación primero *)
 
(* Utilizando la negación primero *)
 +
fun borraDuplicados3 :: "'a list ⇒ 'a list" where
 +
  "borraDuplicados3 []    = []"
 +
| "borraDuplicados3 (x#xs) = (if ¬(estaEn x xs)
 +
                              then (x#(borraDuplicados3 xs))
 +
                              else borraDuplicados3 xs)"
  
−
fun borraDuplicados :: "'a list ⇒ 'a list" where
+
value "borraDuplicados3 [1::nat,2,4,2,3] = [1,4,2,3]"
−
   "borraDuplicados [] = []"
+
 
−
| "borraDuplicados (x#xs) = (if ¬(estaEn x xs) then (x#(borraDuplicados xs)) else borraDuplicados xs)"
+
(* fracorjim1. Utilizo un acumulador para optimizar la eficiencia *)
 +
fun borraDuplicadosAc :: "'a list ⇒ 'a list ⇒ 'a list" where
 +
   "borraDuplicadosAc [] ys = ys"
 +
| "borraDuplicadosAc (x#xs) ys = (if (estaEn x ys)
 +
                                  then (borraDuplicadosAc xs ys)
 +
                                  else (borraDuplicadosAc xs (x#ys)))"
 +
 
 +
(* fracorjim1. Uso un caso base *)
 +
fun borraDuplicados4 :: "'a list ⇒ 'a list" where
 +
  "borraDuplicados4 xs = (if (sinDuplicados xs)  
 +
                          then xs
 +
                          else borraDuplicadosAc xs [])"
  
−
value "borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]"
+
value "borraDuplicados4 [1::nat,2,4,2,3] = [1,4,2,3]"
  
 +
(* Comentario: Falla en el ejemplo anterior. Su valor es [3,4,2,1] *)
 +
                         
 
text {*
 
text {*
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
Línea 92: Línea 174:
 
*}
 
*}
  
−
-- "La demostración automática es"
+
(* crigomgom anaprarod ferrenseg *)
−
(*crigomgom*)
 
 
lemma length_borraDuplicados:
 
lemma length_borraDuplicados:
 
   "length (borraDuplicados xs) ≤ length xs"
 
   "length (borraDuplicados xs) ≤ length xs"
 
by (induct xs, simp_all)
 
by (induct xs, simp_all)
  
−
(* rubgonmar *)
+
(* Comentario: Falla para borraDuplicados1. *)
−
lemma length_borraDuplicados:
+
 
 +
(* rubgonmar wilmorort pablucoto serrodcal migtermor paupeddeg
 +
  fraortmoy marpoldia1 danrodcha juacabsou dancorgar josgarsan
 +
  pabrodmac lucnovdos antsancab1 *)  
 +
lemma length_borraDuplicados2:
 
   "length ( borraDuplicados xs ) ≤ length xs"
 
   "length ( borraDuplicados xs ) ≤ length xs"
 
by (induct xs) auto
 
by (induct xs) auto
 +
 +
(* manmorjim1 marcarmor13 *)
 +
(* soy de ponerlo mejor por pasos *)
 +
lemma length_borraDuplicados3:
 +
  "length ( borraDuplicados xs ) ≤ length xs"
 +
apply (induct xs)
 +
apply auto
 +
done
  
 
(* ivamenjim *)
 
(* ivamenjim *)
 
(* Demostrando objetivo a objetivo *)
 
(* Demostrando objetivo a objetivo *)
−
lemma length_borraDuplicados:
+
lemma length_borraDuplicados4:
 
   "length (borraDuplicados xs) ≤ length xs"
 
   "length (borraDuplicados xs) ≤ length xs"
 
apply (induct xs)
 
apply (induct xs)
Línea 111: Línea 204:
 
apply auto
 
apply auto
 
done
 
done
 +
 +
(* bowma anaprarod *)
 +
lemma length_borraDuplicados5:
 +
  "length (borraDuplicados xs) ≤ length xs"
 +
apply (induct xs)
 +
apply (simp, simp)  (* creo que es mejor poner aquí simp_all *)
 +
done
 +
 +
(* ferrenseg *)
 +
lemma length_borraDuplicados6:
 +
  "length (borraDuplicados xs) ≤ length xs"
 +
by (induct xs) simp_all (* Creo que se puede poner simp_all fuera de
 +
                          paréntesis *)
  
 
text {*
 
text {*
Línea 119: Línea 225:
 
*}
 
*}
  
−
-- "La demostración estructurada es"
 
 
(* crigomgom *)
 
(* crigomgom *)
 
lemma length_borraDuplicados_2:  
 
lemma length_borraDuplicados_2:  
Línea 131: Línea 236:
 
   proof (cases)
 
   proof (cases)
 
     assume "estaEn x xs"
 
     assume "estaEn x xs"
−
     then have "length (borraDuplicados (x#xs)) = length (borraDuplicados xs)" by simp
+
     then have "length (borraDuplicados (x#xs)) =  
 +
              length (borraDuplicados xs)" by simp
 
     also have "...  ≤ length xs" using HI by simp
 
     also have "...  ≤ length xs" using HI by simp
 
     also have "... ≤ length (x#xs)" by simp
 
     also have "... ≤ length (x#xs)" by simp
−
     finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)" by simp
+
     finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"  
 +
      by simp
 
   next
 
   next
 
     assume "(¬ estaEn x xs)"
 
     assume "(¬ estaEn x xs)"
−
     then have "length (borraDuplicados (x#xs)) = length (x#borraDuplicados xs)" by simp
+
     then have "length (borraDuplicados (x#xs)) =  
 +
              length (x#borraDuplicados xs)" by simp
 
     also have "... = 1 +  length (borraDuplicados xs)" by simp
 
     also have "... = 1 +  length (borraDuplicados xs)" by simp
 
     also have "...  ≤ 1 + length xs" using HI by simp
 
     also have "...  ≤ 1 + length xs" using HI by simp
 
     also have "... = length (x#xs)" by simp
 
     also have "... = length (x#xs)" by simp
−
     finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"  by simp
+
     finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"   
 +
      by simp
 
   qed
 
   qed
 
qed
 
qed
  
−
(* ivamenjim *)
+
(* ivamenjim wilmorort ferrenseg rubgonmar juacabsou dancorgar
−
lemma length_borraDuplicados_2:  
+
  josgarsan lucnovdos *)  
 +
lemma length_borraDuplicados_2b:  
 
   "length (borraDuplicados xs) ≤ length xs"
 
   "length (borraDuplicados xs) ≤ length xs"
 
proof (induct xs)
 
proof (induct xs)
Línea 153: Línea 263:
 
   fix a xs
 
   fix a xs
 
   assume HI: "length (borraDuplicados xs) ≤ length xs"
 
   assume HI: "length (borraDuplicados xs) ≤ length xs"
−
   have "length (borraDuplicados (a # xs)) ≤ 1+length (borraDuplicados xs)" by simp
+
   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 danrodcha *)
 +
lemma length_borraDuplicados_2c:
 +
  "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 jeamacpov marcarmor13*)
 +
lemma length_borraDuplicados_2d:
 +
  "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_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
 
   also have "... ≤ 1+length xs" using HI by simp
−
   finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" 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
 +
 
 +
(* Comentario: Responder la pregunta. *)
 +
 
 +
(* migtermor *)
 +
lemma length_borraDuplicados_2g:
 +
  "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 pabrodmac*)
 +
lemma length_borraDuplicados_2h:
 +
  "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í más pasos *)
 +
lemma length_borraDuplicados_2i:
 +
  "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
 +
 
 +
(* antsancab1 *)
 +
(* En este ejercicio probé a mantener el elemento 'a' dentro del métodos length y funciona
 +
Para no tener que hacer 1 + length xs *)
 +
(* Duda:
 +
¿Por qué aparece este mensaje en Isabelle al asumir la hipótesis de inducción?
 +
Introduced fixed type variable(s): 'b in "xsa__" *)
 +
 
 +
lemma length_borraDuplicados_2j: "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 # borraDuplicados (xs))" by simp
 +
  also have "... ≤ length (a # xs)" using HI by simp
 +
   finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs) " by simp
 
qed
 
qed
 +
  
 
text {*
 
text {*
Línea 165: Línea 407:
 
*}
 
*}
  
−
-- "La demostración automática es"
+
(* crigomgom rubgonmar wilmorort pablucoto serrodcal bowma
−
(* crigomgom rubgonmar *)
+
  migtermor fraortmoy marpoldia1 ferrenseg danrodcha  juacabsou
 +
  paupeddeg pabrodmac lucnovdos dancorgar jeamacpov marcarmor13 antsancab1 *)
 
lemma estaEn_borraDuplicados:  
 
lemma estaEn_borraDuplicados:  
 
   "estaEn a (borraDuplicados xs) = estaEn a xs"
 
   "estaEn a (borraDuplicados xs) = estaEn a xs"
 
by (induct xs) auto
 
by (induct xs) auto
  
−
(* ivamenjim *)
+
(* ivamenjim manmorjim1 *)
−
lemma estaEn_borraDuplicados:  
+
lemma estaEn_borraDuplicados2:  
 
   "estaEn a (borraDuplicados xs) = estaEn a xs"
 
   "estaEn a (borraDuplicados xs) = estaEn a xs"
 
apply (induct xs)  
 
apply (induct xs)  
Línea 178: Línea 421:
 
done
 
done
  
 +
(* anaprarod *)
 +
lemma estaEn_borraDuplicados3:
 +
  "estaEn a (borraDuplicados xs) = estaEn a xs"
 +
by (induct xs, simp_all, blast)
 +
 +
(* anaprarod *)
 +
lemma estaEn_borraDuplicados4:
 +
  "estaEn a (borraDuplicados xs) = estaEn a xs"
 +
apply (induct xs)
 +
apply (cases "estaEn x xs")
 +
apply (simp_all)
 +
apply blast
 +
done
 +
 +
(* bowma *)
 +
lemma estaEn_borraDuplicados5:
 +
  "estaEn a (borraDuplicados xs) = estaEn a xs"
 +
apply (induct xs)
 +
apply simp
 +
apply (simp, blast)
 +
done
 +
 
text {*
 
text {*
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
Línea 189: Línea 454:
 
*}
 
*}
  
−
-- "La demostración estructurada es"
+
(* wilmorort *)
 
lemma estaEn_borraDuplicados_2:  
 
lemma estaEn_borraDuplicados_2:  
 
   "estaEn a (borraDuplicados xs) = estaEn a xs"
 
   "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
 +
 +
(* Comentario: Tiene pasos incompletos.*)
 +
 +
(* anaprarod marpoldia1 ferrenseg juacabsou *)
 +
lemma estaEn_borraDuplicados_2b:
 +
"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_2c:
 +
  "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 paupeddeg pabrodmac marcarmor13*)
 +
lemma estaEn_borraDuplicados_2d:
 +
  "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 jeamacpov *)
 +
lemma estaEn_borraDuplicados_2e:
 +
  "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"
 +
      then show "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 ivamenjim *)
 +
lemma estaEn_borraDuplicados_2f:
 +
  "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
 
oops
 
oops
 +
 +
(* Comentario: Demostración incompleta. *)
 +
 +
(* danrodcha pablucoto *)
 +
(* es como la de ruben pero con diferencias de estilo *)
 +
lemma estaEn_borraDuplicados_2g:
 +
  "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 (rule iffI)
 +
    assume H1: "estaEn a (borraDuplicados (x # xs))"
 +
    show "estaEn a (x#xs)"
 +
    proof (cases "estaEn x xs")
 +
      case True
 +
      then show "estaEn a (x#xs)" using H1 HI by simp
 +
    next
 +
      case False
 +
      then show "estaEn a (x#xs)" using H1 HI by simp
 +
    qed
 +
    next
 +
    assume H2: "estaEn a (x#xs)"
 +
    show "estaEn a (borraDuplicados (x # xs))"
 +
    proof (cases "x=a")
 +
      case True
 +
      then show "estaEn a (borraDuplicados (x # xs))" using HI by simp
 +
    next
 +
      case False
 +
      then show "estaEn a (borraDuplicados (x # xs))" using H2 HI
 +
        by simp
 +
    qed
 +
  qed
 +
qed
  
 
text {*
 
text {*
Línea 201: Línea 724:
 
*}
 
*}
  
−
-- "La demostración automática"
+
(* ivamenjim wilmorort serrodcal crigomgom anaprarod fraortmoy
−
 
+
  marpoldia1 ferrenseg danrodcha juacabsou paupeddeg josgarsan
−
(* ivamenjim *)
+
  pabrodmac dancorgar jeamacpov rubgonmar marcarmor13 *)  
 
lemma sinDuplicados_borraDuplicados:
 
lemma sinDuplicados_borraDuplicados:
 
   "sinDuplicados (borraDuplicados xs)"
 
   "sinDuplicados (borraDuplicados xs)"
 
by (induct xs) (auto simp add: estaEn_borraDuplicados)
 
by (induct xs) (auto simp add: estaEn_borraDuplicados)
  
 +
(* migtermor bowma *)
 +
lemma sinDuplicados_borraDuplicados_2:
 +
  "sinDuplicados (borraDuplicados xs)"
 +
by (induct xs, simp_all add: estaEn_borraDuplicados_2)
 +
 +
(* manmorjim1 no caí en usar la demostración anterior y he realizado
 +
  la demostración de que si un elemento no estaba en una lista seguirá
 +
  sin estar después de eliminar los duplicados en esa lista... *)
 +
lemma noEsta_tras_borrarDuplicados:
 +
  "(¬estaEn x xs) ⟶ (¬estaEn x (borraDuplicados xs))"
 +
apply (induct xs)
 +
apply auto
 +
done
 +
 +
lemma sinDuplicados_borraDuplicados_3:
 +
  "sinDuplicados (borraDuplicados xs)"
 +
apply (induct xs)
 +
apply simp
 +
apply (induct xs)
 +
apply auto
 +
apply (simp add: noEsta_tras_borrarDuplicados)
 +
done
 +
 +
(* antsancab1 *)
 +
lemma sinDuplicados_borraDuplicados_4:
 +
  "sinDuplicados (borraDuplicados xs)"
 +
apply (induct xs)
 +
apply simp
 +
apply (simp add:estaEn_borraDuplicados)
 +
done
  
 
text {*
 
text {*
Línea 216: Línea 769:
 
*}
 
*}
  
−
-- "La demostración estructurada es"
+
(* wilmorort pablucoto marcarmor13*)
−
lemma sinDuplicados_borraDuplicados_2:
+
lemma sinDuplicados_borraDuplicados_2a:
 +
  "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 marpoldia1
 +
  ferrenseg bowma juacabsou serrodcal josgarsan pabrodmac dancorgar
 +
  jeamacpov lucnovdos antsancab1 *) 
 +
lemma sinDuplicados_borraDuplicados_2b:
 
   "sinDuplicados (borraDuplicados xs)"
 
   "sinDuplicados (borraDuplicados xs)"
−
oops
+
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 paupeddeg*)
 +
lemma sinDuplicados_borraDuplicados_2c:
 +
  "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
 +
 
 +
(* danrodcha *)
 +
lemma sinDuplicados_borraDuplicados_2d:
 +
  "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 "estaEn x xs")
 +
    case True
 +
    then have 1: "sinDuplicados (borraDuplicados (x#xs))
 +
                = sinDuplicados (borraDuplicados xs)"
 +
      by (simp add: estaEn_borraDuplicados_2)
 +
    show "?P (x#xs)" using HI 1 by simp
 +
    next
 +
    case False
 +
    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 "… = True"  using `¬ estaEn x xs`
 +
      using HI by (simp add:estaEn_borraDuplicados)
 +
    finally show "?P (x#xs)" by simp
 +
  qed
 +
qed
  
 
text {*
 
text {*
Línea 228: Línea 874:
 
*}
 
*}
  
−
(*crigomgom rubgonmar ivamenjim *)
+
(* crigomgom rubgonmar ivamenjim wilmorort pablucoto migtermor
 +
  anaprarod fraortmoy ferrenseg marpoldia1 bowma danrodcha juacabsou
 +
  paupeddeg manmorjim1 serrodcal josgarsan pabrodmac lucnovdos
 +
  dancorgar jeamacpov marcarmor13 antsancab1 *)  
 
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
 
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
 
quickcheck
 
quickcheck

Revisión actual del 13:11 16 jul 2018

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
   danrodcha manmorjim1 jeamacpov marcarmor13*)
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 josgarsan juacabsou dancorgar pabrodmac lucnovdos
   fracorjim1 antsancab1 *)    
(* 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 algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p []     = False"
| "algunos p (x#xs) = (p x ∨ algunos p xs)"

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 josgarsan danrodcha manmorjim1 juacabsou dancorgar
   pabrodmac lucnovdos jeamacpov marcarmor13 antsancab1 *) 
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"

(* fracorjim1 - La versión anterior no prueba el segundo enunciado. La
   que propongo demuestra ambos. *) 
fun sinDuplicados1 :: "'a list ⇒ bool" where
  "sinDuplicados1 [] = True"
| "sinDuplicados1 (x#xs) = (¬(estaEn x xs ∧ sinDuplicados xs))"

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

(* Comentario: La definición sinDuplicados1 no cumple el segundo
   ejemplo. *) 

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

(* Comentario: Uso de ∉ y set *)

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 
   josgarsan danrodcha juacabsou dancorgar manmorjim1 pabrodmac
   lucnovdos jeamacpov marcarmor13 antsancab1 *) 
fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados []     = []"
| "borraDuplicados (x#xs) = (if estaEn x xs 
                             then borraDuplicados xs 
                             else x#borraDuplicados xs)"

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

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

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

(* 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 "borraDuplicados2 [1::nat,2,4,2,3] = [1,4,2,3]"

(* ivamenjim *)
(* Utilizando la negación primero *)
fun borraDuplicados3 :: "'a list ⇒ 'a list" where
  "borraDuplicados3 []     = []"
| "borraDuplicados3 (x#xs) = (if ¬(estaEn x xs) 
                              then (x#(borraDuplicados3 xs)) 
                              else borraDuplicados3 xs)"

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

(* fracorjim1. Utilizo un acumulador para optimizar la eficiencia *)
fun borraDuplicadosAc :: "'a list ⇒ 'a list ⇒ 'a list" where
  "borraDuplicadosAc [] ys = ys"
| "borraDuplicadosAc (x#xs) ys = (if (estaEn x ys) 
                                  then (borraDuplicadosAc xs ys)
                                  else (borraDuplicadosAc xs (x#ys)))"

(* fracorjim1. Uso un caso base *)
fun borraDuplicados4 :: "'a list ⇒ 'a list" where
  "borraDuplicados4 xs = (if (sinDuplicados xs) 
                          then xs 
                          else borraDuplicadosAc xs [])"

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

(* Comentario: Falla en el ejemplo anterior. Su valor es [3,4,2,1] *)
                          
text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
*}

(* crigomgom anaprarod ferrenseg *)
lemma length_borraDuplicados:
  "length (borraDuplicados xs) ≤ length xs"
by (induct xs, simp_all)

(* Comentario: Falla para borraDuplicados1. *)

(* rubgonmar wilmorort pablucoto serrodcal migtermor paupeddeg 
   fraortmoy marpoldia1 danrodcha juacabsou dancorgar josgarsan
   pabrodmac lucnovdos antsancab1 *) 
lemma length_borraDuplicados2:
  "length ( borraDuplicados xs ) ≤ length xs"
by (induct xs) auto

(* manmorjim1 marcarmor13 *)
(* soy de ponerlo mejor por pasos *)
lemma length_borraDuplicados3:
  "length ( borraDuplicados xs ) ≤ length xs"
apply (induct xs)
apply auto
done

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

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

(* ferrenseg *)
lemma length_borraDuplicados6:
  "length (borraDuplicados xs) ≤ length xs"
by (induct xs) simp_all (* Creo que se puede poner simp_all fuera de
                           paréntesis *) 

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

(* 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 rubgonmar juacabsou dancorgar
   josgarsan lucnovdos *) 
lemma length_borraDuplicados_2b: 
  "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 danrodcha *)
lemma length_borraDuplicados_2c: 
  "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 jeamacpov marcarmor13*)
lemma length_borraDuplicados_2d: 
  "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_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

(* Comentario: Responder la pregunta. *)

(* migtermor *)
lemma length_borraDuplicados_2g: 
  "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 pabrodmac*)
lemma length_borraDuplicados_2h:
  "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í más pasos *)
lemma length_borraDuplicados_2i: 
  "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

(* antsancab1 *)
(* En este ejercicio probé a mantener el elemento 'a' dentro del métodos length y funciona
Para no tener que hacer 1 + length xs *)
(* Duda:
¿Por qué aparece este mensaje en Isabelle al asumir la hipótesis de inducción?
Introduced fixed type variable(s): 'b in "xsa__" *)

lemma length_borraDuplicados_2j: "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 # borraDuplicados (xs))" by simp
  also have "... ≤ length (a # 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
  --------------------------------------------------------------------- 
*}

(* crigomgom rubgonmar  wilmorort pablucoto serrodcal bowma 
   migtermor fraortmoy marpoldia1 ferrenseg danrodcha  juacabsou
   paupeddeg pabrodmac lucnovdos dancorgar jeamacpov marcarmor13 antsancab1 *)
lemma estaEn_borraDuplicados: 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto

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

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

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

(* bowma *)
lemma estaEn_borraDuplicados5: 
  "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
  --------------------------------------------------------------------- 
*}

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

(* Comentario: Tiene pasos incompletos.*)

(* anaprarod marpoldia1 ferrenseg juacabsou *)
lemma estaEn_borraDuplicados_2b:
 "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_2c: 
  "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 paupeddeg pabrodmac marcarmor13*)
lemma estaEn_borraDuplicados_2d: 
  "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 jeamacpov *)
lemma estaEn_borraDuplicados_2e: 
  "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"
       then show "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 ivamenjim *)
lemma estaEn_borraDuplicados_2f: 
  "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
oops

(* Comentario: Demostración incompleta. *)

(* danrodcha pablucoto *)
(* es como la de ruben pero con diferencias de estilo *)
lemma estaEn_borraDuplicados_2g: 
  "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 (rule iffI)
    assume H1: "estaEn a (borraDuplicados (x # xs))"
    show "estaEn a (x#xs)"
    proof (cases "estaEn x xs")
      case True
      then show "estaEn a (x#xs)" using H1 HI by simp
    next
      case False
      then show "estaEn a (x#xs)" using H1 HI by simp
    qed
    next
    assume H2: "estaEn a (x#xs)"
    show "estaEn a (borraDuplicados (x # xs))"
    proof (cases "x=a")
      case True
      then show "estaEn a (borraDuplicados (x # xs))" using HI by simp
    next
      case False
      then show "estaEn a (borraDuplicados (x # xs))" using H2 HI 
        by simp
    qed
  qed
qed

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

(* ivamenjim wilmorort serrodcal crigomgom anaprarod fraortmoy 
   marpoldia1 ferrenseg danrodcha juacabsou paupeddeg josgarsan
   pabrodmac dancorgar jeamacpov rubgonmar marcarmor13 *) 
lemma sinDuplicados_borraDuplicados:
  "sinDuplicados (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)

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

(* manmorjim1 no caí en usar la demostración anterior y he realizado
   la demostración de que si un elemento no estaba en una lista seguirá
   sin estar después de eliminar los duplicados en esa lista... *)
lemma noEsta_tras_borrarDuplicados:
  "(¬estaEn x xs) ⟶ (¬estaEn x (borraDuplicados xs))"
apply (induct xs)
apply auto
done

lemma sinDuplicados_borraDuplicados_3:
  "sinDuplicados (borraDuplicados xs)"
apply (induct xs)
apply simp
apply (induct xs)
apply auto
apply (simp add: noEsta_tras_borrarDuplicados)
done

(* antsancab1 *)
lemma sinDuplicados_borraDuplicados_4:
  "sinDuplicados (borraDuplicados xs)"
apply (induct xs)
apply simp
apply (simp add:estaEn_borraDuplicados)
done

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

(* wilmorort pablucoto marcarmor13*)
lemma sinDuplicados_borraDuplicados_2a:
  "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 marpoldia1
   ferrenseg bowma juacabsou serrodcal josgarsan pabrodmac dancorgar
   jeamacpov lucnovdos antsancab1 *)  
lemma sinDuplicados_borraDuplicados_2b:
  "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 paupeddeg*)
lemma sinDuplicados_borraDuplicados_2c:
  "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

(* danrodcha *)
lemma sinDuplicados_borraDuplicados_2d:
  "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 "estaEn x xs")
    case True
    then have 1: "sinDuplicados (borraDuplicados (x#xs)) 
                 = sinDuplicados (borraDuplicados xs)" 
      by (simp add: estaEn_borraDuplicados_2)
    show "?P (x#xs)" using HI 1 by simp
    next
    case False
    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 "… = True"  using `¬ estaEn x xs` 
      using HI by (simp add:estaEn_borraDuplicados)
    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 ferrenseg marpoldia1 bowma danrodcha juacabsou
   paupeddeg manmorjim1 serrodcal josgarsan pabrodmac lucnovdos
   dancorgar jeamacpov marcarmor13 antsancab1 *) 
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
Obtenido de «https://www.glc.us.es/~jalonso/RA2016/index.php?title=Relación_5&oldid=1473»