Examen 2C

text ‹Examen de Lógica Matemática y Fundamentos (9-septiembre-2020)›

theory examen_9_sep
imports Main 
begin

text ‹
  Apellidos:
  Nombre: 
› 

text ‹Sustituye la palabra examen_9_sep por tu usuario de la Universidad 
  de Sevilla y graba el fichero con dicho usuario.thy› 

text ‹Nota 1: El tiempo de realización del ejercicio es de 9:30 a 11:30.› 

text ‹Nota 2: Además de las reglas básicas de deducción natural de la 
  lógica proposicional y de primer orden, también se pueden usar las 
  reglas notnotI y mt que demostramos a  continuación.›

lemma notnotI: "P ⟹ ¬¬ P"
  by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text ‹------------------------------------------------------------------ 
  Ejercicio 1. (2.5 puntos) Demostrar detalladamente con Isabelle, 
  sin usar métodos automáticos (como simp, auto, ...) sino sólo las 
  reglas básicas, que el siguiente argumento es correcto:
  Ningún individuo que sea candidato será derrotado si hace una
  buena campaña. Todo individuo que se postula es un candidato. Cualquier
  candidato que no sea derrotado, será elegido. Todo individuo que sea
  elegido hace una buena campaña. Por tanto, todo individuo que se 
  postula será elegido si y sólo si hace una buena campaña. 

  Simbología: I(x): x es individuo, C(x): x es candidato,
              D(x): x es derrotado, B(x): x hace una buena campaña, 
              P(x): x se postula, E(x): x es elegido. 
---------------------------------------------------------------------›
   


text ‹ -----------------------------------------------------------------
  Ejercicio 2. (2.5 puntos) Consideramos la función
     menores :: int ⇒ int list ⇒ bool
  tal que (menores a xs) es la lista de los elementos de la lista xs que 
  son menores que a. Por ejemplo,
     value "menores 2 [3,0,1] = [0,1]"
     value "menores 2 [3,0,5] = [0]"
  
  fun menores :: "int ⇒ int list ⇒ int list" where
    "menores a []     = []"
  | "menores a (x#xs) = (if x < a then x # (menores a xs)
                                else (menores a xs))"
 
  Demostrar que la longitud de la lista de elementos menores que uno 
  dado es menor o igual que la longitud de la lista original.
-----------------------------------------------------------------------›
 
fun menores :: "int ⇒ int list ⇒ int list" where
  "menores a []     = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
                                else (menores a xs))"
 
value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"
 
lemma menores_menor:
  "length (menores x xs) < 1 + (length xs)"
  oops


text ‹------------------------------------------------------------------
  Ejercicio 3. (2.5 puntos) Sea G un grupo. Demostrar que si se verifica
   ∀x y. (((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭), entonces también se verifica
   ∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = z

  Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
  fast, arith o metis 
  ------------------------------------------------------------------ ›

locale grupo =
  fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
    and neutro ("𝟭") 
    and inverso ("_^" [100] 100)
  assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
      and neutro_i:   "𝟭 ⋅ x = x"
      and neutro_d:   "x ⋅ 𝟭 = x"
      and inverso_d:  "x ⋅ x^ = 𝟭"

(* Notas sobre notación:
   * El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos). 
   * El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
   * El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)

context grupo
begin

lemma
  assumes  "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
  shows "x ⋅ y = z ⋅ x ⟶ y = z"
  oops  

end

text ‹-----------------------------------------------------------------
 Ejercicio 4. (2.5 puntos) El conjunto de los conjuntos finitos 
 se define inductivamente por
    inductive_set Finito :: "'a set set"
      where
        vacioI:   "{} ∈ Finito" |
        insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

 Demostrar detalladamente que la unión de dos conjuntos finitos es 
 finito; es decir.
     ⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito

 Nota: Los únicos métodos que se pueden usar son induct y 
 (simp only: ...).  
 ---------------------------------------------------------------------›

inductive_set Finito :: "'a set set"
  where
    vacioI:   "{} ∈ Finito" |
    insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"


lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
  oops

end