Theory SetSemilat

Up to index of Isabelle/HOL/verificard

(*  Title:      BV/SetSemilat.thy
    ID:         $Id: SetSemilat.thy,v 1.1.2.3 2002/07/11 17:54:41 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: "finite A \<Longrightarrow> acc (op \<subseteq>) (Pow A)"
  apply (unfold acc_def lesssub_def lesub_def)
  apply (simp add: psubset_eq [symmetric])
  apply (rule wf_measure [of "\<lambda>x. card A - card x", THEN wf_subset])
  apply (simp add: measure_def inv_image_def)
  apply clarify
  apply (frule finite_subset, assumption)
  apply (frule finite_subset) back 
   apply assumption
  apply (frule psubset_card_mono, assumption)
  apply (frule card_mono, assumption)
  apply (drule card_mono) 
   apply assumption back
  apply arith
  done

end

lemma

  semilat (UNIV, op <=, op Un)

lemma semilat_set:

  semilat (SetSemilat.sl A)

lemma acc_set:

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