src/HOLCF/SetPcpo.thy
author huffman
Thu, 10 Jan 2008 20:53:06 +0100
changeset 25893 b06a09abf79e
child 25897 e9d45709bece
permissions -rw-r--r--
new theory defining set as a pcpo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/SetPcpo.thy
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     2
    ID:         $Id$
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     3
    Author:     Brian Huffman
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     4
*)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     5
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     6
header {* Set as a pointed cpo *}
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     7
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     8
theory SetPcpo
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
     9
imports Adm
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    10
begin
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    11
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    12
instantiation set :: (type) sq_ord
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    13
begin
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    14
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    15
definition
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    16
  less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    17
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    18
instance ..
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    19
end
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    20
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    21
instance set :: (type) po
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    22
by (intro_classes, auto simp add: less_set_def)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    23
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    24
instance set :: (finite) finite_po ..
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    25
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    26
lemma Union_is_lub: "A <<| Union A"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    27
unfolding is_lub_def is_ub_def less_set_def by fast
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    28
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    29
instance set :: (type) dcpo
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    30
by (intro_classes, rule exI, rule Union_is_lub)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    31
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    32
lemma lub_eq_Union: "lub = Union"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    33
by (rule ext, rule thelubI [OF Union_is_lub])
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    34
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    35
instance set :: (type) pcpo
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    36
proof
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    37
  have "\<forall>y::'a set. {} \<sqsubseteq> y" unfolding less_set_def by simp
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    38
  thus "\<exists>x::'a set. \<forall>y. x \<sqsubseteq> y" ..
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    39
qed
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    40
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    41
lemma UU_eq_empty: "\<bottom> = {}"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    42
by (rule UU_I [symmetric], simp add: less_set_def)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    43
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    44
lemmas set_cpo_simps = less_set_def lub_eq_Union UU_eq_empty
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    45
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    46
subsection {* Admissibility of set predicates *}
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    47
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    48
lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    49
by (rule admI, force simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    50
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    51
lemma adm_in: "adm (\<lambda>A. x \<in> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    52
by (rule admI, simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    53
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    54
lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    55
by (rule admI, simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    56
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    57
lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>A. P A x)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    58
unfolding Ball_def by (simp add: adm_not_in)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    59
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    60
lemma adm_Bex: "adm (\<lambda>A. Bex A P)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    61
by (rule admI, simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    62
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    63
lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    64
by (rule admI, auto simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    65
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    66
lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    67
by (rule admI, auto simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    68
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    69
lemmas adm_set_lemmas =
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    70
  adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    71
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    72
subsection {* Compactness *}
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    73
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    74
lemma compact_empty: "compact {}"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    75
by (fold UU_eq_empty, simp)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    76
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    77
lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    78
unfolding compact_def set_cpo_simps
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    79
by (simp add: adm_set_lemmas)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    80
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    81
lemma finite_imp_compact: "finite A \<Longrightarrow> compact A"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    82
by (induct A set: finite, rule compact_empty, erule compact_insert)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    83
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    84
end