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

RA_Relacion_1

theory Relacion_1 imports Main begin

(* Demostrar los siguientes lemas usando sólo las reglas básicas de deducción

  natural de la lógica proposicional. *)

lemma I: "A ⟶ A" proof

 assume 1: "A"

qed

lemma 0: "A ∧ B ⟶ B ∧ A" proof

 assume 1: "A ∧ B"
 from 1 have 2: "A" by (rule conjunct1) 
 from 1 have 3: "B" by (rule conjunct2)
 from 3 and 2 show "B ∧ A" by (rule conjI)

qed

lemma "A ∧ B ⟶ A ∨ B" proof

 assume 1: "A ∧ B"
 from 1 have 2: "A" by (rule conjunct1)
 from 1 have 3: "B" by (rule conjunct2)
 from 2 show "A ∨ B" by (rule disjI1)

qed

lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)" proof

 assume 1: "(A ∨ B) ∨ C"
 show "A ∨ (B ∨ C)"
 proof -
   note 1
   moreover{
     assume 2: "A ∨ B"
     have "A ∨ (B ∨ C)"
       proof -
         note 2
         moreover{
           assume 3: "A"
           from 3 have 4:"A ∨ (B ∨ C)" by (rule disjI1)
         }
         moreover{
           assume 5:"B"
           from 5 have 6: "B ∨ C" by (rule disjI1)
           from 6 have 7: "A ∨ (B ∨ C)" by (rule disjI2)
         }
         ultimately show "A ∨ (B ∨ C)" by (rule disjE)
       qed
     }
     moreover{
       assume 8: "C"
       from 8 have 9: "B ∨ C" by (rule disjI2)
       from 9 have "A ∨ (B ∨ C)" by (rule disjI2)
     }
     ultimately show "A ∨ (B ∨ C)" by (rule disjE)
   qed

qed

lemma Aux:

 assumes "A"
 shows "B ⟶ A"

using assms by simp

lemma K: "A ⟶ (B ⟶ A)" proof

 assume 1: "A"
 from 1 show "B ⟶ A" by (rule Aux)

qed

lemma S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))" proof

 assume 1: "(A ⟶ (B ⟶ C))"
 show "(A ⟶ B) ⟶ (A ⟶ C)"
 proof
   assume 2: "A ⟶ B"
   show "A ⟶ C"
   proof
     assume 3: "A"
     from 2 and 3 have 4: "B" by (rule mp)
     from 1 and 3 have 5: "B ⟶ C" by (rule mp)
     from 5 and 4 show 6: "C" by (rule mp)
   qed
 qed

qed

lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))" proof

 assume 1: "A ⟶ B"
 show "(B ⟶ C) ⟶ (A ⟶ C)"
 proof
   assume 2: "B ⟶ C"
   show "A ⟶ C"
   proof
     assume 3: "A"
     from 1 and 3 have 4: "B" by (rule mp)
     from 2 and 4 show 5: "C" by (rule mp)
   qed
 qed

qed

lemma "¬¬A ⟶ A" proof

 assume 1: "¬¬A"
 from 1 show "A" by (rule notnotD)

qed

lemma "A ⟶ ¬¬A" proof

 assume 1: "A"
 from 1 show "¬¬A" by (rule contrapos_pn)

qed

lemma MT:

 assumes 1: "F ⟶ G" and
         2: "¬G"
 shows "¬F"

proof (rule notI)

 assume 3: "F"
 from 1 and 3 have 4: "G" by (rule mp)
 from 2 and 4 show False by (rule notE)

qed

lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)" proof

 assume 1: "¬A ⟶ B"
 show "¬B ⟶ A"
 proof
   assume 2: "¬B"
   from 1 and 2 have 3:"¬¬A" by (rule MT)
   from 3 show "A" by (rule notnotD)
 qed

qed

lemma "((A ⟶ B) ⟶ A) ⟶ A" proof

 assume 1: "(A ⟶ B) ⟶ A"
 have 8: "¬¬A"
 proof (rule notI)
     assume 2: "¬A"
     have 3: "A ⟶ B"
     proof (rule impI)
       assume 4: "A"
       from 2 and 4 show "B" by (rule notE)
     qed
     from 1 and 3 have 5: "A" by (rule mp)
     from 2 and 5 show False by (rule notE)
 qed
 from 8 show "A" by (rule notnotD)

qed

lemma "A ∨ ¬A" proof cases

 assume "A" thus ?thesis ..

next

 assume "¬A" thus ?thesis ..

qed

lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)" proof

 {
 assume 1: "¬(A ∧ B)"
 have 2: "¬A ∨ A" by (rule excluded_middle)
 thus "¬A ∨ ¬B"
   proof (rule disjE)
     { assume 3: "¬A"
       thus  "¬A ∨ ¬B" by (rule disjI1) }
   next
     { assume 4: "A"
       have 5: "¬B ∨ B" by (rule excluded_middle)
       thus "¬A ∨ ¬B"
       proof (rule disjE)
         {assume 6: "¬B"
           thus "¬A ∨ ¬B" by (rule disjI2) }
         next
         {assume 7: "B"
            from 4 and 7 have 8: "A ∧ B" by (rule conjI)
            from 1 and 8 show "¬A ∨ ¬B" by (rule notE) }
       qed
     }      
   qed
 }

next

 { assume 1: "¬A ∨ ¬B"
   show "¬(A ∧ B)"
   proof (rule notI)
     assume 2: "A ∧ B"
     from 1 have 3:"¬A ∨ ¬B" .
     moreover
     { assume 4: "¬A"
       from 2 have 5:"A" by (rule conjunct1)
       from 4 and 5 have False by (rule notE) }
     moreover
     { assume 6: "¬B"
       from 2 have 7: "B" by (rule conjunct2)
       from 6 and 7 have False by (rule notE) }
     ultimately show False by (rule disjE)        
   qed

 }

qed

end

RA_Relacion_2

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