src/HOL/HOLCF/Product_Cpo.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 44066 d74182c93f04
child 55414 eab03e9cee8a
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
wenzelm@42151
     1
(*  Title:      HOL/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@44066
    49
    unfolding below_prod_def prod_eq_iff
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@40771
   114
unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
huffman@29531
   115
huffman@40771
   116
lemma lub_Pair:
huffman@31112
   117
  "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
huffman@31112
   118
    \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
huffman@40771
   119
by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
huffman@31112
   120
huffman@40771
   121
lemma is_lub_prod:
huffman@29531
   122
  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
huffman@29531
   123
  assumes S: "chain S"
huffman@29531
   124
  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@40771
   125
using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
huffman@29531
   126
huffman@40771
   127
lemma lub_prod:
huffman@29531
   128
  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
huffman@29531
   129
    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@40771
   130
by (rule is_lub_prod [THEN lub_eqI])
huffman@29531
   131
haftmann@37678
   132
instance prod :: (cpo, cpo) cpo
huffman@29531
   133
proof
huffman@29531
   134
  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
huffman@29531
   135
  assume "chain S"
huffman@29531
   136
  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
huffman@40771
   137
    by (rule is_lub_prod)
huffman@29531
   138
  thus "\<exists>x. range S <<| x" ..
huffman@29531
   139
qed
huffman@29531
   140
haftmann@37678
   141
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
huffman@29531
   142
proof
huffman@29531
   143
  fix x y :: "'a \<times> 'b"
huffman@29531
   144
  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
huffman@44066
   145
    unfolding below_prod_def prod_eq_iff
huffman@29531
   146
    by simp
huffman@29531
   147
qed
huffman@29531
   148
huffman@29531
   149
subsection {* Product type is pointed *}
huffman@29531
   150
huffman@40771
   151
lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
huffman@31076
   152
by (simp add: below_prod_def)
huffman@29531
   153
haftmann@37678
   154
instance prod :: (pcpo, pcpo) pcpo
huffman@40771
   155
by intro_classes (fast intro: minimal_prod)
huffman@29531
   156
huffman@40771
   157
lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
huffman@41430
   158
by (rule minimal_prod [THEN bottomI, symmetric])
huffman@29531
   159
huffman@40321
   160
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
huffman@40771
   161
unfolding inst_prod_pcpo by simp
huffman@29535
   162
huffman@29535
   163
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
huffman@40771
   164
unfolding inst_prod_pcpo by (rule fst_conv)
huffman@29535
   165
huffman@33506
   166
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
huffman@40771
   167
unfolding inst_prod_pcpo by (rule snd_conv)
huffman@29535
   168
huffman@29535
   169
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
huffman@29535
   170
by simp
huffman@29535
   171
huffman@29535
   172
lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
huffman@29535
   173
unfolding split_def by simp
huffman@29531
   174
huffman@35900
   175
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
huffman@29531
   176
huffman@29531
   177
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
huffman@29531
   178
apply (rule contI)
huffman@29531
   179
apply (rule is_lub_Pair)
huffman@29531
   180
apply (erule cpo_lubI)
huffman@40771
   181
apply (rule is_lub_const)
huffman@29531
   182
done
huffman@29531
   183
huffman@29531
   184
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
huffman@29531
   185
apply (rule contI)
huffman@29531
   186
apply (rule is_lub_Pair)
huffman@40771
   187
apply (rule is_lub_const)
huffman@29531
   188
apply (erule cpo_lubI)
huffman@29531
   189
done
huffman@29531
   190
huffman@35914
   191
lemma cont_fst: "cont fst"
huffman@35914
   192
apply (rule contI)
huffman@40771
   193
apply (simp add: lub_prod)
huffman@35914
   194
apply (erule cpo_lubI [OF ch2ch_fst])
huffman@29531
   195
done
huffman@29531
   196
huffman@29531
   197
lemma cont_snd: "cont snd"
huffman@35914
   198
apply (rule contI)
huffman@40771
   199
apply (simp add: lub_prod)
huffman@35914
   200
apply (erule cpo_lubI [OF ch2ch_snd])
huffman@29531
   201
done
huffman@29531
   202
huffman@37079
   203
lemma cont2cont_Pair [simp, cont2cont]:
huffman@29531
   204
  assumes f: "cont (\<lambda>x. f x)"
huffman@29531
   205
  assumes g: "cont (\<lambda>x. g x)"
huffman@29531
   206
  shows "cont (\<lambda>x. (f x, g x))"
huffman@31041
   207
apply (rule cont_apply [OF f cont_pair1])
huffman@31041
   208
apply (rule cont_apply [OF g cont_pair2])
huffman@29533
   209
apply (rule cont_const)
huffman@29531
   210
done
huffman@29531
   211
huffman@37079
   212
lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
huffman@31041
   213
huffman@37079
   214
lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
huffman@31041
   215
huffman@39808
   216
lemma cont2cont_prod_case:
huffman@31041
   217
  assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
huffman@31041
   218
  assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
huffman@31041
   219
  assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
huffman@31041
   220
  assumes g: "cont (\<lambda>x. g x)"
huffman@39144
   221
  shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
huffman@31041
   222
unfolding split_def
huffman@31041
   223
apply (rule cont_apply [OF g])
huffman@31041
   224
apply (rule cont_apply [OF cont_fst f2])
huffman@31041
   225
apply (rule cont_apply [OF cont_snd f3])
huffman@31041
   226
apply (rule cont_const)
huffman@31041
   227
apply (rule f1)
huffman@31041
   228
done
huffman@31041
   229
huffman@39808
   230
lemma prod_contI:
huffman@39808
   231
  assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
huffman@39808
   232
  assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
huffman@39808
   233
  shows "cont f"
huffman@39808
   234
proof -
huffman@39808
   235
  have "cont (\<lambda>(x, y). f (x, y))"
huffman@39808
   236
    by (intro cont2cont_prod_case f1 f2 cont2cont)
huffman@39808
   237
  thus "cont f"
huffman@39808
   238
    by (simp only: split_eta)
huffman@39808
   239
qed
huffman@39808
   240
huffman@39808
   241
lemma prod_cont_iff:
huffman@39808
   242
  "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
huffman@39808
   243
apply safe
huffman@39808
   244
apply (erule cont_compose [OF _ cont_pair1])
huffman@39808
   245
apply (erule cont_compose [OF _ cont_pair2])
huffman@39808
   246
apply (simp only: prod_contI)
huffman@39808
   247
done
huffman@39808
   248
huffman@39808
   249
lemma cont2cont_prod_case' [simp, cont2cont]:
huffman@31041
   250
  assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
huffman@31041
   251
  assumes g: "cont (\<lambda>x. g x)"
huffman@39808
   252
  shows "cont (\<lambda>x. prod_case (f x) (g x))"
huffman@39808
   253
using assms by (simp add: cont2cont_prod_case prod_cont_iff)
huffman@29531
   254
huffman@39144
   255
text {* The simple version (due to Joachim Breitner) is needed if
huffman@39144
   256
  either element type of the pair is not a cpo. *}
huffman@39144
   257
huffman@39144
   258
lemma cont2cont_split_simple [simp, cont2cont]:
huffman@39144
   259
 assumes "\<And>a b. cont (\<lambda>x. f x a b)"
huffman@39144
   260
 shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
huffman@39144
   261
using assms by (cases p) auto
huffman@39144
   262
huffman@40619
   263
text {* Admissibility of predicates on product types. *}
huffman@40619
   264
huffman@40619
   265
lemma adm_prod_case [simp]:
huffman@40619
   266
  assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
huffman@40619
   267
  shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
huffman@40619
   268
unfolding prod_case_beta using assms .
huffman@40619
   269
huffman@29535
   270
subsection {* Compactness and chain-finiteness *}
huffman@29535
   271
huffman@31076
   272
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
huffman@31076
   273
unfolding below_prod_def by simp
huffman@29535
   274
huffman@31076
   275
lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
huffman@31076
   276
unfolding below_prod_def by simp
huffman@29535
   277
huffman@29535
   278
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
huffman@31076
   279
by (rule compactI, simp add: fst_below_iff)
huffman@29535
   280
huffman@29535
   281
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
huffman@31076
   282
by (rule compactI, simp add: snd_below_iff)
huffman@29535
   283
huffman@29535
   284
lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
huffman@31076
   285
by (rule compactI, simp add: below_prod_def)
huffman@29535
   286
huffman@29535
   287
lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
huffman@29535
   288
apply (safe intro!: compact_Pair)
huffman@29535
   289
apply (drule compact_fst, simp)
huffman@29535
   290
apply (drule compact_snd, simp)
huffman@29535
   291
done
huffman@29535
   292
haftmann@37678
   293
instance prod :: (chfin, chfin) chfin
huffman@29535
   294
apply intro_classes
huffman@29535
   295
apply (erule compact_imp_max_in_chain)
huffman@29535
   296
apply (case_tac "\<Squnion>i. Y i", simp)
huffman@29535
   297
done
huffman@29535
   298
huffman@29531
   299
end