src/HOLCF/Product_Cpo.thy
author huffman
Thu, 30 Sep 2010 18:46:19 -0700
changeset 39808 1410c84013b9
parent 39144 23b1e6759359
child 40003 427106657e04
permissions -rw-r--r--
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
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
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
     8
imports Adm
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
     9
begin
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35919
diff changeset
    11
default_sort cpo
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    12
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 33506
diff changeset
    13
subsection {* Unit type is a pcpo *}
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    14
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    15
instantiation unit :: below
29531
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
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    19
  below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
29531
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
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
    35
instantiation prod :: (below, below) below
29531
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
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    39
  below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
29531
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
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
    44
instance prod :: (po, po) po
29531
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"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    48
    unfolding below_prod_def by simp
29531
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"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    52
    unfolding below_prod_def Pair_fst_snd_eq
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    53
    by (fast intro: below_antisym)
29531
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"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    57
    unfolding below_prod_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    58
    by (fast intro: below_trans)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    59
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    60
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 33506
diff changeset
    61
subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    62
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    63
lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    64
unfolding below_prod_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    65
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    66
lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    67
unfolding below_prod_def by simp
29531
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
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    81
lemma ch2ch_Pair [simp]:
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    82
  "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    83
by (rule chainI, simp add: chainE)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    84
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    85
text {* @{term fst} and @{term snd} are monotone *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    86
35919
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    87
lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    88
unfolding below_prod_def by simp
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    89
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    90
lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    91
unfolding below_prod_def by simp
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    92
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    93
lemma monofun_fst: "monofun fst"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    94
by (simp add: monofun_def below_prod_def)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    95
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    96
lemma monofun_snd: "monofun snd"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
    97
by (simp add: monofun_def below_prod_def)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    98
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    99
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   100
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   101
lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   102
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   103
lemma prod_chain_cases:
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   104
  assumes "chain Y"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   105
  obtains A B
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   106
  where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   107
proof
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   108
  from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   109
  from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   110
  show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   111
qed
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   112
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   113
subsection {* Product type is a cpo *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   114
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   115
lemma is_lub_Pair:
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   116
  "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   117
apply (rule is_lubI [OF ub_rangeI])
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   118
apply (simp add: is_ub_lub)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   119
apply (frule ub2ub_monofun [OF monofun_fst])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   120
apply (drule ub2ub_monofun [OF monofun_snd])
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   121
apply (simp add: below_prod_def is_lub_lub)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   122
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   123
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   124
lemma thelub_Pair:
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   125
  "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   126
    \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   127
by (fast intro: thelubI is_lub_Pair elim: thelubE)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   128
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   129
lemma lub_cprod:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   130
  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   131
  assumes S: "chain S"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   132
  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   133
proof -
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   134
  from `chain S` have "chain (\<lambda>i. fst (S i))"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   135
    by (rule ch2ch_fst)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   136
  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   137
    by (rule cpo_lubI)
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   138
  from `chain S` have "chain (\<lambda>i. snd (S i))"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   139
    by (rule ch2ch_snd)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   140
  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   141
    by (rule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   142
  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   143
    using is_lub_Pair [OF 1 2] by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   144
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   145
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   146
lemma thelub_cprod:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   147
  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   148
    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   149
by (rule lub_cprod [THEN thelubI])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   150
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   151
instance prod :: (cpo, cpo) cpo
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   152
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   153
  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   154
  assume "chain S"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   155
  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   156
    by (rule lub_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   157
  thus "\<exists>x. range S <<| x" ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   158
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   159
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   160
instance prod :: (finite_po, finite_po) finite_po ..
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   161
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   162
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   163
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   164
  fix x y :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   165
  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   166
    unfolding below_prod_def Pair_fst_snd_eq
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   167
    by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   168
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   169
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   170
subsection {* Product type is pointed *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   171
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   172
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   173
by (simp add: below_prod_def)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   174
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   175
instance prod :: (pcpo, pcpo) pcpo
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   176
by intro_classes (fast intro: minimal_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   177
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   178
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   179
by (rule minimal_cprod [THEN UU_I, symmetric])
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   180
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   181
lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   182
unfolding inst_cprod_pcpo by simp
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   183
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   184
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   185
unfolding inst_cprod_pcpo by (rule fst_conv)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   186
33506
afb577487b15 fix name of lemma snd_strict
huffman
parents: 31112
diff changeset
   187
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   188
unfolding inst_cprod_pcpo by (rule snd_conv)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   189
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   190
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   191
by simp
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   192
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   193
lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   194
unfolding split_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   195
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 33506
diff changeset
   196
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   197
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   198
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   199
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   200
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   201
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   202
apply (rule lub_const)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   203
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   204
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   205
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   206
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   207
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   208
apply (rule lub_const)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   209
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   210
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   211
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   212
lemma cont_fst: "cont fst"
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   213
apply (rule contI)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   214
apply (simp add: thelub_cprod)
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   215
apply (erule cpo_lubI [OF ch2ch_fst])
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   216
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   217
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   218
lemma cont_snd: "cont snd"
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   219
apply (rule contI)
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   220
apply (simp add: thelub_cprod)
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   221
apply (erule cpo_lubI [OF ch2ch_snd])
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   222
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   223
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36452
diff changeset
   224
lemma cont2cont_Pair [simp, cont2cont]:
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   225
  assumes f: "cont (\<lambda>x. f x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   226
  assumes g: "cont (\<lambda>x. g x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   227
  shows "cont (\<lambda>x. (f x, g x))"
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   228
apply (rule cont_apply [OF f cont_pair1])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   229
apply (rule cont_apply [OF g cont_pair2])
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   230
apply (rule cont_const)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   231
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   232
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36452
diff changeset
   233
lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   234
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36452
diff changeset
   235
lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   236
39808
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   237
lemma cont2cont_prod_case:
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   238
  assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   239
  assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   240
  assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   241
  assumes g: "cont (\<lambda>x. g x)"
39144
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   242
  shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   243
unfolding split_def
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   244
apply (rule cont_apply [OF g])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   245
apply (rule cont_apply [OF cont_fst f2])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   246
apply (rule cont_apply [OF cont_snd f3])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   247
apply (rule cont_const)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   248
apply (rule f1)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   249
done
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   250
39808
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   251
lemma prod_contI:
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   252
  assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   253
  assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   254
  shows "cont f"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   255
proof -
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   256
  have "cont (\<lambda>(x, y). f (x, y))"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   257
    by (intro cont2cont_prod_case f1 f2 cont2cont)
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   258
  thus "cont f"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   259
    by (simp only: split_eta)
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   260
qed
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   261
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   262
lemma prod_cont_iff:
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   263
  "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   264
apply safe
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   265
apply (erule cont_compose [OF _ cont_pair1])
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   266
apply (erule cont_compose [OF _ cont_pair2])
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   267
apply (simp only: prod_contI)
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   268
done
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   269
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   270
lemma cont_fst_snd_D1:
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   271
  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   272
by (drule cont_compose [OF _ cont_pair1], simp)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   273
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   274
lemma cont_fst_snd_D2:
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   275
  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   276
by (drule cont_compose [OF _ cont_pair2], simp)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   277
39808
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   278
lemma cont2cont_prod_case' [simp, cont2cont]:
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   279
  assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   280
  assumes g: "cont (\<lambda>x. g x)"
39808
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   281
  shows "cont (\<lambda>x. prod_case (f x) (g x))"
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   282
using assms by (simp add: cont2cont_prod_case prod_cont_iff)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   283
39144
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   284
text {* The simple version (due to Joachim Breitner) is needed if
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   285
  either element type of the pair is not a cpo. *}
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   286
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   287
lemma cont2cont_split_simple [simp, cont2cont]:
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   288
 assumes "\<And>a b. cont (\<lambda>x. f x a b)"
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   289
 shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   290
using assms by (cases p) auto
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   291
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   292
subsection {* Compactness and chain-finiteness *}
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   293
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   294
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   295
unfolding below_prod_def by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   296
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   297
lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   298
unfolding below_prod_def by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   299
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   300
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   301
by (rule compactI, simp add: fst_below_iff)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   302
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   303
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   304
by (rule compactI, simp add: snd_below_iff)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   305
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   306
lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31041
diff changeset
   307
by (rule compactI, simp add: below_prod_def)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   308
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   309
lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   310
apply (safe intro!: compact_Pair)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   311
apply (drule compact_fst, simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   312
apply (drule compact_snd, simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   313
done
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   314
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   315
instance prod :: (chfin, chfin) chfin
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   316
apply intro_classes
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   317
apply (erule compact_imp_max_in_chain)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   318
apply (case_tac "\<Squnion>i. Y i", simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   319
done
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   320
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   321
end