Examen 1C

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

theory examen_2_jul
imports Main 
begin

text ‹
  Apellidos:
  Nombre: 
› 

text ‹Sustituye la palabra examen_2_jul 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.›

text ‹Nota 3: En el proceso de corrección del examen, y antes de la
  publicación de las calificaciones del mismo, se podrá requerir
  aclaraciones sobre su respuesta. Estas aclaraciones se harán por 
  alguno de los procedimientos virtuales previstos en la PEV. ›

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

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

text ‹------------------------------------------------------------------ 
  Ejercicio 1. 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 
     Si todas las medicinas están contaminadas, entonces todos los
     técnicos negligentes son unos bribones. Si hay medicinas
     contaminadas, entonces todas las medicinas están contaminadas y son
     peligrosas. Todos los germicidas son medicinas. Sólo los
     negligentes son distraídos. Por tanto, si cualquier técnico es
     distraído y si algunos germicidas están contaminados, los técnicos
     son bribones. 
  Usar la siguiente simbología: 
     M(x): x es medicina,  C(x): x está contaminada, 
     T(x): x es técnico,   N(x): x es un negligente, 
     B(x): x es un bribón, G(x): x es germicida, 
     D(x): x es distraído, P(x): x es peligrosa.
  ---------------------------------------------------------------------›


text ‹------------------------------------------------------------------
  Ejercicio 2. Se consideran las definiciones de las siguientes
  funciones (que se dan a continuación)
     estaEn   :: 'a ⇒ 'a list ⇒ bool
     sublista :: "'a list ⇒ 'a list ⇒ bool
     elimina  :: nat ⇒ 'a list ⇒ 'a list
  tales 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
  + (sublista xs ys) se verifica si todos los elementos de la lista xs
    están en la lista ys. Por ejemplo, 
       sublista [(1::nat),2,3] [3,2,1,2] = True
       sublista [(1::nat),2,3] [2,1,2]   = False
  + (elimina n xs) es la lista obtenida eliminando los n primeros
    elementos de xs. Por ejemplo, 
       elimina 2 [a,c,d,b,e] = [d,b,e]

  Demostrar detalladamente que
     sublista (elimina n xs) xs
  ---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x []     = False"
| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

fun sublista :: "'a list ⇒ 'a list ⇒ bool" where
  "sublista [] ys     = True"
| "sublista (x#xs) ys = (estaEn x ys ∧ sublista xs ys )"

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
  "elimina n []           = []"
| "elimina 0 xs           = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

lemma eliminaSublista: "sublista (elimina n xs) xs"
oops

text ‹------------------------------------------------------------------
  Ejercicio 3. Sea G un grupo. Demostrar que las siguientes condiciones
  son equivalentes:
    (+) G es commutativo, es decir, ∀x y. (x ⋅ y = y ⋅ x) 
    (+) ∀x y. (((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭)

  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_i:  "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 = y ⋅ x"
  oops

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

end
      
text ‹------------------------------------------------------------------
  Ejercicio 4. Se define la clausura reflexiva, simétrica y transitiva 
  de una relación binaria r como sigue:
     inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"  
      for r where
       refl1: "rst r x x"
     | trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
     | trans2: "r y x ⟹ rst r y z ⟹ rst r x z" 
                     
  Demostrar detalladamente que la relación (rst es r) simétrica. 
  ---------------------------------------------------------------------›

inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"  
 for r where
  refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z" 

lemma rst_es_simetrica : "rst r x y ⟹ rst r y x"
  oops

end