src/HOLCF/Product_Cpo.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40321 d065b195ec89
child 40619 84edf7177d73
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman@29531
     1
(*  Title:      HOLCF/Product_Cpo.thy
huffman@29531
     2
    Author:     Franz Regensburger
huffman@29531
     3
*)
huffman@29531
     4
huffman@29531
     5
header {* The cpo of cartesian products *}
huffman@29531
     6
huffman@29531
     7
theory Product_Cpo
huffman@29535
     8
imports Adm
huffman@29531
     9
begin
huffman@29531
    10
wenzelm@36452
    11
default_sort cpo
huffman@29531
    12
huffman@35900
    13
subsection {* Unit type is a pcpo *}
huffman@29531
    14
huffman@40090
    15
instantiation unit :: discrete_cpo
huffman@29531
    16
begin
huffman@29531
    17
huffman@29531
    18
definition
huffman@31076
    19
  below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
huffman@29531
    20
huffman@40090
    21
instance proof
huffman@40090
    22
qed simp
huffman@29531
    23
huffman@40090
    24
end
huffman@29531
    25
huffman@29531
    26
instance unit :: pcpo
huffman@29531
    27
by intro_classes simp
huffman@29531
    28
huffman@29531
    29
huffman@29531
    30
subsection {* Product type is a partial order *}
huffman@29531
    31
haftmann@37678
    32
instantiation prod :: (below, below) below
huffman@29531
    33
begin
huffman@29531
    34
huffman@29531
    35
definition
huffman@31076
    36
  below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
huffman@29531
    37
huffman@29531
    38
instance ..
huffman@29531
    39
end
huffman@29531
    40
haftmann@37678
    41
instance prod :: (po, po) po
huffman@29531
    42
proof
huffman@29531
    43
  fix x :: "'a \<times> 'b"
huffman@29531
    44
  show "x \<sqsubseteq> x"
huffman@31076
    45
    unfolding below_prod_def by simp
huffman@29531
    46
next
huffman@29531
    47
  fix x y :: "'a \<times> 'b"
huffman@29531
    48
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
huffman@31076
    49
    unfolding below_prod_def Pair_fst_snd_eq
huffman@31076
    50
    by (fast intro: below_antisym)
huffman@29531
    51
next
huffman@29531
    52
  fix x y z :: "'a \<times> 'b"
huffman@29531
    53
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
huffman@31076
    54
    unfolding below_prod_def
huffman@31076
    55
    by (fast intro: below_trans)
huffman@29531
    56
qed
huffman@29531
    57
huffman@35900
    58
subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
huffman@29531
    59
huffman@31076
    60
lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
huffman@31076
    61
unfolding below_prod_def by simp
huffman@29531
    62
huffman@31076
    63
lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
huffman@31076
    64
unfolding below_prod_def by simp
huffman@29531
    65
huffman@29531
    66
text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
huffman@29531
    67
huffman@29531
    68
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
huffman@29531
    69
by (simp add: monofun_def)
huffman@29531
    70
huffman@29531
    71
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
huffman@29531
    72
by (simp add: monofun_def)
huffman@29531
    73
huffman@29531
    74
lemma monofun_pair:
huffman@29531
    75
  "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
huffman@29531
    76
by simp
huffman@29531
    77
huffman@31112
    78
lemma ch2ch_Pair [simp]:
huffman@31112
    79
  "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
huffman@31112
    80
by (rule chainI, simp add: chainE)
huffman@31112
    81
huffman@29531
    82
text {* @{term fst} and @{term snd} are monotone *}
huffman@29531
    83
huffman@35919
    84
lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
huffman@35919
    85
unfolding below_prod_def by simp
huffman@35919
    86
huffman@35919
    87
lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"
huffman@35919
    88
unfolding below_prod_def by simp
huffman@35919
    89
huffman@29531
    90
lemma monofun_fst: "monofun fst"
huffman@31076
    91
by (simp add: monofun_def below_prod_def)
huffman@29531
    92
huffman@29531
    93
lemma monofun_snd: "monofun snd"
huffman@31076
    94
by (simp add: monofun_def below_prod_def)
huffman@29531
    95
huffman@31112
    96
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
huffman@31112
    97
huffman@31112
    98
lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
huffman@31112
    99
huffman@31112
   100
lemma prod_chain_cases:
huffman@31112
   101
  assumes "chain Y"
huffman@31112
   102
  obtains A B
huffman@31112
   103
  where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
huffman@31112
   104
proof
huffman@31112
   105
  from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
huffman@31112
   106
  from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
huffman@31112
   107
  show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
huffman@31112
   108
qed
huffman@31112
   109
huffman@29531
   110
subsection {* Product type is a cpo *}
huffman@29531
   111
huffman@29531
   112
lemma is_lub_Pair:
huffman@31112
   113
  "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
huffman@29531
   114
apply (rule is_lubI [OF ub_rangeI])
huffman@31112
   115
apply (simp add: is_ub_lub)
huffman@29531
   116
apply (frule ub2ub_monofun [OF monofun_fst])
huffman@29531
   117
apply (drule ub2ub_monofun [OF monofun_snd])
huffman@31076
   118
apply (simp add: below_prod_def is_lub_lub)
huffman@29531
   119
done
huffman@29531
   120
huffman@31112
   121
lemma thelub_Pair:
huffman@31112
   122
  "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
huffman@31112
   123
    \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
huffman@31112
   124
by (fast intro: thelubI is_lub_Pair elim: thelubE)
huffman@31112
   125
huffman@29531
   126
lemma lub_cprod:
huffman@29531
   127
  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
huffman@29531
   128
  assumes S: "chain S"
huffman@29531
   129
  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@29531
   130
proof -
huffman@31112
   131
  from `chain S` have "chain (\<lambda>i. fst (S i))"
huffman@31112
   132
    by (rule ch2ch_fst)
huffman@29531
   133
  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
huffman@29531
   134
    by (rule cpo_lubI)
huffman@31112
   135
  from `chain S` have "chain (\<lambda>i. snd (S i))"
huffman@31112
   136
    by (rule ch2ch_snd)
huffman@29531
   137
  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
huffman@29531
   138
    by (rule cpo_lubI)
huffman@29531
   139
  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@29531
   140
    using is_lub_Pair [OF 1 2] by simp
huffman@29531
   141
qed
huffman@29531
   142
huffman@29531
   143
lemma thelub_cprod:
huffman@29531
   144
  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
huffman@29531
   145
    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@29531
   146
by (rule lub_cprod [THEN thelubI])
huffman@29531
   147
haftmann@37678
   148
instance prod :: (cpo, cpo) cpo
huffman@29531
   149
proof
huffman@29531
   150
  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
huffman@29531
   151
  assume "chain S"
huffman@29531
   152
  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@29531
   153
    by (rule lub_cprod)
huffman@29531
   154
  thus "\<exists>x. range S <<| x" ..
huffman@29531
   155
qed
huffman@29531
   156
haftmann@37678
   157
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
huffman@29531
   158
proof
huffman@29531
   159
  fix x y :: "'a \<times> 'b"
huffman@29531
   160
  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
huffman@31076
   161
    unfolding below_prod_def Pair_fst_snd_eq
huffman@29531
   162
    by simp
huffman@29531
   163
qed
huffman@29531
   164
huffman@29531
   165
subsection {* Product type is pointed *}
huffman@29531
   166
huffman@29531
   167
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
huffman@31076
   168
by (simp add: below_prod_def)
huffman@29531
   169
haftmann@37678
   170
instance prod :: (pcpo, pcpo) pcpo
huffman@29531
   171
by intro_classes (fast intro: minimal_cprod)
huffman@29531
   172
huffman@29531
   173
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
huffman@29531
   174
by (rule minimal_cprod [THEN UU_I, symmetric])
huffman@29531
   175
huffman@40321
   176
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
huffman@29535
   177
unfolding inst_cprod_pcpo by simp
huffman@29535
   178
huffman@29535
   179
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
huffman@29535
   180
unfolding inst_cprod_pcpo by (rule fst_conv)
huffman@29535
   181
huffman@33506
   182
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
huffman@29535
   183
unfolding inst_cprod_pcpo by (rule snd_conv)
huffman@29535
   184
huffman@29535
   185
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
huffman@29535
   186
by simp
huffman@29535
   187
huffman@29535
   188
lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
huffman@29535
   189
unfolding split_def by simp
huffman@29531
   190
huffman@35900
   191
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
huffman@29531
   192
huffman@29531
   193
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
huffman@29531
   194
apply (rule contI)
huffman@29531
   195
apply (rule is_lub_Pair)
huffman@29531
   196
apply (erule cpo_lubI)
huffman@29531
   197
apply (rule lub_const)
huffman@29531
   198
done
huffman@29531
   199
huffman@29531
   200
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
huffman@29531
   201
apply (rule contI)
huffman@29531
   202
apply (rule is_lub_Pair)
huffman@29531
   203
apply (rule lub_const)
huffman@29531
   204
apply (erule cpo_lubI)
huffman@29531
   205
done
huffman@29531
   206
huffman@35914
   207
lemma cont_fst: "cont fst"
huffman@35914
   208
apply (rule contI)
huffman@29531
   209
apply (simp add: thelub_cprod)
huffman@35914
   210
apply (erule cpo_lubI [OF ch2ch_fst])
huffman@29531
   211
done
huffman@29531
   212
huffman@29531
   213
lemma cont_snd: "cont snd"
huffman@35914
   214
apply (rule contI)
huffman@35914
   215
apply (simp add: thelub_cprod)
huffman@35914
   216
apply (erule cpo_lubI [OF ch2ch_snd])
huffman@29531
   217
done
huffman@29531
   218
huffman@37079
   219
lemma cont2cont_Pair [simp, cont2cont]:
huffman@29531
   220
  assumes f: "cont (\<lambda>x. f x)"
huffman@29531
   221
  assumes g: "cont (\<lambda>x. g x)"
huffman@29531
   222
  shows "cont (\<lambda>x. (f x, g x))"
huffman@31041
   223
apply (rule cont_apply [OF f cont_pair1])
huffman@31041
   224
apply (rule cont_apply [OF g cont_pair2])
huffman@29533
   225
apply (rule cont_const)
huffman@29531
   226
done
huffman@29531
   227
huffman@37079
   228
lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
huffman@31041
   229
huffman@37079
   230
lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
huffman@31041
   231
huffman@39808
   232
lemma cont2cont_prod_case:
huffman@31041
   233
  assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
huffman@31041
   234
  assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
huffman@31041
   235
  assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
huffman@31041
   236
  assumes g: "cont (\<lambda>x. g x)"
huffman@39144
   237
  shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
huffman@31041
   238
unfolding split_def
huffman@31041
   239
apply (rule cont_apply [OF g])
huffman@31041
   240
apply (rule cont_apply [OF cont_fst f2])
huffman@31041
   241
apply (rule cont_apply [OF cont_snd f3])
huffman@31041
   242
apply (rule cont_const)
huffman@31041
   243
apply (rule f1)
huffman@31041
   244
done
huffman@31041
   245
huffman@39808
   246
lemma prod_contI:
huffman@39808
   247
  assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
huffman@39808
   248
  assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
huffman@39808
   249
  shows "cont f"
huffman@39808
   250
proof -
huffman@39808
   251
  have "cont (\<lambda>(x, y). f (x, y))"
huffman@39808
   252
    by (intro cont2cont_prod_case f1 f2 cont2cont)
huffman@39808
   253
  thus "cont f"
huffman@39808
   254
    by (simp only: split_eta)
huffman@39808
   255
qed
huffman@39808
   256
huffman@39808
   257
lemma prod_cont_iff:
huffman@39808
   258
  "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
huffman@39808
   259
apply safe
huffman@39808
   260
apply (erule cont_compose [OF _ cont_pair1])
huffman@39808
   261
apply (erule cont_compose [OF _ cont_pair2])
huffman@39808
   262
apply (simp only: prod_contI)
huffman@39808
   263
done
huffman@39808
   264
huffman@39808
   265
lemma cont2cont_prod_case' [simp, cont2cont]:
huffman@31041
   266
  assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
huffman@31041
   267
  assumes g: "cont (\<lambda>x. g x)"
huffman@39808
   268
  shows "cont (\<lambda>x. prod_case (f x) (g x))"
huffman@39808
   269
using assms by (simp add: cont2cont_prod_case prod_cont_iff)
huffman@29531
   270
huffman@39144
   271
text {* The simple version (due to Joachim Breitner) is needed if
huffman@39144
   272
  either element type of the pair is not a cpo. *}
huffman@39144
   273
huffman@39144
   274
lemma cont2cont_split_simple [simp, cont2cont]:
huffman@39144
   275
 assumes "\<And>a b. cont (\<lambda>x. f x a b)"
huffman@39144
   276
 shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
huffman@39144
   277
using assms by (cases p) auto
huffman@39144
   278
huffman@29535
   279
subsection {* Compactness and chain-finiteness *}
huffman@29535
   280
huffman@31076
   281
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
huffman@31076
   282
unfolding below_prod_def by simp
huffman@29535
   283
huffman@31076
   284
lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
huffman@31076
   285
unfolding below_prod_def by simp
huffman@29535
   286
huffman@29535
   287
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
huffman@31076
   288
by (rule compactI, simp add: fst_below_iff)
huffman@29535
   289
huffman@29535
   290
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
huffman@31076
   291
by (rule compactI, simp add: snd_below_iff)
huffman@29535
   292
huffman@29535
   293
lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
huffman@31076
   294
by (rule compactI, simp add: below_prod_def)
huffman@29535
   295
huffman@29535
   296
lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
huffman@29535
   297
apply (safe intro!: compact_Pair)
huffman@29535
   298
apply (drule compact_fst, simp)
huffman@29535
   299
apply (drule compact_snd, simp)
huffman@29535
   300
done
huffman@29535
   301
haftmann@37678
   302
instance prod :: (chfin, chfin) chfin
huffman@29535
   303
apply intro_classes
huffman@29535
   304
apply (erule compact_imp_max_in_chain)
huffman@29535
   305
apply (case_tac "\<Squnion>i. Y i", simp)
huffman@29535
   306
done
huffman@29535
   307
huffman@29531
   308
end