Theory conditions_relativized_infinitary

theory conditions_relativized_infinitary
  imports conditions_relativized conditions_negative_infinitary
begin   

subsection ‹Infinitary Relativized Conditions›

text‹We define and interrelate infinitary variants for some previously introduced
 axiomatic conditions on operators.›

definition iADDIr::"('w σ ⇒ 'w σ) ⇒ bool" (‹iADDIr›)
  where "iADDIr φ  ≡ ∀S. let U=❙⋁S in (φ(❙⋁S) ❙=⇧U ❙⋁⟦φ S⟧)"
definition iADDIr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹iADDIr⇧^a›)
  where "iADDIr⇧^a φ ≡ ∀S. let U=❙⋁S in (φ(❙⋁S) ❙≤⇧U ❙⋁⟦φ S⟧)" 
definition iADDIr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹iADDIr⇧^b›)
  where "iADDIr⇧^b φ ≡ ∀S. let U=❙⋁S in (❙⋁⟦φ S⟧ ❙≤⇧U φ(❙⋁S))" 

definition inADDIr::"('w σ ⇒ 'w σ) ⇒ bool" (‹inADDIr›)
  where "inADDIr φ  ≡ ∀S. let U=❙⋁S in (φ(❙⋁S) ❙=⇧U ❙⋀⟦φ S⟧)"
definition inADDIr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹inADDIr⇧^a›)
  where "inADDIr⇧^a φ ≡ ∀S. let U=❙⋁S in (❙⋀⟦φ S⟧ ❙≤⇧U φ(❙⋁S))"  
definition inADDIr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹inADDIr⇧^b›)
  where "inADDIr⇧^b φ ≡ ∀S. let U=❙⋁S in (φ(❙⋁S) ❙≤⇧U ❙⋀⟦φ S⟧)" 

declare iADDIr_def[cond] iADDIr_a_def[cond] iADDIr_b_def[cond]
        inADDIr_def[cond] inADDIr_a_def[cond] inADDIr_b_def[cond]

definition iMULTr::"('w σ ⇒ 'w σ) ⇒ bool" (‹iMULTr›)
  where "iMULTr φ  ≡ ∀S. let U=❙⋀S in (φ(❙⋀S) ❙=⇩U ❙⋀⟦φ S⟧)"
definition iMULTr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹iMULTr⇧^a›)
  where "iMULTr⇧^a φ ≡ ∀S. let U=❙⋀S in (φ(❙⋀S) ❙≤⇩U ❙⋀⟦φ S⟧)"
definition iMULTr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹iMULTr⇧^b›)
  where "iMULTr⇧^b φ ≡ ∀S. let U=❙⋀S in (❙⋀⟦φ S⟧ ❙≤⇩U φ(❙⋀S))"

definition inMULTr::"('w σ ⇒ 'w σ) ⇒ bool" (‹inMULTr›)
  where "inMULTr φ  ≡ ∀S. let U=❙⋀S in (φ(❙⋀S) ❙=⇩U ❙⋁⟦φ S⟧)"
definition inMULTr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹inMULTr⇧^a›)
  where "inMULTr⇧^a φ ≡ ∀S. let U=❙⋀S in (❙⋁⟦φ S⟧ ❙≤⇩U φ(❙⋀S))"
definition inMULTr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹inMULTr⇧^b›)
  where "inMULTr⇧^b φ ≡ ∀S. let U=❙⋀S in (φ(❙⋀S) ❙≤⇩U ❙⋁⟦φ S⟧)"

declare iMULTr_def[cond] iMULTr_a_def[cond] iMULTr_b_def[cond]
        inMULTr_def[cond] inMULTr_a_def[cond] inMULTr_b_def[cond]

lemma iADDIr_char: "iADDIr φ = (iADDIr⇧^a φ ∧ iADDIr⇧^b φ)" unfolding cond setequ_char setequ_out_char subset_out_char by (meson setequ_char)
lemma iMULTr_char: "iMULTr φ = (iMULTr⇧^a φ ∧ iMULTr⇧^b φ)" unfolding cond setequ_char setequ_in_char subset_in_char by (meson setequ_char)

lemma inADDIr_char: "inADDIr φ = (inADDIr⇧^a φ ∧ inADDIr⇧^b φ)" unfolding cond setequ_char setequ_out_char subset_out_char by (meson setequ_char)
lemma inMULTr_char: "inMULTr φ = (inMULTr⇧^a φ ∧ inMULTr⇧^b φ)" unfolding cond setequ_char setequ_in_char subset_in_char by (meson setequ_char)


text‹Dual interrelations.›
lemma iADDIr_dual1: "iADDIr⇧^a φ = iMULTr⇧^b φ⇧^d" unfolding cond by (smt (z3) BA_cmpl_equ BA_cp BA_deMorgan2 dual_invol iDM_a iDM_b im_prop1 op_dual_def setequ_ext subset_in_char subset_out_char)
lemma iADDIr_dual2: "iADDIr⇧^b φ = iMULTr⇧^a φ⇧^d" unfolding cond by (smt (z3) BA_cmpl_equ BA_cp BA_deMorgan2 dual_invol iDM_a iDM_b im_prop1 op_dual_def setequ_ext subset_in_char subset_out_char)
lemma iADDIr_dual:  "iADDIr φ = iMULTr φ⇧^d" using iADDIr_char iADDIr_dual1 iADDIr_dual2 iMULTr_char by blast

lemma inADDIr_dual1: "inADDIr⇧^a φ = inMULTr⇧^b φ⇧^d" unfolding cond by (smt (z3) BA_cmpl_equ compl_def dual_invol iDM_a iDM_b im_prop3 op_dual_def setequ_ext subset_in_def subset_in_out)
lemma inADDIr_dual2: "inADDIr⇧^b φ = inMULTr⇧^a φ⇧^d" unfolding cond by (smt (z3) BA_cmpl_equ compl_def dual_invol iDM_a iDM_b im_prop3 op_dual_def setequ_ext subset_in_def subset_in_out)
lemma inADDIr_dual:  "inADDIr φ = inMULTr φ⇧^d" using inADDIr_char inADDIr_dual1 inADDIr_dual2 inMULTr_char by blast

text‹Complement interrelations.›
lemma iADDIr_a_cmpl: "iADDIr⇧^a φ = inADDIr⇧^a φ⇧^-" unfolding cond by (smt (z3) compl_def dualcompl_invol iDM_b im_prop2 setequ_ext subset_out_def svfun_compl_def)
lemma iADDIr_b_cmpl: "iADDIr⇧^b φ = inADDIr⇧^b φ⇧^-" unfolding cond by (smt (z3) compl_def iDM_b im_prop2 setequ_ext sfun_compl_invol subset_out_def svfun_compl_def)
lemma iADDIr_cmpl: "iADDIr φ = inADDIr φ⇧^-" by (simp add: iADDIr_a_cmpl iADDIr_b_cmpl iADDIr_char inADDIr_char)

lemma iMULTr_a_cmpl: "iMULTr⇧^a φ = inMULTr⇧^a φ⇧^-" unfolding cond by (smt (z3) compl_def iDM_b im_prop2 setequ_ext subset_in_def svfun_compl_def)
lemma iMULTr_b_cmpl: "iMULTr⇧^b φ = inMULTr⇧^b φ⇧^-" unfolding cond by (smt (z3) compl_def dualcompl_invol iDM_a im_prop2 setequ_ext subset_in_def svfun_compl_def)
lemma iMULTr_cmpl: "MULTr φ = nMULTr φ⇧^-" by (simp add: MULTr_a_cmpl MULTr_b_cmpl MULTr_char nMULTr_char)

text‹Fixed-point interrelations.›
lemma iADDIr_a_fpc: "iADDIr⇧^a φ = iADDIr⇧^a φ⇧^f⇧^p⇧^-" unfolding cond subset_out_def image_def ofp_fixpoint_compl_def supremum_def sdiff_def by (smt (verit))
lemma iADDIr_a_fp: "iADDIr⇧^a φ = inADDIr⇧^a φ⇧^f⇧^p" by (metis iADDIr_a_cmpl iADDIr_a_fpc sfun_compl_invol)
lemma iADDIr_b_fpc: "iADDIr⇧^b φ = iADDIr⇧^b φ⇧^f⇧^p⇧^-" unfolding cond subset_out_def image_def ofp_fixpoint_compl_def supremum_def sdiff_def by (smt (verit))
lemma iADDIr_b_fp: "iADDIr⇧^b φ = inADDIr⇧^b φ⇧^f⇧^p" by (metis iADDIr_b_cmpl iADDIr_b_fpc sfun_compl_invol)

lemma iMULTr_a_fp: "iMULTr⇧^a φ = iMULTr⇧^a φ⇧^f⇧^p" unfolding cond subset_in_def image_def by (smt (z3) dimpl_def infimum_def ofp_invol op_fixpoint_def)
lemma iMULTr_a_fpc: "iMULTr⇧^a φ = inMULTr⇧^a φ⇧^f⇧^p⇧^-" using iMULTr_a_cmpl iMULTr_a_fp by blast
lemma iMULTr_b_fp: "iMULTr⇧^b φ = iMULTr⇧^b φ⇧^f⇧^p" unfolding cond subset_in_def image_def dimpl_def infimum_def op_fixpoint_def by (smt (verit))
lemma iMULTr_b_fpc: "iMULTr⇧^b φ = inMULTr⇧^b φ⇧^f⇧^p⇧^-" using iMULTr_b_cmpl iMULTr_b_fp by blast

end