Theory 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 aA. 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 fG. 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 gG. 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 aA. (λ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 aA. 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 fG. 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 gG. 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 aA. (λ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