Deducción natural en lógica de primer orden con Isabelle/HOL basada en tácticas

theory T4b
imports Main
begin

section "Introducción"

subsection "Reglas de primer orden en Isabelle/HOL"  

thm spec [no_vars]
  (* da ∀x. P x ⟹ P x *)  
  
thm allE [no_vars]
  (* da ⟦∀x. P x; P x ⟹ R⟧ ⟹ R *)  
  
thm allI [no_vars]
  (* da (⋀x. P x) ⟹ ∀x. P x *)  
  
thm exI 
  (* da ?P ?x ⟹ ∃x. ?P x *)  
  
thm exE [no_vars]
  (* da ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q *)  

subsection "Ejemplos de demostraciones"

text {* Ejemplo con spec y exI*}  
lemma "∀x. P x ⟹ ∃y. P y"  
  apply (drule_tac x=a in spec)  (* da P a ⟹ ∃y. P y *)
  apply (rule_tac x=a in exI)    (* da P a ⟹ P a *)
  apply assumption               (* da  No subgoals!*)
  done
  
text {* Ejemplo con spec y exI*}  
lemma "∀x. P x ⟹ ∃x. P x"
  apply (rule exI)    (* da ∀x. P x ⟹ P ?x *)
  apply (erule spec)  (* da No subgoals! *)
  done

text {* Ejemplo con allE y exI*}  
lemma "∀x. P x ⟹ ∃x. P x"
  apply (erule allE)  (* da P ?x ⟹ ∃x. P x*)
  apply (erule exI)   (* da No subgoals! *)
  done
 
text {* Ejemplo con erule_tac *}  
lemma "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z"
  apply (rule allI)              (* da ⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ 
                                           ⟹ Q z *)
  apply (erule_tac x=z in allE)  (* da ⋀z. ⟦∀y. P y; P z ⟶ Q z⟧ 
                                           ⟹ Q z *)
  apply (erule_tac x=z in allE)  (* da ⋀z. ⟦P z ⟶ Q z; P z⟧ ⟹ Q z *)
  apply (erule impE)             (* da ⋀z. P z ⟹ P z
                                       ⋀z. ⟦P z; Q z⟧ ⟹ Q z *)
   apply assumption+             (* da No subgoals! *)
  done

text {* Ejemplo sin erule_tac *}  
lemma "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z"
  apply (rule allI)    (* da ⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z *)  
  apply (erule allE)   (* da ⋀z. ⟦∀y. P y; P (?x2 z) ⟶ Q (?x2 z)⟧ 
                                 ⟹ Q z *)  
  apply (erule allE)   (* da ⋀z. ⟦P (?x2 z) ⟶ Q (?x2 z); P (?y4 z)⟧ 
                                 ⟹ Q z *)  
  apply (erule mp)     (* da ⋀z. P (?y4 z) ⟹ P z *)  
  apply assumption     (* da No subgoals *)  
  done
    
text {* Ejemplo con exE *}    
lemma "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)"
  apply (rule impI)              (* da (∃z. P z) ∧ Q ⟹ ∃y. P y ∧ Q *)
  apply (erule conjE)            (* da ⟦∃z. P z; Q⟧ ⟹ ∃y. P y ∧ Q *)
  apply (erule exE)              (* da ⋀z. ⟦Q; P z⟧ ⟹ ∃y. P y ∧ Q *)
  apply (rule_tac x="z" in exI)  (* da ⋀z. ⟦Q; P z⟧ ⟹ P z ∧ Q *)
  apply (rule conjI)             (* da ⋀z. ⟦Q; P z⟧ ⟹ P z
                                       ⋀z. ⟦Q; P z⟧ ⟹ Q *)
   apply assumption+             (* da No subgoals! *)
  done

subsection "Cálculo de secuentes de primer orden"
  
lemma "A ⟹ ∀x. P x"
  apply (rule allI) (* da ⋀x. A ⟹ P x *)  
  oops
    
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
  apply (erule allE)   (* da ⟦A; P ?x⟧ ⟹ Q *)
  oops

lemma "⟦A; ∀x. P x⟧ ⟹ Q"
  apply (erule_tac x=t in allE)   (* da ⟦A; P t⟧ ⟹ Q *)
  oops

lemma "⟦A; ∀x. P x⟧ ⟹ Q"
  apply (frule spec) (* da ⟦A; ∀x. P x; P ?x⟧ ⟹ Q *)
  oops

lemma "⟦A; ∀x. P x⟧ ⟹ Q"
  apply (frule_tac x=t in spec) (* da ⟦A; ∀x. P x; P t⟧ ⟹ Q *)
  oops

lemma "A ⟹ ∃x. P x"
  apply (rule exI) (* da A ⟹ P ?x *)
  oops
    
lemma "A ⟹ ∃x. P x"
  apply (rule_tac x=t in exI) (* da A ⟹ P t *)
  oops

lemma "⟦A; ∃x. P x⟧ ⟹ Q"
  apply (erule exE)  (* da ⋀x. ⟦A; P x⟧ ⟹ Q *)
  oops  

section "Ejemplos del tema 6"

subsection {* Reglas del cuantificador universal *}

lemma ej1: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
  apply (erule allE)
  apply (erule mp)
  apply assumption
  done
    
lemma ej2: "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)"
  apply (rule allI)
  apply (erule allE)+
  apply (erule mp)
  apply assumption
  done
    
subsection "Reglas del cuantificador existencial"

lemma ej3: "∀x. P x ⟹ ∃y. P y"
  apply (erule allE)
  apply (erule exI)
  done
    
lemma ej4: "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z"
  apply (erule exE)
  apply (erule allE)
  apply (rule exI)
  apply (erule mp)
  apply assumption
  done
    
subsection "Demostraciones de equivalencias"

lemma ej5a: "¬(∀x. P x) ⟹ ∃y. ¬P y"
  apply (rule ccontr)
  apply (erule notE)
  apply (rule allI)
  apply (rule ccontr)
  apply (erule notE)
   apply (erule exI)
  done
    
lemma ej5b: "∃x. ¬P x ⟹ ¬(∀y. P y)"
  apply (rule notI)
  apply (erule exE)
  apply (erule allE)
  apply (erule notE)
  apply assumption
  done
    
lemma ej5: "¬(∀x. P x) ⟷ (∃x. ¬P x)"
  apply (rule iffI)
   apply (erule ej5a)
  apply (erule ej5b)
  done
    
lemma ej6a: "∀x. P(x) ∧ Q(x) ⟹ (∀x. P x) ∧ (∀x. Q x)"
  apply (rule conjI)
   apply (rule allI)
   apply (erule allE)
   apply (erule conjE)
   apply assumption
  apply (rule allI)
  apply (erule allE)
  apply (erule conjE)
  apply assumption
  done
    
lemma ej6b: "(∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x"
  apply (rule allI)
  apply (rule conjI)
   apply (drule conjunct1)
   apply (erule spec)
   apply (drule conjunct2)
  apply (erule spec)
  done
    
lemma ej6: "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)"
  apply (rule iffI)
   apply (erule ej6a)
  apply (erule ej6b)
  done
    
lemma ej7a: "(∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x"
  apply (erule disjE)
   apply (erule exE)
   apply (rule exI)
   apply (erule disjI1)
  apply (erule exE)
  apply (rule exI)
  apply (erule disjI2)
  done
    
lemma ej7b: "∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)"
  apply (erule exE)
  apply (erule disjE)
   apply (rule disjI1)
   apply (erule exI)
  apply (rule disjI2)
  apply (erule exI)
  done
    
lemma ej7: "(∃x. P x) ∨ (∃x. Q x) ⟷ (∃x. P x ∨ Q x)"
  apply (rule iffI)
   apply (erule ej7a)
  apply (erule ej7b)
  done
    
lemma ej8a: "∃x y. P x y ⟹ ∃y x. P x y"
  apply (erule exE)+
  apply (rule exI)+
  apply assumption
  done
    
lemma ej8b: "∃y x. P x y ⟹ ∃x y. P x y"
  apply (erule exE)+
  apply (rule exI)+
  apply assumption
  done

lemma ej8: "(∃x y. P x y) ⟷ (∃y x. P x y)"
  apply (rule iffI)
   apply (erule ej8a)
  apply (erule ej8b)
  done
    
end

Bibliografía

• Isabelle / Proof General Cheat Sheet.
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Cap. 5: The Rules of the Game.