src/HOL/HOLCF/Up.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46125 00cd193a48dc
child 58249 180f1b3508ed
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/Up.thy
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40327
diff changeset
     2
    Author:     Franz Regensburger
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40327
diff changeset
     3
    Author:     Brian Huffman
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
header {* The type of lifted values *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
theory Up
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40327
diff changeset
     9
imports Cfun
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
begin
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    11
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35900
diff changeset
    12
default_sort cpo
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    13
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    14
subsection {* Definition of new type for lifting *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    15
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    16
datatype 'a u = Ibottom | Iup 'a
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
35427
ad039d29e01c proper (type_)notation;
wenzelm
parents: 34941
diff changeset
    18
type_notation (xsymbols)
ad039d29e01c proper (type_)notation;
wenzelm
parents: 34941
diff changeset
    19
  u  ("(_\<^sub>\<bottom>)" [1000] 999)
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    20
34941
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 33808
diff changeset
    21
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 33808
diff changeset
    22
    "Ifup f Ibottom = \<bottom>"
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 33808
diff changeset
    23
 |  "Ifup f (Iup x) = f\<cdot>x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    25
subsection {* Ordering on lifted cpo *}
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    26
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    27
instantiation u :: (cpo) below
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    28
begin
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    30
definition
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    31
  below_up_def:
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    32
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    33
      (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    35
instance ..
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    36
end
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    37
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    38
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    39
by (simp add: below_up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
    41
lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    42
by (simp add: below_up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    44
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    45
by (simp add: below_up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    47
subsection {* Lifted cpo is a partial order *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    49
instance u :: (cpo) po
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    50
proof
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    51
  fix x :: "'a u"
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    52
  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: 29530
diff changeset
    53
    unfolding below_up_def by (simp split: u.split)
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    54
next
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    55
  fix x y :: "'a u"
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    56
  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: 29530
diff changeset
    57
    unfolding below_up_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    58
    by (auto split: u.split_asm intro: below_antisym)
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    59
next
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    60
  fix x y z :: "'a u"
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    61
  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: 29530
diff changeset
    62
    unfolding below_up_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
    63
    by (auto split: u.split_asm intro: below_trans)
25787
398dec10518e update sq_ord/po instance proofs
huffman
parents: 25785
diff changeset
    64
qed
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    66
subsection {* Lifted cpo is a cpo *}
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    67
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    68
lemma is_lub_Iup:
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    69
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    70
unfolding is_lub_def is_ub_def ball_simps
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    71
by (auto simp add: below_up_def split: u.split)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    72
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
    73
lemma up_chain_lemma:
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    74
  assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    75
  | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    76
proof (cases "\<exists>k. Y k \<noteq> Ibottom")
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    77
  case True
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    78
  then obtain k where k: "Y k \<noteq> Ibottom" ..
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    79
  def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    80
  have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    81
  proof
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    82
    fix i :: nat
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    83
    from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    84
    with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    85
    thus "Iup (A i) = Y (i + k)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    86
      by (cases "Y (i + k)", simp_all add: A_def)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    87
  qed
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    88
  from Y have chain_A: "chain A"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    89
    unfolding chain_def Iup_below [symmetric]
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    90
    by (simp add: Iup_A)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    91
  hence "range A <<| (\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    92
    by (rule cpo_lubI)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    93
  hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    94
    by (rule is_lub_Iup)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    95
  hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    96
    by (simp only: Iup_A)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    97
  hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    98
    by (simp only: is_lub_range_shift [OF Y])
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
    99
  with Iup_A chain_A show ?thesis ..
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   100
next
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   101
  case False
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   102
  then have "\<forall>i. Y i = Ibottom" by simp
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   103
  then show ?thesis ..
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   104
qed
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   105
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   106
instance u :: (cpo) cpo
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   107
proof
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   108
  fix S :: "nat \<Rightarrow> 'a u"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   109
  assume S: "chain S"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   110
  thus "\<exists>x. range (\<lambda>i. S i) <<| x"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   111
  proof (rule up_chain_lemma)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   112
    assume "\<forall>i. S i = Ibottom"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   113
    hence "range (\<lambda>i. S i) <<| Ibottom"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40502
diff changeset
   114
      by (simp add: is_lub_const)
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   115
    thus ?thesis ..
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   116
  next
40085
c157ff4d59a6 add type annotation to avoid warning
huffman
parents: 40084
diff changeset
   117
    fix A :: "nat \<Rightarrow> 'a"
c157ff4d59a6 add type annotation to avoid warning
huffman
parents: 40084
diff changeset
   118
    assume "range S <<| Iup (\<Squnion>i. A i)"
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   119
    thus ?thesis ..
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   120
  qed
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   121
qed
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   122
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
   123
subsection {* Lifted cpo is pointed *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   124
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   125
instance u :: (cpo) pcpo
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   126
by intro_classes fast
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   127
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   128
text {* for compatibility with old HOLCF-Version *}
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   129
lemma inst_up_pcpo: "\<bottom> = Ibottom"
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41182
diff changeset
   130
by (rule minimal_up [THEN bottomI, symmetric])
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   131
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 35783
diff changeset
   132
subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   133
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   134
text {* continuity for @{term Iup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   135
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   136
lemma cont_Iup: "cont Iup"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   137
apply (rule contI)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   138
apply (rule is_lub_Iup)
26027
87cb69d27558 add lemma cpo_lubI
huffman
parents: 25922
diff changeset
   139
apply (erule cpo_lubI)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   140
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   141
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   142
text {* continuity for @{term Ifup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   143
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   144
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   145
by (induct x, simp_all)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   146
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   147
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   148
apply (rule monofunI)
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   149
apply (case_tac x, simp)
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   150
apply (case_tac y, simp)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   151
apply (simp add: monofun_cfun_arg)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   152
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   153
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   154
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   155
proof (rule contI2)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   156
  fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   157
  from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   158
  proof (rule up_chain_lemma)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   159
    fix A and k
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   160
    assume A: "\<forall>i. Iup (A i) = Y (i + k)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   161
    assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   162
    hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40502
diff changeset
   163
      by (simp add: lub_eqI contlub_cfun_arg)
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   164
    also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   165
      by (simp add: A)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   166
    also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   167
      using Y' by (rule lub_range_shift)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   168
    finally show ?thesis by simp
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   169
  qed simp
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   170
qed (rule monofun_Ifup2)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   171
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   172
subsection {* Continuous versions of constants *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   173
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
   174
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
   175
  up  :: "'a \<rightarrow> 'a u" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
   176
  "up = (\<Lambda> x. Iup x)"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   177
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
   178
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
   179
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
   180
  "fup = (\<Lambda> f p. Ifup f p)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   181
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   182
translations
26046
1624b3304bb9 fix broken syntax translations
huffman
parents: 26027
diff changeset
   183
  "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 42151
diff changeset
   184
  "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
26046
1624b3304bb9 fix broken syntax translations
huffman
parents: 26027
diff changeset
   185
  "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   186
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   187
text {* continuous versions of lemmas for @{typ "('a)u"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   188
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   189
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   190
apply (induct z)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   191
apply (simp add: inst_up_pcpo)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   192
apply (simp add: up_def cont_Iup)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   193
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   194
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   195
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   196
by (simp add: up_def cont_Iup)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   198
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   199
by simp
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   200
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   201
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   202
by (simp add: up_def cont_Iup inst_up_pcpo)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   203
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
   204
lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
   205
by simp (* FIXME: remove? *)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   206
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29530
diff changeset
   207
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   208
by (simp add: up_def cont_Iup)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   209
35783
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35427
diff changeset
   210
lemma upE [case_names bottom up, cases type: u]:
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35427
diff changeset
   211
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
25788
30cbe0764599 declare upE as cases rule; add new rule up_induct
huffman
parents: 25787
diff changeset
   212
apply (cases p)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   213
apply (simp add: inst_up_pcpo)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   214
apply (simp add: up_def cont_Iup)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   215
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   216
35783
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35427
diff changeset
   217
lemma up_induct [case_names bottom up, induct type: u]:
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35427
diff changeset
   218
  "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
25788
30cbe0764599 declare upE as cases rule; add new rule up_induct
huffman
parents: 25787
diff changeset
   219
by (cases x, simp_all)
30cbe0764599 declare upE as cases rule; add new rule up_induct
huffman
parents: 25787
diff changeset
   220
25827
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25789
diff changeset
   221
text {* lifting preserves chain-finiteness *}
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25789
diff changeset
   222
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   223
lemma up_chain_cases:
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   224
  assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   225
  | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   226
apply (rule up_chain_lemma [OF Y])
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40502
diff changeset
   227
apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   228
done
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   229
25879
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   230
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   231
apply (rule compactI2)
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   232
apply (erule up_chain_cases)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   233
apply simp
25879
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   234
apply (drule (1) compactD2, simp)
40084
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   235
apply (erule exE)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   236
apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
23a1cfdb5acb simplify some proofs, convert to Isar style
huffman
parents: 40002
diff changeset
   237
apply (simp, erule exI)
25879
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   238
done
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   239
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   240
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   241
unfolding compact_def
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40089
diff changeset
   242
by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
25879
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   243
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   244
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   245
by (safe elim!: compact_up compact_upD)
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   246
25827
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25789
diff changeset
   247
instance u :: (chfin) chfin
25921
0ca392ab7f37 change class axiom chfin to rule_format
huffman
parents: 25911
diff changeset
   248
apply intro_classes
25879
98b93782c3b1 new compactness lemmas
huffman
parents: 25827
diff changeset
   249
apply (erule compact_imp_max_in_chain)
25898
d8f17d8cf9d4 compact_chfin is now declared simp
huffman
parents: 25879
diff changeset
   250
apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   251
done
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   252
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   253
text {* properties of fup *}
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   254
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   255
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   256
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   257
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   258
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 29138
diff changeset
   259
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   260
16553
aa36d41e4263 add csplit3, ssplit3, fup3 as simp rules
huffman
parents: 16326
diff changeset
   261
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
25788
30cbe0764599 declare upE as cases rule; add new rule up_induct
huffman
parents: 25787
diff changeset
   262
by (cases x, simp_all)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   263
26962
c8b20f615d6c use new class package for classes profinite, bifinite; remove approx class
huffman
parents: 26407
diff changeset
   264
end