DAO (Demostración asistida por ordenador) DAO (Demostración asistida por ordenador)

header {* R16: Conjuntos mediante listas *}

theory R16
imports Main 
begin 

text {* 
  Los conjuntos finitos se pueden representar mediante listas. En esta
  relación se define la unión y se demuestran algunas de sus
  propiedades. Análogamente se puede hacer con la intersección y
  diferencia. 
*}  

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función 
     union_l :: "'a list ⇒ 'a list ⇒ 'a list"
  tal que (union_l xs ys) es la unión de las listas xs e ys. Por
  ejemplo,  
     union_l [1,2] [2,3] = [1,2,3]
  --------------------------------------------------------------------- 
*}

fun union_l :: "'a list ⇒ 'a list ⇒ 'a list" where
  "union_l xs ys = undefined"

value "union_l [1::nat,2] [2,3]" -- "= [1,2,3]"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar o refutar
     set (union_l xs ys) = set xs ∪ set ys
  --------------------------------------------------------------------- 
*}

lemma set_union_l: "set (union_l xs ys) = set xs ∪ set ys"
oops

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar que si xs e ys no tienen elementos repetidos,
  entonces (union_l xs ys) tampoco los tiene.

  Indicación: Usar la función "distintc" de la teoría List.thy
  --------------------------------------------------------------------- 
*}

lemma:
  assumes "distinct xs" 
          "distinct ys" 
  shows   "distinct (union_l xs ys)"
oops

section {* Cuantificación sobre conjuntos *}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir un conjunto S para que se verifique que
     (∀x∈A. P x) ∧ (∀x∈ B. P x) ⟶ (∀x∈S. P x)
  --------------------------------------------------------------------- 
*}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 5. Definir una propiedad P para que se verifique que
     ∀x∈ A. P (f x) ⟹  ∀y∈ f ` A. Q y
  --------------------------------------------------------------------- 
*}

end