Theory conditions_positive

theory conditions_positive
  imports boolean_algebra_operators
begin

section ‹Topological Conditions›

text‹We define and interrelate some useful axiomatic conditions on unary operations (operators) 
having a 'w-parametric type @{text "('w)σ⇒('w)σ"}.
Boolean algebras extended with such operators give us different sorts of topological Boolean algebras.›

subsection ‹Positive Conditions›

text‹Monotonicity (MONO).›
definition MONO::"('w σ ⇒ 'w σ) ⇒ bool" (‹MONO›)
  where "MONO φ ≡ ∀A B. A ❙≤ B ⟶ φ A ❙≤ φ B"

named_theorems cond (*to group together axiomatic conditions*)
declare MONO_def[cond]

text‹MONO is self-dual.›
lemma MONO_dual: "MONO φ = MONO φ⇧d" by (smt (verit) BA_cp MONO_def dual_invol op_dual_def)


text‹Expansive/extensive (EXPN) and its dual contractive (CNTR).›
definition EXPN::"('w σ ⇒ 'w σ) ⇒ bool" (‹EXPN›)
  where "EXPN φ  ≡ ∀A. A ❙≤ φ A"
definition CNTR::"('w σ ⇒ 'w σ) ⇒ bool" (‹CNTR›)
  where "CNTR φ ≡ ∀A. φ A ❙≤ A"

declare EXPN_def[cond] CNTR_def[cond]

text‹EXPN and CNTR are dual to each other.›
lemma EXPN_CNTR_dual1: "EXPN φ = CNTR φ⇧d" unfolding cond by (metis BA_cp BA_dn op_dual_def setequ_ext)
lemma EXPN_CNTR_dual2: "CNTR φ = EXPN φ⇧d" by (simp add: EXPN_CNTR_dual1 dual_invol)


text‹Normality (NORM) and its dual (DNRM).›
definition NORM::"('w σ ⇒ 'w σ) ⇒ bool" (‹NORM›)
  where "NORM φ  ≡ (φ ❙⊥) ❙= ❙⊥"
definition DNRM::"('w σ ⇒ 'w σ) ⇒ bool" (‹DNRM›)
  where "DNRM φ ≡ (φ ❙⊤) ❙= ❙⊤" 

declare NORM_def[cond] DNRM_def[cond]

text‹NORM and DNRM are dual to each other.›
lemma NOR_dual1: "NORM φ = DNRM φ⇧d" unfolding cond by (simp add: bottom_def compl_def op_dual_def setequ_def top_def)
lemma NOR_dual2: "DNRM φ = NORM φ⇧d" by (simp add: NOR_dual1 dual_invol) 

text‹EXPN (CNTR) entails DNRM (NORM).›
lemma EXPN_impl_DNRM: "EXPN φ ⟶ DNRM φ" unfolding cond by (simp add: setequ_def subset_def top_def)
lemma CNTR_impl_NORM: "CNTR φ ⟶ NORM φ" by (simp add: EXPN_CNTR_dual2 EXPN_impl_DNRM NOR_dual1 dual_invol)


text‹Idempotence (IDEM).›
definition IDEM::"('w σ ⇒ 'w σ) ⇒ bool" (‹IDEM›) 
  where "IDEM φ  ≡ ∀A. φ(φ A) ❙= (φ A)"
definition IDEM_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹IDEM⇧a›) 
  where "IDEM⇧a φ ≡ ∀A. φ(φ A) ❙≤ (φ A)"
definition IDEM_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹IDEM⇧b›) 
  where "IDEM⇧b φ ≡ ∀A.  (φ A) ❙≤ φ(φ A)"

declare IDEM_def[cond] IDEM_a_def[cond] IDEM_b_def[cond]

text‹IDEM-a and IDEM-b are dual to each other.›
lemma IDEM_dual1: "IDEM⇧a φ = IDEM⇧b φ⇧d" unfolding cond by (metis (mono_tags, opaque_lifting) BA_cp BA_dn op_dual_def setequ_ext)
lemma IDEM_dual2: "IDEM⇧b φ = IDEM⇧a φ⇧d" by (simp add: IDEM_dual1 dual_invol)

lemma IDEM_char: "IDEM φ = (IDEM⇧a φ ∧ IDEM⇧b φ)" unfolding cond setequ_char by blast
lemma IDEM_dual: "IDEM φ = IDEM φ⇧d" using IDEM_char IDEM_dual1 IDEM_dual2 by blast


text‹EXPN (CNTR) entail IDEM-b (IDEM-a).›
lemma EXPN_impl_IDEM_b: "EXPN φ ⟶ IDEM⇧b φ" by (simp add: EXPN_def IDEM_b_def)
lemma CNTR_impl_IDEM_a: "CNTR φ ⟶ IDEM⇧a φ" by (simp add: CNTR_def IDEM_a_def)

text‹Moreover, IDEM has some other interesting characterizations. For example, via function composition:›
lemma IDEM_fun_comp_char: "IDEM φ = (φ = φ ∘ φ)" unfolding cond fun_comp_def by (metis setequ_ext)
text‹Or having the property of collapsing the range and the set of fixed-points of an operator:›
lemma IDEM_range_fp_char: "IDEM φ = (⟦φ _⟧ = fp φ)" unfolding cond range_def fixpoints_def by (metis setequ_ext)

text‹Distribution over joins or additivity (ADDI).›
definition ADDI::"('w σ ⇒ 'w σ) ⇒ bool" (‹ADDI›)
  where "ADDI φ   ≡ ∀A B. φ(A ❙∨ B) ❙= (φ A) ❙∨ (φ B)" 
definition ADDI_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹ADDI⇧a›)
  where "ADDI⇧a φ ≡ ∀A B. φ(A ❙∨ B) ❙≤ (φ A) ❙∨ (φ B)"
definition ADDI_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹ADDI⇧b›)
  where "ADDI⇧b φ ≡ ∀A B.  (φ A) ❙∨ (φ B) ❙≤ φ(A ❙∨ B)" 

text‹Distribution over meets or multiplicativity (MULT).›
definition MULT::"('w σ ⇒ 'w σ) ⇒ bool" (‹MULT›) 
  where "MULT φ   ≡ ∀A B. φ(A ❙∧ B) ❙= (φ A) ❙∧ (φ B)" 
definition MULT_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹MULT⇧a›)
  where "MULT⇧a φ ≡ ∀A B. φ(A ❙∧ B) ❙≤ (φ A) ❙∧ (φ B)" 
definition MULT_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹MULT⇧b›)
  where "MULT⇧b φ ≡ ∀A B. (φ A) ❙∧ (φ B) ❙≤ φ(A ❙∧ B)"

declare ADDI_def[cond] ADDI_a_def[cond] ADDI_b_def[cond]
        MULT_def[cond] MULT_a_def[cond] MULT_b_def[cond]

lemma ADDI_char: "ADDI φ = (ADDI⇧a φ ∧ ADDI⇧b φ)" unfolding cond using setequ_char by blast
lemma MULT_char: "MULT φ = (MULT⇧a φ ∧ MULT⇧b φ)" unfolding cond using setequ_char by blast

text‹MONO, MULT-a and ADDI-b are equivalent.›
lemma MONO_MULTa: "MULT⇧a φ = MONO φ" unfolding cond by (metis L10 L3 L4 L5 L8 setequ_char setequ_ext)
lemma MONO_ADDIb: "ADDI⇧b φ = MONO φ" unfolding cond by (metis (mono_tags, lifting) L7 L9 join_def setequ_ext subset_def)

text‹Below we prove several duality relationships between ADDI(a/b) and MULT(a/b).›

text‹Duality between MULT-a and ADDI-b (an easy corollary from the self-duality of MONO).›
lemma MULTa_ADDIb_dual1: "MULT⇧a φ = ADDI⇧b φ⇧d" by (metis MONO_ADDIb MONO_MULTa MONO_dual)
lemma MULTa_ADDIb_dual2: "ADDI⇧b φ = MULT⇧a φ⇧d" by (simp add: MULTa_ADDIb_dual1 dual_invol)
text‹Duality between ADDI-a and MULT-b.›
lemma ADDIa_MULTb_dual1: "ADDI⇧a φ = MULT⇧b φ⇧d" unfolding cond op_dual_def by (metis BA_cp BA_deMorgan1 BA_dn setequ_ext)
lemma ADDIa_MULTb_dual2: "MULT⇧b φ = ADDI⇧a φ⇧d" by (simp add: ADDIa_MULTb_dual1 dual_invol)
text‹Duality between ADDI and MULT.›
lemma ADDI_MULT_dual1: "ADDI φ = MULT φ⇧d" using ADDI_char ADDIa_MULTb_dual1 MULT_char MULTa_ADDIb_dual2 by blast
lemma ADDI_MULT_dual2: "MULT φ = ADDI φ⇧d" by (simp add: ADDI_MULT_dual1 dual_invol)


text‹We verify properties regarding closure over meets/joins for fixed-points.›

text‹MULT implies meet-closedness of the set of fixed-points (the converse requires additional assumptions).›
lemma MULT_meetclosed: "MULT φ ⟹ meet_closed (fp φ)" by (simp add: MULT_def fixpoints_def meet_closed_def setequ_ext)
lemma "meet_closed (fp φ) ⟹ MULT φ" nitpick oops ―‹ countermodel found: needs further assumptions. ›
lemma meetclosed_MULT: "MONO φ ⟹ CNTR φ ⟹ IDEM⇧b φ ⟹ meet_closed (fp φ) ⟹ MULT φ" by (smt (z3) CNTR_def IDEM_b_def MONO_MULTa MONO_def MULT_a_def MULT_def fixpoints_def meet_closed_def meet_def setequ_char setequ_ext subset_def)

text‹ADDI implies join-closedness of the set of fixed-points (the converse requires additional assumptions).›
lemma ADDI_joinclosed: "ADDI φ ⟹ join_closed (fp φ)" by (simp add: ADDI_def fixpoints_def join_closed_def setequ_ext)
lemma "join_closed (fp φ) ⟹ ADDI φ" nitpick oops ―‹ countermodel found: needs further assumptions ›
lemma joinclosed_ADDI: "MONO φ ⟹ EXPN φ ⟹ IDEM⇧a φ ⟹ join_closed (fp φ) ⟹ ADDI φ" by (smt (verit, ccfv_threshold) ADDI_MULT_dual1 BA_deMorgan2 EXPN_CNTR_dual1 IDEM_dual1 MONO_dual fp_dual join_closed_def meet_closed_def meetclosed_MULT sdfun_dcompl_def setequ_ext)

text‹Assuming MONO, we have that EXPN (CNTR) implies meet-closed (join-closed) for the set of fixed-points.›
lemma EXPN_meetclosed: "MONO φ ⟹ EXPN φ ⟹ meet_closed (fp φ)" by (smt (verit) EXPN_def MONO_MULTa MULT_a_def fixpoints_def meet_closed_def setequ_char setequ_ext)
lemma CNTR_joinclosed: "MONO φ ⟹ CNTR φ ⟹ join_closed (fp φ)" by (smt (verit, best) ADDI_b_def CNTR_def MONO_ADDIb fixpoints_def join_closed_def setequ_char setequ_ext)

text‹Further assuming IDEM the above results can be stated to the whole range of an operator.›
lemma "MONO φ ⟹ EXPN φ ⟹ IDEM φ ⟹ meet_closed (⟦φ _⟧)" by (simp add: EXPN_meetclosed IDEM_range_fp_char)
lemma "MONO φ ⟹ CNTR φ ⟹ IDEM φ ⟹ join_closed (⟦φ _⟧)" by (simp add: CNTR_joinclosed IDEM_range_fp_char) 

end