# Theory sse_boolean_algebra

theory sse_boolean_algebra
imports Main
begin

declare[[syntax_ambiguity_warning=false]]
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Shallow embedding of a Boolean algebra of propositions›

text‹\noindent{In this section we present a shallow semantical embedding (SSE, cf. @{cite J41} and @{cite J23})
for a family of logics whose semantics is based upon extensions of (complete and atomic) Boolean algebras.
The range of such logics is indeed very wide, including, as we will see, quantified paraconsistent and
paracomplete (e.g. intuitionistic) logics. Aside from illustrating how the SSE approach works in practice
we show how it allows us to effectively harness theorem provers, model finders and hammers' for reasoning
with quantified non-classical logics. Proof reconstructions have deliberately been avoided.
Most of the proofs (in fact, all one-liners) have been found using Sledgehammer.}›

text‹\noindent{Two notions play a fundamental role in this work: propositions and propositional functions.
Propositions, qua sentence denotations, are modeled as objects of type @{text "w⇒bool"} (shortened as @{text "σ"}).
Propositional functions, as the name indicates, are basically anything with a (parametric) type @{text "'t⇒σ"}.}›

text‹\noindent{We introduce a type @{text "w"} for the domain of points (aka. 'worlds', 'states', etc.).
@{text "σ"} is a type alias for sets of points (i.e. propositions) encoded as characteristic functions.}›
typedecl w
type_synonym σ = "w⇒bool"

text‹\noindent{In the sequel, we introduce the following naming convention for variables:

(i) Latin letters (A, b, M, P, q, X, y, etc.) denote in general propositions (type @{text "σ"});
however, we reserve letters D and S to denote sets of propositions (aka. domains/spaces) and
the letters u, v and w to denote worlds/points.

(ii) Greek letters (in particular @{text "π"}) denote propositional functions (type @{text "'t⇒σ"});
among the latter we may employ the letters @{text "φ"}, @{text "ψ"} and @{text "η"} to explicitly
name those corresponding to unary connectives/operations (type @{text "σ⇒σ"}).}›

subsection ‹Encoding Boolean operations›

abbreviation sequ::"σ⇒σ⇒bool" (infixr "❙≈" 45) where "A ❙≈ B ≡ ∀w. (A w) ⟷ (B w)"
abbreviation subs::"σ⇒σ⇒bool" (infixr "❙≼" 45) where "A ❙≼ B ≡ ∀w. (A w) ⟶ (B w)"
abbreviation sups::"σ⇒σ⇒bool" (infixr "❙≽" 45) where "B ❙≽ A ≡ A ❙≼ B"

text‹\noindent{define meet and join by reusing HOL metalogical conjunction and disjunction,}›
definition meet::"σ⇒σ⇒σ" (infixr "❙∧" 54) where "A ❙∧ B ≡ λw. (A w) ∧ (B w)"
definition join::"σ⇒σ⇒σ" (infixr "❙∨" 53) where "A ❙∨ B ≡ λw. (A w) ∨ (B w)"

text‹\noindent{and introduce further operations to obtain a Boolean 'algebra of propositions'.}›
definition top::"σ" ("❙⊤")    where "❙⊤ ≡ λw. True"
definition bottom::"σ" ("❙⊥") where "❙⊥ ≡ λw. False"
definition impl::"σ⇒σ⇒σ" (infixr "❙→" 51) where "A ❙→ B ≡ λw. (A w)⟶(B w)"
definition dimp::"σ⇒σ⇒σ" (infixr "❙↔" 51) where "A ❙↔ B ≡ λw. (A w)⟷(B w)"
definition diff::"σ⇒σ⇒σ" (infixr "❙↼" 51) where "A ❙↼ B ≡ λw. (A w) ∧ ¬(B w)"
definition compl::"σ⇒σ" ("❙─_" 58) where "❙─A  ≡ λw. ¬(A w)"

named_theorems conn (*algebraic connectives*)
declare meet_def[conn] join_def[conn] top_def[conn] bottom_def[conn]
impl_def[conn] dimp_def[conn] diff_def[conn] compl_def[conn]

text‹\noindent{Quite trivially, we can verify that the algebra satisfies some essential lattice properties.}›
lemma "a ❙∨ a ❙≈ a" unfolding conn by simp
lemma "a ❙∧ a ❙≈ a" unfolding conn by simp
lemma "a ❙≼ a ❙∨ b" unfolding conn by simp
lemma "a ❙∧ b ❙≼ a" unfolding conn by simp
lemma "(a ❙∧ b) ❙∨ b ❙≈ b" unfolding conn by auto (*absorption 1*)
lemma "a ❙∧ (a ❙∨ b) ❙≈ a" unfolding conn by auto (*absorption 2*)
lemma "a ❙≼ c ⟹ b ❙≼ c ⟹ a ❙∨ b ❙≼ c" unfolding conn by simp
lemma "c ❙≼ a ⟹ c ❙≼ b ⟹ c ❙≼ a ❙∧ b" unfolding conn by simp
lemma "a ❙≼ b ≡ (a ❙∨ b) ❙≈ b" unfolding conn by smt
lemma "b ❙≼ a ≡ (a ❙∧ b) ❙≈ b" unfolding conn by smt
lemma "a ❙≼ c ⟹ b ❙≼ d ⟹ (a ❙∨ b) ❙≼ (c ❙∨ d)" unfolding conn by simp
lemma "a ❙≼ c ⟹ b ❙≼ d ⟹ (a ❙∧ b) ❙≼ (c ❙∧ d)" unfolding conn by simp

subsection ‹Second-order operations and fixed-points›

text‹\noindent{We define equality for propositional functions as follows.}›
definition equal_op::"('t⇒σ)⇒('t⇒σ)⇒bool" (infix "❙≡" 60) where "φ ❙≡ ψ ≡ ∀X. φ X ❙≈ ψ X"

text‹\noindent{Moreover, we define some useful Boolean (2nd-order) operations on propositional functions,}›
abbreviation unionOp::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" (infixr "❙⊔" 61) where "φ ❙⊔ ψ ≡ λX. φ X ❙∨ ψ X"
abbreviation interOp::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" (infixr "❙⊓" 62) where "φ ❙⊓ ψ ≡ λX. φ X ❙∧ ψ X"
abbreviation compOp::"('t⇒σ)⇒('t⇒σ)" ("(_⇧c)") where "φ⇧c ≡ λX. ❙─φ X"
text‹\noindent{some of them explicitly targeting operations,}›
definition dual::"(σ⇒σ)⇒(σ⇒σ)" ("(_⇧d)") where "φ⇧d ≡ λX. ❙─(φ(❙─X))"
text‹\noindent{and also define an useful operation (for technical purposes).}›
definition id::"σ⇒σ" ("id") where "id A ≡ A"

text‹\noindent{We now prove some useful lemmas (some of them may help the provers in their hard work).}›
lemma comp_symm: "φ⇧c = ψ ⟹ φ = ψ⇧c" unfolding conn by blast
lemma comp_invol: "φ⇧c⇧c = φ" unfolding conn by blast
lemma dual_symm: "(φ ≡ ψ⇧d) ⟹ (ψ ≡ φ⇧d)" unfolding dual_def conn by simp
lemma dual_comp: "φ⇧d⇧c = φ⇧c⇧d" unfolding dual_def by simp

lemma "id⇧d ❙≡ id"  by (simp add: id_def dual_def equal_op_def conn)
lemma "id⇧c ❙≡ compl"  by (simp add: id_def dual_def equal_op_def conn)
lemma "(A ❙⊔ B)⇧d ❙≡ (A⇧d) ❙⊓ (B⇧d)" by (simp add: dual_def equal_op_def conn)
lemma "(A ❙⊔ B)⇧c ❙≡ (A⇧c) ❙⊓ (B⇧c)" by (simp add: equal_op_def conn)
lemma "(A ❙⊓ B)⇧d ❙≡ (A⇧d) ❙⊔ (B⇧d)" by (simp add: dual_def equal_op_def conn)
lemma "(A ❙⊓ B)⇧c ❙≡ (A⇧c) ❙⊔ (B⇧c)" by (simp add: equal_op_def conn)

text‹\noindent{The notion of a fixed point is a fundamental one. We speak of propositions being fixed points of
operations. For a given operation we define in the usual way a fixed-point predicate for propositions.}›
abbreviation fixedpoint::"(σ⇒σ)⇒(σ⇒bool)" ("fp") where "fp φ ≡ λX. φ X ❙≈ X"

lemma fp_d: "(fp φ⇧d) X = (fp φ)(❙─X)" unfolding dual_def conn by auto
lemma fp_c: "(fp φ⇧c) X = (X ❙≈ ❙─(φ X))" unfolding conn by auto
lemma fp_dc:"(fp φ⇧d⇧c) X = (X ❙≈ φ(❙─X))" unfolding dual_def conn by auto

text‹\noindent{Indeed, we can 'operationalize' this predicate by defining a fixed-point operator as follows:}›
abbreviation fixedpoint_op::"(σ⇒σ)⇒(σ⇒σ)" ("(_⇧f⇧p)") where "φ⇧f⇧p  ≡ λX. (φ X) ❙↔ X"

lemma ofp_c: "(φ⇧c)⇧f⇧p ❙≡ (φ⇧f⇧p)⇧c" unfolding conn equal_op_def by auto
lemma ofp_d: "(φ⇧d)⇧f⇧p ❙≡ (φ⇧f⇧p)⇧d⇧c" unfolding dual_def equal_op_def conn by auto
lemma ofp_dc:"(φ⇧d⇧c)⇧f⇧p ❙≡ (φ⇧f⇧p)⇧d" unfolding dual_def equal_op_def conn by auto
lemma ofp_decomp: "φ⇧f⇧p ❙≡ (id ❙⊓ φ) ❙⊔ ((id ❙⊔ φ)⇧c)" unfolding equal_op_def id_def conn by auto
lemma ofp_invol: "(φ⇧f⇧p)⇧f⇧p ❙≡ φ" unfolding conn equal_op_def by auto

text‹\noindent{Fixed-point predicate and fixed-point operator are closely related.}›
lemma fp_rel: "((fp φ) X) = (φ⇧f⇧p X ❙≈ ❙⊤)" unfolding conn by auto
lemma fp_d_rel:  "((fp φ⇧d) X) = (φ⇧f⇧p(❙─X) ❙≈ ❙⊤)" unfolding dual_def conn by auto
lemma fp_c_rel: "((fp φ⇧c) X) = (φ⇧f⇧p  X  ❙≈ ❙⊥)" unfolding conn by auto
lemma fp_dc_rel: "((fp φ⇧d⇧c) X) = (φ⇧f⇧p(❙─X) ❙≈ ❙⊥)" unfolding dual_def conn by auto

subsection ‹Equality and atomicity›

text‹\noindent{We prove some facts about equality (which may help improve prover's performance).}›
lemma eq_ext: "a ❙≈ b ⟹  a = b" using ext by blast
lemma eq_ext': "a ❙≡ b ⟹  a = b" using ext unfolding equal_op_def by blast
lemma meet_char: "a ❙≼ b ⟷ a ❙∧ b ❙≈ a" unfolding conn by blast
lemma join_char: "a ❙≼ b ⟷ a ❙∨ b ❙≈ b" unfolding conn  by blast

text‹\noindent{We can verify indeed that the algebra is atomic (in three different ways) by relying on the
presence of primitive equality in HOL. A more general class of Boolean algebras could in principle
be obtained in systems without primitive equality or by suitably restricting quantification over
propositions (e.g. defining a topology and restricting quantifiers to open/closed sets).}›
definition "atom a ≡ ¬(a ❙≈ ❙⊥) ∧ (∀p. a ❙≼ p ∨ a ❙≼ ❙─p)"
lemma atomic1: "∀w. ∃q. q w ∧ (∀p. p w ⟶ q ❙≼ p)" using the_sym_eq_trivial by (metis (full_types))
lemma atomic2: "∀w. ∃q. q w ∧ atom(q)" using the_sym_eq_trivial by (metis (full_types) atom_def compl_def bottom_def)
lemma atomic3: "∀p. ¬(p ❙≈ ❙⊥) ⟶ (∃q. atom(q) ∧ q ❙≼ p)" proof - (*using atom_def unfolding conn by fastforce*)
{ fix p
{ assume "¬(p ❙≈ ❙⊥)"
hence "∃v. p v" unfolding conn by simp
then obtain w where 1:"p w" by (rule exE)
let ?q="λv. v = w" (*using HOL primitive equality*)
have 2: "atom ?q" unfolding atom_def unfolding conn by simp
have "∀v. ?q v ⟶ p v" using 1 by simp
hence 3: "?q ❙≼ p" by simp
from 2 3 have "∃q. atom(q) ∧ q ❙≼ p" by blast
} hence "¬(p ❙≈ ❙⊥) ⟶ (∃q. atom(q) ∧ q ❙≼ p)" by (rule impI)
} thus ?thesis by (rule allI)
qed

end


# Theory sse_boolean_algebra_quantification

theory sse_boolean_algebra_quantification
imports sse_boolean_algebra
begin
hide_const(open) List.list.Nil no_notation List.list.Nil ("[]")  (*We have no use for lists... *)
hide_const(open) Relation.converse no_notation Relation.converse ("(_¯)"  999) (*..nor for relations in this work*)
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

subsection ‹Obtaining a complete Boolean Algebra›

text‹\noindent{Our aim is to obtain a complete Boolean algebra which we can use to interpret
quantified formulas (in the spirit of Boolean-valued models for set theory).}›

text‹\noindent{We start by defining infinite meet (infimum) and infinite join (supremum) operations,}›
definition infimum:: "(σ⇒bool)⇒σ" ("❙⋀_") where "❙⋀S ≡ λw. ∀X. S X ⟶ X w"
definition supremum::"(σ⇒bool)⇒σ" ("❙⋁_") where "❙⋁S ≡ λw. ∃X. S X  ∧  X w"

text‹\noindent{and show that the corresponding lattice is complete.}›
abbreviation "upper_bound U S ≡ ∀X. (S X) ⟶ X ❙≼ U"
abbreviation "lower_bound L S ≡ ∀X. (S X) ⟶ L ❙≼ X"
abbreviation "is_supremum U S ≡ upper_bound U S ∧ (∀X. upper_bound X S ⟶ U ❙≼ X)"
abbreviation "is_infimum  L S ≡ lower_bound L S ∧ (∀X. lower_bound X S ⟶ X ❙≼ L)"

lemma sup_char: "is_supremum ❙⋁S S" unfolding supremum_def by auto
lemma sup_ext: "∀S. ∃X. is_supremum X S" by (metis supremum_def)
lemma inf_char: "is_infimum ❙⋀S S" unfolding infimum_def by auto
lemma inf_ext: "∀S. ∃X. is_infimum X S" by (metis infimum_def)

text‹\noindent{We can check that being closed under supremum/infimum entails being closed under join/meet.}›
abbreviation "meet_closed S ≡  ∀X Y. (S X ∧ S Y) ⟶ S(X ❙∧ Y)"
abbreviation "join_closed S ≡  ∀X Y. (S X ∧ S Y) ⟶ S(X ❙∨ Y)"

abbreviation "nonEmpty S ≡ ∃x. S x"
abbreviation "contains S D ≡  ∀X. D X ⟶ S X"
abbreviation "infimum_closed S  ≡ ∀D. nonEmpty D ∧ contains S D ⟶ S(❙⋀D)"
abbreviation "supremum_closed S ≡ ∀D. nonEmpty D ∧ contains S D ⟶ S(❙⋁D)"

lemma inf_meet_closed: "∀S. infimum_closed S ⟶ meet_closed S" proof -
{ fix S
{ assume inf_closed: "infimum_closed S"
hence "meet_closed S" proof -
{ fix X::"σ" and Y::"σ"
let ?D="λZ. Z=X ∨ Z=Y"
{ assume "S X ∧ S Y"
hence "contains S ?D" by simp
moreover have "nonEmpty ?D" by auto
ultimately have "S(❙⋀?D)" using inf_closed by simp
hence "S(λw. ∀Z. (Z=X ∨ Z=Y) ⟶ Z w)" unfolding infimum_def by simp
moreover have "(λw. ∀Z. (Z=X ∨ Z=Y) ⟶ Z w) = (λw. X w ∧ Y w)" by auto
ultimately have "S(λw. X w ∧ Y w)" by simp
} hence "(S X ∧ S Y) ⟶ S(X ❙∧ Y)" unfolding conn by (rule impI)
} thus ?thesis by simp  qed
} hence "infimum_closed S ⟶ meet_closed S" by simp
} thus ?thesis by (rule allI)
qed
lemma sup_join_closed: "∀P. supremum_closed P ⟶ join_closed P" proof -
{ fix S
{ assume sup_closed: "supremum_closed S"
hence "join_closed S" proof -
{ fix X::"σ" and Y::"σ"
let ?D="λZ. Z=X ∨ Z=Y"
{ assume "S X ∧ S Y"
hence "contains S ?D" by simp
moreover have "nonEmpty ?D" by auto
ultimately have "S(❙⋁?D)" using sup_closed by simp
hence "S(λw. ∃Z. (Z=X ∨ Z=Y) ∧ Z w)" unfolding supremum_def by simp
moreover have "(λw. ∃Z. (Z=X ∨ Z=Y) ∧ Z w) = (λw. X w ∨ Y w)" by auto
ultimately have "S(λw. X w ∨ Y w)" by simp
} hence "(S X ∧ S Y) ⟶ S(X ❙∨ Y)" unfolding conn by (rule impI)
} thus ?thesis by simp qed
} hence "supremum_closed S ⟶ join_closed S" by simp
} thus ?thesis by (rule allI)
qed

subsection ‹Adding quantifiers (restricted and unrestricted)›

text‹\noindent{We can harness HOL to define quantification over individuals of arbitrary type (using polymorphism).
These (unrestricted) quantifiers take a propositional function and give a proposition.}›
abbreviation mforall::"('t⇒σ)⇒σ" ("❙∀_" 56) where "❙∀π ≡ λw. ∀X. (π X) w"
abbreviation mexists::"('t⇒σ)⇒σ" ("❙∃_" 56) where "❙∃π ≡ λw. ∃X. (π X) w"
text‹\noindent{To improve readability, we introduce for them an useful binder notation.}›
abbreviation mforallB (binder"❙∀"56) where "❙∀X. π X ≡ ❙∀π"
abbreviation mexistsB (binder"❙∃"56) where "❙∃X. π X ≡ ❙∃π"

(*TODO: is it possible to also add binder notation to the ones below?*)
text‹\noindent{Moreover, we define restricted quantifiers which take a 'functional domain' as additional parameter.
The latter is a propositional function that maps each element 'e' to the proposition 'e exists'.}›
abbreviation mforall_restr::"('t⇒σ)⇒('t⇒σ)⇒σ" ("❙∀⇧R(_)_") where "❙∀⇧R(δ)π ≡ λw.∀X. (δ X) w ⟶ (π X) w"
abbreviation mexists_restr::"('t⇒σ)⇒('t⇒σ)⇒σ" ("❙∃⇧R(_)_") where "❙∃⇧R(δ)π ≡ λw.∃X. (δ X) w  ∧  (π X) w"

subsection ‹Relating quantifiers with further operators›

text‹\noindent{The following 'type-lifting' function is useful for converting sets into 'rigid' propositional functions.}›
abbreviation lift_conv::"('t⇒bool)⇒('t⇒σ)" ("⦇_⦈") where "⦇S⦈ ≡ λX. λw. S X"

text‹\noindent{We introduce an useful operator: the range of a propositional function (resp. restricted over a domain),}›
definition pfunRange::"('t⇒σ)⇒(σ⇒bool)" ("Ra(_)") where "Ra(π) ≡ λY. ∃x. (π x) = Y"
definition pfunRange_restr::"('t⇒σ)⇒('t⇒bool)⇒(σ⇒bool)" ("Ra[_|_]") where "Ra[π|D] ≡ λY. ∃x. (D x) ∧ (π x) = Y"

text‹\noindent{and check that taking infinite joins/meets (suprema/infima) over the range of a propositional function
can be equivalently codified by using quantifiers. This is a quite useful simplifying relationship.}›
lemma Ra_all: "❙⋀Ra(π) = ❙∀π" by (metis (full_types) infimum_def pfunRange_def)
lemma Ra_ex:  "❙⋁Ra(π) = ❙∃π" by (metis (full_types) pfunRange_def supremum_def)
lemma Ra_restr_all: "❙⋀Ra[π|D] = ❙∀⇧R⦇D⦈π" by (metis (full_types) pfunRange_restr_def infimum_def)
lemma Ra_restr_ex:  "❙⋁Ra[π|D] = ❙∃⇧R⦇D⦈π" by (metis pfunRange_restr_def supremum_def)

text‹\noindent{We further introduce the positive (negative) restriction of a propositional function wrt. a domain,}›
abbreviation pfunRestr_pos::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" ("[_|_]⇧P") where "[π|δ]⇧P ≡ λX. λw. (δ X) w ⟶ (π X) w"
abbreviation pfunRestr_neg::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" ("[_|_]⇧N") where "[π|δ]⇧N ≡ λX. λw. (δ X) w  ∧  (π X) w"

text‹\noindent{and check that some additional simplifying relationships obtain.}›
lemma all_restr: "❙∀⇧R(δ)π = ❙∀[π|δ]⇧P" by simp
lemma ex_restr:  "❙∃⇧R(δ)π = ❙∃[π|δ]⇧N" by simp
lemma Ra_all_restr: "❙⋀Ra[π|D] = ❙∀[π|⦇D⦈]⇧P" using Ra_restr_all by blast
lemma Ra_ex_restr:  "❙⋁Ra[π|D] = ❙∃[π|⦇D⦈]⇧N" by (simp add: Ra_restr_ex)

text‹\noindent{Observe that using these operators has the advantage of allowing for binder notation,}›
lemma "❙∀X. [π|δ]⇧P X = ❙∀[π|δ]⇧P" by simp
lemma "❙∃X. [π|δ]⇧N X = ❙∃[π|δ]⇧N" by simp

text‹\noindent{noting that extra care should be taken when working with complements or negations;
always remember to switch P/N (positive/negative restriction) accordingly.}›
lemma "❙∀⇧R(δ)π  = ❙∀X.  [π|δ]⇧P X" by simp
lemma "❙∀⇧R(δ)π⇧c = ❙∀X. ❙─[π|δ]⇧N X" by (simp add: compl_def)
lemma "❙∃⇧R(δ)π  = ❙∃X.  [π|δ]⇧N X" by simp
lemma "❙∃⇧R(δ)π⇧c = ❙∃X. ❙─[π|δ]⇧P X" by (simp add: compl_def)

text‹\noindent{The previous definitions allow us to nicely characterize the interaction
between function composition and (restricted) quantification:}›
lemma Ra_all_comp1: "❙∀(π∘γ) = ❙∀[π|⦇Ra γ⦈]⇧P" by (metis comp_apply pfunRange_def)
lemma Ra_all_comp2: "❙∀(π∘γ) = ❙∀⇧R⦇Ra γ⦈ π" by (metis comp_apply pfunRange_def)
lemma Ra_ex_comp1:  "❙∃(π∘γ) = ❙∃[π|⦇Ra γ⦈]⇧N" by (metis comp_apply pfunRange_def)
lemma Ra_ex_comp2:  "❙∃(π∘γ) = ❙∃⇧R⦇Ra γ⦈ π" by (metis comp_apply pfunRange_def)

text‹\noindent{This useful operator returns for a given domain of propositions the domain of their complements:}›
definition dom_compl::"(σ⇒bool)⇒(σ⇒bool)" ("(_¯)") where "D¯ ≡ λX. ∃Y. (D Y) ∧ (X = ❙─Y)"
lemma dom_compl_def2: "D¯ = (λX. D(❙─X))" unfolding dom_compl_def by (metis comp_symm fun_upd_same)
lemma dom_compl_invol: "D = (D¯)¯" unfolding dom_compl_def by (metis comp_symm fun_upd_same)

text‹\noindent{We can now check an infinite variant of the De Morgan laws,}›
lemma iDM_a: "❙─(❙⋀S) = ❙⋁S¯" unfolding dom_compl_def2 infimum_def supremum_def using compl_def by force
lemma iDM_b:" ❙─(❙⋁S) = ❙⋀S¯" unfolding dom_compl_def2 infimum_def supremum_def using compl_def by force

text‹\noindent{and some useful dualities regarding the range of propositional functions (restricted wrt. a domain).}›
lemma Ra_compl: "Ra[π⇧c|D]  = Ra[π|D]¯" unfolding pfunRange_restr_def dom_compl_def by auto
lemma Ra_dual1: "Ra[π⇧d|D]  = Ra[π|D¯]¯" unfolding pfunRange_restr_def dom_compl_def using dual_def by auto
lemma Ra_dual2: "Ra[π⇧d|D]  = Ra[π⇧c|D¯]" unfolding pfunRange_restr_def dom_compl_def using dual_def by auto
lemma Ra_dual3: "Ra[π⇧d|D]¯ = Ra[π|D¯]" unfolding pfunRange_restr_def dom_compl_def using dual_def comp_symm by metis
lemma Ra_dual4: "Ra[π⇧d|D¯] = Ra[π|D]¯" using Ra_dual3 dual_symm by metis

text‹\noindent{Finally, we check some facts concerning duality for quantifiers.}›
lemma "❙∃π⇧c = ❙─(❙∀π)" using compl_def by auto
lemma "❙∀π⇧c = ❙─(❙∃π)" using compl_def by auto
lemma "❙∃X. ❙─π X = ❙─(❙∀X. π X)" using compl_def by auto
lemma "❙∀X. ❙─π X = ❙─(❙∃X. π X)" using compl_def by auto

lemma "❙∃⇧R(δ)π⇧c = ❙─(❙∀⇧R(δ)π)" using compl_def by auto
lemma "❙∀⇧R(δ)π⇧c = ❙─(❙∃⇧R(δ)π)" using compl_def by auto
lemma "❙∃X. ❙─[π|δ]⇧P X = ❙─(❙∀X. [π|δ]⇧P X)" using compl_def by auto
lemma "❙∀X. ❙─[π|δ]⇧P X = ❙─(❙∃X. [π|δ]⇧P X)" using compl_def by auto
lemma "❙∃X. ❙─[π|δ]⇧N X = ❙─(❙∀X. [π|δ]⇧N X)" using compl_def by auto
lemma "❙∀X. ❙─[π|δ]⇧N X = ❙─(❙∃X. [π|δ]⇧N X)" using compl_def by auto

text‹\noindent{Warning: Do not switch P and N when passing to the dual form.}›
lemma "❙∀X. [π|δ]⇧P X = ❙─(❙∃X. ❙─[π|δ]⇧N X)" nitpick oops ―‹ wrong: counterexample ›
lemma "❙∀X. [π|δ]⇧P X = ❙─(❙∃X. ❙─[π|δ]⇧P X)" using compl_def by auto ―‹ correct ›

end


# Theory sse_operation_positive

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

section ‹Positive semantic conditions for operations›

text‹\noindent{We define and interrelate some useful conditions on propositional functions which do not involve
negative-like properties (hence 'positive'). We focus on propositional functions which correspond to unary
connectives of the algebra (with type @{text "σ⇒σ"}). We call such propositional functions 'operations'.}›

subsection ‹Definitions (finitary case)›

text‹\noindent{Monotonicity (MONO).}›
definition "MONO φ ≡ ∀A B. A ❙≼ B ⟶ φ A ❙≼ φ B"
lemma MONO_ant: "MONO φ ⟹ ∀A B C. A ❙≼ B ⟶ φ(B ❙→ C) ❙≼ φ(A ❙→ C)" by (smt MONO_def conn)
lemma MONO_cons: "MONO φ ⟹ ∀A B C. A ❙≼ B ⟶ φ(C ❙→ A) ❙≼ φ(C ❙→ B)" by (smt MONO_def conn)
lemma MONO_dual: "MONO φ ⟹ MONO φ⇧d" by (smt MONO_def dual_def compl_def)

text‹\noindent{Extensive/expansive (EXP) and its dual (dEXP), aka. 'contractive'.}›
definition "EXP φ  ≡ ∀A. A ❙≼ φ A"
definition "dEXP φ ≡ ∀A. φ A ❙≼ A"
lemma EXP_dual1: "EXP φ ⟹ dEXP φ⇧d" by (metis EXP_def dEXP_def dual_def compl_def)
lemma EXP_dual2: "dEXP φ ⟹ EXP φ⇧d" by (metis EXP_def dEXP_def dual_def compl_def)

text‹\noindent{Idempotence (IDEM).}›
definition "IDEM φ  ≡ ∀A. (φ A) ❙≈ φ(φ A)"
definition "IDEMa φ ≡ ∀A. (φ A) ❙≼ φ(φ A)"
definition "IDEMb φ ≡ ∀A. (φ A) ❙≽ φ(φ A)"
lemma IDEM_dual1: "IDEMa φ ⟹ IDEMb φ⇧d" unfolding dual_def IDEMa_def IDEMb_def compl_def by auto
lemma IDEM_dual2: "IDEMb φ ⟹ IDEMa φ⇧d" unfolding dual_def IDEMa_def IDEMb_def compl_def by auto
lemma IDEM_dual: "IDEM φ = IDEM φ⇧d" by (metis IDEM_def IDEM_dual1 IDEM_dual2 IDEMa_def IDEMb_def dual_symm)

text‹\noindent{Normality (NOR) and its dual (dNOR).}›
definition "NOR φ  ≡ (φ ❙⊥) ❙≈ ❙⊥"
definition "dNOR φ ≡ (φ ❙⊤) ❙≈ ❙⊤"
lemma NOR_dual1: "NOR φ = dNOR φ⇧d" unfolding dual_def NOR_def dNOR_def top_def bottom_def compl_def by simp
lemma NOR_dual2: "dNOR φ = NOR φ⇧d" unfolding dual_def NOR_def dNOR_def top_def bottom_def compl_def by simp

text‹\noindent{Distribution over meets or multiplicativity (MULT).}›
definition "MULT φ   ≡ ∀A B. φ(A ❙∧ B) ❙≈ (φ A) ❙∧ (φ B)"
definition "MULT_a φ ≡ ∀A B. φ(A ❙∧ B) ❙≼ (φ A) ❙∧ (φ B)"
definition "MULT_b φ ≡ ∀A B. φ(A ❙∧ B) ❙≽ (φ A) ❙∧ (φ B)"

definition "ADDI φ   ≡ ∀A B. φ(A ❙∨ B) ❙≈ (φ A) ❙∨ (φ B)"
definition "ADDI_a φ ≡ ∀A B. φ(A ❙∨ B) ❙≼ (φ A) ❙∨ (φ B)"
definition "ADDI_b φ ≡ ∀A B. φ(A ❙∨ B) ❙≽ (φ A) ❙∨ (φ B)"

subsection ‹Relations among conditions (finitary case)›

text‹\noindent{dEXP and dNOR entail NOR.}›
lemma "dEXP φ ⟹ dNOR φ ⟹ NOR φ" by (meson bottom_def dEXP_def NOR_def)

text‹\noindent{EXP and NOR entail dNOR.}›
lemma "EXP φ ⟹ NOR φ ⟹ dNOR φ" by (simp add: EXP_def dNOR_def top_def)

text‹\noindent{Interestingly, EXP and its dual allow for an alternative characterization of fixed-point operators.}›
lemma EXP_fp:  "EXP  φ ⟹ φ⇧f⇧p ❙≡ (φ⇧c ❙⊔ id)" by (smt id_def EXP_def dual_def dual_symm equal_op_def conn)
lemma dEXP_fp: "dEXP φ ⟹ φ⇧f⇧p ❙≡ (φ ❙⊔ compl)" by (smt dEXP_def equal_op_def conn)

text‹\noindent{MONO, MULT-a and ADDI-b are equivalent.}›
lemma MONO_MULTa: "MONO φ = MULT_a φ" proof -
have lr: "MONO φ ⟹ MULT_a φ" by (smt MONO_def MULT_a_def meet_def)
have rl: "MULT_a φ ⟹ MONO φ" proof-
assume multa: "MULT_a φ"
{ fix A B
{ assume "A ❙≼ B"
hence "A ❙≈ A ❙∧ B" unfolding conn by blast
hence "φ A ❙≈ φ(A ❙∧ B)" unfolding conn by simp
moreover from multa have "φ(A ❙∧ B) ❙≼ (φ A) ❙∧ (φ B)" using MULT_a_def by metis
ultimately have "φ A ❙≼ (φ A) ❙∧ (φ B)" by blast
hence "φ A ❙≼ (φ B)" unfolding conn by blast
} hence "A ❙≼ B ⟶ φ A ❙≼ φ B" by (rule impI)
} thus ?thesis by (simp add: MONO_def) qed
from lr rl show ?thesis by auto
qed
have lr: "MONO φ ⟹ ADDI_b φ" by (smt ADDI_b_def MONO_def join_def)
have rl: "ADDI_b φ ⟹ MONO φ" proof -
{ fix A B
{ assume "A ❙≼ B"
hence "B ❙≈ A ❙∨ B" unfolding conn by blast
hence "φ B ❙≈ φ(A ❙∨ B)" unfolding conn by simp
moreover from addib have "(φ A) ❙∨ (φ B) ❙≼ φ(A ❙∨ B)" using ADDI_b_def by metis
ultimately have "(φ A) ❙∨ (φ B) ❙≼ φ B" by blast
hence "φ A ❙≼ (φ B)" unfolding conn by blast
} hence "A ❙≼ B ⟶ φ A ❙≼ φ B" by (rule impI)
} thus ?thesis by (simp add: MONO_def) qed
from lr rl show ?thesis by auto
qed

end


# Theory sse_operation_positive_quantification

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

subsection ‹Definitions (infinitary case)›

text‹\noindent{We define and interrelate infinitary variants for some previously introduced ('positive') conditions
on operations and show how they relate to quantifiers as previously defined.}›

text‹\noindent{Distribution over infinite meets (infima) or infinite multiplicativity (iMULT).}›
definition "iMULT φ   ≡ ∀S. φ(❙⋀S) ❙≈ ❙⋀Ra[φ|S]"
definition "iMULT_a φ ≡ ∀S. φ(❙⋀S) ❙≼ ❙⋀Ra[φ|S]"
definition "iMULT_b φ ≡ ∀S. φ(❙⋀S) ❙≽ ❙⋀Ra[φ|S]"

definition "iADDI φ   ≡ ∀S. φ(❙⋁S) ❙≈ ❙⋁Ra[φ|S]"
definition "iADDI_a φ ≡ ∀S. φ(❙⋁S) ❙≼ ❙⋁Ra[φ|S]"
definition "iADDI_b φ ≡ ∀S. φ(❙⋁S) ❙≽ ❙⋁Ra[φ|S]"

subsection ‹Relations among conditions (infinitary case)›

text‹\noindent{We start by noting that there is a duality between iADDI-a and iMULT-b.}›
lemma iADDI_MULT_dual1: "iADDI_a φ ⟹ iMULT_b φ⇧d" unfolding iADDI_a_def iMULT_b_def by (metis compl_def dual_def iDM_a iDM_b Ra_dual1)

text‹\noindent{MULT-a and iMULT-a are equivalent.}›
lemma iMULTa_rel: "iMULT_a φ = MULT_a φ" proof -
have lr: "iMULT_a φ ⟹ MULT_a φ" proof -
assume imulta: "iMULT_a φ"
{ fix A::"σ" and B::"σ"
let ?S="λZ. Z=A ∨ Z=B"
from imulta have "φ(❙⋀?S) ❙≼ ❙∀⇧R⦇?S⦈ φ" by (simp add: iMULT_a_def Ra_restr_all)
moreover have "❙⋀?S = A ❙∧ B" using infimum_def meet_def by auto
moreover have "❙∀⇧R⦇?S⦈ φ = (φ A) ❙∧ (φ B)" using meet_def by auto
ultimately have "φ(A ❙∧ B) ❙≼ (φ A) ❙∧ (φ B)" by smt
} thus ?thesis by (simp add: MULT_a_def) qed
have rl: "MULT_a φ ⟹ iMULT_a φ" by (smt MONO_def MONO_MULTa Ra_restr_all iMULT_a_def inf_char)
from lr rl show ?thesis by auto
qed
{ fix A::"σ" and B::"σ"
let ?S="λZ. Z=A ∨ Z=B"
moreover have "❙⋁?S = A ❙∨ B" using supremum_def join_def by auto
moreover have "❙∃⇧R⦇?S⦈(φ) = (φ A) ❙∨ (φ B)" using join_def by auto
ultimately have "φ(A ❙∨ B) ❙≽ (φ A) ❙∨ (φ B)" by smt
from lr rl show ?thesis by auto
qed

lemma MONO_iMULTa: "MONO φ = iMULT_a φ" using MONO_MULTa iMULTa_rel by simp

lemma PI_imult: "MONO φ ⟹ iMULT_b φ ⟹ iMULT φ" using MONO_MULTa iMULT_a_def iMULT_b_def iMULT_def iMULTa_rel by auto

text‹\noindent{Interestingly, we can show that suitable (infinitary) conditions on an operation can make the set
of its fixed points closed under infinite meets/joins.}›
lemma fp_inf_closed: "MONO φ ⟹ iMULT_b φ ⟹ infimum_closed (fp φ)" by (metis (full_types) PI_imult Ra_restr_all iMULT_def infimum_def)
lemma fp_sup_closed: "MONO φ ⟹ iADDI_a φ ⟹ supremum_closed (fp φ)" by (metis (full_types) PC_iaddi Ra_restr_ex iADDI_def supremum_def)

subsection ‹Exploring the Barcan formula and its converse›

text‹\noindent{The converse Barcan formula follows readily from monotonicity.}›
lemma CBarcan1: "MONO φ ⟹ ∀π.  φ(❙∀x. π x)  ❙≼ (❙∀x. φ(π x))" by (metis (mono_tags, lifting) MONO_def)
lemma CBarcan2: "MONO φ ⟹ ∀π. (❙∃x. φ(π x)) ❙≼ φ(❙∃x. π x)" by (metis (mono_tags, lifting) MONO_def)

text‹\noindent{However, the Barcan formula requires a stronger assumption (of an infinitary character).}›
lemma Barcan1: "iMULT_b φ ⟹ ∀π. (❙∀x. φ(π x)) ❙≼ φ(❙∀x. π x)" proof -
assume imultb: "iMULT_b φ"
{ fix π::"'a⇒σ"
from imultb have "(❙⋀Ra(φ∘π)) ❙≼ φ(❙⋀Ra(π))" unfolding iMULT_b_def by (smt comp_apply infimum_def pfunRange_def pfunRange_restr_def)
moreover have "❙⋀Ra(π) = (❙∀x. π x)" unfolding Ra_all by simp
moreover have "❙⋀Ra(φ∘π) = (❙∀x. φ(π x))" unfolding Ra_all by simp
ultimately have "(❙∀x. φ(π x)) ❙≼ φ(❙∀x. π x)" by simp
} thus ?thesis by simp
qed
lemma Barcan2: "iADDI_a φ ⟹ ∀π. φ(❙∃x. π x) ❙≼ (❙∃x. φ(π x))" proof -
{ fix π::"'a⇒σ"
from iaddia have "φ(❙⋁Ra(π)) ❙≼ (❙⋁Ra(φ∘π))" unfolding iADDI_a_def Ra_restr_ex by (smt fcomp_comp fcomp_def pfunRange_def sup_char)
moreover have "❙⋁Ra(π) = (❙∃x. π x)" unfolding Ra_ex by simp
moreover have "❙⋁Ra(φ∘π) = (❙∃x. φ(π x))" unfolding Ra_ex by simp
ultimately have "φ(❙∃x. π x) ❙≼ (❙∃x. φ(π x))" by simp
} thus ?thesis by simp
qed

end


# Theory sse_operation_negative

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

section ‹Negative semantic conditions for operations›

text‹\noindent{We define and interrelate some conditions on operations (i.e. propositional functions of type
@{text "σ⇒σ"}), this time involving negative-like properties.}›

named_theorems Defs

subsection ‹Definitions and interrelations (finitary case)›

subsubsection ‹Principles of excluded middle, contradiction and explosion›

text‹\noindent{TND: tertium non datur, aka. law of excluded middle (resp. strong, weak, minimal).}›
abbreviation pTND  ("TND⇧_  _") where "TND⇧a  η ≡       ❙⊤  ❙≈ a ❙∨ (η a)"
abbreviation pTNDw ("TNDw⇧_ _") where "TNDw⇧a η ≡ ∀b. (η b) ❙≼ a ❙∨ (η a)"
abbreviation pTNDm ("TNDm⇧_ _") where "TNDm⇧a η ≡     (η ❙⊥) ❙≼ a ❙∨ (η a)"
definition "TND  η ≡ ∀φ. TND⇧φ  η"
definition "TNDw η ≡ ∀φ. TNDw⇧φ η"
definition "TNDm η ≡ ∀φ. TNDm⇧φ η"
declare TND_def[Defs] TNDw_def[Defs] TNDm_def[Defs]

text‹\noindent{Explore some (non)entailment relations:}›
lemma "TND  η ⟹ TNDw η" unfolding Defs conn by simp
lemma "TNDw η ⟹ TND  η" nitpick oops
lemma "TNDw η ⟹ TNDm η" unfolding Defs by simp
lemma "TNDm η ⟹ TNDw η" nitpick oops

text‹\noindent{ECQ: ex contradictione (sequitur) quodlibet (resp: strong, weak, minimal).}›
abbreviation pECQ  ("ECQ⇧_ _")  where "ECQ⇧a  η ≡     a ❙∧ (η a) ❙≈ ❙⊥"
abbreviation pECQw ("ECQw⇧_ _") where "ECQw⇧a η ≡ ∀b. a ❙∧ (η a) ❙≼ (η b)"
abbreviation pECQm ("ECQm⇧_ _") where "ECQm⇧a η ≡     a ❙∧ (η a) ❙≼ (η ❙⊤)"
definition "ECQ  η ≡ ∀a. ECQ⇧a  η"
definition "ECQw η ≡ ∀a. ECQw⇧a η"
definition "ECQm η ≡ ∀a. ECQm⇧a η"
declare ECQ_def[Defs] ECQw_def[Defs] ECQm_def[Defs]

text‹\noindent{Explore some (non)entailment relations:}›
lemma "ECQ  η ⟹ ECQw η" unfolding Defs conn by blast
lemma "ECQw η ⟹ ECQ  η" nitpick oops
lemma "ECQw η ⟹ ECQm η" unfolding Defs conn by simp
lemma "ECQm η ⟹ ECQw η" nitpick oops

abbreviation pLNC  ("LNC⇧_ _")  where "LNC⇧a η ≡ η(a ❙∧ η a) ❙≈ ❙⊤"
definition "LNC η ≡ ∀a. LNC⇧a η"
declare LNC_def[Defs]

text‹\noindent{ECQ and LNC are in general independent.}›
lemma "ECQ η ⟹ LNC η" nitpick oops
lemma "LNC η ⟹ ECQm η" nitpick oops

subsubsection ‹Contraposition rules›

text‹\noindent{CoP: contraposition (global/rule variants, resp. weak, strong var. 1, strong var. 2, strong var. 3).}›
abbreviation pCoPw ("CoPw⇧_⇧_ _") where "CoPw⇧a⇧b η ≡ a ❙≼ b ⟶ (η b) ❙≼ (η a)"
abbreviation pCoP1 ("CoP1⇧_⇧_ _") where "CoP1⇧a⇧b η ≡ a ❙≼ (η b) ⟶ b ❙≼ (η a)"
abbreviation pCoP2 ("CoP2⇧_⇧_ _") where "CoP2⇧a⇧b η ≡ (η a) ❙≼ b ⟶ (η b) ❙≼ a"
abbreviation pCoP3 ("CoP3⇧_⇧_ _") where "CoP3⇧a⇧b η ≡ (η a) ❙≼ (η b) ⟶ b ❙≼ a"
definition "CoPw  η ≡ ∀a b. CoPw⇧a⇧b η"
definition "CoP1  η ≡ ∀a b. CoP1⇧a⇧b η"
definition "CoP1' η ≡ ∀a b. a ❙≼ (η b) ⟷ b ❙≼ (η a)"
definition "CoP2  η ≡ ∀a b. CoP2⇧a⇧b η"
definition "CoP2' η ≡ ∀a b. (η a) ❙≼ b ⟷ (η b) ❙≼ a"
definition "CoP3  η ≡ ∀a b. CoP3⇧a⇧b η"
declare CoPw_def[Defs] CoP1_def[Defs] CoP1'_def[Defs]
CoP2_def[Defs] CoP2'_def[Defs] CoP3_def[Defs]

lemma CoP1_defs_rel: "CoP1 η = CoP1' η" unfolding Defs by metis
lemma CoP2_defs_rel: "CoP2 η = CoP2' η" unfolding Defs by metis

text‹\noindent{Explore some (non)entailment relations:}›
lemma "CoP1 η ⟹ CoPw η" unfolding Defs by metis
lemma "CoPw η ⟹ CoP1 η" nitpick oops
lemma "CoP2 η ⟹ CoPw η" unfolding Defs by metis
lemma "CoPw η ⟹ CoP2 η" nitpick oops
lemma "CoP3 η ⟹ CoPw η" (*nitpick*) oops ―‹ no countermodel found so far ›
lemma "CoPw η ⟹ CoP3 η" nitpick oops

text‹\noindent{All three strong variants are pairwise independent. However, CoP3 follows from CoP1 plus CoP2.}›
lemma CoP123: "CoP1 η ⟹ CoP2 η ⟹ CoP3 η" unfolding Defs by smt
text‹\noindent{Taking all CoP together still leaves room for a boldly paraconsistent resp. paracomplete logic.}›
lemma "CoP1 η ⟹ CoP2 η ⟹ ECQm η" nitpick oops
lemma "CoP1 η ⟹ CoP2 η ⟹ TNDm η" nitpick oops

subsubsection ‹Modus tollens rules›

text‹\noindent{MT: modus (tollendo) tollens (global/rule variants).}›
abbreviation pMT0 ("MT0⇧_⇧_ _") where "MT0⇧a⇧b η ≡ a ❙≼ b ∧ (η b) ❙≈ ❙⊤ ⟶ (η a) ❙≈ ❙⊤"
abbreviation pMT1 ("MT1⇧_⇧_ _") where "MT1⇧a⇧b η ≡ a ❙≼ (η b) ∧ b ❙≈ ❙⊤ ⟶ (η a) ❙≈ ❙⊤"
abbreviation pMT2 ("MT2⇧_⇧_ _") where "MT2⇧a⇧b η ≡ (η a) ❙≼ b ∧ (η b) ❙≈ ❙⊤ ⟶ a ❙≈ ❙⊤"
abbreviation pMT3 ("MT3⇧_⇧_ _") where "MT3⇧a⇧b η ≡ (η a) ❙≼ (η b) ∧ b ❙≈ ❙⊤ ⟶ a ❙≈ ❙⊤"
definition "MT0 η ≡ ∀a b. MT0⇧a⇧b η"
definition "MT1 η ≡ ∀a b. MT1⇧a⇧b η"
definition "MT2 η ≡ ∀a b. MT2⇧a⇧b η"
definition "MT3 η ≡ ∀a b. MT3⇧a⇧b η"
declare MT0_def[Defs] MT1_def[Defs] MT2_def[Defs] MT3_def[Defs]

text‹\noindent{Again, all MT variants are pairwise independent. We explore some (non)entailment relations:}›
lemma "CoPw η ⟹ MT0 η" unfolding Defs by (metis top_def)
lemma "CoP1 η ⟹ MT1 η" unfolding Defs by (metis top_def)
lemma "CoP2 η ⟹ MT2 η" unfolding Defs by (metis top_def)
lemma "CoP3 η ⟹ MT3 η" unfolding Defs by (metis top_def)
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ CoPw η" nitpick oops
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ ECQm η" nitpick oops
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ TNDm η" nitpick oops
lemma MT123: "MT1 η ⟹ MT2 η ⟹ MT3 η"  unfolding Defs by smt

subsubsection ‹Double negation introduction and elimination›

text‹\noindent{DNI/DNE: double negation introduction/elimination (as axioms).}›
abbreviation pDNI ("DNI⇧_ _") where "DNI⇧a η ≡ a ❙≼ η (η a)"
abbreviation pDNE ("DNE⇧_ _") where "DNE⇧a η ≡ η (η a) ❙≼ a"
definition "DNI η ≡ ∀a. DNI⇧a η"
definition "DNE η ≡ ∀a. DNE⇧a η"
declare DNI_def[Defs] DNE_def[Defs]

text‹\noindent{CoP1 (resp. CoP2) can alternatively be defined as CoPw plus DNI (resp. DNE).}›
lemma "DNI η ⟹ CoP1 η" nitpick oops
lemma CoP1_def2: "CoP1 η = (CoPw η ∧ DNI η)" unfolding Defs by smt
lemma "DNE η ⟹  CoP2 η" nitpick oops
lemma CoP2_def2: "CoP2 η = (CoPw η ∧ DNE η)" unfolding Defs by smt

text‹\noindent{Explore some non-entailment relations:}›
lemma "DNI η ⟹ DNE η ⟹ CoPw η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ TNDm η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ ECQm η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT0 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT1 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT2 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT3 η" nitpick oops

text‹\noindent{DNI/DNE: double negation introduction/elimination (as rules).}›
abbreviation prDNI ("rDNI⇧_ _") where "rDNI⇧a η ≡ a ❙≈ ❙⊤ ⟶ η (η a) ❙≈ ❙⊤"
abbreviation prDNE ("rDNE⇧_ _") where "rDNE⇧a η ≡ η (η a) ❙≈ ❙⊤ ⟶ a ❙≈ ❙⊤"
definition "rDNI η ≡ ∀a. rDNI⇧a η"
definition "rDNE η ≡ ∀a. rDNE⇧a η"
declare rDNI_def[Defs] rDNE_def[Defs]

text‹\noindent{The rule variants are strictly weaker than the axiom variants,}›
lemma "DNI η ⟹ rDNI η" by (simp add: DNI_def rDNI_def top_def)
lemma "rDNI η ⟹ DNI η" nitpick oops
lemma "DNE η ⟹ rDNE η" by (metis DNE_def rDNE_def top_def)
lemma "rDNE η ⟹ DNE η" nitpick oops
lemma MT1_rDNI: "MT1 η ⟹ rDNI η" unfolding Defs by blast
lemma MT2_rDNE: "MT2 η ⟹ rDNE η" unfolding Defs by blast

subsubsection ‹Normality and its dual›

text‹\noindent{n(D)Nor: negative (dual) 'normality'.}›
definition "nNor η ≡ (η ❙⊥) ❙≈ ❙⊤"
definition "nDNor η ≡ (η ❙⊤) ❙≈ ❙⊥"
declare nNor_def[Defs] nDNor_def[Defs]

text‹\noindent{nNor (resp. nDNor) is entailed by CoP1 (resp. CoP2). }›
lemma CoP1_Nor: "CoP1 η ⟹ nNor η" unfolding Defs conn by simp
lemma CoP2_DNor: "CoP2 η ⟹ nDNor η" unfolding Defs conn by fastforce
lemma "DNI η ⟹ nNor η" nitpick oops
lemma "DNE η ⟹ nDNor η" nitpick oops
text‹\noindent{nNor and nDNor together entail the rule variant of DNI (rDNI).}›
lemma nDNor_rDNI: "nNor η ⟹ nDNor η ⟹ rDNI η" unfolding Defs using nDNor_def nNor_def eq_ext by metis
lemma "nNor η ⟹ nDNor η ⟹ rDNE η" nitpick oops

subsubsection ‹De Morgan laws›

text‹\noindent{DM: De Morgan laws.}›
abbreviation pDM1 ("DM1⇧_⇧_ _") where "DM1⇧a⇧b η ≡ η(a ❙∨ b) ❙≼ (η a) ❙∧ (η b)"
abbreviation pDM2 ("DM2⇧_⇧_ _") where "DM2⇧a⇧b η ≡ (η a) ❙∨ (η b) ❙≼ η(a ❙∧ b)"
abbreviation pDM3 ("DM3⇧_⇧_ _") where "DM3⇧a⇧b η ≡ η(a ❙∧ b) ❙≼ (η a) ❙∨ (η b)"
abbreviation pDM4 ("DM4⇧_⇧_ _") where "DM4⇧a⇧b η ≡ (η a) ❙∧ (η b) ❙≼  η(a ❙∨ b)"
definition "DM1 η ≡ ∀a b. DM1⇧a⇧b η"
definition "DM2 η ≡ ∀a b. DM2⇧a⇧b η"
definition "DM3 η ≡ ∀a b. DM3⇧a⇧b η"
definition "DM4 η ≡ ∀a b. DM4⇧a⇧b η"
declare DM1_def[Defs] DM2_def[Defs] DM3_def[Defs] DM4_def[Defs]

text‹\noindent{CoPw, DM1 and DM2 are indeed equivalent.}›
lemma DM1_CoPw: "DM1 η = CoPw η" proof -
have LtoR: "DM1 η ⟹ CoPw η" proof -
assume dm1: "DM1 η"
{ fix a b
{ assume "a ❙≼ b"
hence 1: "a ❙∨ b ❙≼ b" unfolding conn by simp
have 2: "b ❙≼ a ❙∨ b" unfolding conn by simp
from 1 2 have "b = a ❙∨ b" using eq_ext by blast
hence 3: "η b ❙≈ η (a ❙∨ b)" by auto
from dm1 have "η(a ❙∨ b) ❙≼ (η a) ❙∧ (η b)" unfolding Defs by blast
hence 4: "(η b) ❙≼ (η a) ❙∧ (η b)" using 3 by simp
have 5: "(η a) ❙∧ (η b) ❙≼ (η a)" unfolding conn by simp
from 4 5 have "(η b) ❙≼ (η a)" by simp
} hence "a ❙≼ b ⟶ (η b) ❙≼ (η a)" by (rule impI)
} thus ?thesis unfolding Defs by simp
qed
have RtoL: "CoPw η ⟹ DM1 η" unfolding Defs conn by (metis (no_types, lifting))
thus ?thesis using LtoR RtoL by blast
qed
lemma DM2_CoPw: "DM2 η = CoPw η" proof -
have LtoR: "DM2 η ⟹ CoPw η" proof -
assume dm2: "DM2 η"
{ fix a b
{ assume "a ❙≼ b"
hence 1: "a ❙≼ a ❙∧ b" unfolding conn by simp
have 2: "a ❙∧ b ❙≼ a" unfolding conn by simp
from 1 2 have "a = a ❙∧ b" using eq_ext by blast
hence 3: "η a ❙≈ η (a ❙∧ b)" by auto
from dm2 have "(η a) ❙∨ (η b) ❙≼ η(a ❙∧ b)" unfolding Defs by blast
hence 4: "(η a) ❙∨ (η b) ❙≼ (η a) " using 3 by simp
have 5: "(η b) ❙≼ (η a) ❙∨ (η b)" unfolding conn by simp
from 4 5 have "(η b) ❙≼ (η a)" by simp
} hence "a ❙≼ b ⟶ (η b) ❙≼ (η a)" by (rule impI)
} thus ?thesis unfolding Defs by simp
qed
have RtoL: "CoPw η ⟹ DM2 η" unfolding Defs conn by (metis (no_types, lifting))
thus ?thesis using LtoR RtoL by blast
qed
lemma DM12: "DM1 η = DM2 η" by (simp add: DM1_CoPw DM2_CoPw)

text‹\noindent{DM3 (resp. DM4) are entailed by CoPw together with DNE (resp. DNI).}›
lemma CoPw_DNE_DM3: "CoPw η ⟹ DNE η ⟹ DM3 η" proof -
assume copw: "CoPw η" and dne: "DNE η"
{ fix a b
have "η(a) ❙≼ (η a) ❙∨ (η b)" unfolding conn by simp
hence "η(η(a) ❙∨ η(b)) ❙≼ η((η a))" using CoPw_def copw by (metis (no_types, lifting))
hence 1: "η(η(a) ❙∨ η(b)) ❙≼ a" using DNE_def dne by metis
have "η(b) ❙≼ (η a) ❙∨ (η b)" unfolding conn by simp
hence "η(η(a) ❙∨ η(b)) ❙≼ η((η b))" using CoPw_def copw by (metis (no_types, lifting))
hence 2: "η(η(a) ❙∨ η(b)) ❙≼ b" using DNE_def dne by metis
from 1 2 have "η(η(a) ❙∨ η(b)) ❙≼ a ❙∧ b" unfolding conn by simp
hence "η(a ❙∧ b) ❙≼ η(η(η(a) ❙∨ η(b)))" using CoPw_def copw by smt
hence "η(a ❙∧ b) ❙≼ (η a) ❙∨ (η b)" using DNE_def dne by metis
} thus ?thesis by (simp add: DM3_def)
qed
lemma CoPw_DNI_DM4: "CoPw η ⟹ DNI η ⟹ DM4 η" proof -
assume copw: "CoPw η" and dni: "DNI η"
{ fix a b
have "(η a) ❙∧ (η b) ❙≼ η(a)" unfolding conn by simp
hence "η((η a)) ❙≼ η(η(a) ❙∧ η(b))" using CoPw_def copw by (metis (no_types, lifting))
hence 1: "a ❙≼ η(η(a) ❙∧ η(b))" using DNI_def dni by metis
have "(η a) ❙∧ (η b) ❙≼ η(b)" unfolding conn by simp
hence "η((η b)) ❙≼ η(η(a) ❙∧ η(b))" using CoPw_def copw by (metis (no_types, lifting))
hence 2: "b ❙≼ η(η(a) ❙∧ η(b))" using DNI_def dni by metis
from 1 2 have "a ❙∨ b ❙≼ η(η(a) ❙∧ η(b))" unfolding conn by simp
hence "η(η(η(a) ❙∧ η(b))) ❙≼ η(a ❙∨ b)" using CoPw_def copw by auto
hence "η(a) ❙∧ η(b) ❙≼ η(a ❙∨ b)" using DNI_def dni by simp
} thus ?thesis by (simp add: DM4_def)
qed
text‹\noindent{From this follows that DM3 (resp. DM4) is entailed by CoP2 (resp. CoP1).}›
lemma CoP2_DM3: "CoP2 η ⟹ DM3 η" by (simp add: CoP2_def2 CoPw_DNE_DM3)
lemma CoP1_DM4: "CoP1 η ⟹ DM4 η" by (simp add: CoP1_def2 CoPw_DNI_DM4)
text‹\noindent{Explore some non-entailment relations:}›
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ nNor η ⟹ nDNor η ⟹ DNI η" nitpick oops
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ nNor η ⟹ nDNor η ⟹ DNE η" nitpick oops
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ DNI η ⟹ DNE η ⟹ ECQm η" nitpick oops
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ DNI η ⟹ DNE η ⟹ TNDm η" nitpick oops

subsubsection ‹Contextual (strong) contraposition rule›

text‹\noindent{XCoP: contextual contraposition (global/rule variant).}›
abbreviation pXCoP ("XCoP⇧_⇧_ _") where "XCoP⇧a⇧b η ≡ ∀c. c ❙∧ a ❙≼ b ⟶ c ❙∧ (η b) ❙≼ (η a)"
definition "XCoP η ≡ ∀a b. XCoP⇧a⇧b η"
declare XCoP_def[Defs]

text‹\noindent{XCoP can alternatively be defined as ECQw plus TNDw.}›
lemma XCoP_def2: "XCoP η = (ECQw η ∧ TNDw η)" proof -
have LtoR1: "XCoP η ⟹ ECQw η" unfolding XCoP_def ECQw_def conn by auto
have LtoR2: "XCoP η ⟹ TNDw η" unfolding XCoP_def TNDw_def conn by (smt atom_def atomic2 conn)
have RtoL: "ECQw η ∧ TNDw η ⟹ XCoP η" using XCoP_def ECQw_def TNDw_def unfolding conn by metis
from LtoR1 LtoR2 RtoL show ?thesis by blast
qed
text‹\noindent{Explore some (non)entailment relations:}›
lemma "XCoP η ⟹ ECQ η" nitpick oops
lemma "XCoP η ⟹ TND η" nitpick oops
lemma XCoP_CoPw: "XCoP η ⟹ CoPw η" unfolding Defs conn by metis
lemma "XCoP η ⟹ CoP1 η" nitpick oops
lemma "XCoP η ⟹ CoP2 η" nitpick oops
lemma "XCoP η ⟹ CoP3 η" nitpick oops
lemma "CoP1 η ∧ CoP2 η ⟹ XCoP η" nitpick oops
lemma "XCoP η ⟹ nNor η" nitpick oops
lemma "XCoP η ⟹ nDNor η" nitpick oops
lemma "XCoP η ⟹ rDNI η" nitpick oops
lemma "XCoP η ⟹ rDNE η" nitpick oops
lemma XCoP_DM3: "XCoP η ⟹ DM3 η" unfolding DM3_def XCoP_def conn using ECQw_def TNDw_def atom_def atomic2 conn by smt
lemma XCoP_DM4: "XCoP η ⟹ DM4 η" unfolding DM4_def XCoP_def conn using ECQw_def TNDw_def atom_def atomic2 conn by smt

subsubsection ‹Local contraposition axioms›
text‹\noindent{Observe that the definitions below take implication as an additional parameter: @{text "ι"}.}›

text‹\noindent{lCoP: contraposition (local/axiom variants).}›
abbreviation plCoPw ("lCoPw⇧_⇧_ _ _") where "lCoPw⇧a⇧b ι η ≡ (ι a b::σ) ❙≼ (ι (η b) (η a))"
abbreviation plCoP1 ("lCoP1⇧_⇧_ _ _") where "lCoP1⇧a⇧b ι η ≡ (ι a (η b::σ)) ❙≼ (ι b (η a))"
abbreviation plCoP2 ("lCoP2⇧_⇧_ _ _") where "lCoP2⇧a⇧b ι η ≡ (ι (η a) b::σ) ❙≼ (ι (η b) a)"
abbreviation plCoP3 ("lCoP3⇧_⇧_ _ _") where "lCoP3⇧a⇧b ι η ≡ (ι (η a) (η b::σ)) ❙≼ (ι b a)"
definition "lCoPw  ι η ≡ ∀a b. lCoPw⇧a⇧b ι η"
definition "lCoP1  ι η ≡ ∀a b. lCoP1⇧a⇧b ι η"
definition "lCoP1' ι η ≡ ∀a b. (ι a (η b)) ❙≈ (ι b (η a))"
definition "lCoP2  ι η ≡ ∀a b. lCoP2⇧a⇧b ι η"
definition "lCoP2' ι η ≡ ∀a b. (ι (η a) b) ❙≈ (ι (η b) a)"
definition "lCoP3  ι η ≡ ∀a b. lCoP3⇧a⇧b ι η"
declare lCoPw_def[Defs] lCoP1_def[Defs] lCoP1'_def[Defs]
lCoP2_def[Defs] lCoP2'_def[Defs] lCoP3_def[Defs]

lemma lCoP1_defs_rel: "lCoP1 ι η = lCoP1' ι η" by (metis (full_types) lCoP1'_def lCoP1_def)
lemma lCoP2_defs_rel: "lCoP2 ι η = lCoP2' ι η" by (metis (full_types) lCoP2'_def lCoP2_def)

text‹\noindent{All local contraposition variants are in general independent from each other. However if we take
classical implication we can verify some relationships.}›

lemma lCoP1_def2: "lCoP1(❙→) η = (lCoPw(❙→) η ∧ DNI η)" unfolding Defs conn by smt
lemma lCoP2_def2: "lCoP2(❙→) η = (lCoPw(❙→) η ∧ DNE η)" unfolding Defs conn by smt

lemma "lCoP1(❙→) η ⟹ lCoPw(❙→) η" unfolding Defs conn by metis
lemma "lCoPw(❙→) η ⟹ lCoP1(❙→) η" nitpick oops
lemma "lCoP2(❙→) η ⟹ lCoPw(❙→) η" unfolding Defs conn by metis
lemma "lCoPw(❙→) η ⟹ lCoP2(❙→) η" nitpick oops
lemma "lCoP3(❙→) η ⟹ lCoPw(❙→) η" unfolding Defs conn by blast
lemma "lCoPw(❙→) η ⟹ lCoP3(❙→) η" nitpick oops
lemma lCoP123: "lCoP1(❙→) η ∧ lCoP2(❙→) η ⟹ lCoP3(❙→) η" unfolding Defs conn by metis

text‹\noindent{Local variants imply global ones as expected.}›
lemma "lCoPw(❙→) η ⟹ CoPw η" unfolding Defs conn by metis
lemma "lCoP1(❙→) η ⟹ CoP1 η" unfolding Defs conn by metis
lemma "lCoP2(❙→) η ⟹ CoP2 η" unfolding Defs conn by metis
lemma "lCoP3(❙→) η ⟹ CoP3 η" unfolding Defs conn by metis

text‹\noindent{Explore some (non)entailment relations.}›
lemma lCoPw_XCoP: "lCoPw(❙→) η = XCoP η" unfolding Defs conn by (smt XCoP_def XCoP_def2 TNDw_def conn)
lemma lCoP1_TND: "lCoP1(❙→) η ⟹ TND η" by (smt XCoP_CoPw XCoP_def2 CoP1_Nor CoP1_def2 nNor_def TND_def TNDw_def lCoP1_def2 lCoPw_XCoP conn)
lemma "TND η ⟹ lCoP1(❙→) η" nitpick oops
lemma lCoP2_ECQ: "lCoP2(❙→) η ⟹ ECQ η" by (smt XCoP_CoPw XCoP_def2 CoP2_DNor CoP2_def2 nDNor_def ECQ_def ECQw_def lCoP2_def2 lCoPw_XCoP conn)
lemma "ECQ η ⟹ lCoP2(❙→) η" nitpick oops

subsubsection ‹Local modus tollens axioms›

text‹\noindent{lMT: Modus tollens (local/axiom variants).}›
abbreviation plMT0 ("lMT0⇧_⇧_ _ _") where "lMT0⇧a⇧b ι η ≡ (ι a b::σ) ❙∧ (η b) ❙≼ (η a)"
abbreviation plMT1 ("lMT1⇧_⇧_ _ _") where "lMT1⇧a⇧b ι η ≡ (ι a (η b::σ)) ❙∧ b ❙≼ (η a)"
abbreviation plMT2 ("lMT2⇧_⇧_ _ _") where "lMT2⇧a⇧b ι η ≡ (ι (η a) b::σ) ❙∧ (η b) ❙≼ a"
abbreviation plMT3 ("lMT3⇧_⇧_ _ _") where "lMT3⇧a⇧b ι η ≡ (ι (η a) (η b::σ)) ❙∧ b ❙≼ a"
definition "lMT0 ι η ≡ ∀a b. lMT0⇧a⇧b ι η"
definition "lMT1 ι η ≡ ∀a b. lMT1⇧a⇧b ι η"
definition "lMT2 ι η ≡ ∀a b. lMT2⇧a⇧b ι η"
definition "lMT3 ι η ≡ ∀a b. lMT3⇧a⇧b ι η"
declare lMT0_def[Defs] lMT1_def[Defs] lMT2_def[Defs] lMT3_def[Defs]

text‹\noindent{All local MT variants are in general independent from each other and also from local CoP instances.
However if we take classical implication we can verify that local MT and CoP are indeed equivalent.}›
lemma "lMT0(❙→) η = lCoPw(❙→) η" unfolding Defs conn by metis
lemma "lMT1(❙→) η = lCoP1(❙→) η" unfolding Defs conn by metis
lemma "lMT2(❙→) η = lCoP2(❙→) η" unfolding Defs conn by metis
lemma "lMT3(❙→) η = lCoP3(❙→) η" unfolding Defs conn by metis

subsubsection ‹Disjunctive syllogism›

text‹\noindent{DS: disjunctive syllogism.}›
abbreviation pDS1 ("DS1⇧_⇧_ _ _") where "DS1⇧a⇧b ι η ≡ (a ❙∨ b::σ) ❙≼ (ι (η a) b)"
abbreviation pDS2 ("DS2⇧_⇧_ _ _") where "DS2⇧a⇧b ι η ≡ (ι (η a) b::σ) ❙≼ (a ❙∨ b)"
abbreviation pDS3 ("DS3⇧_⇧_ _ _") where "DS3⇧a⇧b ι η ≡ ((η a) ❙∨ b::σ) ❙≼ (ι a b)"
abbreviation pDS4 ("DS4⇧_⇧_ _ _") where "DS4⇧a⇧b ι η ≡ (ι a b::σ) ❙≼ ((η a) ❙∨ b)"
definition "DS1 ι η ≡ ∀a b. DS1⇧a⇧b ι η"
definition "DS2 ι η ≡ ∀a b. DS2⇧a⇧b ι η"
definition "DS3 ι η ≡ ∀a b. DS3⇧a⇧b ι η"
definition "DS4 ι η ≡ ∀a b. DS4⇧a⇧b ι η"
declare DS1_def[Defs] DS2_def[Defs] DS3_def[Defs] DS4_def[Defs]

text‹\noindent{All DS variants are in general independent from each other. However if we take classical implication
we can verify that the pairs DS1-DS3 and DS2-DS4 are indeed equivalent. }›
lemma "DS1(❙→) η = DS3(❙→) η" unfolding Defs by (metis impl_def join_def)
lemma "DS2(❙→) η = DS4(❙→) η" unfolding Defs by (metis impl_def join_def)

text‹\noindent{Explore some (non)entailment relations.}›
lemma DS1_nDNor: "DS1(❙→) η ⟹ nDNor η" unfolding Defs by (metis bottom_def impl_def join_def top_def)
lemma DS2_nNor:  "DS2(❙→) η ⟹ nNor η" unfolding Defs by (metis bottom_def impl_def join_def top_def)
lemma lCoP2_DS1: "lCoP2(❙→) η ⟹ DS1(❙→) η" unfolding Defs conn by metis
lemma lCoP1_DS2: "lCoP1(❙→) η ⟹ DS2(❙→) η" unfolding Defs by (metis (no_types, lifting) conn)
lemma "CoP2 η ⟹ DS1(❙→) η" nitpick oops
lemma "CoP1 η ⟹ DS2(❙→) η" nitpick oops

end


# Theory sse_operation_negative_quantification

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

subsection ‹Definitions and interrelations (infinitary case)›

text‹\noindent{We define and interrelate infinitary variants for some previously introduced ('negative') conditions
on operations. We show how they relate to quantifiers as previously defined.}›

text‹\noindent{iDM: infinitary De Morgan laws.}›
abbreviation riDM1 ("iDM1⇧_ _") where "iDM1⇧S η ≡ η(❙⋁S) ❙≼ ❙⋀Ra[η|S]"
abbreviation riDM2 ("iDM2⇧_ _") where "iDM2⇧S η ≡ ❙⋁Ra[η|S] ❙≼ η(❙⋀S)"
abbreviation riDM3 ("iDM3⇧_ _") where "iDM3⇧S η ≡ η(❙⋀S) ❙≼ ❙⋁Ra[η|S]"
abbreviation riDM4 ("iDM4⇧_ _") where "iDM4⇧S η ≡ ❙⋀Ra[η|S] ❙≼ η(❙⋁S)"
definition "iDM1 η ≡ ∀S. iDM1⇧S η"
definition "iDM2 η ≡ ∀S. iDM2⇧S η"
definition "iDM3 η ≡ ∀S. iDM3⇧S η"
definition "iDM4 η ≡ ∀S. iDM4⇧S η"
declare iDM1_def[Defs] iDM2_def[Defs] iDM3_def[Defs] iDM4_def[Defs]

lemma CoPw_iDM1: "CoPw η ⟹ iDM1 η" unfolding Defs by (smt Ra_restr_all sup_char)
lemma CoPw_iDM2: "CoPw η ⟹ iDM2 η" unfolding Defs by (smt Ra_restr_ex inf_char)
lemma CoP2_iDM3: "CoP2 η ⟹ iDM3 η" by (smt CoP2_def Ra_restr_ex iDM3_def inf_char)
lemma CoP1_iDM4: "CoP1 η ⟹ iDM4 η" by (smt CoP1_def Ra_restr_all iDM4_def sup_char)
lemma "XCoP η ⟹ iDM3 η" nitpick oops
lemma "XCoP η ⟹ iDM4 η" nitpick oops

text‹\noindent{DM1, DM2, iDM1, iDM2 and CoPw are equivalent.}›
lemma iDM1_rel: "iDM1 η ⟹ DM1 η" proof -
assume idm1: "iDM1 η"
{ fix a::"σ" and b::"σ"
let ?S="λZ. Z=a ∨ Z=b"
have "❙⋀Ra[η|?S] = ❙∀⇧R⦇?S⦈ η" using Ra_restr_all by blast
moreover have "❙∀⇧R⦇?S⦈ η = (η a) ❙∧ (η b)" using meet_def by auto
ultimately have "❙⋀Ra[η|?S] = (η a) ❙∧ (η b)" by simp
moreover have "❙⋁?S = a ❙∨ b" using supremum_def join_def by auto
moreover from idm1 have "η(❙⋁?S) ❙≼ ❙⋀Ra[η|?S]" by (simp add: iDM1_def)
ultimately have "η(a ❙∨ b) ❙≼ (η a) ❙∧ (η b)" by simp
} thus ?thesis by (simp add: DM1_def)
qed
lemma iDM2_rel: "iDM2 η ⟹ DM2 η" proof -
assume idm2: "iDM2 η"
{ fix a::"σ" and b::"σ"
let ?S="λZ. Z=a ∨ Z=b"
have "❙⋁Ra[η|?S] = ❙∃⇧R⦇?S⦈ η" using Ra_restr_ex by blast
moreover have "❙∃⇧R⦇?S⦈ η = (η a) ❙∨ (η b)" using join_def by auto
ultimately have "❙⋁Ra[η|?S] = (η a) ❙∨ (η b)" by simp
moreover have "❙⋀?S = a ❙∧ b" using infimum_def meet_def by auto
moreover from idm2 have "❙⋁Ra[η|?S] ❙≼ η(❙⋀?S)" by (simp add: iDM2_def)
ultimately have "(η a) ❙∨ (η b) ❙≼ η(a ❙∧ b)" by auto
} thus ?thesis by (simp add: DM2_def)
qed
lemma "DM1 η = iDM1 η" using CoPw_iDM1 DM1_CoPw iDM1_rel by blast
lemma "DM2 η = iDM2 η" using CoPw_iDM2 DM2_CoPw iDM2_rel by blast
lemma "iDM1 η = iDM2 η" using CoPw_iDM1 CoPw_iDM2 DM1_CoPw DM2_CoPw iDM1_rel iDM2_rel by blast

text‹\noindent{iDM3/4 entail their finitary variants but not the other way round.}›
lemma iDM3_rel: "iDM3 η ⟹ DM3 η" proof -
assume idm3: "iDM3 η"
{ fix a::"σ" and b::"σ"
let ?S="λZ. Z=a ∨ Z=b"
have "❙⋁Ra[η|?S] = ❙∃⇧R⦇?S⦈ η" using Ra_restr_ex by blast
moreover have "❙∃⇧R⦇?S⦈ η = (η a) ❙∨ (η b)" using join_def by auto
ultimately have "❙⋁Ra[η|?S] = (η a) ❙∨ (η b)" by simp
moreover have "❙⋀?S = a ❙∧ b" using infimum_def meet_def by auto
moreover from idm3 have "η(❙⋀?S) ❙≼ ❙⋁Ra[η|?S]" by (simp add: iDM3_def)
ultimately have "η(a ❙∧ b) ❙≼ (η a) ❙∨ (η b)" by auto
} thus ?thesis by (simp add: DM3_def)
qed
lemma iDM4_rel: "iDM4 η ⟹ DM4 η" proof -
assume idm4: "iDM4 η"
{ fix a::"σ" and b::"σ"
let ?S="λZ. Z=a ∨ Z=b"
have "❙⋀Ra[η|?S] = ❙∀⇧R⦇?S⦈ η" using Ra_restr_all by blast
moreover have "❙∀⇧R⦇?S⦈ η = (η a) ❙∧ (η b)" using meet_def by auto
ultimately have "❙⋀Ra[η|?S] = (η a) ❙∧ (η b)" by simp
moreover have "❙⋁?S = a ❙∨ b" using supremum_def join_def by auto
moreover from idm4 have "❙⋀Ra[η|?S] ❙≼ η(❙⋁?S)" by (simp add: iDM4_def)
ultimately have "(η a) ❙∧ (η b) ❙≼ η(a ❙∨ b)" by simp
} thus ?thesis by (simp add: DM4_def)
qed
lemma "DM3 η ⟹ iDM3 η" nitpick oops
lemma "DM4 η ⟹ iDM4 η" nitpick oops

text‹\noindent{Indeed the previous characterization of the infinitary De Morgan laws is fairly general and entails
the traditional version employing quantifiers (though not the other way round).}›
text‹\noindent{The first two variants DM1/2 follow easily from DM1/2, iDM1/2 or CoPw (all of them equivalent).}›
lemma iDM1_trad: "iDM1 η ⟹ ∀π. η(❙∃x. π x)  ❙≼  (❙∀x. η(π x))" by (metis (mono_tags, lifting) CoPw_def DM1_CoPw iDM1_rel)
lemma iDM2_trad: "iDM2 η ⟹ ∀π. (❙∃x. η(π x)) ❙≼ η(❙∀x. π x)" by (metis (mono_tags, lifting) CoPw_def DM2_CoPw iDM2_rel)

text‹\noindent{An analogous relationship holds for variants DM3/4, though the proof is less trivial.
To see how let us first consider an intermediate version of the De Morgan laws, obtained as a
particular case of the general variant above, with S as the range of a propositional function.}›
abbreviation "piDM1 π η ≡ η(❙⋁Ra(π)) ❙≼ ❙⋀Ra[η|Ra(π)]"
abbreviation "piDM2 π η ≡ ❙⋁Ra[η|Ra(π)] ❙≼ η(❙⋀Ra(π))"
abbreviation "piDM3 π η ≡ η(❙⋀Ra(π)) ❙≼ ❙⋁Ra[η|Ra(π)]"
abbreviation "piDM4 π η ≡ ❙⋀Ra[η|Ra(π)] ❙≼ η(❙⋁Ra(π))"

text‹\noindent{They are entailed (unidirectionally) by the general De Morgan laws.}›
lemma "iDM1 η ⟹ ∀π. piDM1 π η" by (simp add: iDM1_def)
lemma "iDM2 η ⟹ ∀π. piDM2 π η" by (simp add: iDM2_def)
lemma "iDM3 η ⟹ ∀π. piDM3 π η" by (simp add: iDM3_def)
lemma "iDM4 η ⟹ ∀π. piDM4 π η" by (simp add: iDM4_def)

text‹\noindent{Drawing upon the relationships shown previously we can rewrite the latter two as:}›
lemma iDM3_aux: "piDM3 π η ≡ η(❙∀π) ❙≼ ❙∃[η|⦇Ra π⦈]⇧N" unfolding Ra_all Ra_ex_restr by simp
lemma iDM4_aux: "piDM4 π η ≡ ❙∀[η|⦇Ra π⦈]⇧P ❙≼ η(❙∃π)" unfolding Ra_ex Ra_all_restr by simp

text‹\noindent{and thus finally obtain the desired formulas.}›
lemma iDM3_trad: "iDM3 η ⟹ ∀π. η(❙∀x. π x)  ❙≼  (❙∃x. η(π x))" by (metis Ra_ex_comp2 iDM3_def iDM3_aux comp_apply)
lemma iDM4_trad: "iDM4 η ⟹ ∀π. (❙∀x. η(π x)) ❙≼ η(❙∃x. π x)" by (metis Ra_all_comp1 iDM4_def iDM4_aux comp_apply)

end


# Theory topo_operators_basic

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

abbreviation implies_rl::"bool⇒bool⇒bool" (infixl "⟵" 25) where "φ ⟵ ψ ≡ ψ ⟶ φ" (*for readability*)

section ‹Topological operators›

text‹\noindent{Below we define some conditions on algebraic operations (aka. operators) with type @{text "σ⇒σ"}.
Those operations are aimed at extending a Boolean 'algebra of propositions' towards different
generalizations of topological algebras.
We divide this section into two parts. In the first we define and interrelate the topological operators of
interior, closure, border and frontier. In the second we introduce the (more fundamental) notion of
derivative (aka. derived set) and its related notion of (Cantorian) coherence, defining both as operators.
We follow the naming conventions introduced originally by Kuratowski @{cite Kuratowski1}
(cf. also @{cite Kuratowski2}) and Zarycki @{cite Zarycki1}.}›

subsection ‹Interior and closure›
text‹\noindent{In this section we examine the traditional notion of topological (closure, resp. interior) algebras
in the spirit of McKinsey \& Tarski @{cite AOT}, but drawing primarily from the works of Zarycki
@{cite Zarycki1} and Kuratowski @{cite Kuratowski1}.
We also explore the less-known notions of border (cf. 'Rand' @{cite Hausdorff}, 'bord' @{cite Zarycki1}) and
frontier (aka. 'boundary'; cf. 'Grenze' @{cite Hausdorff}, 'fronti\ere' @{cite Zarycki1} @{cite Kuratowski2})
as studied by Zarycki @{cite Zarycki1} and define corresponding operations for them.}›

subsubsection ‹Interior conditions›

abbreviation "Int_1 φ  ≡ MULT φ"
abbreviation "Int_1a φ ≡ MULT_a φ"
abbreviation "Int_1b φ ≡ MULT_b φ"
abbreviation "Int_2 φ  ≡ dEXP φ"
abbreviation "Int_3 φ  ≡ dNOR φ"
abbreviation "Int_4 φ  ≡ IDEM φ"
abbreviation "Int_4' φ ≡ IDEMa φ"

abbreviation "Int_5 φ  ≡ NOR φ"
definition "Int_6 φ  ≡ ∀A B. φ(A ❙↼ B) ❙≼ φ(A) ❙↼ φ(B)"
definition "Int_7 φ  ≡ ∀A B. φ(A ❙→ B) ❙≼ φ(A) ❙→ φ(B)"
definition "Int_8 φ  ≡ ∀A B. φ(φ A ❙∨ φ B) ❙≈ (φ A) ❙∨ (φ B)"
definition "Int_9 φ  ≡ ∀A B. φ A ❙≼ B ⟶ φ A ❙≼ φ B"

text‹\noindent{@{text "φ"} is an interior operator (@{text "ℑ(φ)"}) iff it satisfies conditions 1-4 (cf. @{cite Zarycki1}
and also @{cite Kuratowski2}). This characterization is shown consistent by generating a non-trivial model.}›
abbreviation "ℑ φ ≡ Int_1 φ ∧ Int_2 φ ∧ Int_3 φ ∧ Int_4 φ"
lemma "ℑ φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We verify some properties which will become useful later (also to improve provers' performance).}›
lemma PI1: "Int_1 φ = (Int_1a φ ∧ Int_1b φ)" by (metis MULT_def MULT_a_def MULT_b_def)
lemma PI4: "Int_2 φ ⟹ (Int_4 φ = Int_4' φ)" unfolding dEXP_def IDEM_def IDEMa_def by blast
lemma PI5: "Int_2 φ ⟹ Int_5 φ" unfolding dEXP_def NOR_def conn by blast
lemma PI6: "Int_1a φ ⟹ Int_2 φ ⟹ Int_6 φ" by (smt dEXP_def Int_6_def MONO_MULTa MONO_def conn)
lemma PI7: "Int_1 φ ⟹ Int_7 φ" proof -
assume int1: "Int_1 φ"
{ fix a b
have "a ❙∧ b = a ❙∧ (a ❙→ b)" unfolding conn by blast
hence "φ(a ❙∧ b) = φ(a ❙∧ (a ❙→ b))" by simp
moreover from int1 have "φ(a ❙∧ b) ❙≈ φ a ❙∧ φ b" by (simp add: MULT_def)
moreover from int1 have "φ(a ❙∧ (a ❙→ b)) ❙≈ φ a ❙∧ φ (a ❙→ b)" by (simp add: MULT_def)
ultimately have "φ a ❙∧ φ (a ❙→ b) ❙≈ φ a ❙∧ φ b" by simp
hence "φ a ❙∧ φ (a ❙→ b) ❙≈ φ a ❙∧ (φ a ❙→ φ b)" unfolding conn by blast
hence "φ(a ❙→ b) ❙≼ φ a ❙→ φ b" unfolding conn by blast
} thus ?thesis by (simp add: Int_7_def)
qed
lemma PI8: "Int_1a φ ⟹ Int_2 φ ⟹ Int_4 φ ⟹ Int_8 φ" using ADDI_b_def IDEM_def Int_8_def MONO_ADDIb MONO_MULTa dEXP_def join_def by auto
lemma PI9: "Int_1a φ ⟹ Int_4 φ ⟹ Int_9 φ" using IDEM_def Int_9_def MONO_def MONO_MULTa by simp

subsubsection ‹Closure conditions›

abbreviation "Cl_1 φ ≡ ADDI φ"
abbreviation "Cl_1a φ ≡ ADDI_a φ"
abbreviation "Cl_1b φ ≡ ADDI_b φ"
abbreviation "Cl_2 φ ≡ EXP φ"
abbreviation "Cl_3 φ  ≡ NOR φ"
abbreviation "Cl_4 φ ≡ IDEM φ"
abbreviation "Cl_4' φ ≡ IDEMb φ"

abbreviation "Cl_5 φ  ≡ dNOR φ"
definition "Cl_6 φ  ≡ ∀A B. (φ A) ❙↼ (φ B) ❙≼ φ (A ❙↼ B)"
definition "Cl_7 φ ≡ ∀A B. (φ A) ❙→ (φ B) ❙≼ φ (A ❙→ B)"
definition "Cl_8 φ  ≡ ∀A B. φ(φ A ❙∧ φ B) ❙≈ (φ A) ❙∧ (φ B)"
definition "Cl_9 φ  ≡ ∀A B.  A ❙≼ φ B ⟶ φ A ❙≼ φ B"

text‹\noindent{@{text "φ"} is a closure operator (@{text "ℭ(φ)"}) iff it satisfies conditions 1-4 (cf. @{cite Kuratowski1}
@{cite Kuratowski2}). This characterization is shown consistent by generating a non-trivial model.}›
abbreviation "ℭ φ  ≡ Cl_1 φ ∧ Cl_2 φ ∧ Cl_3  φ ∧ Cl_4 φ"
lemma "ℭ φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We verify some properties that will become useful later.}›
lemma PC4: "Cl_2 φ ⟹ (Cl_4 φ = Cl_4' φ)" unfolding EXP_def IDEM_def IDEMb_def by smt
lemma PC5: "Cl_2 φ ⟹ Cl_5 φ" unfolding EXP_def dNOR_def conn by simp
lemma PC6: "Cl_1 φ ⟹ Cl_6 φ" proof -
assume cl1: "Cl_1 φ"
{ fix a b
have "a ❙∨ b = (a ❙↼ b) ❙∨ b" unfolding conn by blast
hence "φ(a ❙∨ b) = φ((a ❙↼ b) ❙∨ b)" by simp
moreover from cl1 have "φ(a ❙∨ b) ❙≈ φ a ❙∨ φ b" by (simp add: ADDI_def)
moreover from cl1 have "φ((a ❙↼ b) ❙∨ b) ❙≈ φ (a ❙↼ b) ❙∨ (φ b)" by (simp add: ADDI_def)
ultimately have "φ a ❙∨ φ b ❙≈ φ(a ❙↼ b) ❙∨ φ b" by simp
hence "(φ a ❙↼ φ b) ❙∨ φ b ❙≈ φ(a ❙↼ b) ❙∨ φ b" unfolding conn by blast
hence "φ a ❙↼ φ b ❙≼ φ (a ❙↼ b)" unfolding conn by blast
} thus ?thesis by (simp add: Cl_6_def)
qed
lemma PC7: "Cl_1b φ ⟹ Cl_2 φ ⟹ Cl_7 φ" by (smt EXP_def Cl_7_def MONO_def PC1 MONO_ADDIb conn)
lemma PC8: "Cl_1b φ ⟹ Cl_2 φ ⟹ Cl_4 φ ⟹ Cl_8 φ" by (smt Cl_8_def EXP_def IDEM_def MONO_ADDIb MONO_MULTa MULT_a_def meet_def)
lemma PC9: "Cl_1b φ ⟹ Cl_4 φ ⟹ Cl_9 φ" by (smt IDEM_def Cl_9_def MONO_def MONO_ADDIb)

subsubsection ‹Exploring dualities›

lemma IC1_dual: "Int_1a φ = Cl_1b φ" using MONO_ADDIb MONO_MULTa by auto
lemma "Int_1b φ = Cl_1a φ" nitpick oops

lemma IC1a: "Int_1a φ ⟹ Cl_1b φ⇧d" by (smt MULT_a_def ADDI_b_def MONO_def MONO_MULTa dual_def conn)
lemma IC1b: "Int_1b φ ⟹ Cl_1a φ⇧d" unfolding MULT_b_def ADDI_a_def dual_def conn by auto
lemma IC1:  "Int_1 φ  ⟹ Cl_1 φ⇧d" unfolding MULT_def ADDI_def dual_def conn by simp
lemma IC2:  "Int_2 φ  ⟹ Cl_2 φ⇧d" unfolding dEXP_def EXP_def dual_def conn by blast
lemma IC3:  "Int_3 φ  ⟹ Cl_3 φ⇧d" unfolding dNOR_def NOR_def dual_def conn by simp
lemma IC4:  "Int_4 φ  ⟹ Cl_4 φ⇧d" unfolding IDEM_def IDEM_def dual_def conn by simp
lemma IC4': "Int_4' φ ⟹ Cl_4' φ⇧d" unfolding IDEMa_def IDEMb_def dual_def conn by metis
lemma IC5:  "Int_5 φ  ⟹ Cl_5 φ⇧d" unfolding NOR_def dNOR_def dual_def conn by simp

lemma CI1a: "Cl_1a φ  ⟹ Int_1b φ⇧d" proof -
assume cl1a: "Cl_1a φ"
{ fix A B
have "❙─φ(❙─(A ❙∧ B)) ❙≈ ❙─φ(❙─A ❙∨ ❙─B)" unfolding conn by simp
moreover from cl1a have "❙─(φ(❙─A) ❙∨ φ(❙─B)) ❙≼ ❙─φ(❙─A ❙∨ ❙─B)" using ADDI_a_def conn by metis
ultimately have "❙─(φ(❙─A)) ❙∧ ❙─(φ(❙─B)) ❙≼ ❙─φ(❙─(A ❙∧ B))" unfolding conn by simp
hence "(φ⇧d A) ❙∧ (φ⇧d B) ❙≼ (φ⇧d (A ❙∧ B))" unfolding dual_def by simp
} thus "Int_1b φ⇧d" using MULT_b_def by blast
qed
lemma CI1b: "Cl_1b φ ⟹ Int_1a φ⇧d" by (metis IC1a MONO_ADDIb MONO_MULTa)
lemma CI1:  "Cl_1 φ  ⟹ Int_1 φ⇧d" by (simp add: CI1a CI1b PC1 PI1)
lemma CI2:  "Cl_2 φ  ⟹ Int_2 φ⇧d" unfolding EXP_def dEXP_def dual_def conn by metis
lemma CI3:  "Cl_3 φ  ⟹ Int_3 φ⇧d" unfolding NOR_def dNOR_def dual_def conn by simp
lemma CI4:  "Cl_4 φ  ⟹ Int_4 φ⇧d" unfolding IDEM_def IDEM_def dual_def conn by simp
lemma CI4': "Cl_4' φ ⟹ Int_4' φ⇧d" unfolding IDEMa_def IDEMb_def dual_def conn by metis
lemma CI5:  "Cl_5 φ  ⟹ Int_5 φ⇧d" unfolding dNOR_def NOR_def dual_def conn by simp

subsection ‹Frontier and border›

subsubsection ‹Frontier conditions›

definition "Fr_1a φ ≡ ∀A B. (A ❙∧ B) ❙∧ φ(A ❙∧ B) ❙≼ (A ❙∧ B) ❙∧ (φ A ❙∨ φ B)"
definition "Fr_1b φ ≡ ∀A B. (A ❙∧ B) ❙∧ φ(A ❙∧ B) ❙≽ (A ❙∧ B) ❙∧ (φ A ❙∨ φ B)"
definition "Fr_1 φ  ≡ ∀A B. (A ❙∧ B) ❙∧ φ(A ❙∧ B) ❙≈ (A ❙∧ B) ❙∧ (φ A ❙∨ φ B)"
definition "Fr_2 φ ≡ ∀A. φ A ❙≈ φ(❙─A)"
abbreviation "Fr_3 φ ≡ NOR φ"
definition "Fr_4 φ ≡ ∀A. φ(φ A) ❙≼ (φ A)"

definition "Fr_5 φ ≡ ∀A. φ(φ(φ A)) ❙≈ φ(φ A)"
definition "Fr_6 φ ≡ ∀A B. A ❙≼ B ⟶ (φ A ❙≼ B ❙∨ φ B)"

text‹\noindent{@{text "φ"} is a topological frontier operator (@{text "𝔉(φ)"}) iff it satisfies conditions 1-4
(cf. @{cite Zarycki1}). This is also shown consistent by generating a non-trivial model.}›
abbreviation "𝔉 φ  ≡ Fr_1 φ ∧ Fr_2 φ ∧ Fr_3 φ ∧ Fr_4 φ"
lemma "𝔉 φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We now verify some useful properties of the frontier operator.}›
lemma PF1: "Fr_1 φ = (Fr_1a φ ∧ Fr_1b φ)" unfolding Fr_1_def Fr_1a_def Fr_1b_def by meson
lemma PF5: "Fr_1 φ ⟹ Fr_4 φ ⟹ Fr_5 φ" proof -
assume fr1: "Fr_1 φ" and fr4: "Fr_4 φ"
{ fix A
from fr1 have "(φ(φ A) ❙∧ (φ A)) ❙∧ φ(φ(φ A) ❙∧ (φ A)) ❙≈ (φ(φ A) ❙∧ (φ A)) ❙∧ (φ(φ(φ A)) ❙∨ φ(φ A))" by (simp add: Fr_1_def)
moreover have r1: "φ(φ A) ❙∧ (φ A) ❙≈ φ(φ A)" using meet_char Fr_4_def fr4 by simp
moreover have r2: "φ(φ(φ A)) ❙∨ φ(φ A) ❙≈ φ(φ A)" using join_char Fr_4_def fr4 by simp
ultimately have "(φ(φ A) ❙∧ (φ A)) ❙∧ φ(φ(φ A)) ❙≈ (φ(φ A) ❙∧ (φ A)) ❙∧ φ(φ A)" unfolding conn by auto
hence "φ(φ(φ A)) ❙≈ φ(φ A)" using r1 r2 conn by auto
} thus ?thesis by (simp add: Fr_5_def)
qed
lemma PF6: "Fr_1b φ ⟹ Fr_2 φ ⟹ Fr_6 φ" proof -
assume fr1b: "Fr_1b φ" and fr2: "Fr_2 φ"
{ fix A B
have "φ(❙─(A ❙∨ B)) ❙≈ φ(❙─A ❙∧ ❙─B)" unfolding conn by simp
hence aux: "φ(❙─A ❙∧ ❙─B) ❙≈ φ(A ❙∨ B)" by (metis (mono_tags) Fr_2_def fr2)
from fr1b have "(❙─A ❙∧ ❙─B) ❙∧ φ(❙─A ❙∧ ❙─B) ❙≽ (❙─A ❙∧ ❙─B) ❙∧ (φ(❙─A) ❙∨ φ(❙─B))" using Fr_1b_def by metis
hence "A ❙∨ B ❙∨ ❙─φ(❙─A ❙∧ ❙─B) ❙≼ A ❙∨ B ❙∨ (❙─(φ A) ❙∧ ❙─(φ B))" using Fr_2_def fr2 conn by auto
hence "❙─A ❙∧ ❙─B ❙∧ ❙─φ(❙─A ❙∧ ❙─B) ❙≼ ❙─A ❙∧ ❙─B ❙∧ ❙─(φ A) ❙∧ ❙─(φ B)" unfolding conn by blast
hence "A ❙∨ B ❙∨ φ(A ❙∨ B) ❙≽ A ❙∨ B ❙∨ (φ A) ❙∨ (φ B)" using aux unfolding conn by blast
hence "A ❙≼ B ⟶ B ❙∨ φ(A ❙∨ B) ❙≽ B ❙∨ (φ A) ❙∨ (φ B)" unfolding conn by auto
hence "A ❙≼ B ⟶ B ❙∨ (φ B) ❙≽ B ❙∨ (φ A) ❙∨ (φ B)" using join_char unfolding conn by simp
hence "A ❙≼ B ⟶ (φ A) ❙≼ B ❙∨ (φ B)" unfolding conn by simp
} thus "Fr_6 φ" by (simp add: Fr_6_def)
qed

subsubsection ‹Border conditions›

definition "Br_1 φ ≡ ∀A B. φ(A ❙∧ B) ❙≈ (A ❙∧ φ B) ❙∨ (B ❙∧ φ A)"
definition "Br_2 φ ≡ (φ ❙⊤) ❙≈ ❙⊥"
definition "Br_3 φ ≡ ∀A. φ(φ⇧d A) ❙≼ A"

definition "Br_4 φ ≡ ∀A B. A ❙≼ B ⟶ A ❙∧ (φ B) ❙≼ φ A"
definition "Br_5a φ ≡ ∀A. φ(φ⇧d A) ❙≼ φ A"
definition "Br_5b φ ≡ ∀A. φ A ❙≼ A"
definition "Br_5c φ ≡ ∀A. A ❙≼ φ⇧d A"
definition "Br_5d φ ≡ ∀A. φ⇧d A ❙≼ φ⇧d(φ A)"
abbreviation "Br_6 φ ≡ IDEM φ"
abbreviation "Br_7 φ ≡ ADDI_a φ"
abbreviation "Br_8 φ ≡ MULT_b φ"
definition "Br_9 φ ≡ ∀A B. φ(A ❙∧ B) ❙≼ (φ A) ❙∨ (φ B)"
definition "Br_10 φ ≡ ∀A. φ(❙─(φ A) ❙∧ φ⇧d A) ❙≈ ❙⊥"

text‹\noindent{@{text "φ"} is a topological border operator (@{text "𝔅(φ)"}) iff it satisfies conditions 1-3
(cf. @{cite Zarycki1}). This is also shown consistent.}›
abbreviation "𝔅 φ  ≡ Br_1 φ ∧ Br_2 φ ∧ Br_3 φ"
lemma "𝔅 φ" nitpick[satisfy, card w=3] oops (*model found: characterization is consistent*)

text‹\noindent{We now verify some useful properties of the border operator.}›
lemma PB4: "Br_1 φ ⟹ Br_4 φ" proof -
assume br1: "Br_1 φ"
{ fix A B
have aux: "φ(A ❙∧ B) ❙≈ (A ❙∧ φ B) ❙∨ (B ❙∧ φ A)" using br1 Br_1_def by simp
{ assume "A ❙≼ B"
hence "φ(A ❙∧ B) ❙≈ φ A" using meet_char unfolding conn by simp
hence "φ A ❙≈ (A ❙∧ φ B) ❙∨ (B ❙∧ φ A)" using aux by auto
hence "A ❙∧ φ B ❙≼ φ A" unfolding conn by auto
} hence "A ❙≼ B ⟶ A ❙∧ φ B ❙≼ φ A" by (rule impI)
} thus "Br_4 φ"  by (simp add: Br_4_def)
qed
lemma PB5b: "Br_1 φ ⟹ Br_5b φ" proof -
assume br1: "Br_1 φ"
{ fix A
from br1 have aux: "φ(A ❙∧ A) ❙≈ (A ❙∧ φ A) ❙∨ (A ❙∧ φ A)" unfolding Br_1_def by blast
hence "φ A ❙≈ (A ❙∧ φ A)" unfolding conn by metis
hence "φ A ❙≼ A" unfolding conn by blast
} thus "Br_5b φ" using Br_5b_def by blast
qed
lemma PB5c: "Br_1 φ ⟹ Br_5c φ" using Br_5b_def Br_5c_def PB5b dual_def unfolding conn by force
lemma PB5a: "Br_1 φ ⟹ Br_3 φ ⟹ Br_5a φ" proof -
assume br1: "Br_1 φ" and br3: "Br_3 φ"
hence br5c: "Br_5c φ" using PB5c by simp
{ fix A
have "A ❙∧ φ(φ⇧d A) ❙≼ φ A" by (metis br5c Br_4_def Br_5c_def PB4 br1)
hence "φ(φ⇧d A) ❙≼ φ A" using Br_3_def br3 unfolding conn by metis
} thus "Br_5a φ" using Br_5a_def by simp
qed
lemma PB5d: "Br_1 φ ⟹ Br_3 φ ⟹ Br_5d φ" proof -
assume br1: "Br_1 φ" and br3: "Br_3 φ"
hence br5a: "Br_5a φ" using PB5a by simp
{ fix A
from br5a have "φ(φ⇧d(❙─A)) ❙≼ φ(❙─A)" unfolding Br_5a_def by simp
hence "❙─φ(❙─A) ❙≼ ❙─φ(φ⇧d(❙─A))" unfolding conn by blast
hence "φ⇧d A ❙≼ φ⇧d(φ A)" unfolding dual_def conn by simp
} thus "Br_5d φ" using Br_5d_def by simp
qed
lemma PB6: "Br_1 φ ⟹ Br_6 φ" by (smt Br_4_def Br_5b_def IDEM_def PB4 PB5b conn)
lemma PB7: "Br_1 φ ⟹ Br_7 φ" using Br_4_def Br_5b_def ADDI_a_def PB4 PB5b unfolding conn by smt
lemma PB8: "Br_1 φ ⟹ Br_8 φ" using Br_1_def Br_5b_def MULT_b_def PB5b unfolding conn by metis
lemma PB9: "Br_1 φ ⟹ Br_9 φ" unfolding Br_1_def Br_9_def conn by simp
lemma PB10: "Br_1 φ ⟹ Br_3 φ ⟹ Br_10 φ" proof - ―‹ proof automagically generated ›
assume a1: "Br_3 φ"
assume a2: "Br_1 φ"
{ fix bb :: "w ⇒ bool" and ww :: w
have "∀p pa w pb. ((pb p w ∨ pb pa w) ∨ ¬pb (pa ❙∧ p) w) ∨ ¬Br_9 pb"
by (metis Br_9_def join_def) (* 20 ms *)
then have "(φ (((φ⇧c) ❙⊓ (φ⇧d)) bb) ww) ∧ (❙⊥ ww) ∨ ¬(φ (((φ⇧c) ❙⊓ (φ⇧d)) bb) ww) ∧ ¬(❙⊥ ww)"
using a2 a1 by (metis (no_types) Br_5a_def Br_5b_def Br_5d_def PB5a PB5b PB5d PB9 bottom_def compl_def dual_def meet_def) (* 86 ms *)
} then show ?thesis unfolding Br_10_def by blast (* 1 ms *)
qed

subsubsection ‹Relation with closure and interior›

text‹\noindent{We define and verify some conversion operators useful to derive border and frontier operators from
closure/interior operators and also between each other.}›

text‹\noindent{Frontier operator as derived from interior.}›
definition Fr_int::"(σ⇒σ)⇒(σ⇒σ)" ("ℱ⇩I") where "ℱ⇩I ℐ ≡ λA. ❙─(ℐ A) ❙∧ ℐ⇧d A"
lemma FI1: "Int_1 φ ⟹ Int_2 φ ⟹  Fr_1(ℱ⇩I φ)" using EXP_def Fr_1_def Fr_int_def IC2 MULT_def conn by auto
lemma FI2: "Fr_2(ℱ⇩I φ)" using Fr_2_def Fr_int_def dual_def dual_symm unfolding conn by smt
lemma FI3: "Int_3 φ ⟹ Fr_3(ℱ⇩I φ)" using NOR_def Fr_int_def IC3 unfolding conn by auto
lemma FI4: "Int_1a φ ⟹ Int_2 φ  ⟹ Int_4 φ ⟹ Fr_4(ℱ⇩I φ)" unfolding Fr_int_def Fr_4_def dual_def conn by (smt Int_9_def MONO_MULTa PI9)

text‹\noindent{Frontier operator as derived from closure.}›
definition Fr_cl::"(σ⇒σ)⇒(σ⇒σ)" ("ℱ⇩C") where "ℱ⇩C 𝒞 ≡ λA. (𝒞 A) ❙∧ 𝒞(❙─A)"
lemma FC1: "Cl_1 φ ⟹ Cl_2 φ ⟹  Fr_1(ℱ⇩C φ)" using CI1 EXP_def Fr_1_def Fr_cl_def MULT_def dual_def unfolding conn by smt
lemma FC2: "Fr_2(ℱ⇩C φ)" using Fr_2_def Fr_cl_def dual_def dual_symm unfolding conn by smt
lemma FC3: "Cl_3 φ ⟹ Fr_3(ℱ⇩C φ)" unfolding NOR_def Fr_cl_def conn by simp
lemma FC4: "Cl_1b φ ⟹ Cl_2 φ ⟹ Cl_4 φ ⟹ Fr_4(ℱ⇩C φ)" using Cl_8_def MONO_ADDIb PC8 unfolding Fr_cl_def Fr_4_def conn by blast

text‹\noindent{Frontier operator as derived from border.}›
definition Fr_br::"(σ⇒σ)⇒(σ⇒σ)" ("ℱ⇩B") where "ℱ⇩B ℬ ≡ λA. ℬ A ❙∨ ℬ(❙─A)"
lemma FB1: "Br_1 φ ⟹  Fr_1(ℱ⇩B φ)" unfolding Fr_br_def Fr_1_def using Br_1_def Br_5b_def PB5b conn by smt
lemma FB2: "Fr_2(ℱ⇩B φ)" unfolding Fr_br_def Fr_2_def conn by auto
lemma FB3: "Br_1 φ ⟹ Br_2 φ ⟹  Fr_3(ℱ⇩B φ)" using Br_2_def Br_5b_def PB5b unfolding Fr_br_def NOR_def conn by force
lemma FB4: "Br_1 φ ⟹ Br_3 φ ⟹  Fr_4(ℱ⇩B φ)" proof -
assume br1: "Br_1 φ" and br3: "Br_3 φ"
{ fix A
have "(ℱ⇩B φ) ((ℱ⇩B φ) A) = φ(φ A ❙∨ φ(❙─A)) ❙∨ φ(❙─(φ A ❙∨ φ(❙─A)))" by (simp add: Fr_br_def conn)
also have "... = φ(φ A ❙∨ φ(❙─A)) ❙∨ φ(❙─(φ A) ❙∧ φ⇧d A)" by (simp add: dual_def conn)
also from br1 br3 have "... = φ(φ A ❙∨ φ(❙─A)) ❙∨ ❙⊥" using Br_10_def PB10 by metis
finally have "(ℱ⇩B φ) ((ℱ⇩B φ) A) ❙≈ φ(φ A ❙∨ φ(❙─A))" unfolding conn by simp
hence "(ℱ⇩B φ) ((ℱ⇩B φ) A) ❙≼ (ℱ⇩B φ) A" using Br_5b_def Fr_br_def PB5b br1 by fastforce
} thus "Fr_4(ℱ⇩B φ)" using Fr_4_def by blast
qed

text‹\noindent{Border operator as derived from interior.}›
definition Br_int::"(σ⇒σ)⇒(σ⇒σ)" ("ℬ⇩I") where "ℬ⇩I ℐ ≡ λA. A ❙↼ (ℐ A)"
lemma BI1: "Int_1 φ ⟹  Br_1 (ℬ⇩I φ)" using Br_1_def Br_int_def MULT_def conn by auto
lemma BI2: "Int_3 φ ⟹  Br_2 (ℬ⇩I φ)" by (simp add: Br_2_def Br_int_def dNOR_def conn)
lemma BI3: "Int_1a φ ⟹ Int_4 φ ⟹ Br_3 (ℬ⇩I φ)" unfolding Br_int_def Br_3_def dual_def by (smt Int_9_def MONO_MULTa PI9 conn)

text‹\noindent{Border operator as derived from closure.}›
definition Br_cl::"(σ⇒σ)⇒(σ⇒σ)" ("ℬ⇩C")  where "ℬ⇩C 𝒞 ≡ λA. A ❙∧ 𝒞(❙─A)"
lemma BC1: "Cl_1 φ ⟹  Br_1(ℬ⇩C φ)" using Br_1_def Br_cl_def CI1 MULT_def dual_def unfolding conn by smt
lemma BC2: "Cl_3 φ ⟹  Br_2(ℬ⇩C φ)" using Br_2_def Br_cl_def CI3 dNOR_def dual_def unfolding conn by auto
lemma BC3: "Cl_1b φ ⟹ Cl_4 φ ⟹ Br_3 (ℬ⇩C φ)" unfolding Br_cl_def Br_3_def dual_def conn by (metis (mono_tags, lifting) Cl_9_def PC9)

text‹\noindent{Note that the previous two conversion functions are related:}›
lemma BI_BC_rel: "(ℬ⇩I φ) = ℬ⇩C(φ⇧d)" by (simp add: Br_cl_def Br_int_def dual_def conn)

text‹\noindent{Border operator as derived from frontier.}›
definition Br_fr::"(σ⇒σ)⇒(σ⇒σ)" ("ℬ⇩F") where "ℬ⇩F ℱ ≡ λA. A ❙∧ (ℱ A)"
lemma BF1: "Fr_1 φ ⟹ Br_1(ℬ⇩F φ)" using Br_1_def Br_fr_def Fr_1_def conn by auto
lemma BF2: "Fr_2 φ ⟹ Fr_3 φ ⟹ Br_2(ℬ⇩F φ)" using Br_2_def Br_fr_def Fr_2_def NOR_def unfolding conn by fastforce
lemma BF3: "Fr_1b φ ⟹ Fr_2 φ ⟹ Fr_4 φ ⟹ Br_3(ℬ⇩F φ)" proof -
assume fr1b: "Fr_1b φ" and fr2: "Fr_2 φ" and fr4: "Fr_4 φ"
{ fix A
from fr1b fr2 have "let M= ❙─A ❙∧ φ A ; N= φ A in M ❙≼ N ⟶ (φ M ❙≼ N ❙∨ φ N)" using PF1 PF6 by (simp add: Fr_6_def)
hence "φ(❙─A ❙∧ φ A) ❙≼ φ A ❙∨ φ(φ A)" unfolding conn by meson
hence "φ(❙─A ❙∧ φ A) ❙≼ φ A" using Fr_4_def fr4 unfolding conn by metis
hence aux: "φ(❙─A ❙∧ φ A) ❙∧ ❙─(φ A) ❙≈ ❙⊥" unfolding conn by blast
have "(ℬ⇩F φ)((ℬ⇩F φ)⇧d A) = ❙─(❙─A ❙∧ φ(❙─A)) ❙∧ φ(❙─(❙─A ❙∧ φ(❙─A)))" unfolding Br_fr_def dual_def by simp
also have "... = (A ❙∨ ❙─φ A) ❙∧ φ(❙─A ❙∧ φ A)" using Fr_2_def fr2 unfolding conn by force
also have "... = (A ❙∧ φ(❙─A ❙∧ φ A)) ❙∨ (❙─φ A ❙∧ φ(❙─A ❙∧ φ A))" unfolding conn by auto
also have "... = (A ❙∧ φ(❙─A ❙∧ φ A))" using aux unfolding conn by blast
finally have "(ℬ⇩F φ)((ℬ⇩F φ)⇧d A) = A ❙∧ φ(❙─A ❙∧ φ A)" unfolding Br_fr_def dual_def conn by simp
} thus "Br_3(ℬ⇩F φ)" unfolding Br_3_def Br_fr_def conn by meson
qed

text‹\noindent{Interior operator as derived from border.}›
definition Int_br::"(σ⇒σ)⇒(σ⇒σ)" ("ℐ⇩B") where "ℐ⇩B ℬ ≡ λA. A ❙↼ (ℬ A)"
lemma IB1: "Br_1 φ ⟹ Int_1(ℐ⇩B φ)" using Br_1_def MULT_def Int_br_def conn by auto
lemma IB2: "Int_2(ℐ⇩B φ)" by (simp add: dEXP_def Int_br_def conn)
lemma IB3: "Br_2 φ ⟹ Int_3(ℐ⇩B φ)" by (simp add: Br_2_def dNOR_def Int_br_def conn)
lemma IB4: "Br_1 φ ⟹ Br_3 φ ⟹ Int_4(ℐ⇩B φ)" unfolding Int_br_def IDEM_def conn
using Br_1_def Br_5c_def Br_5d_def PB5c PB5d dual_def unfolding conn by (metis (full_types))

text‹\noindent{Interior operator as derived from frontier.}›
definition Int_fr::"(σ⇒σ)⇒(σ⇒σ)" ("ℐ⇩F") where "ℐ⇩F ℱ ≡ λA. A ❙↼ (ℱ A)"
lemma IF1a: "Fr_1b φ ⟹ Int_1a(ℐ⇩F φ)" using Fr_1b_def MULT_a_def Int_fr_def conn by auto
lemma IF1b: "Fr_1a φ ⟹ Int_1b(ℐ⇩F φ)" using Fr_1a_def MULT_b_def Int_fr_def conn by auto
lemma IF1: "Fr_1 φ ⟹ Int_1(ℐ⇩F φ)" by (simp add: IF1a IF1b PF1 PI1)
lemma IF2: "Int_2(ℐ⇩F φ)" by (simp add: dEXP_def Int_fr_def conn)
lemma IF3: "Fr_2 φ ⟹ Fr_3 φ ⟹ Int_3(ℐ⇩F φ)" using BF2 Br_2_def Br_fr_def dNOR_def Int_fr_def unfolding conn by auto
lemma IF4: "Fr_1a φ ⟹ Fr_2 φ ⟹ Fr_4 φ ⟹ Int_4(ℐ⇩F φ)"
using Fr_1a_def Fr_2_def Fr_4_def unfolding Int_fr_def IDEM_def conn by metis

text‹\noindent{Closure operator as derived from border.}›
definition Cl_br::"(σ⇒σ)⇒(σ⇒σ)" ("𝒞⇩B") where "𝒞⇩B ℬ ≡ λA. A ❙∨ ℬ(❙─A)"
lemma CB1: "Br_1 φ ⟹ Cl_1(𝒞⇩B φ)" proof -
assume br1: "Br_1 φ"
{ fix A B
have "(𝒞⇩B φ) (A ❙∨ B) = A ❙∨ B ❙∨ φ(❙─(A ❙∨ B))" by (simp add: Cl_br_def conn)
also have "... = A ❙∨ B ❙∨ φ(❙─A ❙∧ ❙─B)" unfolding conn by simp
also have "... = A ❙∨ B ❙∨ (❙─A ❙∧ φ(❙─B)) ❙∨ (❙─B ❙∧ φ(❙─A))" using Br_1_def br1 unfolding conn by auto
also have "... = A ❙∨ φ(❙─A) ❙∨ B ❙∨ φ(❙─B)" unfolding conn by auto
also have "... = (𝒞⇩B φ) A ❙∨ (𝒞⇩B φ) B" by (simp add: Cl_br_def conn)
finally have "(𝒞⇩B φ)(A ❙∨ B) = (𝒞⇩B φ) A ❙∨ (𝒞⇩B φ) B" unfolding Cl_br_def by blast
} thus "Cl_1(𝒞⇩B φ)" unfolding ADDI_def Cl_br_def by simp
qed
lemma CB2: "Cl_2(𝒞⇩B φ)" by (simp add: EXP_def Cl_br_def conn)
lemma CB3: "Br_2 φ ⟹ Cl_3(𝒞⇩B φ)" using Br_2_def Cl_br_def IC3 dNOR_def dual_def dual_symm unfolding conn by smt
lemma CB4: "Br_1 φ ⟹ Br_3 φ ⟹ Cl_4(𝒞⇩B φ)" proof -
assume br1: "Br_1 φ" and br3: "Br_3 φ"
{ fix A
have "(𝒞⇩B φ) ((𝒞⇩B φ) A) = A ❙∨ φ(❙─A) ❙∨ φ(❙─(A ❙∨ φ(❙─A)))" by (simp add: Cl_br_def conn)
also have "... = A ❙∨ φ(❙─A) ❙∨ φ(❙─A ❙∧ φ⇧d A)" unfolding dual_def conn by simp
also have "... = A ❙∨ φ(❙─A) ❙∨ (❙─A ❙∧ φ(φ⇧d A)) ❙∨ (❙─A ❙∧ φ(❙─A))" unfolding dual_def using Br_1_def br1 conn by auto
also have "... = A ❙∨ φ(❙─A)" using Br_3_def br3 unfolding conn by metis
finally have "(𝒞⇩B φ) ((𝒞⇩B φ) A) = (𝒞⇩B φ) A" unfolding Cl_br_def by blast
} thus "Cl_4(𝒞⇩B φ)" unfolding IDEM_def Cl_br_def by simp
qed

text‹\noindent{Closure operator as derived from frontier.}›
definition Cl_fr::"(σ⇒σ)⇒(σ⇒σ)" ("𝒞⇩F") where "𝒞⇩F ℱ ≡ λA. A ❙∨ (ℱ A)"
lemma CF1b: "Fr_1b φ ⟹ Fr_2 φ ⟹ Cl_1b(𝒞⇩F φ)" using Cl_fr_def Fr_6_def MONO_def MONO_ADDIb PF6 unfolding conn by auto
lemma CF1a: "Fr_1a φ ⟹ Fr_2 φ ⟹ Cl_1a(𝒞⇩F φ)" proof -
have aux: "Fr_2 φ ⟹ (ℐ⇩F φ)⇧d = (𝒞⇩F φ)" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def conn)
hence "Fr_1a φ ⟹ Fr_2 φ ⟹ Cl_1a(ℐ⇩F φ)⇧d" using IC1b IF1b by blast
thus "Fr_1a φ ⟹ Fr_2 φ ⟹ Cl_1a(𝒞⇩F φ)" using ADDI_a_def aux unfolding conn by simp
qed
lemma CF1: "Fr_1 φ ⟹ Fr_2 φ ⟹ Cl_1(𝒞⇩F φ)" by (simp add: CF1a CF1b PC1 PF1)
lemma CF2: "Cl_2(𝒞⇩F φ)" by (simp add: EXP_def Cl_fr_def conn)
lemma CF3: "Fr_3 φ ⟹ Cl_3(𝒞⇩F φ)" by (simp add: Cl_fr_def NOR_def conn)
lemma CF4: "Fr_1a φ ⟹ Fr_2 φ ⟹ Fr_4 φ ⟹ Cl_4(𝒞⇩F φ)" proof -
have aux: "Fr_2 φ ⟹ (ℐ⇩F φ)⇧d = (𝒞⇩F φ)"  by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def conn)
hence "Fr_1a φ ⟹ Fr_2 φ ⟹ Fr_4 φ ⟹ Cl_4(ℐ⇩F φ)⇧d" using IC4 IF4 by blast
thus "Fr_1a φ ⟹ Fr_2 φ ⟹ Fr_4 φ ⟹ Cl_4(𝒞⇩F φ)" by (simp add: aux)
qed

subsubsection ‹Infinitary conditions›

text‹\noindent{We define the essential infinitary conditions for the closure and interior operators (entailing infinite
additivity and multiplicativity resp.). Observe that the other direction is implied by monotonicity (MONO).}›
abbreviation "Int_inf φ ≡ iMULT_b(φ)"

text‹\noindent{There exists indeed a condition on frontier operators responsible for the infinitary conditions above:}›
definition "Fr_inf φ ≡ ∀S. ❙⋀S ❙∧ φ(❙⋀S) ❙≼ ❙⋀S ❙∧ ❙⋁Ra[φ|S]"

lemma CF_inf: "Fr_2 φ ⟹ Fr_inf φ ⟹ Cl_inf(𝒞⇩F φ)" unfolding iADDI_a_def  Fr_inf_def
by (smt Cl_fr_def Fr_2_def Ra_restr_ex compl_def dom_compl_def2 iDM_b join_def meet_def supremum_def)
lemma IF_inf: "Fr_inf φ ⟹ Int_inf(ℐ⇩F φ)" unfolding Fr_inf_def iMULT_b_def Int_fr_def Ra_restr_all
by (metis (mono_tags, hide_lams) diff_def infimum_def meet_def pfunRange_restr_def supremum_def)

text‹\noindent{This condition is indeed strong enough to entail closure of the fixed-point predicates under infimum/supremum.}›
lemma fp_IF_inf_closed: "Fr_inf φ ⟹ infimum_closed (fp (ℐ⇩F φ))" by (metis (full_types) IF2 IF_inf Ra_restr_all dEXP_def iMULT_b_def infimum_def)
lemma fp_CF_sup_closed: "Fr_inf φ ⟹ Fr_2 φ ⟹ supremum_closed (fp (𝒞⇩F φ))" by (metis (full_types) CF2 CF_inf EXP_def Ra_restr_ex iADDI_a_def supremum_def)

end


# Theory topo_operators_derivative

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

subsection ‹Derivative and coherence›

text‹\noindent{In this section we investigate two related operators, namely the derivative' (or derived set')
and the (Cantorian) coherence' of a set. The derivative of a set is the set of its accumulation (aka. limit)
points. The coherence of a set A is the set formed by those limit points of A belonging to A.
For the derivative operator we draw upon the works by Kuratowski @{cite Kuratowski1} and
(in more detail) by Zarycki @{cite Zarycki3}; cf.~also McKinsey \& Tarski @{cite AOT}.
For the (Cantorian) coherence operator we follow the treatment given by Zarycki in @{cite Zarycki2}.}›

subsubsection ‹Derivative conditions›

text‹\noindent{The derivative conditions overlap partly with Kuratowski closure conditions @{cite Kuratowski1}.
We try to make both notations coincide when possible.}›

abbreviation "Der_1 φ  ≡ Cl_1 φ"
abbreviation "Der_1a φ ≡ Cl_1a φ"
abbreviation "Der_1b φ ≡ Cl_1b φ"
abbreviation "Der_2 φ  ≡ Cl_5 φ" ―‹ follows from Cl-2 ›
abbreviation "Der_3 φ  ≡ Cl_3 φ"
abbreviation "Der_4 φ  ≡ Cl_4' φ"
definition   "Der_4e φ ≡ ∀A. φ(φ A) ❙≼ (φ A ❙∨ A)"
definition   "Der_5 φ ≡ ∀A. (φ A ❙≼ A) ∧ (A ❙≼ φ⇧d A) ⟶ (A ❙≈ ❙⊥ ∨ A ❙≈ ❙⊤)"

text‹\noindent{Some remarks:
Condition Der-2 basically says (when assuming other derivative axioms) that the space is dense-in-itself,
i.e. that all points are accumulation points (no point is isolated) w.r.t the whole space.
Der-4 is a weakened (left-to-right) variant of Cl-4.
Condition Der-4e corresponds to a (weaker) condition than Der-4 and is used in more recent literature
(in particular in the works of Leo Esakia @{cite Esakia}).
When other derivative axioms are assumed, Der-5 above as used by Zarycki @{cite Zarycki3} says that
the only clopen sets in the space are the top and bottom elements (empty set and universe, resp.).
We verify some properties:}›

lemma Der4e_rel: "Der_4 φ ⟹ Der_4e φ" by (simp add: IDEMb_def Der_4e_def conn)
lemma PD1: "Der_1b φ ⟹ ∀A B. A ❙≼ B ⟶ φ A ❙≼ φ B" using MONO_def MONO_ADDIb by auto
lemma PD2: "Der_1b φ ⟹ ∀A B. A ❙≼ B ⟶ φ⇧d A ❙≼ φ⇧d B" using CI1b MONO_def MONO_MULTa dual_def by fastforce
lemma PD3: "Der_1b φ ⟹ ∀A B. φ(A ❙∧ B) ❙≼ φ A ❙∧ φ B" unfolding conn by (metis (no_types, lifting) PD1)
lemma PD4: "Der_1 φ ⟹ ∀A B. (φ A ❙↼ φ B) ❙≼ φ(A ❙↼ B)" using Cl_6_def PC6 by metis
lemma PD5: "Der_4 φ ⟹ ∀A. φ(φ(❙─(φ A))) ❙≼ φ(❙─(φ A))" unfolding IDEMb_def by blast
text‹\noindent{Observe that the lemmas below require Der-2 as premise:}›
lemma PD6: "Der_1 φ ⟹ Der_2 φ ⟹ ∀A. φ⇧d A ❙≼ φ A" unfolding ADDI_def dNOR_def dual_def conn by fastforce
lemma PD7: "Der_1 φ ⟹ Der_2 φ ⟹ ∀A. φ(φ⇧d A) ❙≼ φ(φ A)" by (metis (mono_tags, lifting) PC1 PD1 PD6)
lemma PD8: "Der_1 φ ⟹ Der_2 φ ⟹ Der_4 φ ⟹ ∀A. φ(φ⇧d A) ❙≼ φ A" by (meson IDEMb_def PD7)
lemma PD9: "Der_1 φ ⟹ Der_2 φ ⟹ Der_4 φ ⟹ ∀A. φ⇧d A ❙≼ φ⇧d(φ A)" by (metis CI4' IDEMa_def PC1 PD2 PD6)
lemma PD10: "Der_1 φ ⟹ Der_2 φ ⟹ Der_4 φ ⟹ ∀A. φ⇧d A ❙≼ φ(φ⇧d A)" using CI4' IDEMa_def PD6 by metis
lemma PD11: "Der_1 φ ⟹ Der_2 φ ⟹ Der_4 φ ⟹ ∀A. ❙─(φ A) ❙≼ φ(❙─(φ A))" using IDEMb_def PD6 dual_def unfolding conn by metis
lemma PD12: "Der_1 φ ⟹ Der_2 φ ⟹ Der_4 φ ⟹ ∀A. (φ⇧d A) ❙∧ (φ A) ❙≈ φ⇧d(A ❙∧ (φ A))" proof -
assume der1: "Der_1 φ" and der2: "Der_2 φ" and der4: "Der_4 φ"
{ fix A
from der1 have "let M=❙─A ; N=❙─(φ A) in φ(M ❙∨ N) ❙≈ (φ M) ❙∨ (φ N)" unfolding ADDI_def by simp
hence aux: "❙─(φ(❙─A) ❙∨ φ(❙─(φ A))) ❙≈ ❙─(φ (❙─A ❙∨ ❙─(φ A)))" unfolding dual_def conn by simp
have "(φ⇧d A ❙∧ φ A) = (φ⇧d A ❙∧ φ⇧d(φ A))" using PD6 PD9 der1 der2 der4 unfolding conn by metis
also have "... = ❙─(φ(❙─A) ❙∨ φ(❙─(φ A)))" unfolding dual_def conn by simp
also from aux have "... = ❙─(φ (❙─A ❙∨ ❙─(φ A)))" unfolding dual_def by blast
also have "... = φ⇧d(A ❙∧ (φ A))" unfolding dual_def conn by simp
finally have "(φ⇧d A) ❙∧ (φ A) ❙≈ φ⇧d(A ❙∧ (φ A))" by simp
} thus ?thesis by simp
qed

text‹\noindent{The conditions below can serve to axiomatize a derivative operator. Different authors consider different
sets of conditions. We define below some corresponding to Zarycki @{cite Zarycki3}, Kuratowski @{cite Kuratowski1}
@{cite Zarycki2}, McKinsey \& Tarski @{cite AOT}, and Esakia @{cite Esakia}, respectively.}›
abbreviation "𝔇z φ  ≡ Der_1 φ ∧ Der_2 φ ∧ Der_3 φ ∧ Der_4 φ ∧ Der_5 φ"
abbreviation "𝔇k φ  ≡ Der_1 φ ∧ Der_2 φ ∧ Der_3 φ ∧ Der_4 φ"
abbreviation "𝔇mt φ ≡ Der_1 φ           ∧ Der_3 φ ∧ Der_4 φ"
abbreviation "𝔇e φ  ≡ Der_1 φ           ∧ Der_3 φ ∧ Der_4e φ"

text‹\noindent{Our default' derivative operator will coincide with @{text "𝔇k"} from Kuratowski (also Zarycki).
However, for proving theorems we will employ the weaker variant Der-4e instead of Der-4 whenever possible.
We start by defining a dual operator and verifying some dualities; we then define conversion operators.
Observe that conditions Der-2 and  Der-5 are not used in the rest of this subsection.
Der-2 will be required later when working with the coherence operator.}›
abbreviation "𝔇 φ ≡ 𝔇k φ"
abbreviation "Σ φ ≡ Int_1 φ ∧ Int_3 φ ∧ Int_4' φ ∧ Int_5 φ" ―‹ 'dual-derivative' operator ›

lemma SD_dual1: "Σ(φ) ⟹ 𝔇(φ⇧d)" using IC1 IC4' IC3 IC5 by simp
lemma SD_dual2: "Σ(φ⇧d) ⟹ 𝔇(φ)" using IC1 IC4' IC3 IC5 dual_symm by metis
lemma DS_dual1: "𝔇(φ) ⟹ Σ(φ⇧d)" using CI1 CI4' CI3 CI5 by simp
lemma DS_dual2: "𝔇(φ⇧d) ⟹ Σ(φ)" using CI1 CI4' CI3 CI5 dual_symm by metis
lemma DS_dual: "𝔇(φ) = Σ(φ⇧d)"  using SD_dual2 DS_dual1 by smt

text‹\noindent{Closure operator as derived from derivative.}›
definition Cl_der::"(σ⇒σ)⇒(σ⇒σ)" ("𝒞⇩D") where  "𝒞⇩D 𝒟 ≡ λA. A ❙∨ 𝒟(A)"
text‹\noindent{Verify properties:}›
lemma CD1a: "Der_1a 𝒟 ⟹ Cl_1a (𝒞⇩D 𝒟)" unfolding Cl_der_def ADDI_a_def conn by auto
lemma CD1b: "Der_1b 𝒟 ⟹ Cl_1b (𝒞⇩D 𝒟)" unfolding Cl_der_def ADDI_b_def conn by auto
lemma CD1 : "Der_1 𝒟 ⟹ Cl_1 (𝒞⇩D 𝒟)" unfolding Cl_der_def ADDI_def conn by blast
lemma CD2: "Cl_2 (𝒞⇩D 𝒟)" unfolding Cl_der_def EXP_def conn by simp
lemma CD3: "Der_3 𝒟 ⟹ Der_3 (𝒞⇩D 𝒟)" unfolding Cl_der_def NOR_def conn by simp
lemma CD4a: "Der_1a 𝒟 ⟹ Der_4e 𝒟 ⟹ Cl_4 (𝒞⇩D 𝒟)" unfolding Cl_der_def by (smt ADDI_a_def Der_4e_def IDEM_def join_def)
lemma "Der_1b 𝒟 ⟹ Der_4 𝒟 ⟹ Cl_4 (𝒞⇩D 𝒟)" nitpick oops (*countermodel*)
lemma CD4: "Der_1 𝒟 ⟹ Der_4e 𝒟 ⟹ Cl_4 (𝒞⇩D 𝒟)" unfolding Cl_der_def by (metis (no_types, lifting) CD4a Cl_der_def IDEM_def PC1)

text‹\noindent{Interior operator as derived from (dual) derivative.}›
definition Int_der::"(σ⇒σ)⇒(σ⇒σ)" ("ℐ⇩D") where "ℐ⇩D 𝒟 ≡ λA. A ❙∧ 𝒟⇧d(A)"
text‹\noindent{Verify definition:}›
lemma Int_der_def2: "ℐ⇩D 𝒟 = (λφ. φ ❙↼ 𝒟(❙─φ))" unfolding Int_der_def dual_def conn by simp
lemma dual_der1: "𝒞⇩D 𝒟 ≡ (ℐ⇩D 𝒟)⇧d" unfolding Cl_der_def Int_der_def dual_def conn by simp
lemma dual_der2: "ℐ⇩D 𝒟 ≡ (𝒞⇩D 𝒟)⇧d" unfolding Cl_der_def Int_der_def dual_def conn by simp
text‹\noindent{Verify properties:}›
lemma ID1: "Der_1 𝒟 ⟹ Int_1 (ℐ⇩D 𝒟)" using Int_der_def MULT_def ADDI_def CI1 unfolding conn by auto
lemma ID1a: "Der_1a 𝒟 ⟹ Int_1b (ℐ⇩D 𝒟)" by (simp add: CI1a dual_der2 CD1a)
lemma ID1b: "Der_1b 𝒟 ⟹ Int_1a (ℐ⇩D 𝒟)" by (simp add: CI1b dual_der2 CD1b)
lemma ID2: "Int_2 (ℐ⇩D 𝒟)" unfolding Int_der_def dEXP_def conn by simp
lemma ID3: "Der_3 𝒟 ⟹ Int_3 (ℐ⇩D 𝒟)" by (simp add: CI3 CD3 dual_der2)
lemma ID4: "Der_1 𝒟 ⟹ Der_4e 𝒟 ⟹ Int_4 (ℐ⇩D 𝒟)" using CI4 CD4 dual_der2 by simp
lemma ID4a: "Der_1a 𝒟 ⟹ Der_4e 𝒟 ⟹ Int_4 (ℐ⇩D 𝒟)" by (simp add: CI4 dual_der2 CD4a)
lemma "Der_1b 𝒟 ⟹ Der_4 𝒟 ⟹ Int_4 (ℐ⇩D 𝒟)" nitpick oops (*countermodel*)

text‹\noindent{Border operator as derived from (dual) derivative.}›
definition Br_der::"(σ⇒σ)⇒(σ⇒σ)" ("ℬ⇩D") where "ℬ⇩D 𝒟 ≡ λA. A ❙↼ 𝒟⇧d(A)"
text‹\noindent{Verify definition:}›
lemma Br_der_def2: "ℬ⇩D 𝒟 = (λA. A ❙∧ 𝒟(❙─A))" unfolding Br_der_def dual_def conn by simp
text‹\noindent{Verify properties:}›
lemma BD1: "Der_1 𝒟 ⟹ Br_1 (ℬ⇩D 𝒟)" using Br_der_def Br_1_def CI1 MULT_def conn by auto
lemma BD2: "Der_3 𝒟 ⟹ Br_2 (ℬ⇩D 𝒟)" using Br_der_def Br_2_def CI3 dNOR_def unfolding conn by auto
lemma BD3: "Der_1b 𝒟 ⟹ Der_4e 𝒟 ⟹ Br_3 (ℬ⇩D 𝒟)" using dual_def Der_4e_def MONO_ADDIb MONO_def  unfolding Br_der_def Br_3_def conn by smt

text‹\noindent{Frontier operator as derived from derivative.}›
definition Fr_der::"(σ⇒σ)⇒(σ⇒σ)" ("ℱ⇩D") where "ℱ⇩D 𝒟 ≡ λA. (A ❙↼ 𝒟⇧d(A)) ❙∨ (𝒟(A) ❙↼ A)"
text‹\noindent{Verify definition:}›
lemma Fr_der_def2: "ℱ⇩D 𝒟 = (λA. (A ❙∨ 𝒟(A)) ❙∧ (❙─A ❙∨ 𝒟(❙─A)))" unfolding Fr_der_def dual_def conn by auto
text‹\noindent{Verify properties:}›
lemma FD1a: "Der_1a 𝒟 ⟹ Fr_1a(ℱ⇩D 𝒟)" unfolding Fr_1a_def Fr_der_def using CI1a MULT_b_def conn by auto
lemma FD1b: "Der_1b 𝒟 ⟹ Fr_1b(ℱ⇩D 𝒟)" unfolding Fr_1b_def Fr_der_def using CI1b MULT_a_def conn by smt
lemma FD1: "Der_1 𝒟 ⟹ Fr_1(ℱ⇩D 𝒟)" unfolding Fr_1_def Fr_der_def using CI1 MULT_def conn by auto
lemma FD2: "Fr_2(ℱ⇩D 𝒟)" using dual_def dual_symm unfolding Fr_2_def Fr_der_def conn by metis
lemma FD3: "Der_3 𝒟 ⟹ Fr_3(ℱ⇩D 𝒟)" by (simp add: NOR_def Fr_der_def conn)
lemma FD4: "Der_1 𝒟 ⟹ Der_4e 𝒟 ⟹ Fr_4(ℱ⇩D 𝒟)" by (metis CD1b CD2 CD4 Cl_8_def Cl_der_def Fr_4_def Fr_der_def2 PC1 PC8 meet_def)

text‹\noindent{Note that the derivative operation cannot be obtained from interior, closure, border, nor frontier.
In this respect the derivative is a fundamental operation.}›

subsubsection ‹Infinitary conditions›

text‹\noindent{The corresponding infinitary condition on derivative operators is inherited from the one for closure.}›
abbreviation "Der_inf φ ≡ Cl_inf(φ)"

lemma CD_inf: "Der_inf φ ⟹ Cl_inf(𝒞⇩D φ)" unfolding iADDI_a_def by (smt Cl_der_def Fr_2_def Ra_restr_ex compl_def dom_compl_def2 iDM_b join_def meet_def supremum_def)
lemma ID_inf: "Der_inf φ ⟹ Int_inf(ℐ⇩D φ)" by (simp add: CD_inf dual_der2 iADDI_MULT_dual1)

text‹\noindent{This condition is indeed strong enough as to entail closure of some fixed-point predicates under infimum/supremum.}›
lemma fp_ID_inf_closed: "Der_inf φ ⟹ infimum_closed (fp (ℐ⇩D φ))" by (metis (full_types) ID2 ID_inf Ra_restr_all dEXP_def iMULT_b_def inf_char)
lemma fp_CD_sup_closed: "Der_inf φ ⟹ supremum_closed (fp (𝒞⇩D φ))" by (metis (full_types) CD_inf Cl_der_def Ra_restr_ex iADDI_a_def join_def supremum_def)

subsubsection ‹Coherence conditions›
text‹\noindent{We finish this section by introducing the coherence' operator (Cantor's Koherenz') as discussed
by Zarycki in @{cite Zarycki2}. As happens with the derivative operator, the coherence operator cannot
be derived from interior, closure, border, nor frontier.}›

definition "Kh_1 φ ≡ ADDI_b φ"
definition "Kh_2 φ ≡ dEXP φ"
definition "Kh_3 φ ≡ ∀A. φ(φ⇧d A) ❙≈ φ⇧d(φ A)"

lemma PK1: "Kh_1 φ ≡ MONO φ" using ADDI_b_def Kh_1_def MONO_ADDIb by auto
lemma PK2: "Kh_1 φ ≡ ∀A B. φ(A ❙∧ B) ❙≼ (φ A) ❙∧ (φ B)" using MULT_a_def MONO_MULTa PK1 by auto
lemma PK3: "Kh_2 φ ⟹ φ ❙⊥ ❙≈ ❙⊥" using Kh_2_def dEXP_def unfolding conn by auto
lemma PK4: "Kh_1 φ ⟹  Kh_3 φ ⟹ φ ❙⊤ ❙≈ ❙⊤" using MONO_def PK1 dual_def unfolding Kh_3_def conn by metis
lemma PK5: "Kh_2 φ ⟹  ∀A. φ(❙─A) ❙≼ ❙─(φ A)" unfolding Kh_2_def dEXP_def conn by metis
lemma PK6: "Kh_1 φ ⟹ Kh_2 φ ⟹  ∀A B. φ(A ❙↼ B) ❙≼ (φ A) ❙↼ (φ B)" unfolding conn by (metis (no_types, lifting) Kh_2_def dEXP_def MONO_def PK1)
lemma PK7: "Kh_3 φ ⟹  ∀A. φ(φ(❙─(φ A))) ❙≈ φ(❙─(φ(φ⇧d A)))" proof -
assume kh3: "Kh_3 φ"
{ fix A
from kh3 have "φ(φ⇧d A) = φ⇧d(φ A)" using Kh_3_def by auto
hence "φ(❙─(φ(φ⇧d A))) ❙≈ φ(φ(❙─(φ A)))" unfolding dual_def conn by simp
} thus ?thesis by simp
qed
lemma PK8: "Kh_3 φ ⟹  ∀A. φ(❙─(φ(φ A))) ❙≈ φ⇧d(φ(❙─(φ A)))" proof -
assume kh3: "Kh_3 φ"
{ fix A
from kh3 have aux: "φ⇧d(φ A) ❙≈ φ(φ⇧d A)" using Kh_3_def by simp
have "let A=❙─(φ A) in (φ⇧d(φ A) ❙≈ φ(φ⇧d A))" using Kh_3_def kh3 by auto
hence "φ(❙─(φ(φ A))) ❙≈ φ⇧d(φ(❙─(φ A)))" unfolding dual_def conn by simp
} thus ?thesis  by simp
qed

text‹\noindent{Coherence operator as derived from derivative (requires conditions Der-2 and Der-4).}›
definition Kh_der::"(σ⇒σ)⇒(σ⇒σ)" ("𝒦⇩D") where "𝒦⇩D 𝒟 ≡ λA. A ❙∧ (𝒟 A)"
text‹\noindent{Verify properties:}›
lemma KD1: "Der_1 φ ⟹ Kh_1 (𝒦⇩D φ)" using PC1 PD3 PK2 ADDI_def Kh_der_def unfolding conn by (metis (full_types))
lemma KD2: "Kh_2 (𝒦⇩D φ)" by (simp add: Kh_2_def dEXP_def Kh_der_def conn)
lemma KD3: "Der_1 φ ⟹ Der_2 φ ⟹ Der_4 φ  ⟹ Kh_3 (𝒦⇩D φ)" proof -
assume der1: "Der_1 φ" and der2: "Der_2 φ" and der4: "Der_4 φ"
{ fix A
from der1 have aux1: "let M=A ; N=(φ⇧d A) in φ(M ❙∨ N) ❙≈ (φ M ❙∨ φ N)" unfolding ADDI_def by simp
from der1 der2 der4 have aux2: "(φ⇧d A) ❙∧ (φ A) ❙≈ φ⇧d(A ❙∧ φ A)" using PD12 by simp
have "(𝒦⇩D φ)((𝒦⇩D φ)⇧d A) = (❙─(❙─A ❙∧ φ (❙─A)) ❙∧ φ (❙─(❙─A ❙∧ φ (❙─A))))" unfolding Kh_der_def dual_def by simp
also have "... = (A ❙∨ φ⇧d A) ❙∧ φ(A ❙∨ φ⇧d A)" unfolding dual_def conn by simp
also from aux1 have "... = (A ❙∨ φ⇧d A) ❙∧ (φ A ❙∨ φ(φ⇧d A))" unfolding conn by meson
also have "... = (A ❙∧ φ A) ❙∨ φ⇧d A" using PD6 PD8 der1 der2 der4 unfolding conn by blast
also have "... = (A ❙∧ φ A) ❙∨ (φ⇧d A ❙∧ φ A)" using PD6 der1 der2 unfolding conn by blast
also have "... = (A ❙∨ φ⇧d A) ❙∧ (φ A)" unfolding conn by auto
also from aux2 have "... = (A ❙∧ φ A) ❙∨ φ⇧d(A ❙∧ φ A)" unfolding dual_def conn by meson
also have "... = ❙─(❙─(A ❙∧ φ A) ❙∧ φ (❙─(A ❙∧ φ A)))" unfolding dual_def conn by simp
also have "... = (𝒦⇩D φ)⇧d((𝒦⇩D φ) A)" unfolding Kh_der_def dual_def by simp
finally have "(𝒦⇩D φ)((𝒦⇩D φ)⇧d A) ❙≈ (𝒦⇩D φ)⇧d((𝒦⇩D φ) A)" by simp
} thus ?thesis unfolding Kh_3_def by simp
qed

end


# Theory topo_alexandrov

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

section ‹Generalized specialization orderings and Alexandrov topologies›

text‹\noindent{A topology is called 'Alexandrov' (after the Russian mathematician Pavel Alexandrov) if the intersection
(resp. union) of any (finite or infinite) family of open (resp. closed) sets is open (resp. closed);
in algebraic terms, this means that the set of fixed points of the interior (closure) operation is closed
under infinite meets (joins). Another common algebraic formulation requires the closure (interior) operation
to satisfy the infinitary variants of additivity (multiplicativity), i.e. iADDI (iMULT) as introduced before.

In the literature, the well-known Kuratowski conditions for the closure (resp. interior) operation are assumed,
namely: ADDI, EXP, NOR, IDEM (resp. MULT, dEXP, dNOR, IDEM). This makes both formulations equivalent.
However, this is not the case in general if those conditions become negotiable.}›

text‹\noindent{Alexandrov topologies have interesting properties relating them to the semantics of modal logic.
Assuming Kuratowski conditions, Alexandrov topological operations defined on subsets of S are in one-to-one
correspondence with preorders on S; in topological terms, Alexandrov topologies are uniquely determined by
their specialization preorders. Since we do not presuppose any Kuratowski conditions to begin with, the
preorders in question are in general not even transitive. Here we just call them 'specialization relations'.
We will still call (generalized) closure/interior-like operations as such (for lack of a better name).
We explore minimal conditions under which some relevant results for the semantics of modal logic obtain.}›

subsection ‹Specialization relations›

text‹\noindent{Specialization relations (among worlds/points) are particular cases of propositional functions with type @{text "w⇒σ"}.}›

text‹\noindent{Define some relevant properties of relations: }›
abbreviation "serial R  ≡ ∀x. ∃y. R x y"
abbreviation "reflexive R  ≡ ∀x. R x x"
abbreviation "transitive R ≡ ∀x y z. R x y ∧ R y z ⟶ R x z"
abbreviation "antisymmetric R  ≡ ∀x y. R x y ∧ R y x ⟶ x = y"
abbreviation "symmetric R  ≡ ∀x y. R x y ⟶ R y x"

text‹\noindent{Closure/interior operations can be derived from an arbitrary relation as operations returning down-/up-sets.}›
definition Cl_rel::"(w⇒σ)⇒(σ⇒σ)" ("𝒞⇩R") where "𝒞⇩R R ≡ λA. λw. ∃v. R w v ∧ A v"
definition Int_rel::"(w⇒σ)⇒(σ⇒σ)" ("ℐ⇩R") where "ℐ⇩R R ≡ λA. λw. ∀v. R w v ⟶ A v"

text‹\noindent{Duality between interior and closure follows directly:}›
lemma dual_rel1: "∀A. (𝒞⇩R R) A ❙≈ (ℐ⇩R R)⇧d A" unfolding Cl_rel_def Int_rel_def dual_def conn by simp
lemma dual_rel2: "∀A. (ℐ⇩R R) A ❙≈ (𝒞⇩R R)⇧d A" unfolding Cl_rel_def Int_rel_def dual_def conn by simp

text‹\noindent{We explore minimal conditions of the specialization relation under which some operation's conditions obtain.}›
lemma rC2: "reflexive R ⟶ EXP (𝒞⇩R R)" unfolding EXP_def Cl_rel_def by auto
lemma rC3: "NOR (𝒞⇩R R)" unfolding Cl_rel_def NOR_def conn by blast
lemma rC4: "reflexive R ∧ transitive R ⟶ IDEM (𝒞⇩R R)" unfolding Cl_rel_def IDEM_def by smt
lemma rC_Barcan: "∀π. (𝒞⇩R R)(❙∃x. π x) ❙≼ (❙∃x. (𝒞⇩R R)(π x))" unfolding Cl_rel_def by auto

lemma rI1: "MULT (ℐ⇩R R)" unfolding Int_rel_def MULT_def conn by blast
lemma rI1i:"iMULT (ℐ⇩R R)" by (smt Int_rel_def Ra_restr_all iMULT_def infimum_def)
lemma rI2: "reflexive R ⟹ dEXP (ℐ⇩R R)" unfolding Int_rel_def dEXP_def Int_rel_def by auto
lemma rI3: "dNOR (ℐ⇩R R)" unfolding Int_rel_def dNOR_def conn by simp
lemma rI4: "reflexive R ⟹ transitive R ⟹ IDEM (ℐ⇩R R)" unfolding IDEM_def Int_rel_def by smt
lemma rI_Barcan: "∀π. (❙∀x. (ℐ⇩R R)(π x)) ❙≼ (ℐ⇩R R)(❙∀x. π x)" unfolding Int_rel_def by simp

text‹\noindent{A specialization relation can be derived from a given operation (intended as a closure-like operation).}›
definition sp_rel::"(σ⇒σ)⇒(w⇒σ)" ("ℛ⇧C") where "ℛ⇧C 𝒞 ≡ λw v. 𝒞 (λu. u=v) w"

text‹\noindent{Preorder properties of the specialization relation follow directly from the corresponding operation's conditions.}›
lemma sp_rel_reflex: "EXP 𝒞 ⟹ reflexive (ℛ⇧C 𝒞)" by (simp add: EXP_def sp_rel_def)
lemma sp_rel_trans: "MONO 𝒞 ⟹ IDEM 𝒞 ⟹ transitive (ℛ⇧C 𝒞)" by (smt IDEM_def MONO_def sp_rel_def)

text‹\noindent{However, we can obtain finite countermodels for antisymmetry and symmetry given all relevant conditions.
We will revisit this issue later and examine their relation with the topological separation axioms T0 and T1 resp.}›
lemma "iADDI 𝒞 ⟹ EXP 𝒞 ⟹ NOR 𝒞 ⟹ IDEM 𝒞 ⟹ antisymmetric (ℛ⇧C 𝒞)" nitpick oops (*counterexample*)
lemma "iADDI 𝒞 ⟹ EXP 𝒞 ⟹ NOR 𝒞 ⟹ IDEM 𝒞 ⟹ symmetric (ℛ⇧C 𝒞)" nitpick oops (*counterexample*)

subsection ‹Alexandrov topology›

text‹\noindent{As mentioned previously, Alexandrov closure (and by duality interior) operations correspond to specialization
relations. It is worth mentioning that in Alexandrov topologies every point has a minimal/smallest neighborhood,
namely the set of points related to it by the specialization (aka. accessibility) relation. Alexandrov spaces are
thus also called 'finitely generated'. We examine below  minimal conditions under which these relations obtain.}›

lemma sp_rel_a:   "MONO 𝒞  ⟹ ∀A. (𝒞⇩R (ℛ⇧C 𝒞)) A ❙≼ 𝒞 A" by (smt Cl_rel_def MONO_def sp_rel_def)
lemma sp_rel_b: "iADDI_a 𝒞 ⟹ ∀A. (𝒞⇩R (ℛ⇧C 𝒞)) A ❙≽ 𝒞 A"  proof -
{ fix A
let ?S="λB::σ. ∃w::w. A w ∧ B=(λu. u=w)"
have "A ❙≈ (❙⋁?S)" using supremum_def by auto
hence "𝒞(A) ❙≈ 𝒞(❙⋁?S)" by (smt eq_ext)
moreover have "❙⋁Ra[𝒞|?S] ❙≈ (𝒞⇩R (ℛ⇧C 𝒞)) A" by (smt Cl_rel_def Ra_restr_ex sp_rel_def)
ultimately have "𝒞 A ❙≼ (𝒞⇩R (ℛ⇧C 𝒞)) A" by simp
} thus ?thesis by simp
qed
text‹\noindent{It is instructive to expand the definitions in the above lemma:}›
lemma "iADDI 𝒞 ⟹  ∀A. ∀w. (𝒞 A) w ⟷ (∃v. A v ∧ (𝒞 (λu. u=v)) w)" using Cl_rel_def sp_rel by fastforce

text‹\noindent{We now turn to the more traditional characterization of Alexandrov topologies in terms of closure under
infinite joins/meets.}›

text‹\noindent{Fixed points of operations satisfying ADDI (MULT) are not in general closed under infinite joins (meets).
For the given conditions countermodels are expected to be infinite. We (sanity) check that nitpick cannot find any.}›
lemma "ADDI(φ) ⟹ supremum_closed (fp φ)" (*nitpick*) oops (*cannot find finite countermodels*)
lemma "MULT(φ) ⟹ infimum_closed  (fp φ)" (*nitpick*) oops (*cannot find finite countermodels*)

text‹\noindent{By contrast, we can show that this obtains if assuming the corresponding infinitary variants (iADDI/iMULT).}›
lemma "iADDI(φ) ⟹ supremum_closed (fp φ)" by (metis (full_types) Ra_restr_ex iADDI_def supremum_def)
lemma "iMULT(φ) ⟹ infimum_closed  (fp φ)" by (metis (full_types) Ra_restr_all iMULT_def infimum_def)

text‹\noindent{As shown above, closure (interior) operations derived from relations readily satisfy iADDI (iMULT),
being thus closed under infinite joins (meets).}›
lemma "supremum_closed (fp (𝒞⇩R R))" by (smt Cl_rel_def supremum_def)
lemma "infimum_closed  (fp (ℐ⇩R R))" by (smt Int_rel_def infimum_def)

subsection ‹(Anti)symmetry and the separation axioms T0 and T1›
text‹\noindent{We can now revisit the relationship between (anti)symmetry and the separation axioms T1 and T0.}›

text‹\noindent{T0: any two distinct points in the space can be separated by an open set (i.e. containing one point and not the other).}›
abbreviation "T0_sep 𝒞 ≡ ∀w v. w ≠ v ⟶ (∃G. (fp 𝒞⇧d)(G) ∧ (G w ≠ G v))"
text‹\noindent{T1: any two distinct points can be separated by (two not necessarily disjoint) open sets, i.e. all singletons are closed.}›
abbreviation "T1_sep 𝒞 ≡ ∀w. (fp 𝒞)(λu. u = w)"

text‹\noindent{We can (sanity) check that T1 entails T0 but not viceversa.}›
lemma "T0_sep 𝒞 ⟹ T1_sep 𝒞" nitpick oops (*counterexample*)
lemma "T1_sep 𝒞 ⟹ T0_sep 𝒞" by (smt compl_def dual_def dual_symm)

text‹\noindent{Under appropriate conditions, T0-separation corresponds to antisymmetry of the specialization relation (here an ordering).}›
lemma "T0_sep 𝒞 ⟷ antisymmetric (ℛ⇧C 𝒞)" nitpick oops (*counterexample*)
lemma T0_antisymm_a: "MONO 𝒞 ⟹ T0_sep 𝒞 ⟶ antisymmetric (ℛ⇧C 𝒞)" by (smt Cl_rel_def compl_def dual_def sp_rel_a)
lemma T0_antisymm_b: "EXP 𝒞 ⟹ IDEM 𝒞 ⟹ antisymmetric (ℛ⇧C 𝒞) ⟶ T0_sep 𝒞" by (metis (full_types) EXP_dual1 IDEM_def IDEM_dual2 IDEMa_def IDEMb_def compl_def dEXP_def dual_def dual_symm sp_rel_def)
lemma T0_antisymm: "MONO 𝒞 ⟹ EXP 𝒞 ⟹ IDEM 𝒞 ⟹ T0_sep 𝒞 = antisymmetric (ℛ⇧C 𝒞)" by (metis T0_antisymm_a T0_antisymm_b)

text‹\noindent{Also, under the appropriate conditions, T1-separation corresponds to symmetry of the specialization relation.}›
lemma T1_symm_a: "T1_sep 𝒞 ⟶ symmetric (ℛ⇧C 𝒞)" using sp_rel_def by auto
lemma T1_symm_b: "MONO 𝒞 ⟹ EXP 𝒞 ⟹ T0_sep 𝒞 ⟹ symmetric (ℛ⇧C 𝒞) ⟶ T1_sep 𝒞" by (metis T0_antisymm_a sp_rel_def sp_rel_reflex)
lemma T1_symm: "MONO 𝒞 ⟹ EXP 𝒞 ⟹ T0_sep 𝒞 ⟹ symmetric (ℛ⇧C 𝒞) = T1_sep 𝒞" by (metis T1_symm_a T1_symm_b)

end


# Theory topo_frontier_algebra

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

section ‹Frontier Algebra›

text‹\noindent{The closure of a set A (@{text "𝒞(A)"}) can be seen as the set A augmented by (i) its boundary points,
or (ii) its accumulation/limit points. In this section we explore the first variant by drawing on the notion
of a frontier algebra, defined in an analogous fashion as the well-known closure and interior algebras.}›

text‹\noindent{Declares a primitive (unconstrained) frontier (aka. boundary) operation and defines others from it.}›
consts ℱ::"σ⇒σ"
abbreviation "ℐ ≡ ℐ⇩F ℱ" ―‹ interior ›
abbreviation "𝒞 ≡ 𝒞⇩F ℱ" ―‹ closure ›
abbreviation "ℬ ≡ ℬ⇩F ℱ" ―‹ border ›

subsection ‹Basic properties›

text‹\noindent{Verifies minimal conditions under which operators resulting from conversion functions coincide.}›
lemma ICdual: "Fr_2 ℱ ⟹ ℐ ❙≡ 𝒞⇧d" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma ICdual': "Fr_2 ℱ ⟹ 𝒞 ❙≡ ℐ⇧d" by (simp add: Cl_fr_def Fr_2_def Int_fr_def dual_def equal_op_def conn)
lemma BI_rel: "ℬ ❙≡ ℬ⇩I ℐ" using Br_fr_def Br_int_def Int_fr_def unfolding equal_op_def conn by auto
lemma IB_rel: "ℐ ❙≡ ℐ⇩B ℬ" using Br_fr_def Int_br_def Int_fr_def unfolding equal_op_def conn by auto
lemma BC_rel: "Fr_2 ℱ ⟹ ℬ ❙≡ ℬ⇩C 𝒞"  using BI_BC_rel BI_rel ICdual' eq_ext' by fastforce
lemma CB_rel: "Fr_2 ℱ ⟹ 𝒞 ❙≡ 𝒞⇩B ℬ" using Br_fr_def Cl_br_def Cl_fr_def Fr_2_def unfolding equal_op_def conn by auto
lemma FI_rel: "Fr_2 ℱ ⟹ ℱ ❙≡ ℱ⇩I ℐ" by (smt Cl_fr_def Fr_int_def ICdual' Int_fr_def compl_def diff_def equal_op_def join_def meet_def)
lemma FC_rel: "Fr_2 ℱ ⟹ ℱ ❙≡ ℱ⇩C 𝒞" by (metis (mono_tags, lifting) FI_rel Fr_2_def Fr_cl_def Fr_int_def ICdual' dual_def eq_ext' equal_op_def)
lemma FB_rel: "Fr_2 ℱ ⟹ ℱ ❙≡ ℱ⇩B ℬ" by (smt Br_fr_def CB_rel Cl_br_def FC_rel Fr_br_def Fr_cl_def equal_op_def join_def meet_def)

text‹\noindent{Fixed-point and other operators are interestingly related.}›
lemma fp1: "ℐ⇧f⇧p ❙≡ ℬ⇧c" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp2: "ℬ⇧f⇧p ❙≡ ℐ⇧c" using Br_fr_def Int_fr_def unfolding equal_op_def conn by auto
lemma fp3: "Fr_2 ℱ ⟹ 𝒞⇧f⇧p ❙≡ ℬ⇧d" using Br_fr_def Cl_fr_def Fr_2_def dual_def equal_op_def conn by fastforce
lemma fp4: "Fr_2 ℱ ⟹ (ℬ⇧d)⇧f⇧p ❙≡ 𝒞" by (smt dimp_def equal_op_def fp3)
lemma fp5: "ℱ⇧f⇧p ❙≡ ℬ ❙⊔ (𝒞⇧c)" using Br_fr_def Cl_fr_def unfolding equal_op_def conn by auto

text‹\noindent{Different inter-relations (some redundant ones are kept to help the provers).}›
lemma monI: "Fr_1b ℱ ⟹ MONO(ℐ)" by (simp add: IF1a MONO_MULTa)
lemma monC: "Fr_6 ℱ ⟹ MONO(𝒞)" by (simp add: Cl_fr_def Fr_6_def MONO_def conn)
lemma pB1: "∀A. ℬ A ❙≈ A ❙↼ ℐ A" using Br_fr_def fp1 unfolding conn equal_op_def by metis
lemma pB2: "∀A. ℬ A ❙≈ A ❙∧ ℱ A" by (simp add: Br_fr_def)
lemma pB3: "Fr_2 ℱ ⟹ ∀A. ℬ(❙─A) ❙≈ ❙─A ❙∧ ℱ A" by (simp add: Fr_2_def pB2 conn)
lemma pB4: "Fr_2 ℱ ⟹ ∀A. ℬ(❙─A) ❙≈ ❙─A ❙∧ 𝒞 A" using CB_rel Cl_br_def pB3 unfolding conn equal_op_def by metis
lemma pB5: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ ∀A. ℬ(𝒞 A) ❙≼ (ℬ A) ❙∨ ℬ(❙─A)"  by (smt BC_rel Br_cl_def Cl_fr_def Fr_6_def PF6 equal_op_def conn)
lemma pF1: "∀A. ℱ A ❙≈ 𝒞 A ❙↼ ℐ A"  using Cl_fr_def Int_fr_def conn by auto
lemma pF2: "Fr_2 ℱ ⟹ ∀A. ℱ A ❙≈ 𝒞 A ❙∧ 𝒞(❙─A)" using Cl_fr_def Fr_2_def conn by auto
lemma pF3: "Fr_2 ℱ ⟹ ∀A. ℱ A ❙≈ ℬ A ❙∨ ℬ(❙─A)" using Br_fr_def Fr_2_def conn by auto
lemma pF4: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4(ℱ) ⟹ ∀A. ℱ(ℐ A) ❙≼ ℱ A" by (smt IDEMa_def IF2 IF4 Int_fr_def MONO_def PF1 PF6 PI4 diff_def monC pF1)
lemma pF5: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. ℱ(𝒞 A) ❙≼ ℱ A" by (metis Br_fr_def CF4 Cl_fr_def IDEM_def PF1 join_def meet_def pB5 pF3)
lemma pA1: "∀A. A ❙≈ ℐ A ❙∨ ℬ A" using Br_fr_def Int_fr_def unfolding conn by auto
lemma pA2: "Fr_2 ℱ ⟹ ∀A. A ❙≈ 𝒞 A ❙↼ ℬ(❙─A)" using pB1 dual_def fp3 unfolding equal_op_def conn by smt
lemma pC1: "Fr_2 ℱ ⟹ ∀A. 𝒞 A ❙≈ A ❙∨ ℬ(❙─A)" using Cl_fr_def pB4 conn by auto
lemma pC2: "∀A. 𝒞 A ❙≈ A ❙∨ ℱ A" using Cl_fr_def by auto
lemma pI1: "∀A. ℐ A ❙≈ A ❙↼ ℬ A" using pA1 pB1 conn by auto
lemma pI2: "∀A. ℐ A ❙≈ A ❙↼ ℱ A" by (simp add: Int_fr_def)

lemma IC_imp: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀A B. ℐ(A ❙→ B) ❙≼ 𝒞 A ❙→ 𝒞 B" proof -
assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr3: "Fr_3 ℱ"
{ fix a b
have "(a ❙→ b) ❙∧ ❙─b ❙→ ❙─a = ❙⊤" unfolding conn by auto
hence "ℐ((a ❙→ b) ❙∧ ❙─b ❙→ ❙─a) ❙≈ ℐ(❙⊤)" by simp
hence "ℐ((a ❙→ b) ❙∧ ❙─b ❙→ ❙─a) ❙≈ ❙⊤" using fr3 IF3 dNOR_def fr2 by auto
moreover have "let A=(a ❙→ b) ❙∧ ❙─b; B=❙─a in ℐ(A ❙→ B) ❙≼ ℐ(A) ❙→ ℐ(B)" using fr1 IF1 PI7 Int_7_def by metis
ultimately have "ℐ((a ❙→ b) ❙∧ ❙─b) ❙→ ℐ(❙─a) ❙≈ ❙⊤" unfolding conn by simp
moreover have "let A=a ❙→ b; B=❙─b in ℐ(A ❙∧ B) ❙≈ ℐ(A) ❙∧ ℐ(B)" using fr1 IF1 MULT_def by simp
ultimately have "ℐ(a ❙→ b) ❙∧ ℐ(❙─b) ❙→ ℐ(❙─a) ❙≈ ❙⊤" unfolding conn by simp
moreover have "∀A. ℐ(❙─A) ❙≈ ❙─𝒞(A)" using Cl_fr_def Fr_2_def Int_fr_def fr2  unfolding conn by auto
ultimately have "ℐ(a ❙→ b) ❙∧ ❙─𝒞(b) ❙→ ❙─𝒞(a) ❙≈ ❙⊤" unfolding conn by simp
hence "ℐ(a ❙→ b) ❙∧ ❙─𝒞(b) ❙≼ ❙─𝒞(a)" unfolding conn by simp
hence "ℐ(a ❙→ b) ❙∧ 𝒞 a ❙≼ 𝒞 b" unfolding conn by metis
} thus ?thesis unfolding conn by simp
qed

text‹\noindent{Defines some fixed-point predicates and prove some properties.}›
abbreviation openset ("Op") where "Op A ≡ fp ℐ A"
abbreviation closedset ("Cl") where "Cl A ≡ fp 𝒞 A"
abbreviation borderset ("Br") where "Br A ≡ fp ℬ A"
abbreviation frontierset ("Fr") where "Fr A ≡ fp ℱ A"

lemma Int_Open: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. Op(ℐ A)" using IF4 IDEM_def by blast
lemma Cl_Closed: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. Cl(𝒞 A)" using CF4 IDEM_def by blast
lemma Br_Border: "Fr_1b ℱ ⟹ ∀A. Br(ℬ A)" using Br_fr_def Fr_1b_def conn by auto
text‹\noindent{In contrast, there is no analogous fixed-point result for frontier:}›
lemma "𝔉 ℱ ⟹ ∀A. Fr(ℱ A)" nitpick oops (*counterexample even if assuming all frontier conditions*)

lemma OpCldual: "Fr_2 ℱ ⟹ ∀A. Cl A ⟷ Op(❙─A)" using Cl_fr_def Fr_2_def Int_fr_def conn by auto
lemma ClOpdual: "Fr_2 ℱ ⟹ ∀A. Op A ⟷ Cl(❙─A)" using ICdual dual_def unfolding equal_op_def conn by auto
lemma Fr_ClBr: "∀A. Fr(A) = (Cl(A) ∧ Br(A))" using Br_fr_def Cl_fr_def join_def meet_def by auto
lemma Cl_F: "Fr_4 ℱ ⟹ ∀A. Cl(ℱ A)" using Cl_fr_def Fr_4_def conn by auto

subsection ‹Further properties›

text‹\noindent{The definitions and theorems below are well known in the literature (e.g. @{cite Kuratowski2}).
Here we uncover the minimal conditions under which they hold (taking frontier operation as primitive).}›
lemma Cl_Bzero: "Fr_2 ℱ ⟹ ∀A. Cl A ⟷ ℬ(❙─A) ❙≈ ❙⊥" using pA2 pC1 unfolding conn by metis
lemma Op_Bzero: "∀A. Op A ⟷ (ℬ A) ❙≈ ❙⊥" using pB1 pI1 unfolding conn by metis
lemma Br_boundary: "Fr_2 ℱ ⟹ ∀A. Br(A) ⟷ ℐ A ❙≈ ❙⊥" by (metis Br_fr_def Int_fr_def bottom_def diff_def meet_def)
lemma Fr_nowhereDense: "Fr_2 ℱ ⟹ ∀A. Fr(A) ⟶ ℐ(𝒞 A) ❙≈ ❙⊥" using Fr_ClBr Br_boundary eq_ext by metis
lemma Cl_FB: "∀A. Cl A ⟷ ℱ A ❙≈ ℬ A" using Br_fr_def Cl_fr_def unfolding conn by auto
lemma Op_FB: "Fr_2 ℱ ⟹ ∀A. Op A ⟷ ℱ A ❙≈ ℬ(❙─A)" using Br_fr_def Fr_2_def Int_fr_def unfolding conn by auto
lemma Clopen_Fzero: "∀A. Cl A ∧ Op A ⟷ ℱ A ❙≈ ❙⊥" using Cl_fr_def Int_fr_def unfolding conn by auto

lemma Int_sup_closed: "Fr_1b ℱ ⟹ supremum_closed (λA. Op A)" by (smt IF1a Int_fr_def MONO_def MONO_MULTa sup_char conn)
lemma Int_meet_closed: "Fr_1a ℱ ⟹ meet_closed (λA. Op A)" using Fr_1a_def Int_fr_def unfolding conn by metis
lemma Int_inf_closed: "Fr_inf ℱ ⟹ infimum_closed (λA. Op A)" by (simp add: fp_IF_inf_closed)
lemma Cl_inf_closed: "Fr_6 ℱ ⟹ infimum_closed (λA. Cl A)" by (smt Cl_fr_def Fr_6_def infimum_def join_def)
lemma Cl_join_closed: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ join_closed (λA. Cl A)" using ADDI_a_def CF1a CF2 EXP_def unfolding conn by metis
lemma Cl_sup_closed: "Fr_2 ℱ ⟹ Fr_inf ℱ ⟹ supremum_closed (λA. Cl A)" by (simp add: fp_CF_sup_closed)
lemma Br_inf_closed: "Fr_1b ℱ ⟹ infimum_closed (λA. Br A)" by (smt BI_rel Br_int_def IF1a MONO_iMULTa MONO_MULTa Ra_restr_all eq_ext' iMULT_a_def inf_char diff_def)
lemma Fr_inf_closed: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ infimum_closed (λA. Fr A)" by (metis (full_types) Br_fr_def Br_inf_closed PF6 Cl_fr_def Cl_inf_closed meet_def join_def)
lemma Br_Fr_join: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A B. Br A ∧ Fr B ⟶ Br(A ❙∨ B)" proof -
assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr4: "Fr_4 ℱ"
{ fix A B
{ assume bra: "Br A" and frb: "Fr B"
from bra have "ℐ A ❙≈ ❙⊥" using Br_boundary fr2 by auto
hence 1: "𝒞(❙─A) ❙≈ ❙⊤" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
from frb have "ℐ(𝒞 B) ❙≈ ❙⊥" by (simp add: Fr_nowhereDense fr2)
hence 2: "𝒞(❙─(𝒞 B)) ❙≈ ❙⊤" by (metis ICdual bottom_def compl_def dual_def eq_ext' fr2 top_def)
from fr1 fr2 have "𝒞(❙─A) ❙↼ 𝒞 B ❙≼ 𝒞((❙─A) ❙↼ B)" using CF1 Cl_6_def PC6 by metis
hence "𝒞(❙─A) ❙↼ 𝒞 B ❙≼ 𝒞(❙─(A ❙∨ B))" unfolding conn by simp
hence "❙⊤ ❙↼ 𝒞 B ❙≼ 𝒞(❙─(A ❙∨ B))" using 1 unfolding conn by simp
hence 3: "❙─(𝒞 B) ❙≼ 𝒞(❙─(A ❙∨ B))" unfolding conn by simp
from fr1 fr2 fr4 have 4: "let M=❙─(𝒞 B); N=❙─(A ❙∨ B) in  M ❙≼ 𝒞 N ⟶ 𝒞 M ❙≼ 𝒞 N" using PC9 CF4 Cl_9_def PF1 CF1b by fastforce
from 3 4 have "𝒞(❙─(𝒞 B)) ❙≼ 𝒞(❙─(A ❙∨ B))" by simp
hence "❙⊤ ❙≈ 𝒞(❙─(A ❙∨ B))" using 2 unfolding top_def by simp
hence "❙⊥ ❙≈ ℐ(A ❙∨ B)" using fr2 ICdual dual_def eq_ext' conn by metis
hence "Br (A ❙∨ B)" using fr2 Br_boundary by simp
} hence "Br A ∧ Fr B ⟶ Br (A ❙∨ B)" by simp
} hence "∀A B. Br A ∧ Fr B ⟶ Br (A ❙∨ B)" by simp
thus ?thesis by simp
qed
lemma Fr_join_closed: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ join_closed (λA. Fr A)" by (smt Br_Fr_join ADDI_a_def CF1a Cl_fr_def PF1 diff_def join_def meet_def pB2 pF1)

text‹\noindent{Introduces a predicate for indicating that two sets are disjoint and proves some properties.}›
abbreviation "Disj A B ≡ A ❙∧ B ❙≈ ❙⊥"

lemma Disj_comm: "∀A B. Disj A B ⟶ Disj B A" unfolding conn by fastforce
lemma Disj_IF: "∀A. Disj (ℐ A) (ℱ A)" by (simp add: Int_fr_def conn)
lemma Disj_B: "∀A. Disj (ℬ A) (ℬ(❙─A))" using Br_fr_def unfolding conn by auto
lemma Disj_I: "∀A. Disj (ℐ A) (❙─A)" by (simp add: Int_fr_def conn)
lemma Disj_BCI: "Fr_2 ℱ ⟹ ∀A. Disj (ℬ(𝒞 A)) (ℐ(❙─A))" using Br_fr_def Cl_fr_def Fr_2_def Int_fr_def conn by metis
lemma Disj_CBI: "Fr_6 ℱ ⟹ Fr_4 ℱ ⟹ ∀A. Disj (𝒞(ℬ(❙─A))) (ℐ(❙─A))" by (metis Br_fr_def Cl_F IB_rel Int_br_def MONO_MULTa MULT_a_def eq_ext' monC conn)

text‹\noindent{Introduces a predicate for indicating that two sets are separated and proves some properties.}›
definition "Sep A B ≡ Disj (𝒞 A) B ∧ Disj (𝒞 B) A"

lemma Sep_comm: "∀A B. Sep A B ⟶ Sep B A" by (simp add: Sep_def)
lemma Sep_disj: "∀A B. Sep A B ⟶ Disj A B" using Cl_fr_def Sep_def conn by fastforce
lemma Sep_I: "Fr_1(ℱ) ⟹ Fr_2(ℱ) ⟹ Fr_4(ℱ) ⟹ ∀A. Sep (ℐ A) (ℐ (❙─A))" using Cl_fr_def pF4 Fr_2_def Int_fr_def unfolding Sep_def conn by metis
lemma Sep_sub: "Fr_6 ℱ  ⟹ ∀A B C D. Sep A B ∧ C ❙≼ A ∧ D ❙≼ B ⟶ Sep C D" using MONO_def monC unfolding Sep_def conn by smt
lemma Sep_Cl_diff: "Fr_6 ℱ ⟹ ∀A B. Cl(A) ∧ Cl(B) ⟶ Sep (A ❙↼ B) (B ❙↼ A)" using Fr_6_def pC2 unfolding Sep_def conn by smt
lemma Sep_Op_diff: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ ∀A B. Op(A) ∧ Op(B) ⟶ Sep (A ❙↼ B) (B ❙↼ A)" proof -
assume fr1b:"Fr_1b ℱ" and fr2:"Fr_2 ℱ"
{ fix A B
from fr1b fr2 have aux: "let M=❙─A ; N=❙─B in (Cl(M) ∧ Cl(N) ⟶ Sep (M ❙↼ N) (N ❙↼ M))" using PF6 Sep_Cl_diff by simp
{ assume "Op(A) ∧ Op(B)"
hence "Cl(❙─A) ∧ Cl(❙─B)" using fr2 ClOpdual by simp
hence "Sep (❙─A ❙↼ ❙─B) (❙─B ❙↼ ❙─A)" using fr1b fr2 aux unfolding conn by simp
moreover have "(❙─A ❙↼ ❙─B) ❙≈ (B ❙↼ A)" unfolding conn by auto
moreover have "(❙─B ❙↼ ❙─A) ❙≈ (A ❙↼ B)" unfolding conn by auto
ultimately have "Sep (B ❙↼ A) (A ❙↼ B)" unfolding conn by simp
hence "Sep (A ❙↼ B) (B ❙↼ A)" using Sep_comm by simp
} hence "Op(A) ∧ Op(B) ⟶ Sep (A ❙↼ B) (B ❙↼ A)" by (rule impI)
} thus ?thesis by simp
qed
lemma Sep_Cl: "∀A B. Cl(A) ∧ Cl(B) ∧ Disj A B ⟶ Sep A B" unfolding Sep_def conn by blast
lemma Sep_Op: "Fr_1b ℱ ⟹ Fr_2 ℱ  ⟹ ∀A B. Op(A) ∧ Op(B) ∧ Disj A B ⟶ Sep A B" proof -
assume fr1b:"Fr_1b ℱ" and fr2:"Fr_2 ℱ"
{ fix A B
from fr1b fr2 have aux: "Op(A) ∧ Op(B) ⟶ Sep (A ❙↼ B) (B ❙↼ A)" using Sep_Op_diff by simp
{ assume op: "Op(A) ∧ Op(B)" and disj: "Disj A B"
hence "(A ❙↼ B) ❙≈ A ∧ (B ❙↼ A) ❙≈ B" unfolding conn by blast
hence "Sep A B" using op aux unfolding conn by simp
} hence "Op(A) ∧ Op(B) ∧ Disj A B ⟶ Sep A B" by simp
} thus ?thesis by simp
qed
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ ∀A B C. Sep A B ∧ Sep A C ⟶ Sep A (B ❙∨ C)" using CF1a ADDI_a_def unfolding Sep_def conn by metis

text‹\noindent{Verifies a neighborhood-based definition of closure.}›
definition "nbhd A p ≡ ∃E. E ❙≼ A ∧ Op(E) ∧ (E p)"
lemma nbhd_def2: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (nbhd A p) = (ℐ A p)" using pF4 MONO_def PF1 monI pI2 unfolding nbhd_def conn by smt

lemma C_def_lr: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (𝒞 A p) ⟶ (∀E. (nbhd E p) ⟶ ¬(Disj E A))" using Cl_fr_def Fr_2_def Fr_6_def PF6 pF1 unfolding nbhd_def conn by smt
lemma C_def_rl: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (𝒞 A p) ⟵ (∀E. (nbhd E p) ⟶ ¬(Disj E A))" using Cl_fr_def pF5 pA1 pB4 unfolding nbhd_def conn by smt
lemma C_def: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A p. (𝒞 A p) ⟷ (∀E. (nbhd E p) ⟶ ¬(Disj E A))" using C_def_lr C_def_rl PF1 by blast

text‹\noindent{Explore the Barcan and converse Barcan formulas.}›
lemma Barcan_I: "Fr_inf ℱ ⟹ ∀P. (❙∀x. ℐ(P x)) ❙≼ ℐ(❙∀x. P x)" using IF_inf Barcan1 by auto
lemma Barcan_C: "Fr_2 ℱ ⟹ Fr_inf ℱ ⟹ ∀P. 𝒞(❙∃x. P x) ❙≼ (❙∃x. 𝒞(P x))" using Fr_2_def CF_inf Barcan2 by metis
lemma CBarcan_I: "Fr_1b ℱ ⟹ ∀P. ℐ(❙∀x. P x)  ❙≼ (❙∀x. ℐ(P x))" by (metis (mono_tags, lifting) MONO_def monI)
lemma CBarcan_C: "Fr_6 ℱ ⟹ ∀P. (❙∃x. 𝒞(P x)) ❙≼ 𝒞(❙∃x. P x)"  by (metis (mono_tags, lifting) MONO_def monC)

end


# Theory topo_negation_conditions

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

section ‹Frontier-based negation - Semantic conditions›

text‹\noindent{We define a paracomplete and a paraconsistent negation employing the interior and closure operation resp.
We take the frontier operator as primitive and explore which semantic conditions are minimally required
to obtain some relevant properties of negation.}›

definition neg_I::"σ⇒σ" ("❙¬⇧I")  where  "❙¬⇧I A ≡ ℐ(❙─A)"
definition neg_C::"σ⇒σ" ("❙¬⇧C")  where  "❙¬⇧C A ≡ 𝒞(❙─A)"
declare neg_I_def[conn] neg_C_def[conn]

text‹\noindent{(We rename the meta-logical HOL negation to avoid terminological confusion)}›
abbreviation cneg::"bool⇒bool" ("∼_" 40) where "∼φ ≡ ¬φ"

subsection ‹'Explosion' (ECQ), non-contradiction (LNC) and excluded middle (TND)›

text‹\noindent{TND}›
lemma "𝔉 ℱ ⟹ TNDm ❙¬⇧I" nitpick oops (*minimally weak TND not valid*)
lemma TND_C: "TND ❙¬⇧C" by (simp add: pC2 Defs conn) (*TND valid in general*)

text‹\noindent{ECQ}›
lemma ECQ_I: "ECQ ❙¬⇧I" by (simp add: pI2 Defs conn) (*ECQ valid in general*)
lemma "𝔉 ℱ ⟹ ECQm ❙¬⇧C" nitpick oops (*minimally weak ECQ not valid*)

text‹\noindent{LNC}›
lemma "LNC ❙¬⇧I" nitpick oops (*countermodel*)
lemma LNC_I: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹  LNC ❙¬⇧I" using ECQ_I ECQ_def IF3 LNC_def dNOR_def unfolding conn by auto
lemma "LNC ❙¬⇧C" nitpick oops (*countermodel*)
lemma LNC_C: "Fr_6 ℱ ⟹ LNC ❙¬⇧C" unfolding Defs by (smt Cl_fr_def MONO_def compl_def join_def meet_def monC neg_C_def top_def)

text‹\noindent{Relations between LNC and different ECQ variants (only relevant for paraconsistent negation).}›
lemma "ECQ ❙¬⇧C ⟶  LNC ❙¬⇧C" by (simp add: pC2 Defs conn)
lemma ECQw_LNC: "ECQw ❙¬⇧C ⟶  LNC ❙¬⇧C" by (smt ECQw_def LNC_def pC2 conn)
lemma ECQm_LNC: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ ECQm ❙¬⇧C ⟶ LNC ❙¬⇧C" using Cl_fr_def Fr_1_def pF2 unfolding Defs conn by metis
lemma "𝔉 ℱ ⟹ LNC ❙¬⇧C ⟶  ECQm ❙¬⇧C" nitpick oops  (*countermodel*)

text‹\noindent{Below we show that enforcing all conditions on the frontier operator still leaves room
for both boldly paraconsistent and paracomplete models. We use Nitpick to generate a non-trivial
model (here a set algebra with 8 elements).}›
lemma "𝔉 ℱ ∧ ∼ECQm ❙¬⇧C" nitpick[satisfy,card w=3] oops (*boldly paraconsistent model found*)
lemma "𝔉 ℱ ∧ ∼TNDm ❙¬⇧I" nitpick[satisfy,card w=3] oops (*boldly paracomplete model found*)

subsection ‹Modus tollens (MT)›

text‹\noindent{MT-I}›
lemma MT0_I: "Fr_1b ℱ ⟹ MT0 ❙¬⇧I"  unfolding Defs by (smt MONO_def compl_def monI neg_I_def top_def)
lemma MT1_I: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ MT1 ❙¬⇧I" unfolding Defs by (metis MONO_def monI IF3 Int_fr_def compl_def dNOR_def diff_def neg_I_def top_def)
lemma "𝔉 ℱ ⟹ MT2 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1a ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "𝔉 ℱ ⟹ MT3 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TNDm ❙¬⇧I ∧ Fr_1a ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ MT3 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ MT0 ❙¬⇧I ∧ MT1 ❙¬⇧I ∧ MT2 ❙¬⇧I ∧ MT3 ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{MT-C}›
lemma "Fr_2 ℱ ⟹ MT0 ❙¬⇧C" nitpick oops (*countermodel*)
lemma MT0_C: "Fr_6 ℱ ⟹ MT0 ❙¬⇧C" unfolding Defs by (smt ICdual MONO_def compl_def monC neg_C_def top_def)
lemma MT1_C: "Fr_6 ℱ ⟹ MT1 ❙¬⇧C" unfolding Defs by (smt Cl_fr_def Fr_6_def conn)
lemma "𝔉 ℱ ⟹ MT2 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQm ❙¬⇧C ∧ 𝔉 ℱ ∧ MT2 ❙¬⇧C" nitpick[satisfy,card w=3] oops (*model found*)
lemma MT3_C: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ MT3 ❙¬⇧C" unfolding Defs using MONO_def monI by (metis ClOpdual IF3 compl_def dNOR_def diff_def neg_C_def pA2 top_def)
lemma "∼ECQm ❙¬⇧C ∧ MT0 ❙¬⇧C ∧ MT1 ❙¬⇧C ∧ MT2 ❙¬⇧C ∧ MT3 ❙¬⇧C" nitpick[satisfy,card w=3] oops

subsection ‹Contraposition rules (CoP)›

text‹\noindent{CoPw-I}›
lemma "CoPw ❙¬⇧I" nitpick oops (*countermodel*)
lemma CoPw_I: "Fr_1b ℱ ⟹ CoPw ❙¬⇧I" unfolding Defs conn by (metis (no_types, lifting) MONO_def monI)
text‹\noindent{CoPw-C}›
lemma "CoPw ❙¬⇧C" nitpick oops (*countermodel*)
lemma CoPw_C: "Fr_6 ℱ ⟹ CoPw ❙¬⇧C" by (smt CoPw_def MONO_def monC conn)

text‹\noindent{We can indeed prove that XCoP is entailed by CoP1 (CoP2) in the particular case of a closure- (interior-)based negation.}›
lemma CoP1_XCoP: "CoP1 ❙¬⇧C ⟶  XCoP ❙¬⇧C" by (metis XCoP_def2 CoP1_def CoP1_def2 DM2_CoPw DM2_def ECQw_def TND_C TND_def TNDw_def top_def)
lemma CoP2_XCoP: "CoP2 ❙¬⇧I ⟶  XCoP ❙¬⇧I" by (smt XCoP_def2 CoP2_DM3 CoP2_def2 CoPw_def DM3_def DNE_def ECQ_I ECQ_def ECQw_def TNDw_def bottom_def join_def)

text‹\noindent{CoP1-I}›
lemma "𝔉 ℱ ⟹ CoP1 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TNDm ❙¬⇧I ∧ 𝔉 ℱ ∧ CoP1 ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{CoP1-C}›
lemma "𝔉 ℱ ⟹ CoP1 ❙¬⇧C" nitpick oops (*counter