src/HOLCF/CompactBasis.thy
author huffman
Mon, 22 Mar 2010 13:27:35 -0700
changeset 35901 12f09bf2c77f
parent 31076 99fe356cbbc2
child 36452 d37c6eed8117
permissions -rw-r--r--
fix LaTeX overfull hbox warnings in HOLCF document
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/CompactBasis.thy
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     3
*)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     4
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     5
header {* Compact bases of domains *}
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     6
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     7
theory CompactBasis
27404
62171da527d6 split Completion.thy from CompactBasis.thy
huffman
parents: 27373
diff changeset
     8
imports Completion
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
     9
begin
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    10
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    11
subsection {* Compact bases of bifinite domains *}
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    12
26407
562a1d615336 rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents: 26041
diff changeset
    13
defaultsort profinite
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    14
26407
562a1d615336 rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents: 26041
diff changeset
    15
typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    16
by (fast intro: compact_approx)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    17
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    18
lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
    19
by (rule Rep_compact_basis [unfolded mem_Collect_eq])
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    20
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    21
instantiation compact_basis :: (profinite) below
26420
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    22
begin
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    23
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    24
definition
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    25
  compact_le_def:
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    26
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    27
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    28
instance ..
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    29
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    30
end
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    31
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    32
instance compact_basis :: (profinite) po
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    33
by (rule typedef_po
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
    34
    [OF type_definition_compact_basis compact_le_def])
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    35
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    36
text {* Take function for compact basis *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    37
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    38
definition
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    39
  compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    40
  "compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    41
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    42
lemma Rep_compact_take:
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    43
  "Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)"
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    44
unfolding compact_take_def
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    45
by (simp add: Abs_compact_basis_inverse)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    46
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    47
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    48
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29511
diff changeset
    49
interpretation compact_basis:
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    50
  basis_take below compact_take
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    51
proof
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    52
  fix n :: nat and a :: "'a compact_basis"
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    53
  show "compact_take n a \<sqsubseteq> a"
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    54
    unfolding compact_le_def
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    55
    by (simp add: Rep_compact_take approx_below)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    56
next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    57
  fix n :: nat and a :: "'a compact_basis"
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    58
  show "compact_take n (compact_take n a) = compact_take n a"
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    59
    by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    60
next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    61
  fix n :: nat and a b :: "'a compact_basis"
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    62
  assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b"
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    63
    unfolding compact_le_def Rep_compact_take
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    64
    by (rule monofun_cfun_arg)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    65
next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    66
  fix n :: nat and a :: "'a compact_basis"
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    67
  show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a"
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    68
    unfolding compact_le_def Rep_compact_take
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    69
    by (rule chainE, simp)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    70
next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    71
  fix n :: nat
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    72
  show "finite (range (compact_take n))"
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    73
    apply (rule finite_imageD [where f="Rep_compact_basis"])
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    74
    apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    75
    apply (clarsimp simp add: Rep_compact_take)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    76
    apply (rule finite_range_approx)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    77
    apply (rule inj_onI, simp add: Rep_compact_basis_inject)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    78
    done
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    79
next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    80
  fix a :: "'a compact_basis"
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    81
  show "\<exists>n. compact_take n a = a"
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    82
    apply (simp add: Rep_compact_basis_inject [symmetric])
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
    83
    apply (simp add: Rep_compact_take)
27309
c74270fd72a8 clean up and rename some profinite lemmas
huffman
parents: 27297
diff changeset
    84
    apply (rule profinite_compact_eq_approx)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    85
    apply (rule compact_Rep_compact_basis)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    86
    done
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    87
qed
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    88
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    89
text {* Ideal completion *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    90
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    91
definition
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
    92
  approximants :: "'a \<Rightarrow> 'a compact_basis set" where
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
    93
  "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
    94
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 29511
diff changeset
    95
interpretation compact_basis:
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    96
  ideal_completion below compact_take Rep_compact_basis approximants
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    97
proof
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
    98
  fix w :: 'a
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
    99
  show "preorder.ideal below (approximants w)"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   100
  proof (rule below.idealI)
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   101
    show "\<exists>x. x \<in> approximants w"
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   102
      unfolding approximants_def
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   103
      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   104
      apply (simp add: Abs_compact_basis_inverse approx_below)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   105
      done
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   106
  next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   107
    fix x y :: "'a compact_basis"
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   108
    assume "x \<in> approximants w" "y \<in> approximants w"
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   109
    thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   110
      unfolding approximants_def
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   111
      apply simp
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   112
      apply (cut_tac a=x in compact_Rep_compact_basis)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   113
      apply (cut_tac a=y in compact_Rep_compact_basis)
27309
c74270fd72a8 clean up and rename some profinite lemmas
huffman
parents: 27297
diff changeset
   114
      apply (drule profinite_compact_eq_approx)
c74270fd72a8 clean up and rename some profinite lemmas
huffman
parents: 27297
diff changeset
   115
      apply (drule profinite_compact_eq_approx)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   116
      apply (clarify, rename_tac i j)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   117
      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   118
      apply (simp add: compact_le_def)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   119
      apply (simp add: Abs_compact_basis_inverse approx_below)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   120
      apply (erule subst, erule subst)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   121
      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   122
      done
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   123
  next
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   124
    fix x y :: "'a compact_basis"
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   125
    assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   126
      unfolding approximants_def
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   127
      apply simp
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   128
      apply (simp add: compact_le_def)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   129
      apply (erule (1) below_trans)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   130
      done
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   131
  qed
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   132
next
27297
2c42b1505f25 removed SetPcpo.thy and cpo instance for type bool;
huffman
parents: 27289
diff changeset
   133
  fix Y :: "nat \<Rightarrow> 'a"
2c42b1505f25 removed SetPcpo.thy and cpo instance for type bool;
huffman
parents: 27289
diff changeset
   134
  assume Y: "chain Y"
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   135
  show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   136
    unfolding approximants_def
27297
2c42b1505f25 removed SetPcpo.thy and cpo instance for type bool;
huffman
parents: 27289
diff changeset
   137
    apply safe
2c42b1505f25 removed SetPcpo.thy and cpo instance for type bool;
huffman
parents: 27289
diff changeset
   138
    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   139
    apply (erule below_trans, rule is_ub_thelub [OF Y])
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   140
    done
26420
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
   141
next
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   142
  fix a :: "'a compact_basis"
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   143
  show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   144
    unfolding approximants_def compact_le_def ..
26420
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
   145
next
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
   146
  fix x y :: "'a"
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   147
  assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   148
    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   149
    apply (rule admD, simp, simp)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   150
    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   151
    apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   152
    apply (simp add: approximants_def Abs_compact_basis_inverse)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   153
    done
26420
57a626f64875 make preorder locale into a superclass of class po
huffman
parents: 26407
diff changeset
   154
qed
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   155
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   156
text {* minimal compact element *}
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   157
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   158
definition
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   159
  compact_bot :: "'a::bifinite compact_basis" where
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   160
  "compact_bot = Abs_compact_basis \<bottom>"
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   161
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   162
lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   163
unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   164
28890
1a36f0050734 renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents: 28611
diff changeset
   165
lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   166
unfolding compact_le_def Rep_compact_bot by simp
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   167
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   168
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   169
subsection {* A compact basis for powerdomains *}
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   170
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   171
typedef 'a pd_basis =
26407
562a1d615336 rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents: 26041
diff changeset
   172
  "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   173
by (rule_tac x="{arbitrary}" in exI, simp)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   174
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   175
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   176
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   177
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   178
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   179
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   180
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   181
text {* unit and plus *}
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   182
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   183
definition
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   184
  PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   185
  "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   186
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   187
definition
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   188
  PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   189
  "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   190
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   191
lemma Rep_PDUnit:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   192
  "Rep_pd_basis (PDUnit x) = {x}"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   193
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   194
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   195
lemma Rep_PDPlus:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   196
  "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   197
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   198
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   199
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   200
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   201
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   202
lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   203
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   204
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   205
lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   206
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   207
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   208
lemma PDPlus_absorb: "PDPlus t t = t"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   209
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   210
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   211
lemma pd_basis_induct1:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   212
  assumes PDUnit: "\<And>a. P (PDUnit a)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   213
  assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   214
  shows "P x"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   215
apply (induct x, unfold pd_basis_def, clarify)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   216
apply (erule (1) finite_ne_induct)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   217
apply (cut_tac a=x in PDUnit)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   218
apply (simp add: PDUnit_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   219
apply (drule_tac a=x in PDPlus)
35901
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
   220
apply (simp add: PDUnit_def PDPlus_def
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
   221
  Abs_pd_basis_inverse [unfolded pd_basis_def])
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   222
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   223
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   224
lemma pd_basis_induct:
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   225
  assumes PDUnit: "\<And>a. P (PDUnit a)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   226
  assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   227
  shows "P x"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   228
apply (induct x rule: pd_basis_induct1)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   229
apply (rule PDUnit, erule PDPlus [OF PDUnit])
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   230
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   231
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   232
text {* fold-pd *}
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   233
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   234
definition
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   235
  fold_pd ::
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   236
    "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   237
  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   238
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
   239
lemma fold_pd_PDUnit:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27406
diff changeset
   240
  assumes "ab_semigroup_idem_mult f"
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
   241
  shows "fold_pd g f (PDUnit x) = g x"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   242
unfolding fold_pd_def Rep_PDUnit by simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   243
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
   244
lemma fold_pd_PDPlus:
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27406
diff changeset
   245
  assumes "ab_semigroup_idem_mult f"
26927
8684b5240f11 rename locales;
huffman
parents: 26806
diff changeset
   246
  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27406
diff changeset
   247
proof -
29511
7071b017cb35 migrated class package to new locale implementation
haftmann
parents: 29252
diff changeset
   248
  interpret ab_semigroup_idem_mult f by fact
35901
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
   249
  show ?thesis unfolding fold_pd_def Rep_PDPlus
12f09bf2c77f fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents: 31076
diff changeset
   250
    by (simp add: image_Un fold1_Un2)
28611
983c1855a7af More occurrences of 'includes' gone.
ballarin
parents: 27406
diff changeset
   251
qed
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   252
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   253
text {* Take function for powerdomain basis *}
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   254
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   255
definition
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   256
  pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
   257
  "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   258
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   259
lemma Rep_pd_take:
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
   260
  "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t"
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   261
unfolding pd_take_def
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   262
apply (rule Abs_pd_basis_inverse)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   263
apply (simp add: pd_basis_def)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   264
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   265
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   266
lemma pd_take_simps [simp]:
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
   267
  "pd_take n (PDUnit a) = PDUnit (compact_take n a)"
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   268
  "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   269
apply (simp_all add: Rep_pd_basis_inject [symmetric])
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   270
apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   271
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   272
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   273
lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   274
apply (induct t rule: pd_basis_induct)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   275
apply (simp add: compact_basis.take_take)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   276
apply simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   277
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   278
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   279
lemma finite_range_pd_take: "finite (range (pd_take n))"
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   280
apply (rule finite_imageD [where f="Rep_pd_basis"])
27406
3897988917a3 rename compact_approx to compact_take
huffman
parents: 27405
diff changeset
   281
apply (rule finite_subset [where B="Pow (range (compact_take n))"])
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   282
apply (clarsimp simp add: Rep_pd_take)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   283
apply (simp add: compact_basis.finite_range_take)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   284
apply (rule inj_onI, simp add: Rep_pd_basis_inject)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   285
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   286
27405
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   287
lemma pd_take_covers: "\<exists>n. pd_take n t = t"
785f5dbec8f4 rename approx_pd to pd_take
huffman
parents: 27404
diff changeset
   288
apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   289
apply (induct t rule: pd_basis_induct)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   290
apply (cut_tac a=a in compact_basis.take_covers)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   291
apply (clarify, rule_tac x=n in exI)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   292
apply (clarify, simp)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30729
diff changeset
   293
apply (rule below_antisym)
27289
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   294
apply (rule compact_basis.take_less)
c49d427867aa move lemmas into locales;
huffman
parents: 27288
diff changeset
   295
apply (drule_tac a=a in compact_basis.take_chain_le)
25904
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   296
apply simp
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   297
apply (clarify, rename_tac i j)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   298
apply (rule_tac x="max i j" in exI, simp)
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   299
done
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   300
8161f137b0e9 new theory of powerdomains
huffman
parents:
diff changeset
   301
end