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. 
  --------------------------------------------------------------------- 
*}

(* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
   macmerflo rafferrod *) 
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p []     = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

value "todos (λx. 1<length x) [[2,1,4],[1,3::nat]] = True"
value " ¬todos (λx. 1<length x) [[2,1,4],[3::nat]] = True"

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. 
  --------------------------------------------------------------------- 
*}

(* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
   macmerflo rafferrod *) 
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p []      = False"
|  "algunos p (x#xs) = (p x ∨ algunos p xs)"

value " algunos (λx. 1<length x) [[2::nat,1,4],[3]] = True"
value " ¬algunos (λx. 1<length x) [[],[3::nat]] = True"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar o refutar automáticamente 
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}
 (* anddonram edupalhid luicedval cesgongut jescudero rafcabgon diwu2
    macmerflo rafferrod *) 
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)
  --------------------------------------------------------------------- 
*}

(* anddonram [conmutatividad and porque no sé hacerlo de otra forma] *)
lemma and_comm: "(a ∧ b) = (b ∧ a)"
  by (cases a) auto

(* anddonram diwu2 *)
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 a xs
  assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos 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 ∧ Q a ∧ todos Q xs ∧ todos P xs)" 
    by (simp add: and_comm)
  also have "... = (P a ∧ todos Q (a # xs) ∧ todos P xs)" by simp
  also have "... = (P a ∧ todos P xs ∧ Q a ∧ todos Q xs)" 
    by (simp add: and_comm)
  finally show "todos (λx. P x ∧ Q x) (a # xs) = 
                (todos P (a # xs) ∧ todos Q (a # xs))"
    by simp
qed

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

(* rafferrod *)
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 a xs
  assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos 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 auto
  finally show "todos (λx. P x ∧ Q x) (a#xs) = 
                (todos P (a#xs) ∧ todos Q (a#xs))" by simp
qed

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

(* anddonram edupalhid cesgongut luicedval jescudero rafcabgon diwu2
   macmerflo cesgongut rafferrod *) 
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)
  --------------------------------------------------------------------- 
*}

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
   cesgongut rafferrod *) 
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

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

(*anddonram*)
lemma "todos P (rev xs) = todos P xs"
  by (induct xs) (simp_all add: todos_append and_comm)

(* edupalhid diwu2 macmerflo rafferrod*)
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

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

(* anddonram diwu2 *)
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
  finally show "todos P (rev (a # xs)) = todos P (a # xs)" 
    by (simp add: and_comm)
qed

(* edupalhid *)
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 ∧ P a)" using HI by simp
  also have "... = (P a ∧ todos P xs)" by arith
  also have "... = (todos P (a#xs))" by simp
  finally show "todos P (rev (a # xs)) = (todos P (a#xs))" by simp    
qed

(* rafferrod *)
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 [a] ∧ todos P xs)" by auto
    finally show "todos P (rev (a#xs)) = todos P (a#xs)" by simp
  qed

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

(* anddonram Contraejemplo*)
value "let xs=[True,False]    
  in (algunos (λx. (λx. (x=False)) x ∧ (λx. x) x) xs =
     (algunos (λx. (x=False)) xs ∧ algunos (λx. x) xs))"

(* edupalhid diwu2 rafferrod*)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
  quickcheck
  oops

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

(* anddonram edupalhid jescudero luicedval rafcabgon diwu2 macmerflo
   cesgongut rafferrod *) 
lemma "algunos P (map f xs) = algunos (P o f) xs"
  by (induct xs) auto

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

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
   rafferrod *) 
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 a xs
  assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
  have "algunos P (map f (a # xs)) = algunos P (f a#map f xs)" by simp
  also have "... = ((P ∘ f) a ∨ algunos P (map f xs))" by simp
  also have "... = ((P ∘ f) a ∨ algunos (P ∘ f) xs) " using HI by simp
  finally show "algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" 
    by simp
qed

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

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

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
   cesgongut rafferrod *) 
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)
  --------------------------------------------------------------------- 
*}

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
   cesgongut rafferrod *) 
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

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

(* anddonram [conmutatividad or porque no sé hacerlo de otra forma] *)
lemma or_comm: "(a ∨ b) = (b ∨ a)"
  by (cases a) auto

(* anddonram *)
lemma "algunos P (rev xs) = algunos P xs"
  by (induct xs) (simp_all add: algunos_append or_comm)
 
(* edupalhid diwu2 rafferrod*)
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)

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

(* anddonram diwu2 *)
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 ∨ P a)" using HI by simp
  also have "... = (P a ∨ algunos P xs)" by (simp add:or_comm)
  finally show " algunos P (rev (a # xs)) = algunos P (a # xs) " 
    by simp
qed

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

(*rafferrod*)
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 auto
  finally show "algunos P (rev (a#xs)) = algunos P (a#xs)" by simp
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.
  --------------------------------------------------------------------- 
*}

(* anddonram edupalhid diwu2 jescudero macmerflo rafferrod rafcabgon *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
 by (induct xs) auto
 
(* anddonram *)
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 ∨ Q a ∨ algunos Q xs ∨ algunos P xs)" 
    by (simp add: or_comm)
  also have "... = (P a ∨  algunos Q (a#xs) ∨ algunos P xs)"  by simp 
  also have "... = (P a ∨  algunos P xs ∨ algunos Q (a#xs))" 
    by (simp add: or_comm)
  finally show "algunos (λx. P x ∨ Q x) (a # xs) = 
                (algunos P (a # xs) ∨ algunos Q (a # xs))"
    by simp
qed
 
(* edupalhid *)
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)" 
      (is "?T xs")
proof (induct xs)
  show "?T []" by simp
next
  fix a xs assume HI: "?T xs"
    have p1:" (Q a ∨ algunos P xs) = (algunos P xs ∨ Q a)" 
      by (simp add: HOL.disj_commute)
    have "algunos (λx. P x ∨ Q x) (a # xs) = 
          (algunos P [a] ∨ algunos 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)" 
      using p1 by simp
    also have "… = (algunos P (a # xs) ∨ algunos Q (a # xs))" by simp
    finally show "?T (a # xs)" by simp
qed

(* rafferrod *)
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 auto
  finally show "algunos (λx. P x ∨ Q x) (a#xs) = 
                (algunos P (a#xs) ∨ algunos Q (a#xs))" by simp
qed

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

(* anddonram edupalhid diwu2 cesgongut rafferrod rafcabgon *)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
 by (induct xs) auto
 
text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.2. Demostrar o refutar datalladamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

(*anddonram edupalhid diwu2 rafferrod*)
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
  show "algunos P [] = (¬ todos (λx. (¬ P x)) [])" by simp
next
  fix a xs
  assume HI:"algunos P xs = (¬ todos (λx. ¬ P x) xs)"
  have "algunos P (a # xs) =(P a ∨ algunos P xs)" by simp
  also have "... = (P a ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
  also have "... = (¬ (¬ P a ∧ todos (λx. ¬ P x) xs))" by simp
  finally show "  algunos P (a # xs) = (¬ todos (λx. ¬ P x) (a # xs))" 
    by simp
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
  --------------------------------------------------------------------- 
*}

(* anddonram edupalhd luicedval rafcabgon diwu2 jescudero macmerflo
   cesgongut rafferrod *) 
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x []     = 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"

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

(* anddonram edupalhid luicedval rafcabgon diwu2 jescudero macmerflo
   cesgongut rafferrod *) 
lemma "estaEn x xs=algunos (λy.(y=x)) xs"
  by (induct xs) auto

(* anddonram edupalhid luicedval rafcabgon jescudero macmerflo cesgongut
   rafferrod *) 
lemma "estaEn x xs=algunos (λy.(y=x)) xs"
proof (induct xs)
  show "estaEn x []=algunos (λy.(y=x)) []" by simp
next
  fix a xs
  assume HI:"estaEn x xs = algunos (λy. y = x) xs"
  have "estaEn x (a # xs) =((a=x) ∨ estaEn x xs)" by simp
  also have "... = ((a=x) ∨ algunos (λy. y = x) xs)" using HI by simp
  finally show "estaEn x (a # xs) = algunos (λy. y = x) (a # xs)" by simp
qed

end