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  φ  φfp  (φc  id)" by (smt id_def EXP_def dual_def dual_symm equal_op_def conn)
lemma dEXP_fp: "dEXP φ  φfp  (φ  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