Relación 2

header {* 2ª relación de ejercicios *}

theory Relacion_2
imports Main 
begin

text {*
  Demostrar o refutar los siguientes lemas usando sólo las reglas
  básicas de deducción natural de la lógica proposicional y de la lógica
  de predicados (allI, allE, exI y exE). 
*}

lemma "(∃x.∀y. P x y) ⟶ (∀y.∃x. P x y)"
proof (rule impI)
  assume 1: "∃x. ∀y. P x y"
  show "∀y. ∃x. P x y"
  proof (rule allI)
    from 1 obtain "x" where 2: "∀y. P x y" by (rule exE)
    fix y
    from 2 have 3: "P x y" by (rule allE)
    from 3 show 4: "∃x. P x y" by (rule exI)
  qed
qed

lemma "(∀x. P x ⟶ Q) = ((∃x. P x) ⟶ Q)"
proof
 { assume 1: "∀x. P x ⟶ Q"
   show "(∃x. P x) ⟶ Q"
   proof
     assume "∃x. P x"
     then obtain a where "P a" by (rule exE)
     have "P a ⟶ Q" using 1 by (rule allE)
     thus "Q" using `P a` by (rule mp)
   qed }
next
 { assume 2: "(∃x. P x) ⟶ Q"
   show "∀x. P x ⟶ Q"
   proof
     fix a
     show "P a ⟶ Q"
     proof
       assume "P a"
       hence 3: "∃x. P x" by (rule exI)
       from 2 and 3 show "Q" by (rule mp)
     qed
   qed }
qed

lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
proof
  { assume 1: "(∀ x. P x) ∧ (∀ x. Q x)"
    show "∀ x. (P x ∧ Q x)"
    proof (rule allI)
      from 1 have 2: "∀ x. P x" by (rule conjE)
      from 1 have 3: "∀ x. Q x" by (rule conjE)
      fix a
      from 2 have 4: "P a" by (rule allE)
      from 3 have 5: "Q a" by (rule allE)
      from 4 and 5 show 6: "(P a) ∧ (Q a)" by (rule conjI)
    qed }
next
  { assume 7: "∀ x. (P x ∧ Q x)"
    show "(∀ x. P x) ∧ (∀ x. Q x)"
    proof
      show "(∀ x. P x)"
      proof (rule allI)
        fix a
        from 7 have 8: "P a ∧ Q a" by (rule allE)
        from 8 show "P a" by (rule conjE)
      qed
    next
      show "(∀ x. Q x)"
      proof (rule allI)
        fix a
        from 7 have 9: "P a ∧ Q a" by (rule allE)
        from 9 show "Q a" by (rule conjE)
      qed 
    qed }
qed

lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
oops

text {* 
  Esta fórmula de la lógica de predicados es falsa. La implicación de
  izquierda a derecha sí es cierta y a continuación la probamos:
*}

lemma "((∀ x. P x) ∨ (∀ x. Q x)) ⟶ (∀ x. (P x ∨ Q x))"
proof (rule impI)
  assume 1: "(∀ x. P x) ∨ (∀ x. Q x)"
  show "∀ x. (P x ∨ Q x)"
  proof (rule allI)
    fix x
    note 1
    moreover{
      assume 11: "∀ x. P x"   
      from 11 have 111: "P x" by (rule allE)
      from 111 have "P x ∨ Q x" by (rule disjI1)}
    moreover{  
      assume 12: "∀ x. Q x"
      from 12 have 121: "Q x" by (rule allE)
      from 121 have "P x ∨ Q x" by (rule disjI2)}
    ultimately show "(P x ∨ Q x)" by (rule disjE)
  qed
qed

text {* 
  La implicación de derecha a izquierda es falsa y a continuación
  construimos un contraejemplo. Supongamos un modelo en el que fuese
  verdadera: 
    (∀ x. (P x ∨ Q x)) ∧ (∃x. ¬P x ) ∧ (∃x. ¬Q x),
  lo cual equivale a 
    (∀ x. (P x ∨ Q x)) ∧ ¬(∀ x. P x ) ∧ ¬(∀ x. Q x)
  y esto es contradictorio con 
    (∀ x. P x) ∨ (∀ x. Q x). 
  Un ejemplo en lenguaje natural que ilustra esto es el siguiente: todos 
  los números reales son algebraicos o trascendentes, pero de ello no
  podemos concluir que o bien todos los números reales son algebraicos o bien todos los
  números reales son trascendentes.
*}

text {*
  Comentario de J.A. Alonso: ¿Cómo se calcula un contraejemplo con Isabelle?
*}

lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
proof
  {assume 1:"((∃ x. P x) ∨ (∃ x. Q x))"
   show "(∃ x. (P x ∨ Q x))"
   proof -
     note 1
     moreover
     { assume 2: "(∃ x. P x)"
       obtain a where 3: "P a" using 2 by (rule exE)
       from 3 have 4: "P a ∨ Q a" .. 
       from 4 have "(∃ x. (P x ∨ Q x))" by (rule exI) }
     moreover
     { assume 2: "(∃ x. Q x)"
       obtain a where 3: "Q a" using 2 by (rule exE)
       from 3 have 4: "P a ∨ Q a" .. 
       from 4 have "(∃ x. (P x ∨ Q x))" by (rule exI) }
     ultimately show "(∃ x. (P x ∨ Q x))" by (rule disjE)  
   qed}
next
  {assume 1:"(∃ x. (P x ∨ Q x))"
   obtain a where 2: "P a ∨ Q a" using 1 by (rule exE)
   show "((∃ x. P x) ∨ (∃ x. Q x))" using 2
   proof 
     { assume 3: "P a"
       from 3 have 4: "(∃ x. P x)" by (rule exI)
       from 4 show "((∃ x. P x) ∨ (∃ x. Q x))" .. }
     { assume 3: "Q a"
       from 3 have 4: "(∃ x. Q x)" by (rule exI)
       from 4 show "((∃ x. P x) ∨ (∃ x. Q x))" .. }
   qed }
qed

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops

text {*
  Esta fórmula de la lógica de predicados es falsa y a continuación
  construimos un contraejemplo. Supongamos un modelo en el que fuese verdadera:
    (∀x.∃y. P x y) ∧ (∀x. P x x) ∧ (∀x.∀y. (¬(x = y) ⟶ ¬(P y x))) ∧ (∃x.∃y. (¬(x = y))) 
  y esto es contradictorio con 
    (∃y. ∀x. P x y).
  Si interpretamos P como <<tener exactamente los mismos padres y los
  mismos hermanos que>> es obvio que la implicación es falsa. Un
  contraejemplo más conocido se obtiene interpretando P como la relación
  <<menor o igual que>> sobre los números reales, de modo que el
  antecedente indicaría que dichos números no están acotados
  superiormente, mientras que el consecuente indicaría que el conjunto
  de los reales tiene al menos una cota superior.
 *}

text {*
  Comentario de J.A. Alonso: ¿Cómo se calcula un contraejemplo con Isabelle?
*}

-- "La forma más corta y más automática es la que sigue"
lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
by auto

end