Theory Conj_Disj

header {* 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 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)" "(op 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 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)" "(op 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) )}"
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)" "(op o)"
  done

lemma fun_eq: "x = y ==> f x = f y"
  by simp

lemma "Apply.Conjunctive = Comp.Conjunctive"
  apply (simp add: Apply.Conjunctive_def Comp.Conjunctive_def)
  apply safe
  apply (simp add: fun_eq_iff  Inf_fun_def comp_def image_def)
  apply (simp only: INF_def)
  apply safe
  apply (rule_tac f = Inf in fun_eq)
  apply auto
  apply (drule_tac x = "{x . ∃ y ∈ X . x = (λ u . y)}" in spec)
  apply (simp add: fun_eq_iff  Inf_fun_def comp_def image_def)
  apply (drule_tac x = "bot" in spec)
  apply (subgoal_tac "{y::'a. ∃f . (∃y ∈ X. ∀x::'a . f x = y) ∧ y = f bot} = X ∧ 
      {y::'a. ∃f. (∃xa. (∃y ∈ X. ∀x::'a. xa x = y) ∧ 
      (∀xb::'a. f xb = x (xa xb))) ∧ y = f bot} = {y::'a. ∃xa::'a∈X. y = x xa}")
  apply (simp add: INF_def image_def, safe)
  apply simp_all
  apply auto[1]
  apply auto [1]
  apply (rule_tac x = "λ u . x xaa" in exI)
  by auto

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 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)" "(op o)"
  done

lemma apply_comp_Disjunctive: "Apply.Disjunctive = Comp.Disjunctive"
  apply (simp add: Apply.Disjunctive_def Comp.Disjunctive_def)
  apply safe
  apply (simp add: fun_eq_iff  Sup_fun_def comp_def image_def)
  apply (simp only: SUP_def)
  apply safe
  apply (rule_tac f = Sup in fun_eq)
  apply auto
  apply (drule_tac x = "{x . ∃ y ∈ X . x = (λ u . y)}" in spec)
  apply (simp add: fun_eq_iff  Sup_fun_def comp_def image_def)
  apply (drule_tac x = "bot" in spec)
  apply (subgoal_tac "{y. ∃f::'a => 'a. (∃y∈X. ∀x. f x = y) ∧ y = f bot} = X 
    ∧ {y. ∃f::'a => 'a. (∃xa. (∃y∈X. ∀x. xa x = y) ∧ (∀xb. f xb = x (xa xb))) ∧ y = f bot} = {y. ∃xa∈X. y = x xa}")
  apply (simp add: SUP_def image_def, safe)
  apply simp_all
  apply auto[1]
  apply auto [1]
  apply (rule_tac x = "λ u . x xaa" in exI)
  by auto


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 (rule lfp_lemma2, simp)
  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 SUP_def)

end