# Theory Conj_Disj

Up to index of Isabelle/HOL/LatticeProperties

theory Conj_Disj
imports Main
`header {* Conjunctive and Disjunctive Functions *}(*    Author: Viorel Preoteasa*)theory Conj_Disjimports Mainbegintext{*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"begindefinition  "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)endinterpretation Apply: conjunctive "inf::'a::semilattice_inf => 'a => 'a"  "inf::'b::semilattice_inf => 'b => 'b" "λ f . f"  doneinterpretation Comp: conjunctive "inf::('a::lattice => 'a) => ('a => 'a) => ('a => 'a)"   "inf::('a::lattice => 'a) => ('a => 'a) => ('a => 'a)" "(op o)"  donelemma "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 simplocale disjunctive =  fixes sup_b :: "'b => 'b => 'b"  and sup_c :: "'c => 'c => 'c"  and times_abc :: "'a => 'b => 'c"begindefinition  "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)endinterpretation Apply: disjunctive "sup::'a::semilattice_sup => 'a => 'a"  "sup::'b::semilattice_sup => 'b => 'b" "λ f . f"  doneinterpretation Comp: disjunctive "sup::('a::lattice => 'a) => ('a => 'a) => ('a => 'a)"   "sup::('a::lattice => 'a) => ('a => 'a) => ('a => 'a)" "(op o)"  donelemma 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 simplocale Conjunctive =  fixes Inf_b :: "'b set => 'b"  and Inf_c :: "'c set => 'c"  and times_abc :: "'a => 'b => 'c"begindefinition  "Conjunctive = {x . (∀ X . times_abc x (Inf_b X) = Inf_c ((times_abc x) ` X) )}"endinterpretation Apply: Conjunctive Inf Inf "λ f . f"  doneinterpretation Comp: Conjunctive "Inf::(('a::complete_lattice => 'a) set) => ('a => 'a)"   "Inf::(('a::complete_lattice => 'a) set) => ('a => 'a)" "(op o)"  donelemma fun_eq: "x = y ==> f x = f y"  by simplemma "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 autolocale Disjunctive =  fixes Sup_b :: "'b set => 'b"  and Sup_c :: "'c set => 'c"  and times_abc :: "'a => 'b => 'c"begindefinition  "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)endinterpretation Apply: Disjunctive Sup Sup "λ f . f"  doneinterpretation Comp: Disjunctive "Sup::(('a::complete_lattice => 'a) set) => ('a => 'a)"   "Sup::(('a::complete_lattice => 'a) set) => ('a => 'a)" "(op o)"  donelemma 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 autolemma [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 simplemma [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_alllemma [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 simplemma [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 simplemma [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 simplemma 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`