src/HOLCF/Product_Cpo.thy
author huffman
Wed, 14 Jan 2009 18:18:48 -0800
changeset 29533 7f4a32134447
parent 29531 2eb29775b0b6
child 29535 08824fad8879
permissions -rw-r--r--
minimize dependencies
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Product_Cpo.thy
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     2
    Author:     Franz Regensburger
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     3
*)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     4
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     5
header {* The cpo of cartesian products *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     6
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     7
theory Product_Cpo
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
     8
imports Cont
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     9
begin
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    10
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    11
defaultsort cpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    12
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    13
subsection {* Type @{typ unit} is a pcpo *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    14
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    15
instantiation unit :: sq_ord
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    16
begin
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    17
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    18
definition
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    19
  less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    20
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    21
instance ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    22
end
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    23
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    24
instance unit :: discrete_cpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    25
by intro_classes simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    26
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    27
instance unit :: finite_po ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    28
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    29
instance unit :: pcpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    30
by intro_classes simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    31
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    32
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    33
subsection {* Product type is a partial order *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    34
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    35
instantiation "*" :: (sq_ord, sq_ord) sq_ord
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    36
begin
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    37
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    38
definition
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    39
  less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    40
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    41
instance ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    42
end
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    43
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    44
instance "*" :: (po, po) po
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    45
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    46
  fix x :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    47
  show "x \<sqsubseteq> x"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    48
    unfolding less_cprod_def by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    49
next
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    50
  fix x y :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    51
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    52
    unfolding less_cprod_def Pair_fst_snd_eq
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    53
    by (fast intro: antisym_less)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    54
next
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    55
  fix x y z :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    56
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    57
    unfolding less_cprod_def
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    58
    by (fast intro: trans_less)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    59
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    60
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    61
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    62
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    63
lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    64
unfolding less_cprod_def by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    65
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    66
lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    67
unfolding less_cprod_def by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    68
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    69
text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    70
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    71
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    72
by (simp add: monofun_def)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    73
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    74
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    75
by (simp add: monofun_def)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    76
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    77
lemma monofun_pair:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    78
  "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    79
by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    80
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    81
text {* @{term fst} and @{term snd} are monotone *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    82
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    83
lemma monofun_fst: "monofun fst"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    84
by (simp add: monofun_def less_cprod_def)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    85
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    86
lemma monofun_snd: "monofun snd"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    87
by (simp add: monofun_def less_cprod_def)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    88
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    89
subsection {* Product type is a cpo *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    90
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    91
lemma is_lub_Pair:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    92
  "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    93
apply (rule is_lubI [OF ub_rangeI])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    94
apply (simp add: less_cprod_def is_ub_lub)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    95
apply (frule ub2ub_monofun [OF monofun_fst])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    96
apply (drule ub2ub_monofun [OF monofun_snd])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    97
apply (simp add: less_cprod_def is_lub_lub)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    98
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    99
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   100
lemma lub_cprod:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   101
  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   102
  assumes S: "chain S"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   103
  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   104
proof -
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   105
  have "chain (\<lambda>i. fst (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   106
    using monofun_fst S by (rule ch2ch_monofun)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   107
  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   108
    by (rule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   109
  have "chain (\<lambda>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   110
    using monofun_snd S by (rule ch2ch_monofun)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   111
  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   112
    by (rule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   113
  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   114
    using is_lub_Pair [OF 1 2] by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   115
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   116
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   117
lemma thelub_cprod:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   118
  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   119
    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   120
by (rule lub_cprod [THEN thelubI])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   121
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   122
instance "*" :: (cpo, cpo) cpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   123
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   124
  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   125
  assume "chain S"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   126
  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   127
    by (rule lub_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   128
  thus "\<exists>x. range S <<| x" ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   129
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   130
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   131
instance "*" :: (finite_po, finite_po) finite_po ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   132
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   133
instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   134
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   135
  fix x y :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   136
  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   137
    unfolding less_cprod_def Pair_fst_snd_eq
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   138
    by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   139
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   140
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   141
subsection {* Product type is pointed *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   142
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   143
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   144
by (simp add: less_cprod_def)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   145
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   146
instance "*" :: (pcpo, pcpo) pcpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   147
by intro_classes (fast intro: minimal_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   148
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   149
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   150
by (rule minimal_cprod [THEN UU_I, symmetric])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   151
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   152
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   153
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   154
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   155
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   156
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   157
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   158
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   159
apply (rule lub_const)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   160
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   161
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   162
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   163
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   164
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   165
apply (rule lub_const)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   166
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   167
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   168
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   169
lemma contlub_fst: "contlub fst"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   170
apply (rule contlubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   171
apply (simp add: thelub_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   172
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   173
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   174
lemma contlub_snd: "contlub snd"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   175
apply (rule contlubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   176
apply (simp add: thelub_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   177
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   178
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   179
lemma cont_fst: "cont fst"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   180
apply (rule monocontlub2cont)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   181
apply (rule monofun_fst)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   182
apply (rule contlub_fst)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   183
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   184
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   185
lemma cont_snd: "cont snd"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   186
apply (rule monocontlub2cont)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   187
apply (rule monofun_snd)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   188
apply (rule contlub_snd)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   189
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   190
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   191
lemma cont2cont_Pair [cont2cont]:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   192
  assumes f: "cont (\<lambda>x. f x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   193
  assumes g: "cont (\<lambda>x. g x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   194
  shows "cont (\<lambda>x. (f x, g x))"
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   195
apply (rule cont2cont_apply [OF _ cont_pair1 f])
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   196
apply (rule cont2cont_apply [OF _ cont_pair2 g])
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   197
apply (rule cont_const)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   198
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   199
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   200
lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   201
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   202
lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   203
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   204
end