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

RA_Relacion_1

theory Relacion_2 imports Main begin

(* 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
     fix a
     from 7 have 8: "P a ∧ Q a" by (rule allE)
     from 8 have 9: "P a" by (rule conjE)
     (* seguir... *)
     from 8 have 11: "Q a" by (rule allE)
     (* seguir... *)
   qed

} qed

oops

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))" oops

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)" oops (* proof (rule impI)

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

• )

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)" proof {

 assume 1: "¬ (∀ x. P x)" 
 show "∃ x. ¬ P x"
   proof
     

   qed

} next {

 assume 2: "∃ x. ¬ P x"
 show "¬ (∀ x. P x)"
   proof
     
   qed

} qed

end