Quelle Bounded_Set.thy Sprache: Isabelle

(*  Title:      HOL/Cardinals/Bounded_Set.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Copyright   2015

Bounded powerset type.
*)

section \<open>Sets Strictly Bounded by an Infinite Cardinal\<close>

theory Bounded_Set
imports Cardinals
begin

typedef ('a, 'k) bset (\<open>_ set[_]\<close> [22, 21] 21) =
  "{A :: 'a set. |A|
  morphisms set_bset Abs_bset
  by (rule exI[of _ "{}"]) (auto simp: card_of_empty4 csum_def)

setup_lifting type_definition_bset

lift_definition map_bset ::
  "('a \ 'b) \ 'a set['k] \ 'b set['k]" is image
  using card_of_image ordLeq_ordLess_trans by blast

lift_definition rel_bset ::
  "('a \ 'b \ bool) \ 'a set['k] \ 'b set['k] \ bool" is rel_set
  .

lift_definition bempty :: "'a set['k]" is "{}"
  by (auto simp: card_of_empty4 csum_def)

lift_definition binsert :: "'a \ 'a set['k] \ 'a set['k]" is "insert"
  using infinite_card_of_insert ordIso_ordLess_trans Field_card_of Field_natLeq UNIV_Plus_UNIV
   csum_def finite_Plus_UNIV_iff finite_insert finite_ordLess_infinite2 infinite_UNIV_nat by metis

definition bsingleton where
  "bsingleton x = binsert x bempty"

lemma set_bset_to_set_bset: "|A|
  set_bset (the_inv set_bset A :: 'a set['k]) = A"
  apply (rule f_the_inv_into_f[unfolded inj_on_def])
  apply (simp add: set_bset_inject range_eqI Abs_bset_inverse[symmetric])
  apply (rule range_eqI Abs_bset_inverse[symmetric] CollectI)+
  .

lemma rel_bset_aux_infinite:
  fixes a :: "'a set['k]" and b :: "'b set['k]"
  shows "(\t \ set_bset a. \u \ set_bset b. R t u) \ (\u \ set_bset b. \t \ set_bset a. R t u) \
   ((BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset fst))\<inverse>\<inverse> OO
    BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset snd)) a b" (is "?L \<longleftrightarrow> ?R")
proof
  assume ?L
  define R' :: "('a \<times> 'b) set['k]"
    where "R' = the_inv set_bset (Collect (case_prod R) \ (set_bset a \ set_bset b))"
      (is "_ = the_inv set_bset ?L'")
  have "|?L'|
    unfolding csum_def Field_natLeq
    by (intro ordLeq_ordLess_trans[OF card_of_mono1[OF Int_lower2]]
      card_of_Times_ordLess_infinite)
      (simp, (transfer, simp add: csum_def Field_natLeq)+)
  hence *: "set_bset R' = ?L'" unfolding R'_def by (intro set_bset_to_set_bset)
  show ?R unfolding Grp_def relcompp.simps conversep.simps
  proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    from * show "a = map_bset fst R'" using conjunct1[OF \<open>?L\<close>]
      by (transfer, auto simp add: image_def Int_def split: prod.splits)
    from * show "b = map_bset snd R'" using conjunct2[OF \<open>?L\<close>]
      by (transfer, auto simp add: image_def Int_def split: prod.splits)
  qed (auto simp add: *)
next
  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
    by transfer force
qed

bnf "'a set['k]"
  map: map_bset
  sets: set_bset
  bd: "natLeq +c card_suc |UNIV :: 'k set|"
  wits: bempty
  rel: rel_bset
proof -
  show "map_bset id = id" by (rule ext, transfer) simp
next
  fix f g
  show "map_bset (f o g) = map_bset f o map_bset g" by (rule ext, transfer) auto
next
  fix X f g
  assume "\z. z \ set_bset X \ f z = g z"
  then show "map_bset f X = map_bset g X" by transfer force
next
  fix f
  show "set_bset \ map_bset f = (`) f \ set_bset" by (rule ext, transfer) auto
next
  fix X :: "'a set['k]"
  have "|set_bset X| by transfer blast
  then show "|set_bset X|
    by (rule ordLess_ordLeq_trans[OF _ csum_mono2[OF ordLess_imp_ordLeq[OF card_suc_greater[OF card_of_card_order_on]]]])
next
  fix R S
  show "rel_bset R OO rel_bset S \ rel_bset (R OO S)"
    by (rule predicate2I, transfer) (auto simp: rel_set_OO[symmetric])
next
  fix R :: "'a \ 'b \ bool"
  show "rel_bset R = ((\x y. \z. set_bset z \ {(x, y). R x y} \
    map_bset fst z = x \<and> map_bset snd z = y) :: 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool)"
    by (simp add: rel_bset_def map_fun_def o_def rel_set_def
      rel_bset_aux_infinite[unfolded OO_Grp_alt])
next
  fix x
  assume "x \ set_bset bempty"
  then show False by transfer simp
qed (simp_all add: card_order_bd_fun Cinfinite_bd_fun regularCard_bd_fun)

lemma map_bset_bempty[simp]: "map_bset f bempty = bempty"
  by transfer auto

lemma map_bset_binsert[simp]: "map_bset f (binsert x X) = binsert (f x) (map_bset f X)"
  by transfer auto

lemma map_bset_bsingleton: "map_bset f (bsingleton x) = bsingleton (f x)"
  unfolding bsingleton_def by simp

lemma bempty_not_binsert: "bempty \ binsert x X" "binsert x X \ bempty"
  by (transfer, auto)+

lemma bempty_not_bsingleton[simp]: "bempty \ bsingleton x" "bsingleton x \ bempty"
  unfolding bsingleton_def by (simp_all add: bempty_not_binsert)

lemma bsingleton_inj[simp]: "bsingleton x = bsingleton y \ x = y"
  unfolding bsingleton_def by transfer auto

lemma rel_bsingleton[simp]:
  "rel_bset R (bsingleton x1) (bsingleton x2) = R x1 x2"
  unfolding bsingleton_def
  by transfer (auto simp: rel_set_def)

lemma rel_bset_bsingleton[simp]:
  "rel_bset R (bsingleton x1) = (\X. X \ bempty \ (\x2\set_bset X. R x1 x2))"
  "rel_bset R X (bsingleton x2) = (X \ bempty \ (\x1\set_bset X. R x1 x2))"
  unfolding bsingleton_def fun_eq_iff
  by (transfer, force simp add: rel_set_def)+

lemma rel_bset_bempty[simp]:
  "rel_bset R bempty X = (X = bempty)"
  "rel_bset R Y bempty = (Y = bempty)"
  by (transfer, simp add: rel_set_def)+

definition bset_of_option where
  "bset_of_option = case_option bempty bsingleton"

lift_definition bgraph :: "('a \ 'b option) \ ('a \ 'b) set['a set]" is
  "\f. {(a, b). f a = Some b}"
proof -
  fix f :: "'a \ 'b option"
  have "|{(a, b). f a = Some b}| \o |UNIV :: 'a set|"
    by (rule surj_imp_ordLeq[of _ "\x. (x, the (f x))"]) auto
  also have "|UNIV :: 'a set|
    by simp
  also have "|UNIV :: 'a set set| \o natLeq +c |UNIV :: 'a set set|"
    by (rule ordLeq_csum2) simp
  finally show "|{(a, b). f a = Some b}| .
qed

lemma rel_bset_False[simp]: "rel_bset (\x y. False) x y = (x = bempty \ y = bempty)"
  by transfer (auto simp: rel_set_def)

lemma rel_bset_of_option[simp]:
  "rel_bset R (bset_of_option x1) (bset_of_option x2) = rel_option R x1 x2"
  unfolding bset_of_option_def bsingleton_def[abs_def]
  by transfer (auto simp: rel_set_def split: option.splits)

lemma rel_bgraph[simp]:
  "rel_bset (rel_prod (=) R) (bgraph f1) (bgraph f2) = rel_fun (=) (rel_option R) f1 f2"
  apply transfer
  apply (auto simp: rel_fun_def rel_option_iff rel_set_def split: option.splits)
  using option.collapse apply fastforce+
  done

lemma set_bset_bsingleton[simp]:
  "set_bset (bsingleton x) = {x}"
  unfolding bsingleton_def by transfer auto

lemma binsert_absorb[simp]: "binsert a (binsert a x) = binsert a x"
  by transfer simp

lemma map_bset_eq_bempty_iff[simp]: "map_bset f X = bempty \ X = bempty"
  by transfer auto

lemma map_bset_eq_bsingleton_iff[simp]:
  "map_bset f X = bsingleton x \ (set_bset X \ {} \ (\y \ set_bset X. f y = x))"
  unfolding bsingleton_def by transfer auto

lift_definition bCollect :: "('a \ bool) \ 'a set['a set]" is Collect
  apply (rule ordLeq_ordLess_trans[OF card_of_mono1[OF subset_UNIV]])
  apply (rule ordLess_ordLeq_trans[OF card_of_set_type])
  apply (rule ordLeq_csum2[OF card_of_Card_order])
  done

lift_definition bmember :: "'a \ 'a set['k] \ bool" is "(\)" .

lemma bmember_bCollect[simp]: "bmember a (bCollect P) = P a"
  by transfer simp

lemma bset_eq_iff: "A = B \ (\a. bmember a A = bmember a B)"
  by transfer auto

(* FIXME: Lifting does not work with dead variables,
   that is why we are hiding the below setup in a locale*)
locale bset_lifting
begin

declare bset.rel_eq[relator_eq]
declare bset.rel_mono[relator_mono]
declare bset.rel_compp[symmetric, relator_distr]
declare bset.rel_transfer[transfer_rule]

lemma bset_quot_map[quot_map]: "Quotient R Abs Rep T \
  Quotient (rel_bset R) (map_bset Abs) (map_bset Rep) (rel_bset T)"
  unfolding Quotient_alt_def5 bset.rel_Grp[of UNIV, simplified, symmetric]
    bset.rel_conversep[symmetric] bset.rel_compp[symmetric]
    by (auto elim: bset.rel_mono_strong)

lemma set_relator_eq_onp [relator_eq_onp]:
  "rel_bset (eq_onp P) = eq_onp (\A. Ball (set_bset A) P)"
  unfolding fun_eq_iff eq_onp_def by transfer (auto simp: rel_set_def)

end

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.