# 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
```