Theory LatticeProperties.Conj_Disj

section ‹Conjunctive and Disjunctive Functions›

(*
    Author: Viorel Preoteasa
*)

theory Conj_Disj
imports Main
begin

text‹
This theory introduces the definitions and some properties for 
conjunctive, disjunctive, universally conjunctive, and universally 
disjunctive functions.
›

locale conjunctive =
  fixes inf_b :: "'b ⇒ 'b ⇒ 'b"
  and inf_c :: "'c ⇒ 'c ⇒ 'c"
  and times_abc :: "'a ⇒ 'b ⇒ 'c"
begin

definition
  "conjunctive = {x . (∀ y z . times_abc x (inf_b y z) = inf_c (times_abc x y) (times_abc x z))}"

lemma conjunctiveI:
  assumes "(⋀b c. times_abc a (inf_b b c) = inf_c (times_abc a b) (times_abc a c))"
  shows "a ∈ conjunctive"
  using assms by (simp add: conjunctive_def)

lemma conjunctiveD: "x ∈ conjunctive ⟹ times_abc x (inf_b y z) = inf_c (times_abc x y) (times_abc x z)"
  by (simp add: conjunctive_def)

end

interpretation Apply: conjunctive "inf::'a::semilattice_inf ⇒ 'a ⇒ 'a"
  "inf::'b::semilattice_inf ⇒ 'b ⇒ 'b" "λ f . f"
  done

interpretation Comp: conjunctive "inf::('a::lattice ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" 
  "inf::('a::lattice ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" "(o)"
  done

lemma "Apply.conjunctive = Comp.conjunctive"
  apply (simp add: Apply.conjunctive_def Comp.conjunctive_def)
  apply safe
  apply (simp_all add: fun_eq_iff inf_fun_def)
  apply (drule_tac x = "λ u . y" in spec)
  apply (drule_tac x = "λ u . z" in spec)
  by simp

locale disjunctive =
  fixes sup_b :: "'b ⇒ 'b ⇒ 'b"
  and sup_c :: "'c ⇒ 'c ⇒ 'c"
  and times_abc :: "'a ⇒ 'b ⇒ 'c"
begin

definition
  "disjunctive = {x . (∀ y z . times_abc x (sup_b y z) = sup_c (times_abc x y) (times_abc x z))}"

lemma disjunctiveI:
  assumes "(⋀b c. times_abc a (sup_b b c) = sup_c (times_abc a b) (times_abc a c))"
  shows "a ∈ disjunctive"
  using assms by (simp add: disjunctive_def)

lemma disjunctiveD: "x ∈ disjunctive ⟹ times_abc x (sup_b y z) = sup_c (times_abc x y) (times_abc x z)"
  by (simp add: disjunctive_def)

end

interpretation Apply: disjunctive "sup::'a::semilattice_sup ⇒ 'a ⇒ 'a"
  "sup::'b::semilattice_sup ⇒ 'b ⇒ 'b" "λ f . f"
  done

interpretation Comp: disjunctive "sup::('a::lattice ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" 
  "sup::('a::lattice ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" "(o)"
  done

lemma apply_comp_disjunctive: "Apply.disjunctive = Comp.disjunctive"
  apply (simp add: Apply.disjunctive_def Comp.disjunctive_def)
  apply safe
  apply (simp_all add: fun_eq_iff sup_fun_def)
  apply (drule_tac x = "λ u . y" in spec)
  apply (drule_tac x = "λ u . z" in spec)
  by simp

locale Conjunctive =
  fixes Inf_b :: "'b set ⇒ 'b"
  and Inf_c :: "'c set ⇒ 'c"
  and times_abc :: "'a ⇒ 'b ⇒ 'c"
begin

definition
  "Conjunctive = {x . (∀ X . times_abc x (Inf_b X) = Inf_c ((times_abc x) ` X) )}"

lemma ConjunctiveI:
  assumes "⋀A. times_abc a (Inf_b A) = Inf_c ((times_abc a) ` A)"
  shows "a ∈ Conjunctive"
  using assms by (simp add: Conjunctive_def)

lemma ConjunctiveD:
  assumes "a ∈ Conjunctive"
  shows "times_abc a (Inf_b A) = Inf_c ((times_abc a) ` A)"
  using assms by (simp add: Conjunctive_def)

end

interpretation Apply: Conjunctive Inf Inf "λ f . f"
  done

interpretation Comp: Conjunctive "Inf::(('a::complete_lattice ⇒ 'a) set) ⇒ ('a ⇒ 'a)" 
  "Inf::(('a::complete_lattice ⇒ 'a) set) ⇒ ('a ⇒ 'a)" "(o)"
  done

lemma "Apply.Conjunctive = Comp.Conjunctive"
proof
  show "Apply.Conjunctive ⊆ (Comp.Conjunctive :: ('a ⇒ 'a) set)"
  proof
    fix f
    assume "f ∈ (Apply.Conjunctive :: ('a ⇒ 'a) set)"
    then have *: "f (Inf A) = (INF a∈A. f a)" for A
      by (auto dest!: Apply.ConjunctiveD)
    show "f ∈ (Comp.Conjunctive :: ('a ⇒ 'a) set)"
    proof (rule Comp.ConjunctiveI)
      fix G :: "('a ⇒ 'a) set"
      from * have "f (INF f∈G. f a) = Inf (f ` (λf. f a) ` G)"
        for a :: 'a .
      then show "f ∘ Inf G = Inf (comp f ` G)"
        by (simp add: fun_eq_iff image_comp)
    qed
  qed
  show "Comp.Conjunctive ⊆ (Apply.Conjunctive :: ('a ⇒ 'a) set)"
  proof
    fix f
    assume "f ∈ (Comp.Conjunctive :: ('a ⇒ 'a) set)"
    then have *: "f ∘ Inf G = (INF g∈G. f ∘ g)" for G :: "('a ⇒ 'a) set"
      by (auto dest!: Comp.ConjunctiveD)
    show "f ∈ (Apply.Conjunctive :: ('a ⇒ 'a) set)"
    proof (rule Apply.ConjunctiveI)
      fix A :: "'a set"
      from * have "f ∘ (INF a∈A. (λb :: 'a. a)) = Inf ((∘) f ` (λa b. a) ` A)" .
      then show "f (Inf A) = Inf (f ` A)"
        by (simp add: fun_eq_iff image_comp)
    qed
  qed
qed  
        
locale Disjunctive =
  fixes Sup_b :: "'b set ⇒ 'b"
  and Sup_c :: "'c set ⇒ 'c"
  and times_abc :: "'a ⇒ 'b ⇒ 'c"
begin

definition
  "Disjunctive = {x . (∀ X . times_abc x (Sup_b X) = Sup_c ((times_abc x) ` X) )}"

lemma DisjunctiveI:
  assumes "⋀A. times_abc a (Sup_b A) = Sup_c ((times_abc a) ` A)"
  shows "a ∈ Disjunctive"
  using assms by (simp add: Disjunctive_def)

lemma DisjunctiveD: "x ∈ Disjunctive ⟹ times_abc x (Sup_b X) = Sup_c ((times_abc x) ` X)"
  by (simp add: Disjunctive_def)

end

interpretation Apply: Disjunctive Sup Sup "λ f . f"
  done

interpretation Comp: Disjunctive "Sup::(('a::complete_lattice ⇒ 'a) set) ⇒ ('a ⇒ 'a)" 
  "Sup::(('a::complete_lattice ⇒ 'a) set) ⇒ ('a ⇒ 'a)" "(o)"
  done

lemma "Apply.Disjunctive = Comp.Disjunctive"
proof
  show "Apply.Disjunctive ⊆ (Comp.Disjunctive :: ('a ⇒ 'a) set)"
  proof
    fix f
    assume "f ∈ (Apply.Disjunctive :: ('a ⇒ 'a) set)"
    then have *: "f (Sup A) = (SUP a∈A. f a)" for A
      by (auto dest!: Apply.DisjunctiveD)
    show "f ∈ (Comp.Disjunctive :: ('a ⇒ 'a) set)"
    proof (rule Comp.DisjunctiveI)
      fix G :: "('a ⇒ 'a) set"
      from * have "f (SUP f∈G. f a) = Sup (f ` (λf. f a) ` G)"
        for a :: 'a .
      then show "f ∘ Sup G = Sup (comp f ` G)"
        by (simp add: fun_eq_iff image_comp)
    qed
  qed
  show "Comp.Disjunctive ⊆ (Apply.Disjunctive :: ('a ⇒ 'a) set)"
  proof
    fix f
    assume "f ∈ (Comp.Disjunctive :: ('a ⇒ 'a) set)"
    then have *: "f ∘ Sup G = (SUP g∈G. f ∘ g)" for G :: "('a ⇒ 'a) set"
      by (auto dest!: Comp.DisjunctiveD)
    show "f ∈ (Apply.Disjunctive :: ('a ⇒ 'a) set)"
    proof (rule Apply.DisjunctiveI)
      fix A :: "'a set"
      from * have "f ∘ (SUP a∈A. (λb :: 'a. a)) = Sup ((∘) f ` (λa b. a) ` A)" .
      then show "f (Sup A) = Sup (f ` A)"
        by (simp add: fun_eq_iff image_comp)
    qed
  qed
qed  

lemma [simp]: "(F::'a::complete_lattice ⇒ 'b::complete_lattice) ∈ Apply.Conjunctive ⟹ F ∈ Apply.conjunctive"
  apply (simp add: Apply.Conjunctive_def Apply.conjunctive_def)
  apply safe
  apply (drule_tac x = "{y, z}" in spec)
  by simp

lemma [simp]: "F ∈ Apply.conjunctive ⟹ mono F"
  apply (simp add: Apply.conjunctive_def mono_def)
  apply safe
  apply (drule_tac x = "x" in spec)
  apply (drule_tac x = "y" in spec)
  apply (subgoal_tac "inf x y = x")
  apply simp
  apply (subgoal_tac "inf (F x) (F y) ≤ F y")
  apply simp
  apply (rule inf_le2)
  apply (rule antisym)
  by simp_all

lemma [simp]: "(F::'a::complete_lattice ⇒ 'b::complete_lattice) ∈ Apply.Conjunctive ⟹ F top = top"
  apply (simp add: Apply.Conjunctive_def)
  apply (drule_tac x="{}" in spec)
  by simp

lemma [simp]: "(F::'a::complete_lattice ⇒ 'b::complete_lattice) ∈ Apply.Disjunctive ⟹ F ∈ Apply.disjunctive"
  apply (simp add: Apply.Disjunctive_def Apply.disjunctive_def)
  apply safe
  apply (drule_tac x = "{y, z}" in spec)
  by simp

lemma [simp]: "F ∈ Apply.disjunctive ⟹ mono F"
  apply (simp add: Apply.disjunctive_def mono_def)
  apply safe
  apply (drule_tac x = "x" in spec)
  apply (drule_tac x = "y" in spec)
  apply (subgoal_tac "sup x y = y")
  apply simp
  apply (subgoal_tac "F x ≤ sup (F x) (F y)")
  apply simp
  apply (rule sup_ge1)
  apply (rule antisym)
  apply simp
  by (rule sup_ge2)

lemma [simp]: "(F::'a::complete_lattice ⇒ 'b::complete_lattice) ∈ Apply.Disjunctive ⟹ F bot = bot"
  apply (simp add: Apply.Disjunctive_def)
  apply (drule_tac x="{}" in spec)
  by simp

lemma weak_fusion: "h ∈ Apply.Disjunctive ⟹ mono f ⟹ mono g ⟹ 
    h o f ≤ g o h ⟹ h (lfp f) ≤ lfp g"
  apply (rule_tac P = "λ x . h x ≤ lfp g" in lfp_ordinal_induct, simp_all)
  apply (rule_tac y = "g (h S)" in order_trans)
  apply (simp add: le_fun_def)
  apply (rule_tac y = "g (lfp g)" in order_trans)
  apply (rule_tac f = g in monoD, simp_all)
  apply (simp add: lfp_unfold [symmetric])
  apply (simp add: Apply.DisjunctiveD)
  by (rule SUP_least, blast)

lemma inf_Disj: "(λ (x::'a::complete_distrib_lattice) . inf x y) ∈ Apply.Disjunctive"
  by (simp add: Apply.Disjunctive_def fun_eq_iff Sup_inf)

end