Theory Complete_Domain

(* Title:      Complete Domain
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Complete Domain›

theory Complete_Domain

imports Relative_Domain Complete_Tests

begin

class complete_antidomain_semiring = relative_antidomain_semiring + complete_tests +
  assumes a_dist_Sum: "ascending_chain f ⟶ -(Sum f) = Prod (λn . -f n)"
  assumes a_dist_Prod: "descending_chain f ⟶ -(Prod f) = Sum (λn . -f n)"
begin

lemma a_ascending_chain:
  "ascending_chain f ⟹ descending_chain (λn . -f n)"
  by (simp add: a_antitone ascending_chain_def descending_chain_def)

lemma a_descending_chain:
  "descending_chain f ⟹ ascending_chain (λn . -f n)"
  by (simp add: a_antitone ord.ascending_chain_def ord.descending_chain_def)

lemma d_dist_Sum:
  "ascending_chain f ⟹ d(Sum f) = Sum (λn . d(f n))"
  by (simp add: d_def a_ascending_chain a_dist_Prod a_dist_Sum)

lemma d_dist_Prod:
  "descending_chain f ⟹ d(Prod f) = Prod (λn . d(f n))"
  by (simp add: d_def a_dist_Sum a_dist_Prod a_descending_chain)

end

end