Razonamiento automático (2010-11) Razonamiento automático (2010-11)

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 }
      
      { 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





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

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
oops

end