src/HOL/HOLCF/Up.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 46125 00cd193a48dc
child 58249 180f1b3508ed
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Up.thy
huffman@40502
     2
    Author:     Franz Regensburger
huffman@40502
     3
    Author:     Brian Huffman
huffman@15576
     4
*)
huffman@15576
     5
huffman@15576
     6
header {* The type of lifted values *}
huffman@15576
     7
huffman@15577
     8
theory Up
huffman@40502
     9
imports Cfun
huffman@15577
    10
begin
huffman@15576
    11
wenzelm@36452
    12
default_sort cpo
huffman@15599
    13
huffman@15593
    14
subsection {* Definition of new type for lifting *}
huffman@15576
    15
huffman@16753
    16
datatype 'a u = Ibottom | Iup 'a
huffman@15576
    17
wenzelm@35427
    18
type_notation (xsymbols)
wenzelm@35427
    19
  u  ("(_\<^sub>\<bottom>)" [1000] 999)
huffman@18290
    20
haftmann@34941
    21
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
haftmann@34941
    22
    "Ifup f Ibottom = \<bottom>"
haftmann@34941
    23
 |  "Ifup f (Iup x) = f\<cdot>x"
huffman@15576
    24
huffman@18290
    25
subsection {* Ordering on lifted cpo *}
huffman@15593
    26
huffman@31076
    27
instantiation u :: (cpo) below
huffman@25787
    28
begin
huffman@15576
    29
huffman@25787
    30
definition
huffman@31076
    31
  below_up_def:
huffman@16753
    32
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
huffman@16753
    33
      (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
huffman@15576
    34
huffman@25787
    35
instance ..
huffman@25787
    36
end
huffman@25787
    37
huffman@16753
    38
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
huffman@31076
    39
by (simp add: below_up_def)
huffman@15576
    40
huffman@41182
    41
lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
huffman@31076
    42
by (simp add: below_up_def)
huffman@15576
    43
huffman@31076
    44
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
huffman@31076
    45
by (simp add: below_up_def)
huffman@15576
    46
huffman@18290
    47
subsection {* Lifted cpo is a partial order *}
huffman@15576
    48
huffman@15599
    49
instance u :: (cpo) po
huffman@25787
    50
proof
huffman@25787
    51
  fix x :: "'a u"
huffman@25787
    52
  show "x \<sqsubseteq> x"
huffman@31076
    53
    unfolding below_up_def by (simp split: u.split)
huffman@25787
    54
next
huffman@25787
    55
  fix x y :: "'a u"
huffman@25787
    56
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
huffman@31076
    57
    unfolding below_up_def
huffman@31076
    58
    by (auto split: u.split_asm intro: below_antisym)
huffman@25787
    59
next
huffman@25787
    60
  fix x y z :: "'a u"
huffman@25787
    61
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
huffman@31076
    62
    unfolding below_up_def
huffman@31076
    63
    by (auto split: u.split_asm intro: below_trans)
huffman@25787
    64
qed
huffman@15576
    65
huffman@18290
    66
subsection {* Lifted cpo is a cpo *}
huffman@15593
    67
huffman@16319
    68
lemma is_lub_Iup:
huffman@16319
    69
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
huffman@40084
    70
unfolding is_lub_def is_ub_def ball_simps
huffman@40084
    71
by (auto simp add: below_up_def split: u.split)
huffman@15599
    72
huffman@17838
    73
lemma up_chain_lemma:
huffman@40084
    74
  assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom"
huffman@40084
    75
  | A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
huffman@40084
    76
proof (cases "\<exists>k. Y k \<noteq> Ibottom")
huffman@40084
    77
  case True
huffman@40084
    78
  then obtain k where k: "Y k \<noteq> Ibottom" ..
huffman@40084
    79
  def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)"
huffman@40084
    80
  have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)"
huffman@40084
    81
  proof
huffman@40084
    82
    fix i :: nat
huffman@40084
    83
    from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)
huffman@40084
    84
    with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto)
huffman@40084
    85
    thus "Iup (A i) = Y (i + k)"
huffman@40084
    86
      by (cases "Y (i + k)", simp_all add: A_def)
huffman@40084
    87
  qed
huffman@40084
    88
  from Y have chain_A: "chain A"
huffman@40084
    89
    unfolding chain_def Iup_below [symmetric]
huffman@40084
    90
    by (simp add: Iup_A)
huffman@40084
    91
  hence "range A <<| (\<Squnion>i. A i)"
huffman@40084
    92
    by (rule cpo_lubI)
huffman@40084
    93
  hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)"
huffman@40084
    94
    by (rule is_lub_Iup)
huffman@40084
    95
  hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)"
huffman@40084
    96
    by (simp only: Iup_A)
huffman@40084
    97
  hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)"
huffman@40084
    98
    by (simp only: is_lub_range_shift [OF Y])
huffman@40084
    99
  with Iup_A chain_A show ?thesis ..
huffman@40084
   100
next
huffman@40084
   101
  case False
huffman@40084
   102
  then have "\<forall>i. Y i = Ibottom" by simp
huffman@40084
   103
  then show ?thesis ..
huffman@40084
   104
qed
huffman@15576
   105
huffman@15599
   106
instance u :: (cpo) cpo
huffman@40084
   107
proof
huffman@40084
   108
  fix S :: "nat \<Rightarrow> 'a u"
huffman@40084
   109
  assume S: "chain S"
huffman@40084
   110
  thus "\<exists>x. range (\<lambda>i. S i) <<| x"
huffman@40084
   111
  proof (rule up_chain_lemma)
huffman@40084
   112
    assume "\<forall>i. S i = Ibottom"
huffman@40084
   113
    hence "range (\<lambda>i. S i) <<| Ibottom"
huffman@40771
   114
      by (simp add: is_lub_const)
huffman@40084
   115
    thus ?thesis ..
huffman@40084
   116
  next
huffman@40085
   117
    fix A :: "nat \<Rightarrow> 'a"
huffman@40085
   118
    assume "range S <<| Iup (\<Squnion>i. A i)"
huffman@40084
   119
    thus ?thesis ..
huffman@40084
   120
  qed
huffman@40084
   121
qed
huffman@15593
   122
huffman@18290
   123
subsection {* Lifted cpo is pointed *}
huffman@15576
   124
huffman@15599
   125
instance u :: (cpo) pcpo
huffman@40084
   126
by intro_classes fast
huffman@15593
   127
huffman@15593
   128
text {* for compatibility with old HOLCF-Version *}
huffman@16753
   129
lemma inst_up_pcpo: "\<bottom> = Ibottom"
huffman@41430
   130
by (rule minimal_up [THEN bottomI, symmetric])
huffman@15593
   131
huffman@35900
   132
subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
huffman@15593
   133
huffman@15593
   134
text {* continuity for @{term Iup} *}
huffman@15576
   135
huffman@16319
   136
lemma cont_Iup: "cont Iup"
huffman@16215
   137
apply (rule contI)
huffman@15599
   138
apply (rule is_lub_Iup)
huffman@26027
   139
apply (erule cpo_lubI)
huffman@15576
   140
done
huffman@15576
   141
huffman@15593
   142
text {* continuity for @{term Ifup} *}
huffman@15576
   143
huffman@16319
   144
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
huffman@16753
   145
by (induct x, simp_all)
huffman@15576
   146
huffman@16319
   147
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
huffman@16319
   148
apply (rule monofunI)
huffman@16753
   149
apply (case_tac x, simp)
huffman@16753
   150
apply (case_tac y, simp)
huffman@16319
   151
apply (simp add: monofun_cfun_arg)
huffman@15576
   152
done
huffman@15576
   153
huffman@16319
   154
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
huffman@40084
   155
proof (rule contI2)
huffman@40084
   156
  fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))"
huffman@40084
   157
  from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"
huffman@40084
   158
  proof (rule up_chain_lemma)
huffman@40084
   159
    fix A and k
huffman@40084
   160
    assume A: "\<forall>i. Iup (A i) = Y (i + k)"
huffman@40084
   161
    assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
huffman@40084
   162
    hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
huffman@40771
   163
      by (simp add: lub_eqI contlub_cfun_arg)
huffman@40084
   164
    also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
huffman@40084
   165
      by (simp add: A)
huffman@40084
   166
    also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
huffman@40084
   167
      using Y' by (rule lub_range_shift)
huffman@40084
   168
    finally show ?thesis by simp
huffman@40084
   169
  qed simp
huffman@40084
   170
qed (rule monofun_Ifup2)
huffman@15576
   171
huffman@15593
   172
subsection {* Continuous versions of constants *}
huffman@15576
   173
wenzelm@25131
   174
definition
wenzelm@25131
   175
  up  :: "'a \<rightarrow> 'a u" where
wenzelm@25131
   176
  "up = (\<Lambda> x. Iup x)"
huffman@16319
   177
wenzelm@25131
   178
definition
wenzelm@25131
   179
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
wenzelm@25131
   180
  "fup = (\<Lambda> f p. Ifup f p)"
huffman@15593
   181
huffman@15593
   182
translations
huffman@26046
   183
  "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
wenzelm@46125
   184
  "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
huffman@26046
   185
  "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
huffman@15593
   186
huffman@15593
   187
text {* continuous versions of lemmas for @{typ "('a)u"} *}
huffman@15576
   188
huffman@16753
   189
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
huffman@16753
   190
apply (induct z)
huffman@16319
   191
apply (simp add: inst_up_pcpo)
huffman@16319
   192
apply (simp add: up_def cont_Iup)
huffman@15576
   193
done
huffman@15576
   194
huffman@16753
   195
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
huffman@16319
   196
by (simp add: up_def cont_Iup)
huffman@15576
   197
huffman@16753
   198
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
huffman@16753
   199
by simp
huffman@16319
   200
huffman@17838
   201
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
huffman@16319
   202
by (simp add: up_def cont_Iup inst_up_pcpo)
huffman@15576
   203
huffman@41182
   204
lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
huffman@31076
   205
by simp (* FIXME: remove? *)
huffman@15576
   206
huffman@31076
   207
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
huffman@16319
   208
by (simp add: up_def cont_Iup)
huffman@16319
   209
huffman@35783
   210
lemma upE [case_names bottom up, cases type: u]:
huffman@35783
   211
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@25788
   212
apply (cases p)
huffman@16319
   213
apply (simp add: inst_up_pcpo)
huffman@16319
   214
apply (simp add: up_def cont_Iup)
huffman@15576
   215
done
huffman@15576
   216
huffman@35783
   217
lemma up_induct [case_names bottom up, induct type: u]:
huffman@35783
   218
  "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
huffman@25788
   219
by (cases x, simp_all)
huffman@25788
   220
huffman@25827
   221
text {* lifting preserves chain-finiteness *}
huffman@25827
   222
huffman@17838
   223
lemma up_chain_cases:
huffman@40084
   224
  assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
huffman@40084
   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)"
huffman@40084
   226
apply (rule up_chain_lemma [OF Y])
huffman@40771
   227
apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
huffman@40084
   228
done
huffman@17838
   229
huffman@25879
   230
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
huffman@25879
   231
apply (rule compactI2)
huffman@40084
   232
apply (erule up_chain_cases)
huffman@40084
   233
apply simp
huffman@25879
   234
apply (drule (1) compactD2, simp)
huffman@40084
   235
apply (erule exE)
huffman@40084
   236
apply (drule_tac f="up" and x="x" in monofun_cfun_arg)
huffman@40084
   237
apply (simp, erule exI)
huffman@25879
   238
done
huffman@25879
   239
huffman@25879
   240
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
huffman@25879
   241
unfolding compact_def
huffman@40327
   242
by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
huffman@25879
   243
huffman@25879
   244
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
huffman@25879
   245
by (safe elim!: compact_up compact_upD)
huffman@25879
   246
huffman@25827
   247
instance u :: (chfin) chfin
huffman@25921
   248
apply intro_classes
huffman@25879
   249
apply (erule compact_imp_max_in_chain)
huffman@25898
   250
apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
huffman@17838
   251
done
huffman@17838
   252
huffman@17838
   253
text {* properties of fup *}
huffman@17838
   254
huffman@16319
   255
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@29530
   256
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
huffman@15576
   257
huffman@16319
   258
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
huffman@29530
   259
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
huffman@15576
   260
huffman@16553
   261
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
huffman@25788
   262
by (cases x, simp_all)
huffman@15576
   263
huffman@26962
   264
end