src/HOL/HOLCF/Pcpo.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
child 54863 82acc20ded73
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: 41431
diff changeset
     1
(*  Title:      HOL/HOLCF/Pcpo.thy
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     2
    Author:     Franz Regensburger
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     3
*)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 15563
diff changeset
     4
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 15563
diff changeset
     5
header {* Classes cpo and pcpo *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 15563
diff changeset
     6
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     7
theory Pcpo
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
imports Porder
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
begin
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    11
subsection {* Complete partial orders *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    12
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    13
text {* The class cpo of chain complete partial orders *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    14
29614
1f7b1b0df292 simplified handling of base sort, dropped axclass
haftmann
parents: 29138
diff changeset
    15
class cpo = po +
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    16
  assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    17
begin
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    18
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    19
text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    20
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    21
lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40500
diff changeset
    22
  by (fast dest: cpo elim: is_lub_lub)
26026
f9647c040b58 add lemma cpo_lubI
huffman
parents: 26023
diff changeset
    23
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    24
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40500
diff changeset
    25
  by (blast dest: cpo intro: is_lub_lub)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    26
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    27
text {* Properties of the lub *}
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    28
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    29
lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40500
diff changeset
    30
  by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    31
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    32
lemma is_lub_thelub:
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    33
  "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40500
diff changeset
    34
  by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2])
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    35
39969
0b8e19f588a4 new lemmas about lub
huffman
parents: 39302
diff changeset
    36
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
0b8e19f588a4 new lemmas about lub
huffman
parents: 39302
diff changeset
    37
  by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
0b8e19f588a4 new lemmas about lub
huffman
parents: 39302
diff changeset
    38
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    39
lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    40
  by (simp add: lub_below_iff)
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    41
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    42
lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)"
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    43
  by (erule below_trans, erule is_ub_thelub)
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    44
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    45
lemma lub_range_mono:
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    46
  "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    47
    \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    48
apply (erule lub_below)
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    49
apply (subgoal_tac "\<exists>j. X i = Y j")
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    50
apply  clarsimp
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    51
apply  (erule is_ub_thelub)
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    52
apply auto
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    53
done
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    54
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    55
lemma lub_range_shift:
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    56
  "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
    57
apply (rule below_antisym)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    58
apply (rule lub_range_mono)
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    59
apply    fast
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    60
apply   assumption
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    61
apply (erule chain_shift)
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    62
apply (rule lub_below)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    63
apply assumption
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    64
apply (rule_tac i="i" in below_lub)
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    65
apply (erule chain_shift)
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 25921
diff changeset
    66
apply (erule chain_mono)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    67
apply (rule le_add1)
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    68
done
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    69
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    70
lemma maxinch_is_thelub:
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    71
  "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)"
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    72
apply (rule iffI)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40500
diff changeset
    73
apply (fast intro!: lub_eqI lub_finch1)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    74
apply (unfold max_in_chain_def)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
    75
apply (safe intro!: below_antisym)
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 25921
diff changeset
    76
apply (fast elim!: chain_mono)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    77
apply (drule sym)
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    78
apply (force elim!: is_ub_thelub)
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    79
done
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    80
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    81
text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    82
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    83
lemma lub_mono:
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
    84
  "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
    85
    \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
    86
by (fast elim: lub_below below_lub)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    87
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    88
text {* the = relation between two chains is preserved by their lubs *}
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    89
35492
5d200f2d7a4f add lemma lub_eq
huffman
parents: 33523
diff changeset
    90
lemma lub_eq:
5d200f2d7a4f add lemma lub_eq
huffman
parents: 33523
diff changeset
    91
  "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
5d200f2d7a4f add lemma lub_eq
huffman
parents: 33523
diff changeset
    92
  by simp
5d200f2d7a4f add lemma lub_eq
huffman
parents: 33523
diff changeset
    93
16203
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
    94
lemma ch2ch_lub:
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
    95
  assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
    96
  assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
    97
  shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
    98
apply (rule chainI)
25923
5fe4b543512e convert lemma lub_mono to rule_format
huffman
parents: 25922
diff changeset
    99
apply (rule lub_mono [OF 2 2])
16203
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
   100
apply (rule chainE [OF 1])
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
   101
done
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
   102
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   103
lemma diag_lub:
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   104
  assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   105
  assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   106
  shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
   107
proof (rule below_antisym)
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   108
  have 3: "chain (\<lambda>i. Y i i)"
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   109
    apply (rule chainI)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
   110
    apply (rule below_trans)
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   111
    apply (rule chainE [OF 1])
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   112
    apply (rule chainE [OF 2])
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   113
    done
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   114
  have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
16203
b3268fe39838 added theorem ch2ch_lub
huffman
parents: 16201
diff changeset
   115
    by (rule ch2ch_lub [OF 1 2])
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   116
  show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
   117
    apply (rule lub_below [OF 4])
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
   118
    apply (rule lub_below [OF 2])
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40498
diff changeset
   119
    apply (rule below_lub [OF 3])
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
   120
    apply (rule below_trans)
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 25921
diff changeset
   121
    apply (rule chain_mono [OF 1 le_maxI1])
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 25921
diff changeset
   122
    apply (rule chain_mono [OF 2 le_maxI2])
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   123
    done
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   124
  show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
25923
5fe4b543512e convert lemma lub_mono to rule_format
huffman
parents: 25922
diff changeset
   125
    apply (rule lub_mono [OF 3 4])
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   126
    apply (rule is_ub_thelub [OF 2])
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   127
    done
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   128
qed
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   129
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   130
lemma ex_lub:
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   131
  assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   132
  assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   133
  shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)"
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   134
  by (simp add: diag_lub 1 2)
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   135
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   136
end
16201
7bb51c8196cb added theorems diag_lub and ex_lub
huffman
parents: 16070
diff changeset
   137
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   138
subsection {* Pointed cpos *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   139
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   140
text {* The class pcpo of pointed cpos *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   141
29614
1f7b1b0df292 simplified handling of base sort, dropped axclass
haftmann
parents: 29138
diff changeset
   142
class pcpo = cpo +
1f7b1b0df292 simplified handling of base sort, dropped axclass
haftmann
parents: 29138
diff changeset
   143
  assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   144
begin
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   145
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   146
definition bottom :: "'a"
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   147
  where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   148
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   149
notation (xsymbols)
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   150
  bottom ("\<bottom>")
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   151
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   152
lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   153
unfolding bottom_def
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   154
apply (rule the1I2)
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   155
apply (rule ex_ex1I)
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   156
apply (rule least)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
   157
apply (blast intro: below_antisym)
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   158
apply simp
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   159
done
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   160
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   161
end
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   162
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   163
text {* Old "UU" syntax: *}
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   164
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   165
syntax UU :: logic
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   166
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   167
translations "UU" => "CONST bottom"
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   168
31024
0fdf666e08bf reimplement reorientation simproc using theory data
huffman
parents: 29634
diff changeset
   169
text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
16739
9ffd706ae402 add UU_reorient_simproc
huffman
parents: 16627
diff changeset
   170
31024
0fdf666e08bf reimplement reorientation simproc using theory data
huffman
parents: 29634
diff changeset
   171
setup {*
33523
96730ad673be modernized structure Reorient_Proc;
wenzelm
parents: 31076
diff changeset
   172
  Reorient_Proc.add
41429
cf5f025bc3c7 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents: 40774
diff changeset
   173
    (fn Const(@{const_name bottom}, _) => true | _ => false)
31024
0fdf666e08bf reimplement reorientation simproc using theory data
huffman
parents: 29634
diff changeset
   174
*}
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   175
33523
96730ad673be modernized structure Reorient_Proc;
wenzelm
parents: 31076
diff changeset
   176
simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   177
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   178
text {* useful lemmas about @{term \<bottom>} *}
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   179
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41429
diff changeset
   180
lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   181
by (simp add: po_eq_conv)
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   182
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41429
diff changeset
   183
lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   184
by simp
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   185
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41429
diff changeset
   186
lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41429
diff changeset
   187
by (subst eq_bottom_iff)
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
   188
40045
e0f372e18f3e add lemma lub_eq_bottom_iff
huffman
parents: 39969
diff changeset
   189
lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41429
diff changeset
   190
by (simp only: eq_bottom_iff lub_below_iff)
40045
e0f372e18f3e add lemma lub_eq_bottom_iff
huffman
parents: 39969
diff changeset
   191
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   192
subsection {* Chain-finite and flat cpos *}
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   193
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   194
text {* further useful classes for HOLCF domains *}
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   195
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   196
class chfin = po +
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   197
  assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   198
begin
25814
eb181909e7a4 new axclass finite_po < finite, po
huffman
parents: 25781
diff changeset
   199
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   200
subclass cpo
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   201
apply default
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   202
apply (frule chfin)
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   203
apply (blast intro: lub_finch1)
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   204
done
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   205
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   206
lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y"
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   207
  by (simp add: chfin finite_chain_def)
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   208
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   209
end
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   210
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   211
class flat = pcpo +
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   212
  assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   213
begin
15640
2d1d6ea579a1 chfin now a subclass of po, proved instance chfin < cpo
huffman
parents: 15588
diff changeset
   214
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   215
subclass chfin
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   216
apply default
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   217
apply (unfold max_in_chain_def)
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
   218
apply (case_tac "\<forall>i. Y i = \<bottom>")
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   219
apply simp
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   220
apply simp
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   221
apply (erule exE)
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
   222
apply (rule_tac x="i" in exI)
15588
14e3228f18cc arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   223
apply clarify
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 25921
diff changeset
   224
apply (blast dest: chain_mono ax_flat)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   225
done
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   226
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
   227
lemma flat_below_iff:
25826
f9aa43287e42 new lemma flat_less_iff
huffman
parents: 25814
diff changeset
   228
  shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   229
  by (safe dest!: ax_flat)
25826
f9aa43287e42 new lemma flat_less_iff
huffman
parents: 25814
diff changeset
   230
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   231
lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   232
  by (safe dest!: ax_flat)
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   233
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   234
end
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
   235
40091
1ca61fbd8a79 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents: 40089
diff changeset
   236
subsection {* Discrete cpos *}
26023
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   237
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 31071
diff changeset
   238
class discrete_cpo = below +
29614
1f7b1b0df292 simplified handling of base sort, dropped axclass
haftmann
parents: 29138
diff changeset
   239
  assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   240
begin
26023
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   241
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   242
subclass po
29614
1f7b1b0df292 simplified handling of base sort, dropped axclass
haftmann
parents: 29138
diff changeset
   243
proof qed simp_all
26023
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   244
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   245
text {* In a discrete cpo, every chain is constant *}
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   246
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   247
lemma discrete_chain_const:
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   248
  assumes S: "chain S"
26023
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   249
  shows "\<exists>x. S = (\<lambda>i. x)"
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   250
proof (intro exI ext)
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   251
  fix i :: nat
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   252
  have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono)
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   253
  hence "S 0 = S i" by simp
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   254
  thus "S i = S 0" by (rule sym)
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   255
qed
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   256
40091
1ca61fbd8a79 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents: 40089
diff changeset
   257
subclass chfin
26023
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   258
proof
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   259
  fix S :: "nat \<Rightarrow> 'a"
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   260
  assume S: "chain S"
40091
1ca61fbd8a79 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents: 40089
diff changeset
   261
  hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const)
1ca61fbd8a79 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents: 40089
diff changeset
   262
  hence "max_in_chain 0 S"
1ca61fbd8a79 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents: 40089
diff changeset
   263
    unfolding max_in_chain_def by auto
1ca61fbd8a79 make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents: 40089
diff changeset
   264
  thus "\<exists>i. max_in_chain i S" ..
26023
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   265
qed
29c1e3e98276 new discrete_cpo axclass
huffman
parents: 25923
diff changeset
   266
31071
845a6acd3bf3 localized (complete) partial order classes
haftmann
parents: 31024
diff changeset
   267
end
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 15563
diff changeset
   268
16626
d28314d2dce3 cleaned up
huffman
parents: 16203
diff changeset
   269
end