Theory PMLinHOL_deep_tests

section‹Appendix: proof automation tests\label{sec:automation_tests}›
subsection‹Tests with the deep embedding›

theory PMLinHOL_deep_tests  
  imports PMLinHOL_deep                                               
begin   

―‹Hilbert calculus: proving that the schematic axioms and rules implied by the embedding›
lemma H1: "⊨⇧^d φ ⊃⇧^d (ψ ⊃⇧^d φ)" by auto
lemma H2: "⊨⇧^d (φ ⊃⇧^d (ψ ⊃⇧^d γ)) ⊃⇧^d ((φ ⊃⇧^d ψ) ⊃⇧^d (φ ⊃⇧^d γ)) " by auto
lemma H3: "⊨⇧^d (¬⇧^dφ  ⊃⇧^d ¬⇧^dψ) ⊃⇧^d (ψ ⊃⇧^d φ)" by auto
lemma MP: "⊨⇧^d φ ⟹ ⊨⇧^d (φ  ⊃⇧^d ψ) ⟹ ⊨⇧^d ψ" by auto

―‹Reasoning with the Hilbert calculus: interactive and fully automated›
lemma HCderived1: "⊨⇧^d (φ ⊃⇧^d φ)" ―‹sledgehammer(HC1 HC2 HC3 MP) returns: by (metis HC1 HC2 MP)›  
proof -  
  have 1: "⊨⇧^d φ ⊃⇧^d ((ψ ⊃⇧^d φ) ⊃⇧^d φ)" using H1 by auto 
  have 2: "⊨⇧^d (φ ⊃⇧^d ((ψ ⊃⇧^d φ) ⊃⇧^d φ)) ⊃⇧^d ((φ ⊃⇧^d (ψ ⊃⇧^d φ)) ⊃⇧^d (φ ⊃⇧^d φ))" using H2 by auto 
  have 3: "⊨⇧^d (φ ⊃⇧^d (ψ ⊃⇧^d φ)) ⊃⇧^d (φ ⊃⇧^d φ)" using 1 2 MP by meson
  have 4: "⊨⇧^d φ ⊃⇧^d (ψ  ⊃⇧^d φ)" using H1 by auto 
  thus ?thesis using 3 4 MP by meson 
qed

lemma HCderived2: "⊨⇧^d φ ⊃⇧^d (¬⇧^dφ  ⊃⇧^d ψ) " by (metis H1 H2 H3 MP) 
lemma HCderived3: "⊨⇧^d (¬⇧^dφ  ⊃⇧^d φ) ⊃⇧^d φ" by (metis H1 H2 H3 MP) 
lemma HCderived4: "⊨⇧^d (φ ⊃⇧^d ψ) ⊃⇧^d (¬⇧^dψ ⊃⇧^d ¬⇧^dφ) " by auto   

―‹Modal logic: the schematic necessitation rule and distribution axiom are implied›
lemma Nec: "⊨⇧^d φ ⟹ ⊨⇧^d □⇧^dφ" by auto
lemma Dist:  "⊨⇧^d □⇧^d(φ ⊃⇧^d ψ) ⊃⇧^d (□⇧^dφ ⊃⇧^d □⇧^dψ) " by auto

―‹Correspondence theory: correct statements›
lemma cM:  "reflexive R ⟷ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d □⇧^dφ ⊃⇧^d φ)" ―‹sledgehammer: Proof found› oops (**)
lemma cBa: "symmetric R ⟶ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ))" by auto 
(**)lemma cBb: "symmetric R ⟵ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d φ ⊃⇧^d □⇧^d(◇⇧^dφ))" ―‹sledgehammer: No proof› oops
lemma c4a: "transitive R ⟶ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d □⇧^dφ ⊃⇧^d □⇧^d(□⇧^dφ))" by (metis RelativeTruthD.simps)  
(**)lemma c4b: "transitive R ⟵ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d □⇧^dφ ⊃⇧^d □⇧^d(□⇧^dφ))" ―‹sledgehammer: No proof› oops

―‹Correspondence theory: incorrect statements›
lemma "reflexive R ⟶ (∀φ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d □⇧^dφ ⊃⇧^d □⇧^d(□⇧^dφ))" nitpick[card 𝗐=3] oops ―‹nitpick: Cex.›

―‹Simple, incorrect validity statements›
lemma "⊨⇧^d φ ⊃⇧^d □⇧^dφ" nitpick[card 𝗐=2, card 𝒮= 1] oops ―‹nitpick: Counterexample: modal collapse not implied›
lemma "⊨⇧^d □⇧^d( □⇧^dφ ⊃⇧^d  □⇧^dψ) ∨⇧^d □⇧^d( □⇧^dψ ⊃⇧^d  □⇧^dφ)" nitpick[card 𝗐=3] oops ―‹nitpick: Counterexample›
lemma "⊨⇧^d (◇⇧^d(□⇧^d φ)) ⊃⇧^d  □⇧^d(◇⇧^d φ)" nitpick[card 𝗐=2] oops ―‹nitpick: Counterexample› 

―‹Implied axiom schemata in S5›
lemma KB: "symmetric R ⟶ (∀φ ψ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d (◇⇧^d(□⇧^dφ)) ⊃⇧^d  □⇧^d(◇⇧^dφ))" by auto
lemma K4B: "symmetric R ∧ transitive R ⟶ (∀φ ψ W V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d □⇧^d( □⇧^dφ ⊃⇧^d  □⇧^dψ) ∨⇧^d □⇧^d( □⇧^dψ ⊃⇧^d  □⇧^dφ))" by (smt (z3) OrD_def RelativeTruthD.simps)
end