Theory topo_strict_implication

theory topo_strict_implication
  imports topo_frontier_algebra
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Strict implication›

text‹\noindent{We can also employ the closure and interior operations to define different sorts of implications.
In this section we preliminary explore a sort of strict implication and check some relevant properties.}›

text‹\noindent{A 'strict' implication should entail the classical one. Hence we define it using the interior operator.}›
definition imp_I::"σ⇒σ⇒σ" (infix "❙⇒" 51) where "α ❙⇒ β ≡ ℐ(α ❙→ β)"
abbreviation imp_I'::"σ⇒σ⇒σ" (infix "❙⇐" 51) where "β ❙⇐ α ≡ α ❙⇒ β"
declare imp_I_def[conn]

lemma imp_rel: "∀a b. a ❙⇒ b ❙≼ a ❙→ b" by (simp add: Int_fr_def conn)

text‹\noindent{Under appropriate conditions this implication satisfies a weak variant of the deduction theorem (DT),}›
lemma DTw1: "∀a b. a ❙⇒ b ❙≈ ❙⊤ ⟶ a ❙≼ b" by (simp add: Int_fr_def conn)
lemma DTw2: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b.  a ❙≼ b ⟶ a ❙⇒ b ❙≈ ❙⊤" using IF3 dNOR_def unfolding conn by auto
text‹\noindent{and a variant of modus ponens and modus tollens resp.}›
lemma MP: "∀a b. a ❙∧ (a ❙⇒ b) ❙≼ b" by (simp add: Int_fr_def conn)
lemma MT: "∀a b. (a ❙⇒ b) ❙∧ ❙─b ❙≼ ❙─a" using MP conn by auto

text‹\noindent{However the full DT (actually right-to-left: implication introduction) is not valid.}›
lemma DT1: "∀a b X. X ❙≼ a ❙⇒ b ⟶ X ❙∧ a ❙≼ b" by (simp add: Int_fr_def conn)
lemma DT2: "𝔉 ℱ ⟹ ∀a b X. X ❙∧ a ❙≼ b ⟶ X ❙≼ a ❙⇒ b" nitpick oops (*counterexample*)

text‹\noindent{This implication has thus a sort of 'relevant' behaviour. For instance, the following are not valid:}›
lemma "𝔉 ℱ ⟹ ∀a b. (a ❙⇒ (b ❙⇒ a)) ❙≈ ❙⊤" nitpick oops (*counterexample*)
lemma "𝔉 ℱ ⟹ ∀a b. (a ❙⇒ ((a ❙⇒ b) ❙⇒ b)) ❙≈ ❙⊤" nitpick oops (*counterexample*)
lemma "𝔉 ℱ ⟹ ∀a b c. (a ❙⇒ b) ❙∨ (b ❙⇒ c) ❙≈ ❙⊤" nitpick oops (*counterexample*)
lemma "𝔉 ℱ ⟹ ∀a b. ((a ❙⇒ b) ❙⇒ a) ❙⇒ a ❙≈ ❙⊤" nitpick oops (*counterexample*) 

text‹\noindent{In contrast the properties below are valid for appropriate conditions.}›
lemma iprop0: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a. a ❙⇒ a ❙≈ ❙⊤" using DTw2 pI2 by fastforce
lemma iprop1: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b. a ❙∧ (a ❙⇒ b) ❙⇒ b  ❙≈ ❙⊤" using DTw2 pI2 unfolding conn by fastforce
lemma iprop2: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b. a ❙⇒ (b ❙⇒ b) ❙≈ ❙⊤" using DTw2 pI2 unfolding conn by fastforce
lemma iprop3: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b. ((a ❙⇒ a) ❙⇒ b) ❙⇒ b ❙≈ ❙⊤" using DTw2 pI2 unfolding conn by fastforce
lemma iprop4: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b. (a ❙∧ b) ❙⇒ a ❙≈ ❙⊤" using DTw2 pI2 unfolding conn by fastforce
lemma iprop5: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b. a ❙⇒ (a ❙∨ b) ❙≈ ❙⊤" using DTw2 pI2 unfolding conn by fastforce
lemma iprop6a: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. (a ❙∧ (b ❙∨ c)) ❙⇒ ((a ❙∧ b) ❙∨ (a ❙∧ c)) ❙≈ ❙⊤" using DTw2 pI2 unfolding conn by fastforce
lemma iprop6b: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. (a ❙∧ (b ❙∨ c)) ❙⇐ ((a ❙∧ b) ❙∨ (a ❙∧ c)) ❙≈ ❙⊤" using DTw2 unfolding conn by fastforce

lemma iprop7': "Fr_1 ℱ ⟹ ∀a b c. (a ❙⇒ b) ❙∧ (b ❙⇒ c) ❙≼ (a ❙⇒ c)" proof -
 assume fr1: "Fr_1 ℱ"
  { fix a b c
    have "(a ❙→ b) ❙∧ (b ❙→ c) ❙≼ (a ❙→ c)" unfolding conn by simp
    hence "ℐ((a ❙→ b) ❙∧ (b ❙→ c)) ❙≼ ℐ(a ❙→ c)" using MONO_def PF1 fr1 monI by simp 
    moreover from fr1 have "let A=(a ❙→ b); B=(b ❙→ c) in  ℐ(A ❙∧ B) ❙≈ ℐ A ❙∧ ℐ B" using IF1 MULT_def by simp
    ultimately have "ℐ(a ❙→ b) ❙∧ ℐ(b ❙→ c) ❙≼ ℐ(a ❙→ c)" unfolding conn by simp
  } thus ?thesis unfolding conn by blast
qed
lemma iprop7: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (b ❙⇒ c)) ❙⇒ (a ❙⇒ c) ❙≈ ❙⊤" by (simp add: DTw2 iprop7')

lemma iprop8a': "Fr_1 ℱ ⟹ ∀a b c. (a ❙⇒ b) ❙∧ (a ❙⇒ c) ❙≼ a ❙⇒ (b ❙∧ c)" proof -
  assume fr1: "Fr_1 ℱ"
  { fix a b c
    have "(a ❙→ b) ❙∧ (a ❙→ c) ❙≼ (a ❙→ (b ❙∧ c))" unfolding conn by simp
    hence "ℐ((a ❙→ b) ❙∧ (a ❙→ c)) ❙≼ ℐ(a ❙→ (b ❙∧ c))" using MONO_def PF1 fr1 monI by simp
    moreover from fr1 have "let A=(a ❙→ b); B=(a ❙→ c) in  ℐ(A ❙∧ B) ❙≈ ℐ A ❙∧ ℐ B" using IF1 MULT_def by simp
    ultimately have "ℐ(a ❙→ b) ❙∧ ℐ(a ❙→ c) ❙≼ ℐ(a ❙→ (b ❙∧ c))" unfolding conn by simp
  } thus ?thesis unfolding conn by simp
qed
lemma iprop8b': "Fr_1b ℱ ⟹ ∀a b c. (a ❙⇒ b) ❙∧ (a ❙⇒ c) ❙≽ a ❙⇒ (b ❙∧ c)" by (smt MONO_def monI conn)
lemma iprop8a: "Fr_1 ℱ  ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (a ❙⇒ c)) ❙⇒ (a ❙⇒ (b ❙∧ c)) ❙≈ ❙⊤" by (simp add: DTw2 iprop8a')
lemma iprop8b: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (a ❙⇒ c)) ❙⇐ (a ❙⇒ (b ❙∧ c)) ❙≈ ❙⊤" by (simp add: DTw2 iprop8b')

lemma iprop9a': "Fr_1 ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (c ❙⇒ b)) ❙≼ ((a ❙∨ c) ❙⇒ b)" proof -
  assume fr1: "Fr_1 ℱ"
  { fix a b c
    have "(a ❙→ b) ❙∧ (c ❙→ b) ❙≼ (a ❙∨ c) ❙→ b" unfolding conn by simp
    hence "ℐ((a ❙→ b) ❙∧ (c ❙→ b)) ❙≼ ℐ((a ❙∨ c) ❙→ b)" using MONO_def PF1 fr1 monI by simp
    moreover from fr1 have "let A=(a ❙→ b); B=(c ❙→ b) in  ℐ(A ❙∧ B) ❙≈ ℐ A ❙∧ ℐ B" using IF1 MULT_def by simp
    ultimately have "ℐ(a ❙→ b) ❙∧ ℐ(c ❙→ b) ❙≼ ℐ((a ❙∨ c) ❙→ b)" unfolding conn by simp
  } thus ?thesis unfolding conn by simp
qed
lemma iprop9b': "Fr_1b ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (c ❙⇒ b)) ❙≽ ((a ❙∨ c) ❙⇒ b)" by (smt MONO_def monI conn)
lemma iprop9a: "Fr_1 ℱ  ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (c ❙⇒ b)) ❙⇒ ((a ❙∨ c) ❙⇒ b) ❙≈ ❙⊤" by (simp add: DTw2 iprop9a')
lemma iprop9b: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. ((a ❙⇒ b) ❙∧ (c ❙⇒ b)) ❙⇐ ((a ❙∨ c) ❙⇒ b) ❙≈ ❙⊤" by (simp add: DTw2 iprop9b')

lemma iprop10': "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀a b c. a ❙⇒ (b ❙⇒ c) ❙≼ (a ❙⇒ b) ❙⇒ (a ❙⇒ c)" proof -
  assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr4: "Fr_4 ℱ"
  { fix a b c
    have "a ❙→ (b ❙→ c) ❙≼ (a ❙→ b) ❙→ (a ❙→ c)" unfolding conn by simp
    hence "a ❙→ (b ❙⇒ c) ❙≼ (a ❙→ b) ❙→ (a ❙→ c)" using Int_fr_def conn by auto
    hence "ℐ(a ❙→ (b ❙⇒ c)) ❙≼ ℐ((a ❙→ b) ❙→ (a ❙→ c))" using MONO_def PF1 fr1 monI by simp
    moreover from fr1 have "let A=(a ❙→ b); B=(a ❙→ c) in ℐ(A ❙→ B) ❙≼ ℐ A ❙→ ℐ B" using IF1 Int_7_def PI7 by auto
    ultimately have "ℐ(a ❙→ (b ❙⇒ c)) ❙≼ ℐ(a ❙→ b) ❙→ ℐ(a ❙→ c)" by (metis (full_types))
    hence "ℐ(ℐ(a ❙→ (b ❙⇒ c))) ❙≼ ℐ(ℐ(a ❙→ b) ❙→ ℐ(a ❙→ c))" using MONO_def PF1 fr1 monI by simp
    hence "ℐ(a ❙→ (b ❙⇒ c)) ❙≼ ℐ(ℐ(a ❙→ b) ❙→ ℐ(a ❙→ c))" using Int_Open PF1 fr1 fr2 fr4 by blast
    hence "(a ❙⇒ (b ❙⇒ c)) ❙≼ (a ❙⇒ b) ❙⇒ (a ❙⇒ c)" using Int_Open PF1 fr1 fr2 fr4 unfolding conn by blast
  } thus ?thesis by blast
qed
lemma iprop10: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ Fr_4 ℱ ⟹ ∀a b c. (a ❙⇒ (b ❙⇒ c)) ❙⇒ ((a ❙⇒ b) ❙⇒ (a ❙⇒ c)) ❙≈ ❙⊤" by (simp add: DTw2 iprop10')
lemma "𝔉 ℱ ⟹ ∀a b c. a ❙⇒ (b ❙⇒ c) ❙≽ (a ❙⇒ b) ❙⇒ (a ❙⇒ c)" nitpick oops (*counterexample*)

lemma iprop11a': "Fr_1 ℱ ⟹ ∀a b. (a ❙⇒ (a ❙⇒ b)) ❙≼ (a ❙⇒ b)" by (smt MONO_def PF1 imp_rel monI conn)
lemma iprop11b': "𝔉 ℱ    ⟹ ∀a b. (a ❙⇒ (a ❙⇒ b)) ❙≽ (a ❙⇒ b)" unfolding PF1 by (metis Int_Open MONO_def imp_I_def impl_def monI)
lemma iprop11a: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ  ⟹ ∀a b. (a ❙⇒ (a ❙⇒ b)) ❙⇒ (a ❙⇒ b) ❙≈ ❙⊤" using DTw2 iprop11a' by blast
lemma iprop11b: "𝔉 ℱ                            ⟹ ∀a b. (a ❙⇒ (a ❙⇒ b)) ❙⇐ (a ❙⇒ b) ❙≈ ❙⊤" using DTw2 iprop11b' by blast

text‹\noindent{In particular, 'strenghening the antecedent' is valid only under certain conditions:}›
lemma SA':"Fr_1b ℱ                        ⟹ ∀a b c.  a ❙⇒ c  ❙≼  (a ❙∧ b) ❙⇒ c" by (smt MONO_def monI conn)
lemma SA: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. (a ❙⇒ c) ❙⇒ ((a ❙∧ b) ❙⇒ c) ❙≈ ❙⊤" using SA' using DTw2 by fastforce 
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ Fr_4 ℱ ⟹ ∀a b c.  a ❙⇒ c  ❙≼  (a ❙∧ b) ❙⇒ c" nitpick oops (*counterexample*)
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ Fr_4 ℱ ⟹ ∀a b c. (a ❙⇒ c) ❙⇒ ((a ❙∧ b) ❙⇒ c) ❙≈ ❙⊤" nitpick oops  (*counterexample*)

text‹\noindent{Similarly, 'weakening the consequent' is valid only under certain conditions.}›
lemma WC':"Fr_1b ℱ ⟹                        ∀a b c.  a ❙⇒ c  ❙≼  a ❙⇒ (c ❙∨ b)" by (smt MONO_def monI conn)
lemma WC: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀a b c. (a ❙⇒ c) ❙⇒ (a ❙⇒ (c ❙∨ b)) ❙≈ ❙⊤" using DTw2 WC' by fastforce
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ Fr_4 ℱ ⟹ ∀a b c.  a ❙⇒ c  ❙≼  a ❙⇒ (c ❙∨ b)" nitpick oops (*counterexample*)
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ Fr_4 ℱ ⟹ ∀a b c. (a ❙⇒ c) ❙⇒ (a ❙⇒ (c ❙∨ b)) ❙≈ ❙⊤" nitpick oops (*counterexample*)

end