Examen 2C sol

theory examen_9_sep_sol
imports Main 
begin

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. 
---------------------------------------------------------------------›
lemma 
  assumes "∀x. (I(x)∧C(x))∧B(x)⟶¬D(x)"
          "∀x. I(x)∧P(x) ⟶ C(x)"
          "∀x. C(x) ∧ ¬D(x) ⟶ E(x)"
          "∀x. I(x)∧E(x) ⟶ B(x)"
  shows   "∀x. I(x)∧P(x)⟶(E(x)⟷B(x))"
  proof (rule allI)
  fix a
  show "I(a)∧P(a) ⟶ (E(a)⟷B(a))"
    proof
      assume "I(a)∧P(a)"
      show "E(a)⟷B(a)"
        proof
          assume "E(a)"
          show  "B(a)"
             proof -
              have "I(a)" using ‹I(a)∧P(a)› by (rule conjunct1)
              then have 1:"I(a)∧E(a)" using ‹E(a)› by (rule conjI)
              have "I(a)∧E(a) ⟶ B(a)" using assms(4) by (rule allE)
              then show "B(a)" using 1 by (rule mp)
             qed  
        next
          assume "B(a)"
          show   "E(a)"
             proof -
              have "I(a)∧P(a) ⟶ C(a)" using assms(2) by (rule allE)
              then have "C(a)" using   ‹I(a)∧P(a)› by (rule mp)
              have "I(a)" using  ‹I(a)∧P(a)› by (rule conjunct1)
              then have "I(a)∧C(a)" using ‹C(a)› by (rule conjI)
              then have 2:"(I(a)∧C(a))∧B(a)" using ‹B(a)› 
                by (rule conjI)
              have "(I(a)∧C(a))∧B(a)⟶¬D(a)" using assms(1) 
                by (rule allE)
              then have "¬D(a)" using 2 by (rule mp)
              have 3:"C(a) ∧ ¬D(a) ⟶ E(a)" using assms(3) 
                by (rule allE)
              have "C(a)∧¬D(a)" using ‹C(a)› ‹¬D(a)› by (rule conjI)
              with 3 show "E(a)" by (rule mp)
             qed
        qed
    qed
  qed              


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))"
 
value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"
 
text ‹ -----------------------------------------------------------------
  Demostrar que la longitud de la lista de elementos menores que uno 
  dado es menor o igual que la longitud de la lista original.
-----------------------------------------------------------------------›

― ‹Demostración estructurada:›

lemma menores_menor_1:
  "length (menores x xs) < Suc (length xs)"
proof(induct xs)
    show "length (menores x [])<Suc(length [])" by simp
  next
    fix xs a
    assume HI: "length (menores x xs) < Suc (length xs)"
    show "length (menores x (a#xs))< Suc(length (a#xs))"
    proof(cases "a<x")
      case True
      then have "length (menores x (a#xs)) = length(a#(menores x xs))" 
        by simp
      also have "... = Suc(length(menores x xs))" by simp
      also have "...< Suc(Suc( length  xs))" using HI by simp
      also have "... = Suc(length(a#xs))" by simp
      finally show ?thesis by simp
  next
    case False
    then have "length (menores x (a#xs)) = length(menores x xs)" by simp
    also have "... < Suc (length xs)" using HI by simp
    also have "... < Suc (length (a#xs))" by simp
    finally show ?thesis by simp
  qed
qed

― ‹Demostración detallada:›

lemma menores_menor_detallada:
  "length (menores x xs) < Suc (length xs)"
proof(induct xs)
  show "length (menores x []) < Suc (length [])" 
    by  (simp only: list.size lessI menores.simps(1))
next
  fix xs a
  assume HI: "length (menores x xs) < Suc (length xs)"
  show "length (menores x (a#xs))< Suc(length (a#xs))"
  proof (cases "a<x")
    case True
    then have "menores x (a#xs) = a#(menores x xs)" 
      by (simp only:if_True menores.simps)
    then have "length (menores x (a#xs)) = length(a#(menores x xs))" 
     by (simp only:)
    also have "... = Suc(length(menores x xs))" by (simp only:list.size)
    also have "...< Suc(Suc( length  xs))" using HI by (simp only:)
    also have "... = Suc(length(a#xs))" by (simp only: list.size)
    finally show ?thesis by this
  next
    case False
    then have "menores x (a#xs) = menores x xs" 
      by (simp only: if_False menores.simps(2))
    then have "length (menores x (a#xs)) = length(menores x xs)" 
      by (simp only:)
    also have "... < Suc (length xs)" using HI by (simp only:)
    also have "... < Suc (length (a#xs))" by (simp only: list.size)
    finally show ?thesis by this
  qed
qed

― ‹Demostración aplicativa:›

lemma menores_menor_aplicativa:
  "length (menores x xs) < Suc (length xs)"
  apply (induct xs)
   apply (simp only: list.size lessI menores.simps(1))
  apply (simp only:menores.simps(2))
  apply(split if_split)
  apply (rule conjI)
   apply (rule impI)
   apply (simp only: list.size)
  apply (rule impI)
  apply (simp only: list.size)
  done

― ‹Demostración automática:›

lemma menores_menor_auto:
  "length (menores x xs) < Suc (length xs)"
by (induct xs) auto


lemma 
  "length (menores x xs) < 1 + length xs"
proof(induct xs)
  show "length (menores x []) < 1 + (length [])" 
    by  (simp only: list.size lessI menores.simps(1))
next
  fix xs a
  assume HI: "length (menores x xs) < 1 + length xs"
  show "length (menores x (a#xs)) < 1 + length (a#xs)"
  proof (cases "a<x")
    case True
    then have "menores x (a#xs) = a#(menores x xs)" 
      by (simp only:if_True menores.simps)
    then have "length (menores x (a#xs)) = length(a#(menores x xs))" 
     by (simp only:)
    also have "... = 1 + (length(menores x xs))" by (simp only:list.size)
    also have "...< 1 + (1 + ( length  xs))" using HI by (simp only:)
    also have "... = 1 + (length(a#xs))" by (simp only: list.size)
    finally show ?thesis by this
  next
    case False
    then have "menores x (a#xs) = menores x xs" 
      by (simp only: if_False menores.simps(2))
    then have "length (menores x (a#xs)) = length(menores x xs)" 
      by (simp only:)
    also have "... < 1 +  (length xs)" using HI by (simp only:)
    also have "... < 1 +  (length (a#xs))" by (simp only: list.size)
    finally show ?thesis by this
  qed
qed

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"
proof (rule impI)
  assume 1: "x ⋅ y = z ⋅ x"
  show "y = z"
  proof-
    have  2: "x ⋅ y = y ⋅ x"
    proof-
      have "x ⋅ y = (x ⋅ y) ⋅ 𝟭" by (simp only:  neutro_d)
      also have "… =  (x ⋅ y) ⋅ (((y^ ⋅ x^) ⋅ y) ⋅ x)" 
        using assms by (simp only:)
      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: neutro_d)
      also have "… = 𝟭 ⋅ y ⋅ x"
        by (simp only: inverso_d)
      also have "… = y ⋅ x"
         by (simp only: neutro_i)
       finally show  "x ⋅ y = y ⋅ x" 
         by this
     qed
     have "y ⋅ x = z ⋅ x" using 1 2 by (simp only:)
     then have "(y ⋅ x) ⋅ x^ = (z ⋅ x) ⋅ x^" by (simp only:)
     then have "y ⋅ (x ⋅ x^) = z ⋅ (x ⋅ x^)" by (simp only:asociativa)
     then have "y ⋅ 𝟭 = z ⋅ 𝟭" by (simp only:inverso_d)
     then show "y = z " by (simp only:neutro_d)
    qed
qed

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"

― ‹ Demostración declarativa  detallada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
proof (induct rule: Finito.induct)
  assume "B ∈ Finito"
  then show "{} ∪ B ∈ Finito" by (simp only: Un_empty_left)
next
  fix A a
  assume AF: "A ∈ Finito" and
         HI: "B ∈ Finito ⟹ A ∪ B ∈ Finito" and
         BF: "B ∈ Finito"
  have "A ∪ B ∈ Finito" by (simp only: HI BF)
  then have "insert a (A ∪ B) ∈ Finito" by (simp only: insertaI)
  then show "(insert a A) ∪ B ∈ Finito" 
    by (simp only: Set.Un_insert_left)
qed

― ‹ Demostración estructurada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
proof (induct rule: Finito.induct)
  assume "B ∈ Finito"
  then show "{} ∪ B ∈ Finito" by simp
next
  fix A a
  assume "A ∈ Finito" 
         "B ∈ Finito ⟹ A ∪ B ∈ Finito" 
         "B ∈ Finito"
  then have "A ∪ B ∈ Finito" by simp
  then show "(insert a A) ∪ B ∈ Finito" by (simp add: insertaI)
qed

― ‹ Demostración aplicativa  detallada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
  apply (erule Finito.induct)
   apply (simp only: Un_empty_left)
  apply (simp only: Set.Un_insert_left)
  apply (simp only: insertaI)
  done

― ‹ Demostración aplicativa estructurada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
  apply (erule Finito.induct)
   apply simp 
  apply (auto intro: insertaI)
  done

― ‹ Demostración automática ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
  by (induct rule: Finito.induct)
     (auto intro: insertaI)

end