src/HOLCF/Product_Cpo.thy
author huffman
Fri, 08 May 2009 16:19:51 -0700
changeset 31076 99fe356cbbc2
parent 31041 85b4843d9939
child 31112 4dcda8ca5d59
permissions -rw-r--r--
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
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
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
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
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
    35
instantiation "*" :: (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
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"
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
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
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
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"
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
    84
by (simp add: monofun_def below_prod_def)
29531
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"
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
    87
by (simp add: monofun_def below_prod_def)
29531
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])
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
apply (simp add: below_prod_def is_ub_lub)
29531
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])
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
apply (simp add: below_prod_def is_lub_lub)
29531
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"
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
   137
    unfolding below_prod_def Pair_fst_snd_eq
29531
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"
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
   144
by (simp add: below_prod_def)
29531
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
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   152
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
   153
unfolding inst_cprod_pcpo by simp
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   154
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   155
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   156
unfolding inst_cprod_pcpo by (rule fst_conv)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   157
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   158
lemma csnd_strict [simp]: "snd \<bottom> = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   159
unfolding inst_cprod_pcpo by (rule snd_conv)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   160
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   161
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   162
by simp
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   163
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   164
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
   165
unfolding split_def by simp
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   166
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   167
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   168
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   169
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   170
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   171
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   172
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   173
apply (rule lub_const)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   174
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   175
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   176
lemma cont_pair2: "cont (\<lambda>y. (x, y))"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   177
apply (rule contI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   178
apply (rule is_lub_Pair)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   179
apply (rule lub_const)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   180
apply (erule cpo_lubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   181
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   182
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   183
lemma contlub_fst: "contlub fst"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   184
apply (rule contlubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   185
apply (simp add: thelub_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   186
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   187
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   188
lemma contlub_snd: "contlub snd"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   189
apply (rule contlubI)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   190
apply (simp add: thelub_cprod)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   191
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   192
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   193
lemma cont_fst: "cont fst"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   194
apply (rule monocontlub2cont)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   195
apply (rule monofun_fst)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   196
apply (rule contlub_fst)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   197
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   198
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   199
lemma cont_snd: "cont snd"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   200
apply (rule monocontlub2cont)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   201
apply (rule monofun_snd)
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   202
apply (rule contlub_snd)
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 cont2cont_Pair [cont2cont]:
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   206
  assumes f: "cont (\<lambda>x. f x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   207
  assumes g: "cont (\<lambda>x. g x)"
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   208
  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
   209
apply (rule cont_apply [OF f cont_pair1])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   210
apply (rule cont_apply [OF g cont_pair2])
29533
7f4a32134447 minimize dependencies
huffman
parents: 29531
diff changeset
   211
apply (rule cont_const)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   212
done
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   213
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   214
lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   215
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   216
lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   217
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   218
lemma cont2cont_split:
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   219
  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
   220
  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
   221
  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
   222
  assumes g: "cont (\<lambda>x. g x)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   223
  shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   224
unfolding split_def
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   225
apply (rule cont_apply [OF g])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   226
apply (rule cont_apply [OF cont_fst f2])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   227
apply (rule cont_apply [OF cont_snd f3])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   228
apply (rule cont_const)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   229
apply (rule f1)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   230
done
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   231
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   232
lemma cont_fst_snd_D1:
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   233
  "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
   234
by (drule cont_compose [OF _ cont_pair1], simp)
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   235
31041
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   236
lemma cont_fst_snd_D2:
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   237
  "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
   238
by (drule cont_compose [OF _ cont_pair2], simp)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   239
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   240
lemma cont2cont_split' [cont2cont]:
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   241
  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
   242
  assumes g: "cont (\<lambda>x. g x)"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   243
  shows "cont (\<lambda>x. split (f x) (g x))"
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   244
proof -
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   245
  note f1 = f [THEN cont_fst_snd_D1]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   246
  note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   247
  note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   248
  show ?thesis
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   249
    unfolding split_def
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   250
    apply (rule cont_apply [OF g])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   251
    apply (rule cont_apply [OF cont_fst f2])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   252
    apply (rule cont_apply [OF cont_snd f3])
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   253
    apply (rule cont_const)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   254
    apply (rule f1)
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   255
    done
85b4843d9939 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents: 29535
diff changeset
   256
qed
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   257
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   258
subsection {* Compactness and chain-finiteness *}
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   259
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
   260
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
   261
unfolding below_prod_def by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   262
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
   263
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
   264
unfolding below_prod_def by simp
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   265
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   266
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
   267
by (rule compactI, simp add: fst_below_iff)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   268
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   269
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
   270
by (rule compactI, simp add: snd_below_iff)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   271
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   272
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
   273
by (rule compactI, simp add: below_prod_def)
29535
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   274
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   275
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
   276
apply (safe intro!: compact_Pair)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   277
apply (drule compact_fst, simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   278
apply (drule compact_snd, simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   279
done
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
instance "*" :: (chfin, chfin) chfin
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   282
apply intro_classes
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   283
apply (erule compact_imp_max_in_chain)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   284
apply (case_tac "\<Squnion>i. Y i", simp)
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   285
done
08824fad8879 add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents: 29533
diff changeset
   286
29531
2eb29775b0b6 add Product_Cpo.thy
huffman
parents:
diff changeset
   287
end