Theory conditions_negative

theory conditions_negative
  imports conditions_positive
begin

subsection ‹Negative Conditions›

text‹We continue defining and interrelating axiomatic conditions on unary operations (operators). 
  We now move to conditions commonly satisfied by negation-like logical operations.›

text‹Anti-tonicity (ANTI).›
definition ANTI::"('w σ ⇒ 'w σ) ⇒ bool" ("ANTI")
  where "ANTI φ ≡ ∀A B. A ❙≤ B ⟶ φ B ❙≤ φ A"

declare ANTI_def[cond]

text‹ANTI is self-dual.›
lemma ANTI_dual: "ANTI φ = ANTI φ⇧d" by (smt (verit) BA_cp ANTI_def dual_invol op_dual_def)
text‹ANTI is the 'complement' of MONO.›
lemma ANTI_MONO: "MONO φ = ANTI φ⇧-" by (metis ANTI_def BA_cp MONO_def svfun_compl_def)


text‹Anti-expansive/extensive (nEXPN) and its dual anti-contractive (nCNTR).›
definition nEXPN::"('w σ ⇒ 'w σ) ⇒ bool" ("nEXPN")
  where "nEXPN φ  ≡ ∀A. φ A ❙≤ ❙─A"
definition nCNTR::"('w σ ⇒ 'w σ) ⇒ bool" ("nCNTR")
  where "nCNTR φ ≡ ∀A. ❙─A ❙≤ φ A"

declare nEXPN_def[cond] nCNTR_def[cond]

text‹nEXPN and nCNTR are dual to each other.›
lemma nEXPN_nCNTR_dual1: "nEXPN φ = nCNTR φ⇧d" unfolding cond by (metis BA_cp BA_dn op_dual_def setequ_ext)
lemma nEXPN_nCNTR_dual2: "nCNTR φ = nEXPN φ⇧d" by (simp add: dual_invol nEXPN_nCNTR_dual1)

text‹nEXPN and nCNTR are the 'complements' of EXPN and CNTR respectively.›
lemma nEXPN_CNTR_compl: "EXPN φ = nEXPN φ⇧-" by (metis BA_cp EXPN_def nEXPN_def svfun_compl_def)
lemma nCNTR_EXPN_compl: "CNTR φ = nCNTR φ⇧-" by (metis EXPN_CNTR_dual2 dual_compl_char1 dual_compl_char2 nEXPN_CNTR_compl nEXPN_nCNTR_dual2)

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

declare nNORM_def[cond] nDNRM_def[cond]

text‹nNORM and nDNRM are dual to each other.›
lemma nNOR_dual1: "nNORM φ = nDNRM φ⇧d" unfolding cond by (simp add: bottom_def compl_def op_dual_def setequ_def top_def)
lemma nNOR_dual2: "nDNRM φ = nNORM φ⇧d" by (simp add: dual_invol nNOR_dual1) 

text‹nNORM and nDNRM are the 'complements' of NORM and DNRM respectively.›
lemma nNORM_NORM_compl: "NORM φ = nNORM φ⇧-" by (simp add: NORM_def bottom_def compl_def nNORM_def setequ_def svfun_compl_def top_def)
lemma nDNRM_DNRM_compl: "DNRM φ = nDNRM φ⇧-" by (simp add: DNRM_def bottom_def compl_def nDNRM_def setequ_def svfun_compl_def top_def)

text‹nEXPN (nCNTR) entail nDNRM (nNORM).›
lemma nEXPN_impl_nDNRM: "nEXPN φ ⟶ nDNRM φ" unfolding cond by (metis bottom_def compl_def setequ_def subset_def top_def)
lemma nCNTR_impl_nNORM: "nCNTR φ ⟶ nNORM φ" by (simp add: nEXPN_impl_nDNRM nEXPN_nCNTR_dual2 nNOR_dual1)


text‹Anti-Idempotence (nIDEM).›
definition nIDEM::"('w σ ⇒ 'w σ) ⇒ bool" ("nIDEM") 
  where "nIDEM φ  ≡ ∀A. φ(❙─(φ A)) ❙= (φ A)"
definition nIDEM_a::"('w σ ⇒ 'w σ) ⇒ bool" ("nIDEM⇧a") 
  where "nIDEM_a φ ≡ ∀A. (φ A) ❙≤ φ(❙─(φ A))"
definition nIDEM_b::"('w σ ⇒ 'w σ) ⇒ bool" ("nIDEM⇧b") 
  where "nIDEM_b φ ≡ ∀A. φ(❙─(φ A)) ❙≤ (φ A)"

declare nIDEM_def[cond] nIDEM_a_def[cond] nIDEM_b_def[cond]

text‹nIDEM-a and nIDEM-b are dual to each other.›
lemma nIDEM_dual1: "nIDEM⇧a φ = nIDEM⇧b φ⇧d" unfolding cond by (metis BA_cp BA_dn op_dual_def setequ_ext)
lemma nIDEM_dual2: "nIDEM⇧b φ = nIDEM⇧a φ⇧d" by (simp add: dual_invol nIDEM_dual1)

lemma nIDEM_char: "nIDEM φ = (nIDEM⇧a φ ∧ nIDEM⇧b φ)" unfolding cond setequ_char by blast
lemma nIDEM_dual: "nIDEM φ = nIDEM φ⇧d" using nIDEM_char nIDEM_dual1 nIDEM_dual2 by blast

text‹nIDEM(a/b) and IDEM(a/b) are the 'complements' each other.›
lemma nIDEM_a_compl: "IDEM⇧a φ = nIDEM⇧a φ⇧-" by (metis (no_types, lifting) BA_cp IDEM_a_def nIDEM_a_def sfun_compl_invol svfun_compl_def)
lemma nIDEM_b_compl: "IDEM⇧b φ = nIDEM⇧b φ⇧-" by (metis IDEM_dual2 dual_compl_char1 dual_compl_char2 nIDEM_a_compl nIDEM_dual2)
lemma nIDEM_compl: "nIDEM φ = IDEM φ⇧-" by (simp add: IDEM_char nIDEM_a_compl nIDEM_b_compl nIDEM_char sfun_compl_invol)

text‹nEXPN (nCNTR) entail nIDEM-a (nIDEM-b).›
lemma nEXPN_impl_nIDEM_a: "nEXPN φ ⟶ nIDEM⇧b φ" by (metis nEXPN_def nIDEM_b_def sfun_compl_invol svfun_compl_def)
lemma nCNTR_impl_nIDEM_b: "nCNTR φ ⟶ nIDEM⇧a φ" by (simp add: nEXPN_impl_nIDEM_a nEXPN_nCNTR_dual2 nIDEM_dual1)


text‹Anti-distribution over joins or anti-additivity (nADDI) and its dual.›
definition nADDI::"('w σ ⇒ 'w σ) ⇒ bool" ("nADDI")
  where "nADDI φ  ≡ ∀A B. φ(A ❙∨ B) ❙= (φ A) ❙∧ (φ B)" 
definition nADDI_a::"('w σ ⇒ 'w σ) ⇒ bool" ("nADDI⇧a")
  where "nADDI⇧a φ ≡ ∀A B. (φ A) ❙∧ (φ B) ❙≤ φ(A ❙∨ B)" 
definition nADDI_b::"('w σ ⇒ 'w σ) ⇒ bool" ("nADDI⇧b")
  where "nADDI⇧b φ ≡ ∀A B. φ(A ❙∨ B) ❙≤ (φ A) ❙∧ (φ B)"

text‹Anti-distribution over meets or anti-multiplicativity (nMULT).›
definition nMULT::"('w σ ⇒ 'w σ) ⇒ bool" ("nMULT") 
  where "nMULT φ  ≡ ∀A B. φ(A ❙∧ B) ❙= (φ A) ❙∨ (φ B)" 
definition nMULT_a::"('w σ ⇒ 'w σ) ⇒ bool" ("nMULT⇧a")
  where "nMULT⇧a φ ≡ ∀A B. (φ A) ❙∨ (φ B) ❙≤ φ(A ❙∧ B)"
definition nMULT_b::"('w σ ⇒ 'w σ) ⇒ bool" ("nMULT⇧b")
  where "nMULT⇧b φ ≡ ∀A B. φ(A ❙∧ B) ❙≤ (φ A) ❙∨ (φ B)" 

declare nADDI_def[cond] nADDI_a_def[cond] nADDI_b_def[cond]
        nMULT_def[cond] nMULT_a_def[cond] nMULT_b_def[cond]

lemma nADDI_char: "nADDI φ = (nADDI⇧a φ ∧ nADDI⇧b φ)" unfolding cond using setequ_char by blast
lemma nMULT_char: "nMULT φ = (nMULT⇧a φ ∧ nMULT⇧b φ)" unfolding cond using setequ_char by blast

text‹ANTI, nMULT-a and nADDI-b are equivalent.›
lemma ANTI_nMULTa: "nMULT⇧a φ = ANTI φ" unfolding cond by (smt (z3) L10 L7 join_def meet_def setequ_ext subset_def)
lemma ANTI_nADDIb: "nADDI⇧b φ = ANTI φ" unfolding cond by (smt (verit) BA_cp BA_deMorgan1 L10 L3 L5 L8 L9 setequ_char setequ_ext)

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

text‹Duality between nMULT-a and nADDI-b (an easy corollary from the self-duality of ANTI).›
lemma nMULTa_nADDIb_dual1: "nMULT⇧a φ = nADDI⇧b φ⇧d" using ANTI_nADDIb ANTI_nMULTa ANTI_dual by blast
lemma nMULTa_nADDIb_dual2: "nADDI⇧b φ = nMULT⇧a φ⇧d" by (simp add: dual_invol nMULTa_nADDIb_dual1)
text‹Duality between nADDI-a and nMULT-b.›
lemma nADDIa_nMULTb_dual1: "nADDI⇧a φ = nMULT⇧b φ⇧d" unfolding cond by (metis (no_types, lifting) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext)
lemma nADDIa_nMULTb_dual2: "nMULT⇧b φ = nADDI⇧a φ⇧d" by (simp add: dual_invol nADDIa_nMULTb_dual1)
text‹Duality between ADDI and MULT.›
lemma nADDI_nMULT_dual1: "nADDI φ = nMULT φ⇧d" using nADDI_char nADDIa_nMULTb_dual1 nMULT_char nMULTa_nADDIb_dual2 by blast
lemma nADDI_nMULT_dual2: "nMULT φ = nADDI φ⇧d" by (simp add: dual_invol nADDI_nMULT_dual1)

text‹nADDI and nMULT are the 'complements' of ADDI and MULT respectively.›
lemma nADDIa_compl: "ADDI⇧a φ = nADDI⇧a φ⇧-" by (metis ADDI_a_def BA_cp BA_deMorgan1 nADDI_a_def setequ_ext svfun_compl_def)
lemma nADDIb_compl: "ADDI⇧b φ = nADDI⇧b φ⇧-" by (simp add: ANTI_nADDIb ANTI_MONO MONO_ADDIb sfun_compl_invol)
lemma nADDI_compl: "ADDI φ = nADDI φ⇧-" by (simp add: ADDI_char nADDI_char nADDIa_compl nADDIb_compl)
lemma nMULTa_compl: "MULT⇧a φ = nMULT⇧a φ⇧-" by (simp add: ANTI_MONO ANTI_nMULTa MONO_MULTa sfun_compl_invol)
lemma nMULTb_compl: "MULT⇧b φ = nMULT⇧b φ⇧-" by (metis BA_cp BA_deMorgan2 MULT_b_def nMULT_b_def setequ_ext svfun_compl_def)
lemma nMULT_compl: "MULT φ = nMULT φ⇧-" by (simp add: MULT_char nMULT_char nMULTa_compl nMULTb_compl)


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

text‹nMULT for an operator implies join-closedness of the set of fixed-points of its dual-complement.›
lemma nMULT_joinclosed: "nMULT φ ⟹ join_closed (fp (φ⇧d⇧-))" by (smt (verit, del_insts) ADDI_MULT_dual2 ADDI_joinclosed BA_deMorgan1 MULT_def dual_compl_char2 nMULT_def setequ_ext svfun_compl_def)
lemma "join_closed (fp (φ⇧d⇧-)) ⟹ nMULT φ" nitpick oops ―‹ countermodel found: needs further assumptions ›
lemma joinclosed_nMULT: "ANTI φ ⟹ nCNTR φ ⟹ nIDEM⇧b φ ⟹ join_closed (fp (φ⇧d⇧-)) ⟹ nMULT φ" by (metis ANTI_MONO ANTI_dual IDEM_char IDEM_dual dual_compl_char1 dual_compl_char2 joinclosed_ADDI nADDI_compl nADDI_nMULT_dual2 nCNTR_impl_nIDEM_b nEXPN_CNTR_compl nEXPN_nCNTR_dual2 nIDEM_char nIDEM_compl sfun_compl_invol)

text‹nADDI for an operator implies meet-closedness of the set of fixed-points of its dual-complement.›
lemma nADDI_meetclosed: "nADDI φ ⟹ meet_closed (fp (φ⇧d⇧-))" by (smt (verit, ccfv_threshold) ADDI_MULT_dual1 ADDI_def BA_deMorgan2 MULT_meetclosed dual_compl_char2 nADDI_def setequ_ext svfun_compl_def)
lemma "meet_closed (fp (φ⇧d⇧-)) ⟹ nADDI φ" nitpick oops ―‹ countermodel found: needs further assumptions ›
lemma meetclosed_nADDI: "ANTI φ ⟹ nEXPN φ ⟹ nIDEM⇧a φ ⟹ meet_closed (fp (φ⇧d⇧-)) ⟹ nADDI φ" by (metis ADDI_MULT_dual2 ADDI_joinclosed ANTI_MONO ANTI_dual dual_compl_char1 dual_compl_char2 joinclosed_nMULT meetclosed_MULT nADDI_nMULT_dual1 nCNTR_EXPN_compl nEXPN_nCNTR_dual1 nIDEM_b_compl nIDEM_dual1 sfun_compl_invol)

text‹Assuming ANTI, we have that nEXPN (nCNTR) implies meet-closed (join-closed) for the set of fixed-points.›
lemma nEXPN_meetclosed: "ANTI φ ⟹ nEXPN φ ⟹ meet_closed (fp φ)" by (metis (full_types) L10 compl_def fixpoints_def meet_closed_def nEXPN_def setequ_ext subset_def)
lemma nCNTR_joinclosed: "ANTI φ ⟹ nCNTR φ ⟹ join_closed (fp φ)" by (smt (verit, ccfv_threshold) BA_impl L9 fixpoints_def impl_char join_closed_def nCNTR_def setequ_char setequ_ext)

end