Theory PMLinHOL_shallow_minimal_further_tests


theory PMLinHOL_shallow_minimal_further_tests  
  imports PMLinHOL_shallow_minimal_tests 
begin 

―‹Implied modal principle›
lemma K_Dia: "⊨⇧^m (□⇧^m(φ ⊃⇧^m ψ)) ⊃⇧^m ((◇⇧^mφ) ⊃⇧^m ◇⇧^mψ)" by auto 

―‹Example 6.10 of Sider (2009) Logic for Philosophy›
lemma T1a: "⊨⇧^m □⇧^mp⇧^m ⊃⇧^m ((◇⇧^mq⇧^m) ⊃⇧^m ◇⇧^m(p⇧^m ∧⇧^m q⇧^m))" by auto ―‹fast automation in meta-logic HOL›
lemma T1b: "⊨⇧^m □⇧^mp⇧^m ⊃⇧^m ((◇⇧^mq⇧^m) ⊃⇧^m ◇⇧^m(p⇧^m ∧⇧^m q⇧^m))" ―‹alternative interactive proof in modal object logic K› 
  proof -   
    have 1: "⊨⇧^m p⇧^m ⊃⇧^m (q⇧^m ⊃⇧^m (p⇧^m ∧⇧^m q⇧^m))" unfolding AndM_def using H1 H2 H3 MP by metis
    have 2: "⊨⇧^m □⇧^m(p⇧^m ⊃⇧^m (q⇧^m ⊃⇧^m (p⇧^m ∧⇧^m q⇧^m)))" using 1 Nec by metis
    have 3: "⊨⇧^m □⇧^mp⇧^m ⊃⇧^m □⇧^m(q⇧^m ⊃⇧^m (p⇧^m ∧⇧^m q⇧^m))" using 2 Dist MP by metis
    have 4: "⊨⇧^m (□⇧^m(q⇧^m ⊃⇧^m (p⇧^m ∧⇧^m q⇧^m))) ⊃⇧^m ((◇⇧^mq⇧^m) ⊃⇧^m ◇⇧^m(p⇧^m ∧⇧^m q⇧^m))" using K_Dia by metis
    have 5: "⊨⇧^m □⇧^mp⇧^m ⊃⇧^m ((◇⇧^mq⇧^m) ⊃⇧^m ◇⇧^m(p⇧^m ∧⇧^m q⇧^m))" using 3 4 H1 H2 MP by metis 
    thus ?thesis . 
  qed
end