Relación 9

chapter {* R9: Deducción natural LPO en Isabelle/HOL *}

theory R9_Deduccion_natural_LPO
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, de los
  cuantificadores y de la igualdad: 
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P

  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y
*}

text {*
  Se usarán las reglas notnotI, mt y not_ex que demostramos a continuación.
  *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

lemma ejercicio_1: 
  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
oops
  

(* migtermor ferrenseg juacabsou josgarsan pablucoto*)
lemma ejercicio_1: 
  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
 { assume 1: "P a"
   have 2: "∃x. Q x" using assms 1 by (rule mp)} 
 then obtain b where 3: "Q b" by (rule exE)          
   (* No sé por qué salta un aviso aquí. Aún así, sin esto no se
      finaliza correctamente la demostración, y con ello sí. *) 
 then have 4: "(P a) ⟶ (Q b)" by (rule impI)
 then show 5: "∃x. P a ⟶ Q x" by (rule exI)
qed

(* ivamenjim bowma rubgonmar *)

lemma ejercicio_1_1:  
  assumes 1: "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
   {assume 2: "P a"
    have 3: "(∃x. Q x)" using 1 2 by (rule mp)
    obtain b where 4: "Q b" using 3 by (rule exE)
    then have 5: "P a ⟶ Q b" by (rule impI)
    then have 6: "∃x. P a ⟶ Q x" by (rule exI)}
   then show "∃x. P a ⟶ Q x" by simp
qed  

(* crigomgom *)
lemma ejercicio_1_2: 
  assumes 0: "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have "¬(P a) ∨ P a" by (rule excluded_middle)
  then show "∃x. P a ⟶ Q x"
  proof (rule disjE)
    assume 1 : "¬(P a)"
    {assume 2 : "P a"
     have  "Q b" using 1 2 by (rule notE)}
     then have "P a ⟶ Q b" by (rule impI)
     then show "∃x. P a ⟶ Q x" by (rule exI)
  next
    assume 3 : "P a"
    have  "∃x. Q x" using 0 3 by (rule mp)
    then obtain b where "Q b"  by (rule exE)
    then have  "P a ⟶ Q b" by (rule impI)
    then show  "∃x. P a ⟶ Q x" by (rule exI)
  qed
qed 

(* fracorjim1 *)
(* Entre corchetes se demuestra que efectivamente existe un caso *)
lemma ejercicio_1_3: 
  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
	{	
		assume "P a"
		with assms have "∃x. Q x" by (rule mp)
		then obtain x where "Q x" by (rule exE)
		hence "P a ⟶ Q x" by (rule impI)
		hence "∃x. P a ⟶ Q x" by (rule exI) 
	}
  thus ?thesis by simp
qed

(* Comentario: Usa simp *)

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       {∀x y z. R x y ∧ R y z ⟶ R x z, 
        ∀x. ¬(R x x)}
       ⊢ ∀x y. R x y ⟶ ¬(R y x)
  ------------------------------------------------------------------ *}

(* migtermor ferrenseg ivamenjim marcarmor13 serrodcal juacabsou
   marpoldia1 crigomgom bowma josgarsan rubgonmar pablucoto*) 
lemma ejercicio_2: 
  fixes R :: "'b ⇒ 'b ⇒ bool" 
  assumes 1: "∀x y z. R x y ∧ R y z ⟶ R x z"
  assumes 2: "∀x. ¬(R x x)"
  shows   "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)
fix x
show "∀y. R x y ⟶ ¬(R y x)" 
 proof (rule allI) 
  fix y
  {assume 3: "R x y"
   {assume 4: "R y x"
    have 5: "R x y ∧ R y x" using 3 4 by (rule conjI)
    also have 6: "∀ z1 z2. R x z1 ∧ R z1 z2 ⟶ R x z2" using 1 by (rule allE)
    then have 7: "∀ z. R x y ∧ R y z ⟶ R x z" by (rule allE)
    then have 8: "R x y ∧ R y x ⟶ R x x" by (rule allE)
    then have 9: "R x x" using 5 by (rule mp)
    have 10: "¬(R x x)" using 2 by (rule allE)
    then have 11: "False" using 9 by (rule notE)}
  then have 12: "¬ (R y x)" by (rule notI)}
  thus "R x y ⟶ ¬(R y x)" by (rule impI)
 qed
qed

(* ivamenjim *)
(* Semejante al anterior, pero indicando que se pruebe por la regla
  correspondiente *) 
lemma ejercicio_2_1: 
  assumes 1: "∀x y z. R x y ∧ R y z ⟶ R x z"
  assumes 2: "∀x. ¬(R x x)"
  shows   "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)
fix x
show "∀y. R x y ⟶ ¬(R y x)" 
 proof (rule allI) 
  fix y
  {assume 3: "R x y"
   {assume 4: "R y x"
    have 5: "R x y ∧ R y x" using 3 4 ..
    have 6: "∀ y z. R x y ∧ R y z ⟶ R x z" using 1 ..
    then have 7: "∀ z. R x y ∧ R y z ⟶ R x z" ..
    then have 8: "R x y ∧ R y x ⟶ R x x" ..
    then have 9: "R x x" using 5 ..
    have 10: "¬(R x x)" using 2 ..
    then have 11: "False" using 9 ..}
  then have 12: "¬ (R y x)" ..}
  thus "R x y ⟶ ¬(R y x)" ..
 qed
qed 

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}

(* ivamenjim ferrenseg paupeddeg serrodcal juacabsou marpoldia1
   crigomgom bowma josgarsan rubgonmar pablucoto*) 
lemma ejercicio_3: 
  assumes "(∀x. ∃y. P x y)"
  shows   "(∃y. ∀x. P x y)"
  quickcheck
oops  

(* Y se encuentra el contraejemplo: P = (λx. undefined)(a1 := {a2}, a2 := {a1}) *)

(* migtermor *)
fun P :: "'a ⇒ 'a ⇒ bool" where
  "P x y = (x=y)"

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

(* dancorgar *)
lemma ejercicio_3_3:
  shows   "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
oops

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
     ⊢ ∃z. P (f a) z (f (f a))
  ------------------------------------------------------------------ *}

(* ferrenseg ivamenjim *)
lemma ejercicio_4:
  fixes P :: "'b ⇒ 'b ⇒ 'b ⇒ bool" 
  assumes 1: "∀x. P a x x" and 
          2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have 4:"P a (f a) (f a)" using 1 ..
  also have 5:"∀y z. P a y z ⟶ P (f a) y (f z)" using 2 ..
  then have 6:"∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
  then have 7:"P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  also have 8:"P (f a) (f a) (f (f a))" using 7 4 by (rule mp)
  then show "∃z. P (f a) z (f (f a))" ..
qed

(* migtermor serrodcal crigomgom pablucoto*)
lemma ejercicio_4_2: 
  fixes P :: "'b ⇒ 'b ⇒ 'b ⇒ bool" 
  assumes 1: "∀x. P a x x"
  assumes 2: "∀x y z.  P x y z ⟶ P (f x) y (f z)"
  shows   " ∃z. P (f a) z (f (f a))"
proof (rule exI)
 have 3: "P a (f a) (f a)" using 1 by (rule allE)
 have 4: "∀y z.  P a y z ⟶ P (f a) y (f z)" using 2 by (rule allE)
 then have 5: "∀z.  P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
 then have 6: "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
 then show "P (f a) (f a) (f (f a))" using 3 by (rule mp)
qed

(* paupeddeg juacabsou marpoldia1 bowma rubgonmar josgarsan*)
lemma ejercicio_4_3:
  fixes P :: "'b ⇒ 'b ⇒ 'b ⇒ bool" 
  assumes " ∀x. P a x x " 
          " ∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof
  have "∀ y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
  hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)"  by (rule allE)
  hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))"  by (rule allE)
  have "P a (f a) (f a)" using assms(1) by (rule allE)
  show "P (f a) (f a) (f (f a))" 
    using `P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))` `P a (f a) (f a)`  
    by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     {∀y. Q a y, 
      ∀x y. Q x y ⟶ Q (s x) (s y)} 
     ⊢ ∃z. Qa z ∧ Q z (s (s a))
  ------------------------------------------------------------------ *}

(* ferrenseg ivamenjim *)
lemma ejercicio_5:
  assumes 1: "∀y. Q a y" and 
          2: "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof
  have 3:"Q a (s a)" using 1 ..
  also have 4:"∀y. Q a y ⟶ Q (s a) (s y)" using 2 ..
  then have 5:"Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have 6:"Q (s a) (s (s a))" using 3 by (rule mp)
  show "Q a (s a) ∧ Q (s a) (s (s a))" using 3 6 by (rule conjI)
qed

(* migtermor *)
lemma ejercicio_5_2: 
  fixes P :: "'b ⇒ 'b ⇒ bool" 
  assumes 1: "∀y. Q a y"
  assumes 2: "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows   " ∃z. Q a z ∧ Q z (s (s a))"
proof -
 have 3: "Q a (s a)" using 1 by (rule allE)
 have 4: "∀y. Q a y ⟶ Q (s a) (s y)" using 2 by (rule allE)
 then have 5: "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
 then have 6: "Q (s a) (s (s a))" using 3 by (rule mp)
 have "Q a (s a) ∧ Q (s a) (s (s a))" using 3 6 by (rule conjI)
 then show "∃z. Q a z ∧ Q z (s (s a))" by (rule exI)
qed

(* paupeddeg serrodcal juacabsou marpoldia1 crigomgom bowma rubgonmar pablucoto*)
lemma ejercicio_5_3:
  assumes "∀y. Q a y" 
          "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof 
 have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
 hence "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
 have "Q a (s a)" using assms(1) by (rule allE)
 have "Q (s a) (s (s a))" using `Q a (s a) ⟶ Q (s a) (s (s a))` `Q a (s a)` by (rule mp)
 show "Q a (s a) ∧ Q (s a) (s (s a))" 
   using `Q a (s a)` `Q (s a) (s (s a))` by (rule conjI)
qed

end