Theory SetSemilat

Up to index of Isabelle/HOL/arrays

(*  Title:      BV/SetSemilat.thy
    ID:         $Id: SetSemilat.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2002 TUM
*)

header "Power Sets are Semilattices"

theory SetSemilat = Semilat + Err:

text {* In fact, arbitrary sets are semilattices, as is trivial to see: *}
lemma "semilat (UNIV, op \<subseteq>, op \<union>)"
  by (unfold semilat_def supremum_def order_def plussub_def lesub_def) auto 

text {*
  Unfortunately, arbitrary sets do not satisfy the ascending chain
  condition @{term acc}, so we work with finite power sets.
*}
constdefs
  sl :: "'a set \<Rightarrow> 'a set err sl"
  "sl A \<equiv> Err.sl (esl (Pow A, op \<subseteq>, op \<union>))"

text {*
  The semilattice property is still easy:
*}
lemma semilat_set: "semilat (sl A)"
proof -
  have "semilat (Pow A, op \<subseteq>, op \<union>)"
    by (unfold semilat_def supremum_def closed_def 
               order_def lesub_def plussub_def) auto
  thus ?thesis by (unfold sl_def) fast
qed

text {*
  The ascending chain condition holds when @{term A} is finite, because then
  the size of @{term A} is an upper bound to the length of ascending chains.
*}
lemma acc_set:
  assumes finite: "finite A"
  shows "acc (op \<subseteq>) (Pow A)"
proof -
  let "?m x" = "card A - card (x::'a set)"
  let ?S = "{(y, x). x \<in> Pow A \<and> y \<in> Pow A \<and> x \<subset> y}"
  
  { fix a b 
    assume sub: "b \<subseteq> A" "a \<subseteq> A"
    with finite have "finite a" "finite b" by (blast dest: finite_subset)+
    moreover assume "b \<subset> a"
    ultimately 
    have "card b < card a" by - (rule psubset_card_mono) 
    moreover
    from finite sub 
    have "card b \<le> card A" "card a \<le> card A" by (blast dest: card_mono)+
    ultimately
    have "card A - card a < card A - card b" by arith      
  } 
  hence "{(y, x). x \<subseteq> A \<and> y \<subseteq> A \<and> x \<subset> y} \<subseteq> {(x, y). ?m x < ?m y}"
    by blast    
  hence "?S \<subseteq> measure (\<lambda>x. ?m x)" 
    by (simp add: measure_def inv_image_def)
  hence "wf ?S" 
    by (rule wf_measure [THEN wf_subset])
  thus ?thesis by (simp add: psubset_eq acc_def lesssub_def lesub_def)
qed

end

lemma

  semilat (UNIV, op <=, op Un)

lemma semilat_set:

  semilat (SetSemilat.sl A)

lemma

  finite A ==> acc op <= (Pow A)