Relación 4

chapter {* R4: Cuantificadores sobre listas *}

theory R4_Cuantificadores_sobre_listas
imports Main 
begin

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función 
     todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (todos p xs) se verifica si todos los elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     todos (λx. 1<length x) [[2,1,4],[1,3]]
     ¬todos (λx. 1<length x) [[2,1,4],[3]]

  Nota: La función todos es equivalente a la predefinida list_all. 
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon alfmarcua josgomrom4 aribatval cammonagu
   raffergon2 enrparalv gleherlop chrgencar benber giafus1 pabbergue 
   alikan marfruman1 antramhur juacanrod hugrubsan *) 
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p [] = True" |
  "todos p (x#xs) = (p x ∧ todos p xs)"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función 
     algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (algunos p xs) se verifica si algunos elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     algunos (λx. 1<length x) [[2,1,4],[3]]
     ¬algunos (λx. 1<length x) [[],[3]]"

  Nota: La función algunos es equivalente a la predefinida list_ex. 
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon alfmarcua josgomrom4 cammonagu aribatval
   raffergon2 enrparalv gleherlop chrgencar benber giafus1 pabbergue
   alikan marfruman1 antramhur juacanrod hugrubsan *) 
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = False" |
  "algunos p (x#xs) = (p x ∨ algunos p xs)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar o refutar automáticamente 
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon alfmarcua josgomrom4 cammonagu raffergon2
   enrparalv gleherlop chrgencar benber giafus1 pabbergue alikan 
   marfruman1 antramhur juacanrod hugrubsan aribatval *) 
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.2. Demostrar o refutar detalladamente
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}

(* pabalagon *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P P Q xs")
proof (induct xs)
  fix P Q
  show "?P P Q []" by simp
next
  fix a xs
  assume HI: "?P P Q xs"
  have "todos (λx. P x ∧ Q x) (a#xs) = 
        ((P a ∧ Q a) ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" 
    using HI by simp
  also have "... = ((P a ∧ todos P xs) ∧ (Q a ∧ todos Q xs))" 
    by (simp add: HOL.conj_comms)
  also have "... = (todos P (a#xs) ∧ (Q a ∧ todos Q xs))" by simp
  finally show "todos (λx. P x ∧ Q x) (a#xs) = 
                (todos P (a#xs) ∧ todos Q (a#xs))" by simp
qed

(* alfmarcua juacanrod *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" (is "?P xs")
proof (induct xs)
  have "todos (λx. P x ∧ Q x) [] = (True)" 
    by (simp only: todos.simps(1))
  also have "... = (True ∧ True)" by (simp only: conj_absorb)
  also have "... = (todos P [] ∧ todos Q [])" 
    by (simp only: todos.simps(1))
  finally show "?P []" .
next
  fix x xs
  assume HI: "?P xs"
  have "todos (λx. P x ∧ Q x) (x # xs) = 
        ((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs)"
    by (simp only: todos.simps(2))
  also have "... = ((P x ∧ Q x) ∧  (todos P xs ∧ todos Q xs))" 
    by (simp only: HI)
  also have "... = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" 
    by (simp only: HOL.conj_comms)
  also have "... = (todos P (x # xs) ∧ todos Q (x # xs))" 
    by (simp only: todos.simps(2))
  finally show "?P (x#xs)" .
qed

(* manperjim josgomrom4 raffergon2 cammonagu enrparalv gleherlop
   chrgencar giafus1 pabbergue alikan marfruman1 antramhur hugrubsan
   aribatval *)  
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
  show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
  fix n xs
  assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)" 
  have "todos (λx. P x ∧ Q x) (n # xs) =  
        ((P n ∧ Q n) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
  also have "... = ((P n ∧ todos P xs) ∧ (Q n ∧ todos Q xs))" by arith
  also have "... = ((todos P(n#xs)) ∧ (todos Q(n#xs)))" by simp
 finally show "todos (λx. P x ∧ Q x) (n#xs) = 
               (todos P (n#xs) ∧ todos Q (n#xs))" by simp 
qed

(* benber *)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
  case Nil
  have "todos (λx. P x ∧ Q x) [] = True" by (simp only: todos.simps(1))
  also have "... = (todos P [] ∧ todos Q [])" 
    by (simp only: todos.simps(1) conj_absorb)
  finally show ?case.
next
  case (Cons x xs)
  assume IH: "todos (λy. P y ∧ Q y) xs = (todos P xs ∧ todos Q xs)"
  have "todos (λy. P y ∧ Q y) (x # xs) = 
       ( (P x ∧ Q x) ∧ todos (λy. P y ∧ Q y) xs )"
    by (simp only: todos.simps(2))
  also have "... = ( (P x ∧ Q x) ∧ todos P xs ∧ todos Q xs )" 
    by (simp only: IH)
  also have "... = ( P x ∧ (Q x ∧ todos P xs) ∧ todos Q xs )" 
    by (simp only: conj_assoc)
  also have "... = ( P x ∧ (todos P xs ∧ Q x) ∧ todos Q xs )" 
    by (simp only: conj_commute)
  also have "... = ( (P x ∧ todos P xs) ∧ Q x ∧ todos Q xs )" 
    by (simp only: conj_assoc)
  also have "... = ( todos P (x#xs) ∧ todos Q (x#xs) )" 
    by (simp only: todos.simps(2))
  finally show ?case.
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon alfmarcua josgomrom4 aritbatval cammonagu
   raffergon2 enrparalv benber gleherlop chrgencar giafus1 pabbergue
   alikan marfruman1 antramhur juacanrod hugrubsan aribatval *) 
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
  by (induct x) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.2. Demostrar o refutar detalladamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 raffergon2 cammonagu enrparalv
   gleherlop chrgencar giafus1 pabbergue alikan antramhur juacanrod
   hugrubsan *)  
lemma todos_append:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
  show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
  fix a x
  assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
  have "todos P ((a#x) @ y) = (P a ∧ todos P (x @ y))" by simp
  also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
  finally show "todos P ((a#x) @ y) = (todos P (a#x) ∧ todos P y)" 
    by simp
qed

(* alfmarcua marfruman1 *)
lemma todos_append_2:
  "todos P (x @ y) = (todos P x ∧ todos P y)" (is "?P x")
proof (induct x)
  have "todos P ([] @ y) = todos P y" by (simp only: append_Nil)
  also have "... = (True ∧ todos P y)" by (simp only: simp_thms(22))
  also have "... = (todos P [] ∧ todos P y)" 
    by (simp only: todos.simps(1))
  finally show "?P []" .
next
  fix a x
  assume HI:"?P x"
  have "todos P ((a # x) @ y) = todos P (a # (x @ y))"
    by (simp only:List.append.append_Cons)
  also have "... = (P a ∧ todos P (x @ y))" 
    by (simp only: todos.simps(2))
  also have "... = (P a ∧ todos P x ∧ todos P y)" by (simp only:HI)
  also have "... = ((P a ∧ todos P x) ∧ todos P y)"  
    by (simp only:HOL.conj_assoc)
  also have "... = (todos P (a#x) ∧ todos P y)" 
    by (simp only: todos.simps(2))
  finally show "?P (a#x)" .
qed

(* benber *)
lemma todos_append_3:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x )
  case Nil
  have "todos P ( [] @ y ) = todos P y" 
    by (simp only: List.append.left_neutral)
  also have "... = (todos P [] ∧ todos P y)" 
    by (simp only: todos.simps(1) simp_thms(22))
  finally show ?case.
next
  case (Cons a x)
  assume IH: "todos P (x @ y) = (todos P x ∧ todos P y)"
  have "todos P ((a # x) @ y) = (P a ∧ todos P (x @ y))"
    by (simp only: todos.simps(2) List.append.append_Cons)
  also have "... = (P a ∧ todos P x ∧ todos P y)" by (simp only: IH)
  also have "... = (todos P (a#x) ∧ todos P y)" 
    by (simp only: todos.simps(2) conj_assoc )
  finally show ?case.
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.1. Demostrar o refutar automáticamente 
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua aribatval cammonagu
   raffergon2 giafus1 pabbergue enrparalv alikan antramhur juacanrod
   hugrubsan *)  
lemma "todos P (rev xs) = todos P xs"
  by (induct xs) (simp_all add: HOL.conj_comms todos_append)

(* benber marfruman1*)
lemma "todos P (rev xs) = todos P xs"
  using todos_append by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.2. Demostrar o refutar detalladamente
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 raffergon2 cammonagu gleherlop giafus1
   pabbergue enrparalv marfruman1 alikan chrgencar antramhur juacanrod
   hugrubsan aribatval *)  
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
  show "todos P (rev []) = todos P []" by simp
next
  fix a xs
  assume HI: "todos P (rev xs) = todos P xs"
  have "todos P (rev (a#xs)) = todos P ((rev xs) @ [a])" by simp
  also have "... = (todos P (rev xs) ∧ todos P [a])" 
    by (simp add: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" using HI by simp
  also have "... = (todos P xs ∧ P a)" by simp
  also have "... = (P a ∧ todos P xs)" by (simp add: HOL.conj_comms)
  finally show "todos P (rev (a#xs)) = todos P (a#xs)" by simp
qed

(* alfmarcua *)
lemma "todos P (rev xs) = todos P xs" (is "?P xs")
proof (induct xs)
  show "?P []" by (simp only: rev.simps(1))
next
  fix a xs
  assume HI:"?P xs"
  have "todos P (rev (a # xs)) = todos P (rev xs @ [a])" 
    by (simp only: rev.simps(2))
  also have "... = (todos P (rev xs) ∧ todos P [a])" 
    by (simp only: todos_append)
  also have "... = (todos P xs ∧ todos P [a])" by (simp only: HI)
  also have "... = (todos P (a#[]) ∧ todos P xs)" 
    by (simp only: HOL.conj_comms)
  also have "... = ((P a ∧ True) ∧ todos P xs)" 
    by (simp only: todos.simps)
  also have "... = (P a ∧ todos P xs)"  
    by (simp only: HOL.simp_thms(21))
  also have "... = todos P (a#xs)" by (simp only: todos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
  case Nil
  show "todos P (rev []) = todos P []" by (simp only: rev.simps(1))
next
  case (Cons x xs)
  assume IH: "todos P (rev xs) = todos P xs"
  have "todos P (rev (x#xs)) = todos P (rev xs @ [x])" 
    by (simp only: rev.simps(2))
  also have "... = (todos P (rev xs) ∧ todos P [x] )" 
    by (simp only: todos_append)
  also have "... = (todos P (rev xs) ∧ P x ∧ todos P [])" 
    by (simp only: todos.simps(2))
  also have "... = (todos P (rev xs) ∧ P x)" 
    by (simp only: todos.simps(1) simp_thms(21))
  also have "... = (todos P xs ∧ P x)" by (simp only: IH)
  also have "... = (todos P (x#xs))" 
    by (simp only: todos.simps(2) conj_commute)
  finally show ?case.
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar:
    algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
  --------------------------------------------------------------------- 
*}

(* pabalagon *)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
  nitpick
  oops

(* Contraejemplo *)
value "algunos (λx. even x ∧ odd x) [1, 2::nat] ≠
  algunos even [1, 2::nat] ∧ algunos odd [1, 2::nat]"

(* manperjim alfmarcua raffergon2 gleherlop chrgencar cammonagu giafus1
   pabbergue marfruman1 alikan antramhur juacanrod hugrubsan 
   aribatval *) 
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
  quickcheck
  oops

(* benber (demostración no completa) *)
fun is_zero :: "nat ⇒ bool" where
  "is_zero n = (n = 0)"
fun is_one :: "nat ⇒ bool" where
  "is_one n = (n = 1)"
lemma "¬( ∀P Q xs. algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs) )"
proof -
  let ?P = is_one
  let ?Q = is_zero
  have "algunos (λx. ?P x ∧ ?Q x) [0,1] ≠ 
       (algunos ?P [0,1] ∧ algunos ?Q [0,1])" by simp
  hence "∃ xs. algunos (λx. ?P x ∧ ?Q x) xs ≠ 
         (algunos ?P xs ∧ algunos ?Q xs)" by (simp only: exI)
  hence "∃Q xs. algunos (λx. ?P x ∧ Q x) xs ≠ 
         (algunos ?P xs ∧ algunos Q xs)"
    by  (simp only: exI[of "λQ. ∃ xs. algunos (λx. ?P x ∧ Q x) xs ≠ (algunos ?P xs ∧ algunos Q xs)"])
  hence "∃P Q xs. algunos (λx. P x ∧ Q x) xs ≠ (algunos P xs ∧ algunos Q xs)"
    (*
      No sé por qué esto no funciona:
      by (simp only: exI[of "λP Q xs. algunos (λx. P x ∧ Q x) xs ≠ (algunos P xs ∧ algunos Q xs)" ?P])

      Parece que el problema es la expresión lambda.
    *)
    sorry
  thus ?thesis by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.1. Demostrar o refutar automáticamente 
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop
   cammonagu benber giafus1 pabbergue enrparalv marfruman1 alikan
   antramhur juacanrod hugrubsan aribatval *)  
lemma "algunos P (map f xs) = algunos (P o f) xs"
  by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.2. Demostrar o refutar detalladamente
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon cammonagu giafus1 gleherlop chrgencar pabbergue
   enrparalv marfruman1 alikan antramhur juacanrod hugrubsan *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P ∘ f) []" by simp
next
  fix a xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (a#xs)) = (P (f a) ∨ algunos P (map f xs))" 
    by simp
  also have "... = (P (f a) ∨ algunos (P ∘ f) xs)" using HI by simp
  also have "... = ((P ∘ f) a ∨ algunos (P ∘ f) xs)" by simp
  finally show "algunos P (map f (a#xs)) = algunos (P ∘ f) (a#xs)" 
    by simp
qed

(* josgomrom4 *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  show "algunos P (map f []) = algunos (P o f) []" by simp
next
  fix x xs
  assume HI: "algunos P (map f xs) = algunos (P o f) xs"
  have "algunos P (map f (x#xs)) = (P (f x) ∨ algunos P (map f xs))" 
    by simp
  also have "... = (P (f x) ∨ algunos (P o f) xs)" using HI by simp
  finally show "algunos P (map f (x#xs)) = algunos (P o f) (x#xs)" 
    by simp
qed

(* alfmarcua *)
lemma "algunos P (map f xs) = algunos (P o f) xs" (is "?P xs")
proof (induct xs)
  have "algunos P (map f []) = algunos P []" 
    by (simp only: List.list.map(1))
  also have "... =  algunos (P o f) []" by (simp only: algunos.simps(1))
  finally show "?P []" .
next
  fix a xs
  assume HI:"?P xs"
  have "algunos P (map f (a # xs)) =  algunos P (f a # map f xs)" 
    by (simp only: List.list.map(2))
  also have "... = (P (f a) ∨ algunos P (map f xs))" 
    by (simp only: algunos.simps(2))
  also have "... = (P (f a) ∨ algunos (P o f) xs)" by (simp only:HI)
  also have "... = ((P o f) a ∨ algunos (P o f) xs)" 
    by (simp only: Fun.comp_apply)
  also have "... = algunos (P o f) (a#xs)" by (simp only: algunos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
  case Nil
  have "algunos P (map f []) = algunos P []" by (simp only: list.map(1))
  also have "... = False" by (simp only: algunos.simps(1))
  also have "False = algunos (P ∘ f) []" by (simp only: algunos.simps(1))
  finally show ?case.
next
  case (Cons x xs)
  assume IH: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (x # xs)) = algunos P (f x # map f xs)" 
    by (simp only: list.map(2))
  also have "... = ( (P ∘ f) x ∨ algunos P (map f xs) )" 
    by (simp only: algunos.simps(2) o_apply)
  also have "... = ( (P ∘ f) x ∨ algunos (P ∘ f) xs )" 
    by (simp only: IH)
  also have "... = algunos (P ∘ f) (x#xs)" 
    by (simp only: algunos.simps(2))
  finally show ?case .
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.1. Demostrar o refutar automáticamente 
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
   gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1 
   alikan antramhur juacanrod hugrubsan aribatval *) 
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.2. Demostrar o refutar detalladamente
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 raffergon2 gleherlop cammonagu giafus1
   pabbergue enrparalv marfruman1 alikan antramhur juacanrod hugrubsan *) 
lemma algunos_append:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
  show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
  fix a xs
  assume HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
  have "algunos P ((a#xs) @ ys) = (P a ∨ algunos P (xs @ ys))" by simp
  also have "... = (P a ∨ algunos P xs ∨ algunos P ys)" using HI by simp
  finally show  "algunos P ((a#xs) @ ys) = 
                 (algunos P (a#xs) ∨ algunos P ys)" by simp
qed

(* alfmarcua *)
lemma algunos_append_2:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)" (is "?P xs")
proof (induct xs)
  have "algunos P ([] @ ys) = algunos P ys" by (simp only: append_Nil)
  also have "... = (False ∨ algunos P ys)" by (simp only: simp_thms(32))
  also have "... = (algunos P [] ∨ algunos P ys)" 
    by (simp only: algunos.simps(1))
  finally show "?P []" .
next
  fix a xs
  assume HI:"?P xs"
  have "algunos P ((a # xs) @ ys) = algunos P (a # (xs @ ys))"
    by (simp only:List.append.append_Cons)
  also have "... = (P a ∨ algunos P (xs @ ys))" 
    by (simp only: algunos.simps(2))
  also have "... = (P a ∨ algunos P xs ∨ algunos P ys)" 
    by (simp only:HI)
  also have "... = ((P a ∨ algunos P xs) ∨ algunos P ys)"  
    by (simp only:HOL.disj_assoc)
  also have "... = (algunos P (a#xs) ∨ algunos P ys)" 
    by (simp only: algunos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma algunos_append_3:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
  case Nil
  have "algunos P ([] @ ys) = algunos P ys" 
    by (simp only: append.left_neutral)
  also have "... = ( algunos P [] ∨ algunos P ys )" 
    by (simp only: algunos.simps(1) simp_thms(32))
  finally show ?case .
next
  case (Cons x xs)
  assume IH: "algunos P (xs @ ys) = ( algunos P xs ∨ algunos P ys )"
  have "algunos P ((x#xs) @ ys) = algunos P (x#(xs @ ys))" 
    by (simp only: append_Cons)
  also have "... = ( P x ∨ algunos P (xs @ ys) )" 
    by (simp only: algunos.simps(2))
  also have "... = ( P x ∨ algunos P xs ∨ algunos P ys )" 
    by (simp only: IH)
  also have "... = ( algunos P (x#xs) ∨ algunos P ys )" 
    by (simp only: algunos.simps(2) disj_assoc)
  finally show ?case .
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 gleherlop chrgencar 
   cammonagu giafus1 pabbergue enrparalv alikan antramhur juacanrod
   hugrubsan aribatval *)  
lemma "algunos P (rev xs) = algunos P xs"
  by (induct xs) (simp_all add: HOL.disj_comms algunos_append)

(* benber marfruman1 *)
lemma "algunos P (rev xs) = algunos P xs"
  using algunos_append by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.2. Demostrar o refutar detalladamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

(* pabalagon juacanrod *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
next
  fix a xs
  assume HI: "algunos P (rev xs) = algunos P xs"
  have "algunos P (rev (a#xs)) = algunos P (rev xs @ [a])" by simp
  also have "... = (algunos P (rev xs) ∨ algunos P [a])" 
    by (simp add: algunos_append)
  also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
  also have "... = (algunos P xs ∨ P a)" by simp
  also have "... = (P a ∨ algunos P xs)" by (simp add: HOL.disj_comms)
  finally show "algunos P (rev (a#xs)) = algunos P (a#xs)" by simp
qed

(* manperjim josgomrom4 raffergon2 gleherlop chrgencar cammonagu giafus1
   pabbergue enrparalv marfruman1 alikan antramhur hugrubsan *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  show "algunos P (rev []) = algunos P []" by simp
next
  fix a xs
  assume HI:"algunos P (rev xs) = algunos P xs"
  have "algunos P (rev (a # xs)) = algunos P ((rev xs) @ [a])" by simp
  also have "... = ((algunos P (rev xs)) ∨ (algunos P [a]))" 
    by (simp add: algunos_append)
  also have "... = ((algunos P xs) ∨ (algunos P [a]))" using HI by simp
  also have "... = ((algunos P [a]) ∨ (algunos P xs))" by arith
  finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

(* alfmarcua *)
lemma "algunos P (rev xs) = algunos P xs" (is "?P xs")
proof (induct xs)
  show "?P []" by (simp only: rev.simps(1))
next
  fix a xs
  assume HI:"?P xs"
  have "algunos P (rev (a # xs)) = algunos P (rev xs @ [a])" 
    by (simp only: rev.simps(2))
  also have "... = (algunos P (rev xs) ∨ algunos P [a])" 
    by (simp only: algunos_append)
  also have "... = (algunos P xs ∨ algunos P [a])" by (simp only: HI)
  also have "... = (algunos P (a#[]) ∨ algunos P xs)" 
    by (simp only: HOL.disj_comms)
  also have "... = ((P a ∨ False) ∨ algunos P xs)" 
    by (simp only: algunos.simps)
  also have "... = (P a ∨ algunos P xs)"  
    by (simp only: HOL.simp_thms(31))
  also have "... = algunos P (a#xs)" by (simp only: algunos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
  case Nil
  show ?case by (simp only: algunos.simps(1) rev.simps(1))
next
  case (Cons x xs)
  assume IH: "algunos P (rev xs) = algunos P xs"
  have "algunos P (rev (x#xs)) = algunos P ( (rev xs) @ [x] )" 
    by (simp only: rev.simps(2))
  also have "... = ( algunos P (rev xs) ∨ algunos P [x] )" 
    by (simp only: algunos_append)
  also have "... = ( algunos P (rev xs) ∨ P x ∨ algunos P [] )" 
    by (simp only: algunos.simps(2))
  also have "... = ( algunos P (rev xs) ∨ P x )" 
    by (simp only: algunos.simps(1) simp_thms(31))
  also have "... = (algunos P xs ∨ P x)" by (simp only: IH)
  also have "... = algunos P (x#xs)" 
    by (simp only: algunos.simps(2) disj_commute)
  finally show ?case.
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la 
  siguiente ecuación:
     algunos (λx. P x ∨ Q x) xs = Z
  y demostrar la equivalencia de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
   gleherlop chrgencar benber giafus1 enrparalv marfruman1 antramhur
   alikan hugrubsan aribatval *)  
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
  by (induct xs) auto

(* pabalagon josgomrom4 cammonagu pabbergue marfruman1 antramhur
   juacanrod alikan *) 
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
proof (induct xs)
  show "algunos (λx. P x ∨ Q x) [] = (algunos P [] ∨ algunos Q [])" 
    by simp
next
  fix a xs
  assume HI: "algunos (λx. P x ∨ Q x) xs = 
              (algunos P xs ∨ algunos Q xs)"
  have "algunos (λx. P x ∨ Q x) (a#xs) = 
        (P a ∨ Q a ∨ algunos (λx. P x ∨ Q x) xs)" by simp
  also have "... = (P a ∨ Q a ∨ algunos P xs ∨ algunos Q xs)" 
    using HI by simp
  also have "... = (P a ∨ algunos P xs ∨ Q a ∨ algunos Q xs)" 
    by (simp add: HOL.disj_comms)
  finally show "algunos (λx. P x ∨ Q x) (a#xs) = 
                (algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
qed

(* alfmarcua *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)" 
      (is "?P xs")
proof (induct xs)
  show "?P []" by (simp only: algunos.simps(1) HOL.simp_thms(33))
next
  fix a xs
  assume HI:"?P xs"
  have "algunos (λx. P x ∨ Q x) (a # xs) = 
        ((P a ∨ Q a) ∨ algunos (λx. P x ∨ Q x) xs)" 
    by (simp only: algunos.simps(2))
  also have "... = ((P a ∨ Q a) ∨ algunos P xs ∨ algunos Q xs)" 
    by (simp only: HI)
  also have "... = ((P a ∨ algunos P xs) ∨ Q a  ∨ algunos Q xs)" 
    by (simp only: HOL.disj_assoc HOL.disj_comms)
  also have "... = (algunos P (a # xs) ∨ algunos Q (a # xs))" 
    by (simp only: algunos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma "algunos (λx. P x ∨ Q x) xs = ( algunos P xs ∨ algunos Q xs )"
proof (induct xs)
  case Nil
  have "algunos (λx. P x ∨ Q x) [] = False" 
    by (simp only: algunos.simps(1))
  also have "... = ( algunos P [] ∨ algunos Q [] )" 
    by (simp only: algunos.simps(1) simp_thms(31))
  finally show ?case.
next
  case (Cons x xs)
  let ?R = "λx. P x ∨ Q x"
  assume IH: "algunos ?R xs = ( algunos P xs ∨ algunos Q xs )"
  have "algunos ?R (x#xs) = ( ?R x ∨ algunos ?R xs )" 
    by (simp only: algunos.simps(2))
  also have "... = ( P x ∨ Q x ∨ algunos P xs ∨ algunos Q xs )" 
    by (simp only: IH disj_assoc)
  also have "... = ( P x ∨ (Q x ∨ algunos P xs) ∨ algunos Q xs )" 
    by (simp only: disj_assoc)
  also have "... = ( P x ∨ (algunos P xs ∨ Q x) ∨ algunos Q xs )" 
    by (simp only: disj_commute)
  also have "... = ( algunos P (x#xs) ∨ algunos Q (x#xs) )" 
    by (simp only: algunos.simps(2) disj_assoc)
  finally show ?case .
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.1. Demostrar o refutar automáticamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
   gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
   antramhur juacanrod alikan hugrubsan aribatval *) 
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
  by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.2. Demostrar o refutar detalladamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 cammonagu pabbergue enrparalv
   marfruman1 antramhur juacanrod alikan hugrubsan aribatval *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
  have "algunos P [] = False" by simp
  also have "... = (¬ todos (λx. (¬ P x)) [])" by simp
  finally show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
  fix a xs
  assume HI: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
  have "(¬ todos (λx. (¬ P x)) (a#xs)) = 
        (¬ ((¬ P a) ∧ todos (λx. (¬ P x)) xs))" by simp
  also have "... = (P a ∨ ¬ todos (λx. (¬ P x)) xs)" by simp
  also have "... = (P a ∨ algunos P xs)" using HI by simp
  finally show "algunos P (a#xs) = (¬ todos (λx. (¬ P x)) (a#xs))" 
    by simp
qed

(* alfmarcua *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)" (is "?P xs")
proof (induct xs)
  have "algunos P [] = False" by (simp only:algunos.simps(1))
  also have "... = (¬ True)" by (simp only: HOL.simp_thms(7))
  also have "... = (¬ todos (λx. (¬ P x)) [])" 
    by (simp only: todos.simps(1))
  finally show "?P []" .
next
  fix a xs
  assume HI:"?P xs"
  have "algunos P (a # xs) = (P a ∨ algunos P xs)" 
    by (simp only: algunos.simps(2))
  also have "... = (P a ∨ ¬ todos (λx. (¬ P x)) xs)" 
    by (simp only: HI)
  also have "... = (¬ ¬ P a ∨ ¬ todos (λx. (¬ P x)) xs)" 
    by (simp only: HOL.simp_thms(1))
  also have "... = (¬ (¬ P a ∧ todos (λx. (¬ P x)) xs))" 
    by (simp only: HOL.de_Morgan_conj)
  also have "... = (¬ todos (λx. (¬ P x)) (a#xs))" 
    by (simp only: todos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
  case Nil
  have "algunos P [] = False" by (simp only: algunos.simps(1))
  also have "False = (¬ todos (λx. ¬ P x) [])" 
    by (simp only: todos.simps(1) not_True_eq_False)
  finally show ?case .
next
  case (Cons x xs)
  assume IH: "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
  have "algunos P (x#xs) = ( P x ∨ algunos P xs )" 
    by (simp only: algunos.simps(2))
  also have "... = ( P x ∨ (¬ todos (λx. (¬ P x)) xs) )" 
    by (simp only: IH)
  also have "... = ( ¬( ¬ P x ∧ todos (λx. (¬ P x)) xs) )" 
    by (simp only: not_not de_Morgan_conj)
  also have "... = (¬ todos (λx. (¬ P x)) (x#xs))" 
    by (simp only: todos.simps(2))
  finally show ?case .
qed
     
text {*
  --------------------------------------------------------------------- 
  Ejercicio 12. 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
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua raffergon2 cammonagu
   gleherlop chrgencar benber giafus1 pabbergue enrparalv marfruman1
   antramhur juacanrod alikan hugrubsan aribatval *) 
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x [] = False" |
  "estaEn x (y#xs) = (x=y ∨ estaEn x xs)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Expresar la relación existente entre estaEn y algunos. 
  Demostrar dicha relación de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

(* manperjim pabalagon josgomrom4 alfmarcua cammonagu gleherlop
   chrgencar benber giafus1 pabbergue marfruman1 antramhur juacanrod
   alikan *)  
lemma "estaEn x xs = algunos (λa. x=a) xs"
  by (induct xs) auto

(* pabalagon josgomrom4 cammonagu marfruman1 antramhur *)
lemma "estaEn x xs = algunos (λa. x=a) xs"
proof (induct xs)
  show "estaEn x [] = algunos (λa. x=a) []" by simp
next
  fix y xs
  assume HI: "estaEn x xs = algunos (λa. x=a) xs"
  have "estaEn x (y#xs) = (x=y ∨ estaEn x xs)" by simp
  also have "... = (x=y ∨ algunos (λa. x=a) xs)" using HI by simp
  finally show "estaEn x (y#xs) = algunos (λa. x=a) (y#xs)" by simp
qed

(* alfmarcua *)
lemma "estaEn x xs = algunos (λk. x=k) xs" (is "?P xs")
proof (induct xs)
  show "?P []" by (simp only: estaEn.simps(1) algunos.simps(1))
next
  fix a xs
  assume HI:"?P xs"
  have "estaEn x (a # xs) = (x=a ∨ estaEn x xs)" 
    by (simp only: estaEn.simps(2))
  also have "... = (x=a ∨ algunos (λk. x=k) xs)" by (simp only: HI)
  (* also have "... = ((λk. x=k) a ∨ algunos (λk. x=k) xs)" by (simp only:HOL.simp_thms(6)) *)
  also have "... = algunos (λk. x=k) (a#xs)" by (simp only: algunos.simps(2))
  finally show "?P (a#xs)" .
qed

(* benber *)
lemma "estaEn x xs = (algunos (λy. y = x) xs)"
proof (induct xs)
  case Nil
  have "estaEn x [] = False" by (simp only: estaEn.simps(1))
  also have "False = (algunos (λy. y = x) [])" 
    by (simp only: algunos.simps(1))
  finally show ?case .
next
  case (Cons z xs)
  assume IH: "estaEn x xs = algunos (λy. y = x) xs"
  have "estaEn x (z#xs) = ( z = x ∨ estaEn x xs )" by force
  also have "... = ( z = x ∨ algunos (λy. y = x) xs)" by (simp only: IH)
  also have "... = (algunos (λy. y = x) (z#xs))" 
    by (simp only: algunos.simps(2))
  finally show ?case .
qed

end