Edición de «Deducción natural proposicional con Isabelle/HOL basada en tácticas» - Lógica matemática y fundamentos (2018-19)

<source lang=isabelle">
theory T2b
imports Main
begin

section "Introducción"

subsection "Enunciado de teoremas"  
  
theorem primerEjemplo: "(A ⟶ B) ∨ (B ⟶ A)"
oops  

subsection "Demostración por asunción"

lemma "⟦A; B; C⟧ ⟹ B"
  apply assumption
  done

subsection "Ejemplo de aplicación de rule"

text {* 1º ejemplo de aplicación de rule *}
lemma "A ∧ B ⟹ B ∧ A"
  apply (rule conjI)
  oops

text {* 2º ejemplo de aplicación de rule *}
lemma "A ∧ B ⟹ B ∨ A"
  apply (rule disjI1)
  oops

lemma "⟦(A ∧ B) ∨ C; D⟧ ⟹ B ∨ C"    
  apply (rule disjE)
    apply assumption
  oops   
    
subsection "Ejemplo de demostración con rule y assumption"

theorem K: "A ⟶ (B ⟶ A)"
  apply (rule impI)  (* da  A ⟹ B ⟶ A *)
  apply (rule impI)  (* da ⟦A; B⟧ ⟹ A *)
  apply assumption   (* da No subgoals! *)
  done

subsection "Ejemplo de derivación con hipótesis"    
        
text {* Derivación de A, B ⊢ A ∧ (B ∧ A) *}
theorem "⟦A; B⟧ ⟹ A ∧ (B ∧ A)"
  apply (rule conjI)  (* da ⟦A; B⟧ ⟹ A
                            ⟦A; B⟧ ⟹ B ∧ A *)
   apply assumption   (* da ⟦A; B⟧ ⟹ B ∧ A *)
  apply (rule conjI)  (* da ⟦A; B⟧ ⟹ B
                            ⟦A; B⟧ ⟹ A *)
   apply assumption   (* da ⟦A; B⟧ ⟹ A *)
  apply assumption    (* da No subgoals *)
  done 

text {* La prueba anterior se puede simplificar usando assumption+ *}
theorem "⟦A; B⟧ ⟹ A ∧ (B ∧ A)"
  apply (rule conjI)  (* da ⟦A; B⟧ ⟹ A
                            ⟦A; B⟧ ⟹ B ∧ A *)
   apply assumption   (* da ⟦A; B⟧ ⟹ B ∧ A *)
  apply (rule conjI)  (* da ⟦A; B⟧ ⟹ B
                            ⟦A; B⟧ ⟹ A *)
   apply assumption+  (* da No subgoals *)
  done 
    
subsection "Ejemplo de aplicación de erule"
    
lemma "⟦(A ∧ B) ∨ C; D⟧ ⟹ B ∨ C"    
  apply (erule disjE)
  oops

text {* Demostración con erule *}    
lemma "A ∨ B ⟹ B ∨ A"
  apply (erule disjE)   (* da A ⟹ B ∨ A
                              B ⟹ B ∨ A*)
   apply (rule disjI2)  (* da A ⟹ A
                              B ⟹ B ∨ A *)
   apply assumption     (* da B ⟹ B ∨ A *)
  apply (rule disjI1)   (* da B ⟹ B *)
  apply assumption      (* da No subgoals *)
  done

text {* Variación de la demostración anterior cambiando erule por rule *}
lemma "A ∨ B ⟹ B ∨ A"
  apply (rule disjE)    (* da A ∨ B ⟹ ?P ∨ ?Q
                              ⟦A ∨ B; ?P⟧ ⟹ B ∨ A
                              ⟦A ∨ B; ?Q⟧ ⟹ B ∨ A *)
    apply assumption    (* da ⟦A ∨ B; A⟧ ⟹ B ∨ A
                              ⟦A ∨ B; B⟧ ⟹ B ∨ A *) 
   apply (rule disjI2)  (* da ⟦A ∨ B; A⟧ ⟹ A
                              ⟦A ∨ B; B⟧ ⟹ B ∨ A*)
   apply assumption     (* da ⟦A ∨ B; B⟧ ⟹ B ∨ A *)
  apply (rule disjI1)   (* da ⟦A ∨ B; B⟧ ⟹ B *)
  apply assumption      (* da No subgoals! *)
  done
    
subsection "Ejemplo de aplicación de drule"
    
lemma "⟦A ⟶ B; A ∧ C⟧ ⟹ B ∧ C"    
  apply (drule mp)
  oops

text {* Demostración con drule *}    
lemma "A ∧ B ⟹ A"
  apply (drule conjunct1) (* da A ⟹ A *)
  apply assumption        (* da No subgoals! *)
  done   

subsection "Ejemplo de aplicación de frule"
    
lemma "⟦A ⟶ B; A ∧ C⟧ ⟹ B ∧ C"    
  apply (frule mp)
  oops

text {* Demostración con frule *}    
lemma "A ∧ B ⟹ A"
  apply (frule conjunct1)  (* da ⟦A ∧ B; A⟧ ⟹ A *)
  apply assumption         (* da No subgoals! *)
  done  
  
subsection "Ejemplo de aplicación de erule_tac"
    
lemma "⟦A ∧ B; C ∧ (B ∧ D)⟧ ⟹ B ∧ D"
  apply (erule_tac Q="B ∧ D" in conjE)
  apply assumption
  done

lemma "⟦A ∧ B; C ∧ (B ∧ D)⟧ ⟹ B ∧ D"
  apply (erule conjE)
  oops

text {* Demostración con erule_tac *}    
lemma "⟦A ∧ B; C ∧ D⟧ ⟹ D"
  apply (erule_tac P=C in conjE)  (* da ⟦A ∧ B; C; D⟧ ⟹ D *)
  apply assumption                (* da No subgoals! *)
  done  
    
text {* Demostración sin erule_tac *}    
lemma "⟦A ∧ B; C ∧ D⟧ ⟹ D"
  apply (erule conjE)  (* da ⟦C ∧ D; A; B⟧ ⟹ D *)
  apply (erule conjE)  (* da ⟦A; B; C; D⟧ ⟹ D *)
  apply assumption     (* da No subgoals! *)
  done  
    
subsection "Cálculo de secuentes"
    
lemma "A ⟹ P ∧ Q"  
  apply (rule conjI)
  oops
    
lemma "⟦A; P ∧ Q⟧ ⟹ R"
  apply (erule conjE)
  oops
    
lemma "A ⟹ P ∨ Q"
  apply (rule disjI1)
  oops
    
lemma "A ⟹ P ∨ Q"
  apply (rule disjI2)
  oops
    
lemma "⟦A; P ∨ Q⟧ ⟹ R"
  apply (erule disjE)
  oops
    
lemma "A ⟹ P ⟶ Q"
  apply (rule impI)
  oops

lemma "⟦A; P ⟶ Q⟧ ⟹ R"
  apply (erule impE)
  oops
    
lemma "⟦A; False⟧ ⟹ P"
  apply (erule FalseE)
  done
    
lemma "A ⟹ ¬P"
  apply (rule notI)
  oops
    
lemma "⟦A; P; ¬P⟧ ⟹ R"
  apply (erule notE, assumption)
  done

lemma "A ⟹ ¬P ∨ P"
  apply (rule excluded_middle)
  done   
    
subsection "Ejemplos de pruebas"
  
lemma "((S ∨ R) ∧ ¬S) ⟶ R" 
  apply (rule impI)        (* da (S ∨ R) ∧ ¬ S ⟹ R *)
  apply (frule conjunct1)  (* da ⟦(S ∨ R) ∧ ¬ S; S ∨ R⟧ ⟹ R *)
  apply (erule disjE)      (* da ⟦(S ∨ R) ∧ ¬ S; S⟧ ⟹ R
                                 ⟦(S ∨ R) ∧ ¬ S; R⟧ ⟹ R *)
   apply (drule conjunct2) (* da ⟦S; ¬ S⟧ ⟹ R
                                 ⟦(S ∨ R) ∧ ¬ S; R⟧ ⟹ R *)
   apply (erule notE)      (* da S ⟹ S
                                 ⟦(S ∨ R) ∧ ¬ S; R⟧ ⟹ R *)
   apply assumption+       (* da No subgoals! *)
  done
  
lemma "(C ∨ P) ∧ (C ⟶ S) ∧ ¬P ⟶ S"
  apply (rule impI)     (* da (C ∨ P) ∧ (C ⟶ S) ∧ ¬ P ⟹ S *)
  apply (erule conjE)+  (* da ⟦C ∨ P; C ⟶ S; ¬ P⟧ ⟹ S *)
  apply (erule disjE)   (* da ⟦C ⟶ S; ¬ P; C⟧ ⟹ S
                              ⟦C ⟶ S; ¬ P; P⟧ ⟹ S *)
   apply (erule impE)   (* da ⟦¬ P; C⟧ ⟹ C
                              ⟦¬ P; C; S⟧ ⟹ S
                              ⟦C ⟶ S; ¬ P; P⟧ ⟹ S *)
    apply assumption+   (* da ⟦C ⟶ S; ¬ P; P⟧ ⟹ S *)
  apply (erule notE)    (* da ⟦C ⟶ S; P⟧ ⟹ P *)
  apply assumption      (* da No subgoals! *)
  done

subsection "La regla de corte"
  
lemma aux: "A ⟹ A ∨ B"
  sorry
    
lemma "P ∧ Q ⟹ Q"
  apply (cut_tac aux) 
  oops

lemma "¬(¬p ∧ ¬q) ⟹ p ∨ q"
  apply (cut_tac P=p in excluded_middle)
  apply (erule disjE)
   apply (cut_tac P=q in excluded_middle)
   apply (erule disjE)
    apply (erule notE)
    apply (rule conjI)
     apply assumption+
   apply (erule disjI2)
  apply (erule disjI1)
  done
    
text {* Ejemplo de case_tac *}
lemma "P ∧ Q ⟹ Q"
  apply (case_tac "P") (* da ⟦P ∧ Q; P⟧ ⟹ Q
                             ⟦P ∧ Q; ¬ P⟧ ⟹ Q *)
  oops

text {* La demostración anterior usando case_tac *}    
lemma "¬(¬p ∧ ¬q) ⟹ p ∨ q"
  apply (case_tac p)
   apply (erule disjI1)
  apply (case_tac q)
  apply (erule disjI2)
  apply (erule notE)
  apply (rule conjI)
  apply assumption+
  done
    
subsection "Ejemplo de demostración automática"

lemma "⟦A ∧ B; C ∧ (B ∧ D)⟧ ⟹ B ∧ D"
  apply simp
  done

section "Ejemplos del tema 2"

subsection {* Reglas de la conjunción *}

text {* 
  Ejemplo 1 (p. 4). Demostrar que
     p ∧ q, r ⊢ q ∧ r.
  *}     

lemma ejemplo_1:  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  apply (rule conjI)
  apply (erule conjunct2)
  apply assumption  
  done  
     
subsection {* Reglas de la doble negación *}

text {*
  La regla de eliminación de la doble negación es
  · notnotD: ¬¬ P ⟹ P

  Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
  introducción de la doble negación
  · notnotI: P ⟹ ¬¬ P
  aunque, de momento, no detallamos su demostración.
*}

lemma notnotI [intro!]: "P ⟹ ¬¬ P"
by auto

text {*
  Ejemplo 2. (p. 5)
       p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r
*}

lemma ejemplo_2_A: "⟦p; ¬¬(q ∧ r) ⟧ ⟹ ¬¬p ∧ r"
  apply (rule conjI)
   apply (rule notnotI)
   apply assumption
  apply (drule notnotD)
  apply (erule conjunct2)
  done
  
subsection {* Regla de eliminación del condicional *}

text {*
  La regla de eliminación del condicional es la regla del modus ponens
  · mp: ⟦P ⟶ Q; P⟧ ⟹ Q 
*}

text {* 
  Ejemplo 3. (p. 6) Demostrar que
     ¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p
*}

lemma ejemplo_3: "⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p"
  apply (erule mp)
  apply assumption
  done
    
text {* 
  Ejemplo 4 (p. 6) Demostrar que
     p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r
 *}

lemma ejemplo_4: "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
  apply (drule mp)
   apply assumption
  apply (drule mp)
   apply assumption
  apply (drule mp)
   apply assumption+
  done    
      
subsection {* Regla derivada del modus tollens *}

text {*
  Para ajustarnos al tema de LI vamos a introducir la regla del modus
  tollens
  · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  aunque, de momento, sin detallar su demostración.
*}

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

text {*
  Ejemplo 5 (p. 7). Demostrar
     p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q
 *}

lemma ejemplo_5_: "⟦p ⟶ (q ⟶ r); p; ¬r ⟧ ⟹ ¬q"
  apply (drule mp)
   apply assumption
  apply (erule mt)
  apply assumption
  done
    
text {* 
  Ejemplo 6. (p. 7) Demostrar 
     ¬p ⟶ q, ¬q ⊢ p
*}

lemma ejemplo_6: "⟦¬p ⟶ q; ¬q⟧ ⟹ p"  
  apply (drule mt)
   apply assumption
  apply (erule notnotD)
  done
    
text {* 
  Ejemplo 7. (p. 7) Demostrar
     p ⟶ ¬q, q ⊢ ¬p
  *}

lemma ejemplo_7: "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"  
  apply (erule mt)
  apply (erule notnotI)
  done
    
subsection {* Regla de introducción del condicional *}

text {*
  La regla de introducción del condicional es
  · impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

text {* 
  Ejemplo 8. (p. 8) Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
*}

lemma ejemplo_8: "p ⟶ q ⟹ ¬q ⟶ ¬p"
  apply (rule impI)
  apply (erule mt)
  apply assumption
  done
    
text {* 
  Ejemplo 9. (p. 9) Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ ¬¬q
*}

lemma ejemplo_9: "¬q ⟶ ¬p ⟹ p ⟶ ¬¬q"  
  apply (rule impI)
  apply (erule mt)
  apply (rule notnotI)
  apply assumption
  done
    
text {* 
  Ejemplo 10 (p. 9). Demostrar
     ⊢ p ⟶ p
*}

lemma ejemplo_10: "p ⟶ p"
  apply (rule impI)
  apply assumption
  done
    
text {*
  Ejemplo 11 (p. 10) Demostrar
     ⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))
 *}

lemma ejemplo_11_A: "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"  
  apply (rule impI)+
  apply (erule mp)
  apply (drule mt)
   apply (rule notnotI)
   apply assumption
  apply (rule notnotD)
  apply assumption
  done
    
subsection {* Reglas de la disyunción *}

text {*
  Las reglas de la introducción de la disyunción son
  · disjI1: P ⟹ P ∨ Q
  · disjI2: Q ⟹ P ∨ Q
  La regla de elimación de la disyunción es
  · disjE:  ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
*}

text {* 
  Ejemplo 12 (p. 11). Demostrar
     p ∨ q ⊢ q ∨ p
*}

lemma ejemplo_12: "p ∨ q ⟹ q ∨ p"  
  apply (erule disjE)
   apply (rule disjI2)
   prefer 2
   apply (rule disjI1)
   apply assumption+ 
  done
    
text {* 
  Ejemplo 13. (p. 12) Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
*}

lemma ejemplo_13_A: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"  
  apply (rule impI)
  apply (erule disjE)
   apply (rule disjI1)
   prefer 2
   apply (drule mp)
  prefer 2
    apply (rule disjI2)
    apply assumption+
  done
  
subsection {* Regla de copia *}

text {* 
  Ejemplo 14 (p. 13). Demostrar
     ⊢ p ⟶ (q ⟶ p)
*}

lemma ejemplo_14_A: "p ⟶ (q ⟶ p)"  
  apply (rule impI)+
  apply assumption
  done
    
subsection {* Reglas de la negación *}

text {*
  La regla de eliminación de lo falso es
  · FalseE: False ⟹ P
  La regla de eliminación de la negación es
  · notE: ⟦¬P; P⟧ ⟹ R
  La regla de introducción de la negación es
  · notI: (P ⟹ False) ⟹ ¬P
*}

text {*
  Ejemplo 15 (p. 15). Demostrar
     ¬p ∨ q ⊢ p ⟶ q
*}

lemma ejemplo_15: "¬p ∨ q ⟹ p ⟶ q"  
  apply (rule impI)
  apply (erule disjE)
   apply (erule notE)
   apply assumption+
  done
    
text {* 
  Ejemplo 16 (p. 16). Demostrar
     p ⟶ q, p ⟶ ¬q ⊢ ¬p
*}

lemma ejemplo_16_A: "⟦p ⟶ q; p ⟶ ¬q⟧ ⟹ ¬p"  
  apply (rule notI)
  apply (drule mp)+
    apply assumption+
  apply (drule mp)
    prefer 2
   apply (erule notE)
   apply assumption+
  done
  
subsection {* Reglas del bicondicional *}

text {*
  La regla de introducción del bicondicional es
  · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q
  Las reglas de eliminación del bicondicional son
  · iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P 
  · iffD2: ⟦P ⟷ Q; Q⟧ ⟹ P
*}

text {* 
  Ejemplo 17 (p. 17) Demostrar
*}

lemma ejemplo_17: "(p ∧ q) ⟷ (q ∧ p)"  
  apply (rule iffI)
   apply (rule conjI)
    apply (erule conjunct2)
   apply (erule conjunct1)
    apply (rule conjI)
    apply (erule conjunct2)
  apply (erule conjunct1)
  done
  
text {*
  Ejemplo 18 (p. 18). Demostrar
     p ⟷ q, p ∨ q ⊢ p ∧ q
*}

lemma ejemplo_18_A: "⟦p ⟷ q; p ∨ q⟧ ⟹ p ∧ q"  
  apply (erule disjE)
   apply (rule conjI)
    apply assumption
    apply (erule iffD1)
    apply assumption
    apply (rule conjI)
    apply (erule iffD2)
   apply assumption+
  done
    
subsection {* Reglas derivadas *}

subsubsection {* Regla del modus tollens *}

text {* 
  Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir de
  las reglas básicas. 
*}

lemma ejemplo_20: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"  
  apply (rule notI)
  apply (drule mp)
   apply assumption
  apply (erule notE)
  apply assumption
  done
    
subsubsection {* Regla de la introducción de la doble negación *}

text {*
  Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
  negación a partir de las reglas básicas.
*}

lemma ejemplo_21_A: "F ⟹ ¬¬F"  
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done
    
subsubsection {* Regla de reducción al absurdo *}

text {*
  La regla de reducción al absurdo en Isabelle se corresponde con la
  regla clásica de contradicción 
  · ccontr: (¬P ⟹ False) ⟹ P
*}

subsubsection {* Ley del tercio excluso *}

text {*
  La ley del tercio excluso es 
  · excluded_middle: ¬P ∨ P
*}

text {*
  Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
  las reglas básicas.  
*}
  
lemma ejemplo_22: "F ∨ ¬F"
  oops

text {*
  Ejemplo 23 (p. 24). Demostrar
     p ⟶ q ⊢ ¬p ∨ q
*}

lemma ejemplo_23: "p ⟶ q ⟹ ¬p ∨ q"
  apply (cut_tac P="p" in excluded_middle)
  apply (erule disjE)
   apply (rule disjI1)
    prefer 2
   apply (drule mp)
    prefer 2
    apply (rule disjI2)
    apply assumption+
    done
  
subsection {* Demostraciones por contradicción *}

text {* 
  Ejemplo 24. Demostrar que 
     ¬p, p ∨ q ⊢ q
*}

lemma ejemplo_24: "⟦¬p ; p ∨ q⟧ ⟹ q"  
  apply (erule disjE)
   apply (erule notE)
   apply assumption+
  done
   
end  
</source>

=== Bibliografía ===

* [http://www.phil.cmu.edu/~avigad/formal/FormalCheatSheet.pdf Isabelle / Proof General Cheat Sheet].
* [https://isabelle.in.tum.de/dist/Isabelle2018/doc/tutorial.pdf Isabelle/HOL: A Proof Assistant for Higher-Order Logic]. Cap. 5: The Rules of the Game.