src/HOL/HOLCF/Product_Cpo.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44066 d74182c93f04
child 55414 eab03e9cee8a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41430
diff changeset
     1
(*  Title:      HOL/HOLCF/Product_Cpo.thy
29531
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
40090
d57357cda8bb direct instantiation unit :: discrete_cpo
huffman
parents: 40089
diff changeset
    15
instantiation unit :: discrete_cpo
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
40090
d57357cda8bb direct instantiation unit :: discrete_cpo
huffman
parents: 40089
diff changeset
    21
instance proof
d57357cda8bb direct instantiation unit :: discrete_cpo
huffman
parents: 40089
diff changeset
    22
qed simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    23
40090
d57357cda8bb direct instantiation unit :: discrete_cpo
huffman
parents: 40089
diff changeset
    24
end
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    25
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    26
instance unit :: pcpo
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    27
by intro_classes simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    28
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    29
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    30
subsection {* Product type is a partial order *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    31
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
    32
instantiation prod :: (below, below) below
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    33
begin
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    34
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    35
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
    36
  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
    37
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    38
instance ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    39
end
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    40
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
    41
instance prod :: (po, po) po
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    42
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    43
  fix x :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    44
  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
    45
    unfolding below_prod_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    46
next
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    47
  fix x y :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    48
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
44066
d74182c93f04 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents: 42151
diff changeset
    49
    unfolding below_prod_def prod_eq_iff
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
    50
    by (fast intro: below_antisym)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    51
next
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    52
  fix x y z :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    53
  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
    54
    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
    55
    by (fast intro: below_trans)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    56
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    57
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 33506
diff changeset
    58
subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    59
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
    60
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
    61
unfolding below_prod_def by simp
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 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
    64
unfolding below_prod_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    65
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    66
text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    67
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    68
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    69
by (simp add: monofun_def)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    70
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    71
lemma monofun_pair2: "monofun (\<lambda>y. (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_pair:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    75
  "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    76
by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    77
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    78
lemma ch2ch_Pair [simp]:
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    79
  "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    80
by (rule chainI, simp add: chainE)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    81
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    82
text {* @{term fst} and @{term snd} are monotone *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    83
35919
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    84
lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    85
unfolding below_prod_def by simp
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    86
676c6005ad03 add lemmas fst_monofun, snd_monofun
huffman
parents: 35914
diff changeset
    87
lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd 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
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    90
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
    91
by (simp add: monofun_def below_prod_def)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    92
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    93
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
    94
by (simp add: monofun_def below_prod_def)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
    95
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    96
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    97
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    98
lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
    99
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   100
lemma prod_chain_cases:
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   101
  assumes "chain Y"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   102
  obtains A B
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   103
  where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   104
proof
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   105
  from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   106
  from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   107
  show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   108
qed
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   109
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   110
subsection {* Product type is a cpo *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   111
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   112
lemma is_lub_Pair:
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   113
  "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   114
unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   115
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   116
lemma lub_Pair:
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   117
  "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   118
    \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   119
by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
31112
4dcda8ca5d59 new lemmas
huffman
parents: 31076
diff changeset
   120
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   121
lemma is_lub_prod:
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   122
  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   123
  assumes S: "chain S"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   124
  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   125
using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   126
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   127
lemma lub_prod:
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   128
  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   129
    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   130
by (rule is_lub_prod [THEN lub_eqI])
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   131
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   132
instance prod :: (cpo, cpo) cpo
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   133
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   134
  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   135
  assume "chain S"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   136
  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   137
    by (rule is_lub_prod)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   138
  thus "\<exists>x. range S <<| x" ..
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   139
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   140
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   141
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   142
proof
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   143
  fix x y :: "'a \<times> 'b"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   144
  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
44066
d74182c93f04 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents: 42151
diff changeset
   145
    unfolding below_prod_def prod_eq_iff
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   146
    by simp
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   147
qed
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   148
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   149
subsection {* Product type is pointed *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   150
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   151
lemma minimal_prod: "(\<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
   152
by (simp add: below_prod_def)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   153
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   154
instance prod :: (pcpo, pcpo) pcpo
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   155
by intro_classes (fast intro: minimal_prod)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   156
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   157
lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 40774
diff changeset
   158
by (rule minimal_prod [THEN bottomI, symmetric])
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   159
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40090
diff changeset
   160
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   161
unfolding inst_prod_pcpo by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   162
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   163
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   164
unfolding inst_prod_pcpo by (rule fst_conv)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   165
33506
afb577487b15 fix name of lemma snd_strict
huffman
parents: 31112
diff changeset
   166
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   167
unfolding inst_prod_pcpo by (rule snd_conv)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   168
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   169
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   170
by simp
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   171
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   172
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
   173
unfolding split_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   174
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 33506
diff changeset
   175
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   176
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   177
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   178
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   179
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   180
apply (erule cpo_lubI)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   181
apply (rule is_lub_const)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   182
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   183
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   184
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   185
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   186
apply (rule is_lub_Pair)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   187
apply (rule is_lub_const)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   188
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   189
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   190
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   191
lemma cont_fst: "cont fst"
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   192
apply (rule contI)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   193
apply (simp add: lub_prod)
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   194
apply (erule cpo_lubI [OF ch2ch_fst])
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   195
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   196
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   197
lemma cont_snd: "cont snd"
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   198
apply (rule contI)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40619
diff changeset
   199
apply (simp add: lub_prod)
35914
91a7311177c4 remove contlub predicate
huffman
parents: 35900
diff changeset
   200
apply (erule cpo_lubI [OF ch2ch_snd])
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   201
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   202
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36452
diff changeset
   203
lemma cont2cont_Pair [simp, cont2cont]:
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   204
  assumes f: "cont (\<lambda>x. f x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   205
  assumes g: "cont (\<lambda>x. g x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   206
  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
   207
apply (rule cont_apply [OF f cont_pair1])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   208
apply (rule cont_apply [OF g cont_pair2])
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   209
apply (rule cont_const)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   210
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   211
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36452
diff changeset
   212
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
   213
37079
0cd15d8c90a0 remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents: 36452
diff changeset
   214
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
   215
39808
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   216
lemma cont2cont_prod_case:
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   217
  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
   218
  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
   219
  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
   220
  assumes g: "cont (\<lambda>x. g x)"
39144
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   221
  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
   222
unfolding split_def
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   223
apply (rule cont_apply [OF g])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   224
apply (rule cont_apply [OF cont_fst f2])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   225
apply (rule cont_apply [OF cont_snd f3])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   226
apply (rule cont_const)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   227
apply (rule f1)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   228
done
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   229
39808
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   230
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
   231
  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
   232
  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
   233
  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
   234
proof -
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   235
  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
   236
    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
   237
  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
   238
    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
   239
qed
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   240
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   241
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
   242
  "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
   243
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
   244
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
   245
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
   246
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
   247
done
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   248
1410c84013b9 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents: 39144
diff changeset
   249
lemma cont2cont_prod_case' [simp, cont2cont]:
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   250
  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
   251
  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
   252
  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
   253
using assms by (simp add: cont2cont_prod_case prod_cont_iff)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   254
39144
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   255
text {* The simple version (due to Joachim Breitner) is needed if
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   256
  either element type of the pair is not a cpo. *}
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   257
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   258
lemma cont2cont_split_simple [simp, cont2cont]:
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   259
 assumes "\<And>a b. cont (\<lambda>x. f x a b)"
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   260
 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
   261
using assms by (cases p) auto
23b1e6759359 add lemma cont2cont_split_simple
huffman
parents: 37678
diff changeset
   262
40619
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   263
text {* Admissibility of predicates on product types. *}
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   264
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   265
lemma adm_prod_case [simp]:
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   266
  assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   267
  shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   268
unfolding prod_case_beta using assms .
84edf7177d73 add lemma adm_prod_case
huffman
parents: 40321
diff changeset
   269
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   270
subsection {* Compactness and chain-finiteness *}
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   271
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
   272
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
   273
unfolding below_prod_def by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   274
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
   275
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
   276
unfolding below_prod_def by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   277
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   278
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
   279
by (rule compactI, simp add: fst_below_iff)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   280
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   281
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
   282
by (rule compactI, simp add: snd_below_iff)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   283
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   284
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
   285
by (rule compactI, simp add: below_prod_def)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   286
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   287
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
   288
apply (safe intro!: compact_Pair)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   289
apply (drule compact_fst, simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   290
apply (drule compact_snd, simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   291
done
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   292
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37079
diff changeset
   293
instance prod :: (chfin, chfin) chfin
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   294
apply intro_classes
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   295
apply (erule compact_imp_max_in_chain)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   296
apply (case_tac "\<Squnion>i. Y i", simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   297
done
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   298
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   299
end