Theory TestsHOMLinS4

subsection‹TestsHOMLinS4.thy›
text‹Tests and verifications of properties for the embedding of HOML (S4) in HOL.›
theory TestsHOMLinS4 imports HOMLinHOLonlyS4
begin 

―‹Test for S5 modal logic›
lemma axM: "⌊❙□φ ❙⊃ φ⌋" using Rrefl by blast
lemma axD: "⌊❙□φ ❙⊃ ❙◇φ⌋" using Rrefl by blast
lemma axB: "⌊φ ❙⊃ ❙□❙◇φ⌋" 
  nitpick[expect=genuine] oops ―‹Countermodel found›
lemma ax4: "⌊❙□φ ❙⊃ ❙□❙□φ⌋" using Rtrans by blast
lemma ax5: "⌊❙◇φ ❙⊃ ❙□❙◇φ⌋" 
  nitpick[expect=genuine] oops ―‹Countermodel found›

―‹Test for Barcan and converse Barcan formula:›
lemma BarcanAct: "⌊(❙∀⇧Ex.❙□(φ x)) ❙⊃ ❙□(❙∀⇧Ex.(φ x))⌋" 
  nitpick[expect=genuine] oops ―‹Countermodel found›
lemma ConvBarcanAct: "⌊❙□(❙∀⇧Ex.(φ x)) ❙⊃ (❙∀⇧Ex.❙□(φ x))⌋" 
  nitpick[expect=genuine] oops ―‹Countermodel found›
lemma BarcanPoss: "⌊(❙∀x.❙□(φ x)) ❙⊃ ❙□(❙∀x. φ x)⌋" by blast 
lemma ConvBarcanPoss: "⌊❙□(❙∀x.(φ x)) ❙⊃ (❙∀x.❙□(φ x))⌋" by blast

―‹A simple Hilbert system for classical propositional logic is derived›
lemma Hilbert_A1: "⌊A ❙⊃ (B ❙⊃ A)⌋" by blast
lemma Hilbert_A2: "⌊(A ❙⊃ (B ❙⊃ C)) ❙⊃ ((A ❙⊃ B) ❙⊃ (A ❙⊃ C))⌋" by blast
lemma Hilbert_MP: assumes "⌊A⌋" and "⌊A ❙⊃ B⌋" shows "⌊B⌋" using assms by blast 

―‹We have a polymorphic possibilist quantifier for which existential import holds›
lemma Quant_1: assumes "⌊A⌋" shows "⌊❙∀x::'a. A⌋" using assms by auto

―‹Existential import holds for possibilist quantifiers›
lemma ExImPossibilist1: "⌊❙∃x::e. x ❙= x⌋" by blast 
lemma ExImPossibilist2: "⌊❙∃x::e. x ❙≡ x⌋" by blast
lemma ExImPossibilist3: "⌊❙∃x::e. x ❙= t⌋" by blast 
lemma ExImPossibilist4: "⌊❙∃x::'a. x ❙≡ t::'a⌋" by blast
lemma ExImPossibilist: "⌊❙∃x::'a. ❙⊤⌋" by blast

―‹We have an actualist quantifier for individuals for which existential import does not hold›
lemma Quant_2: assumes "⌊A⌋" shows "⌊❙∀⇧Ex::e. A⌋" using assms by auto

―‹Existential import does not hold for our actualist quantifiers (for individuals)›
lemma ExImActualist1: "⌊❙∃⇧Ex::e. x ❙= x⌋" 
  nitpick[card=1,expect=genuine] oops ―‹Countermodel found›
lemma ExImActualist2: "⌊❙∃⇧Ex::e. x ❙≡ x⌋" 
  nitpick[card=1,expect=genuine] oops ―‹Countermodel found›
lemma ExImActualist3: "⌊❙∃⇧Ex::e. x ❙= t⌋" 
  nitpick[card=1,expect=genuine] oops ―‹Countermodel found›
lemma ExImActualist: "⌊❙∃⇧Ex::e. ❙⊤⌋" 
  nitpick[card=1,expect=genuine] oops ―‹Countermodel found›

―‹Properties of the embedded primitive equality, which coincides with Leibniz equality›
lemma EqRefl: "⌊x ❙= x⌋" by blast
lemma EqSym: "⌊(x ❙= y) ❙↔ (y ❙= x)⌋" by blast
lemma EqTrans: "⌊((x ❙= y) ❙∧ (y ❙= z)) ❙⊃ (x ❙= z)⌋" by blast
lemma EQCong: "⌊(x ❙= y) ❙⊃ ((φ x) ❙= (φ y))⌋" by blast
lemma EQFuncExt: "⌊(φ ❙= ψ) ❙⊃ (❙∀x. ((φ x) ❙= (ψ x)))⌋" by blast
lemma EQBoolExt1: "⌊(φ ❙= ψ) ❙⊃ (φ ❙↔ ψ)⌋" by blast
lemma EQBoolExt2: "⌊(φ ❙↔ ψ) ❙⊃ (φ ❙= ψ)⌋" 
  nitpick[card=2] oops ―‹Countermodel found›
lemma EQBoolExt3: "⌊(φ ❙↔ ψ)⌋ ⟶ ⌊(φ ❙= ψ)⌋" by blast 
lemma EqPrimLeib: "⌊(x ❙= y) ❙↔ (x ❙≡ y)⌋" by auto

―‹Comprehension is natively supported in HOL (due to lambda-abstraction)›
lemma Comprehension1: "⌊❙∃φ. ❙∀x. (φ x) ❙↔ A⌋" by force
lemma Comprehension2: "⌊❙∃φ. ❙∀x. (φ x) ❙↔ (A x)⌋" by force
lemma Comprehension3: "⌊❙∃φ. ❙∀x y. (φ x y) ❙↔ (A x y)⌋" by force

―‹Modal collapse does not hold›
lemma ModalCollapse: "⌊❙∀φ. φ ❙⊃ ❙□φ⌋" 
  nitpick[card=2,expect=genuine] oops ―‹Countermodel found›

―‹Empty property and self-difference›
lemma TruePropertyAndSelfIdentity: "⌊(λx::e. ❙⊤) ❙= (λx. x ❙= x)⌋" by blast 
lemma EmptyPropertyAndSelfDifference: "⌊(λx::e. ❙⊥) ❙= (λx. x ❙≠ x)⌋" by blast 
lemma EmptyProperty2: "⌊❙∃x. φ x⌋ ⟶ ⌊φ ❙≠ (λx::e. ❙⊥)⌋" by blast 
lemma EmptyProperty3: "⌊❙∃⇧Ex. φ x⌋ ⟶ ⌊φ ❙≠ (λx::e. ❙⊥)⌋" by blast 
lemma EmptyProperty4: "⌊φ ❙≠ (λx::e. ❙⊥)⌋ ⟶ ⌊❙∃x. φ x⌋" 
  nitpick[expect=genuine] oops ―‹Countermodel found›
lemma EmptyProperty5: "⌊φ ❙≠ (λx::e. ❙⊥)⌋ ⟶ ⌊❙∃⇧Ex. φ x⌋" 
  nitpick[expect=genuine] oops ―‹Countermodel found›

end