Ver el código de «Examen 1C sol»

<source lang = "isabelle">
theory examen_2_jul_sol
imports Main 
begin

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.
  ---------------------------------------------------------------------›

― ‹Formalización y demostración›

― ‹Formalización:›
lemma 
  assumes "(∀x. M(x) ⟶ C(x)) ⟶ (∀y. (T(y) ∧ N(y)) ⟶ B(y))"
          "(∃x. M(x) ∧ C(x)) ⟶ (∀x. M(x) ⟶ C(x) ∧ P(x))"
          "∀x. G(x) ⟶ M(x)"
          "∀y. ¬N(y) ⟶ ¬D(y)"
  shows   "(∀y. T y ⟶ D y) ∧ (∃x. G x ∧ C x) ⟶ (∀z. T z ⟶ B z)"
  oops

― ‹Auxiliar›
lemma previo:
  assumes "∀x. M(x) ⟶ C(x) ∧ P(x)"
  shows   "∀x. M(x) ⟶ C(x)"
proof (rule allI)
  fix a
  show "M(a) ⟶ C(a)"
  proof (rule impI)
    assume "M(a)"
      have "M(a) ⟶ C(a) ∧ P(a)" using assms by (rule allE)
      then have "C(a) ∧ P(a)" using ‹M(a)› by (rule mp)
      then show "C(a)" by (rule conjunct1)
    qed
  qed


― ‹Demostración declarativa detallada:›
lemma 
  assumes "(∀x. M(x) ⟶ C(x)) ⟶ (∀y. (T(y) ∧ N(y)) ⟶ B(y))"
          "(∃x. M(x) ∧ C(x)) ⟶ (∀x. M(x) ⟶ C(x) ∧ P(x))"
          "∀x. G(x) ⟶ M(x)"
          "∀y. ¬N(y) ⟶ ¬D(y)"
  shows   "(∀y. T y ⟶ D y) ∧ (∃x. G x ∧ C x) ⟶ (∀z. T z ⟶ B z)" 
proof (rule impI)
  assume 1: "(∀y. T(y) ⟶ D(y)) ∧ (∃x. G(x) ∧ C(x))"
  show "∀z. T(z) ⟶ B(z)"
  proof (rule allI)
    fix a
    show "T(a) ⟶ B(a)"
    proof (rule impI)
      assume "T(a)"
      show   "B(a)"
      proof -
        have "∀y. T(y) ⟶ D(y)" using 1 by (rule conjunct1)
        then have "T(a) ⟶ D(a)" by (rule allE)
        then have "D(a)" using  `T(a)` by (rule mp)
        then have "¬¬D(a)" by (rule notnotI) 
        have "¬N(a)⟶¬D(a)"  using assms(4) by (rule allE)
        then have "¬¬N(a)" using `¬¬D(a)` by (rule mt)
        then have "N(a)"  by (rule notnotD)
        have "∃x. G(x) ∧ C(x)"  using 1 by (rule conjunct2)
        then obtain b where "G(b) ∧ C(b)" by (rule exE)
        then have "G(b)" by (rule conjunct1)
        have "C(b)" using `G(b) ∧ C(b)` by (rule conjunct2)
        have "G(b) ⟶ M(b)" using assms(3) by (rule allE)
        then have "M(b)" using  `G(b)` by (rule mp)
        then have "M(b) ∧ C(b)" using `C(b)` by (rule conjI)
        then have "∃x. M(x) ∧ C(x)"  by (rule exI)
        with assms(2) have "∀x. M(x) ⟶ C(x) ∧ P(x)" by (rule mp)
        then have "∀x. M(x) ⟶ C(x)" by (rule previo)
        with assms(1) have "∀y. (T(y) ∧ N(y)) ⟶ B(y)" by (rule mp)
        then have "(T(a) ∧ N(a))⟶B(a)" by (rule allE)
        have "T(a) ∧ N(a)" using `T(a)` `N(a)` by (rule conjI)
        with `(T(a) ∧ N(a)) ⟶ B(a)` show "B(a)"  by (rule mp)
      qed
    qed
  qed
qed

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"

― ‹Auxiliares:›

lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y#ys)"
  apply (induct xs)
   apply (simp only: sublista.simps(1))
  apply (simp only: sublista.simps(2))
  apply (rule conjI)
   apply (erule conjE)
   apply (simp only: estaEn.simps(2))
   apply (rule disjI2)
   apply (simp only: implies_True_equals)+
  done
   
lemma estaEn1: "estaEn x (x#xs)"
  apply (simp only: estaEn.simps(2))
  apply (rule disjI1)
  apply (rule refl)
  done

lemma sublistaReflexiva: "sublista xs xs"
  apply (induct xs)
   apply (simp only: sublista.simps(1))
  apply (simp only: sublista.simps(2))
  apply (rule conjI)
   apply (rule estaEn1)
  apply (rule sublistaMono, assumption)
  done


― ‹Demostración declarativa detallada:›  
lemma eliminaSublista_dec: "sublista (elimina n xs) xs"
proof (induct rule: elimina.induct)
  fix n
  show "sublista (elimina n []) []"
    by (simp only: elimina.simps(1) sublista.simps(1))
next
  fix x :: "'a" and  xs :: "'a list"
  show "sublista (elimina 0 (x # xs)) (x # xs)"
  by (simp only: elimina.simps(2) sublistaReflexiva)
next
   fix n and x :: "'a" and xs :: "'a list"
   show "sublista (elimina n xs) xs ⟹ 
         sublista (elimina (Suc n) (x # xs)) (x # xs)"
   by  (simp only: elimina.simps(3) sublistaMono)
qed

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

― ‹Auxiliar para una implicación:›

lemma inverso_d: 
  "x ⋅ x^ = 𝟭"
proof -
  have "x ⋅ x^ = 𝟭 ⋅ (x ⋅ x^)" 
    by (simp only: neutro_i)
  also have "… = (𝟭 ⋅ x) ⋅ x^" 
    by (simp only: asociativa)
  also have "… = (((x^)^ ⋅ x^) ⋅ x) ⋅ x^" 
    by (simp only: inverso_i)
  also have "… = ((x^)^ ⋅ (x^ ⋅ x)) ⋅ x^" 
    by (simp only: asociativa)
  also have "… = ((x^)^ ⋅ 𝟭) ⋅ x^" 
    by (simp only: inverso_i)
  also have "… = (x^)^ ⋅ (𝟭 ⋅ x^)" 
    by (simp only: asociativa)
  also have "… = (x^)^ ⋅ x^" 
    by (simp only: neutro_i)
  also have "… = 𝟭" 
    by (simp only: inverso_i)
  finally show ?thesis 
    by this
qed

lemma 
  assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
  shows   "x ⋅ y = y ⋅ x"
proof -
  have "x ⋅ y = (x ⋅ y) ⋅ 𝟭" 
    by (rule neutro_d [THEN sym])
  also have "… =  (x ⋅ y) ⋅ (((y^ ⋅ x^) ⋅ y) ⋅ x)" 
    using assms by (rule arg_cong [THEN sym])
  also have "… =  (x ⋅ ((y ⋅ y^) ⋅ x^) ⋅ y) ⋅ x" 
    by (simp only: asociativa)
  also have "… =  ((x ⋅ (𝟭 ⋅ x^)) ⋅ y) ⋅ x" 
    by (simp only: inverso_d)
  also have "… =  (x ⋅ ((𝟭 ⋅ x^) ⋅ y)) ⋅ x " 
    by  (simp only: asociativa)
  also have "… =  (x ⋅ (x^ ⋅ y)) ⋅ x" 
    by  (simp only: neutro_i)
  also have "… =  ((x ⋅ x^) ⋅ y) ⋅ x" 
    by  (simp only: asociativa)
  also have "… = (𝟭 ⋅ y) ⋅ x" 
    by  (simp only: inverso_d)
  also have "… = 𝟭 ⋅ (y ⋅ x)" 
    by  (simp only: asociativa)
  also have "… = y ⋅ x" 
    by (simp only: neutro_i)
  finally show  "x ⋅ y = y ⋅ x" 
    by this
qed

― ‹Recíproco:›
lemma 
  assumes "x ⋅ y = y ⋅ x"
  shows   "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
proof -
  have "y ⋅ x = x ⋅ y" using assms by (rule sym)
  then have "x^ ⋅ (y ⋅ x) = x^ ⋅ (x ⋅ y)" by (rule arg_cong)
  then have "y^ ⋅ (x^ ⋅ (y ⋅ x)) =y^ ⋅ (x^ ⋅ (x ⋅ y))" by (rule arg_cong)
  then have "((y^ ⋅ x^) ⋅ y) ⋅ x =y^ ⋅ ((x^ ⋅ x) ⋅ y)" 
    by (simp only: asociativa)
  also have "... = y^ ⋅ (𝟭 ⋅ y)" by (simp only: inverso_i)
  also have "... = y^ ⋅ y " by (simp only: neutro_i)
  also have "... = 𝟭" by (simp only: inverso_i)
  finally show "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭" by this
qed

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" 

― ‹Lemas auxiliares:›

lemma r_subset_rst: "r x y ⟹ rst r x y"
  by (simp only: refl1 trans1)

lemma r_subset_rst_b: "r x y ⟹ rst r y x"
  by (simp only: refl1 trans2)


lemma rst_sc1_declarativo: "rst r x y  ⟹ r y z ⟹ rst r x z"
proof  (induct rule:rst.induct)
  case (refl1 x)
  then show ?case by (rule r_subset_rst) 
next
  case (trans1 x y z)
  then show ?case by (simp only: rst.trans1)
next
  case (trans2 y x z)
  then show ?case  by (simp only: rst.trans2)
qed
  

lemma rst_sc2_declarativo: "rst r z y ⟹ r x y ⟹ rst r z x"
proof  (induct rule:rst.induct)
  case (refl1 x)
  then show ?case by (rule r_subset_rst_b) 
next
  case (trans1 x y z)
  then show ?case by (simp only: rst.trans1)
next
  case (trans2 y x z)
  then show ?case by (simp only: rst.trans2)
qed


― ‹Demostración declarativa detallada:›
lemma rstSimetrica_declarativa: "rst r x y ⟹ rst r y x"
proof (induct rule: rst.induct)
  fix x 
  show "rst r x x" by (rule refl1)
next
  fix x y z
  assume "r x y" and "rst r y z" and "rst r z y"
  then show "rst r z x" by (simp only: rst_sc2_declarativo)
next 
  fix x y z
  assume "r y x" and "rst r y z" and "rst r z y"
  then show "rst r z x" by (simp only: rst_sc1_declarativo)        
qed
 
end
</source>