src/HOLCF/SetPcpo.thy
author huffman
Fri, 16 May 2008 21:41:07 +0200
changeset 26921 5d9f78c3d6de
parent 26837 535290c908ae
child 27180 51f3f3557ef4
permissions -rw-r--r--
fix looping simplifier
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
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    12
instantiation bool :: po
25893
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
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    16
  less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)"
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    17
25897
e9d45709bece use new-style class for po
huffman
parents: 25893
diff changeset
    18
instance
26921
5d9f78c3d6de fix looping simplifier
huffman
parents: 26837
diff changeset
    19
by (intro_classes, unfold less_bool_def, safe)
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    20
25897
e9d45709bece use new-style class for po
huffman
parents: 25893
diff changeset
    21
end
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    22
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    23
lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)"
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    24
  by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq)
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    25
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    26
instance bool :: finite_po ..
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    27
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    28
lemma Union_is_lub: "A <<| Union A"
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    29
unfolding is_lub_def is_ub_def less_set_eq by fast
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    30
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    31
instance bool :: cpo ..
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    32
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    33
lemma lub_eq_Union: "lub = Union"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    34
by (rule ext, rule thelubI [OF Union_is_lub])
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    35
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    36
instance bool :: pcpo
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    37
proof
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    38
  have "\<forall>y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    39
  thus "\<exists>x::bool. \<forall>y. x \<sqsubseteq> y" ..
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    40
qed
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    41
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    42
lemma UU_eq_empty: "\<bottom> = {}"
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    43
by (rule UU_I [symmetric], simp add: less_set_eq)
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    44
26837
535290c908ae Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents: 25906
diff changeset
    45
lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty
25893
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    46
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    47
subsection {* Admissibility of set predicates *}
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    48
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    49
lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    50
by (rule admI, force simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    51
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    52
lemma adm_in: "adm (\<lambda>A. x \<in> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    53
by (rule admI, simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    54
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    55
lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    56
by (rule admI, simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    57
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    58
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
    59
unfolding Ball_def by (simp add: adm_not_in)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    60
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    61
lemma adm_Bex: "adm (\<lambda>A. Bex A P)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    62
by (rule admI, simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    63
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    64
lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    65
by (rule admI, auto simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    66
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    67
lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    68
by (rule admI, auto simp add: lub_eq_Union)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    69
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    70
lemmas adm_set_lemmas =
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    71
  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
    72
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    73
subsection {* Compactness *}
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    74
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    75
lemma compact_empty: "compact {}"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    76
by (fold UU_eq_empty, simp)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    77
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    78
lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    79
unfolding compact_def set_cpo_simps
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    80
by (simp add: adm_set_lemmas)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    81
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    82
lemma finite_imp_compact: "finite A \<Longrightarrow> compact A"
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    83
by (induct A set: finite, rule compact_empty, erule compact_insert)
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    84
b06a09abf79e new theory defining set as a pcpo
huffman
parents:
diff changeset
    85
end