# 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)"

text‹\noindent{Distribution over joins or additivity (ADDI).}›
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
lemma MONO_ADDIb: "MONO φ = ADDI_b φ" proof -
have lr: "MONO φ ⟹ ADDI_b φ" by (smt ADDI_b_def MONO_def join_def)
have rl: "ADDI_b φ ⟹ MONO φ" proof -
assume addib: "ADDI_b φ"
{ 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
lemma ADDIb_MULTa: "ADDI_b φ = MULT_a φ" using MONO_ADDIb MONO_MULTa by auto

end