src/HOLCF/Up.thy
author huffman
Fri Jan 04 00:01:02 2008 +0100 (2008-01-04)
changeset 25827 c2adeb1bae5c
parent 25789 c0506ac5b6b4
child 25879 98b93782c3b1
permissions -rw-r--r--
new instance proofs for classes finite_po, chfin, flat
huffman@15599
     1
(*  Title:      HOLCF/Up.thy
huffman@15576
     2
    ID:         $Id$
wenzelm@16070
     3
    Author:     Franz Regensburger and Brian Huffman
huffman@15576
     4
huffman@15576
     5
Lifting.
huffman@15576
     6
*)
huffman@15576
     7
huffman@15576
     8
header {* The type of lifted values *}
huffman@15576
     9
huffman@15577
    10
theory Up
huffman@19105
    11
imports Cfun
huffman@15577
    12
begin
huffman@15576
    13
huffman@15599
    14
defaultsort cpo
huffman@15599
    15
huffman@15593
    16
subsection {* Definition of new type for lifting *}
huffman@15576
    17
huffman@16753
    18
datatype 'a u = Ibottom | Iup 'a
huffman@15576
    19
huffman@18290
    20
syntax (xsymbols)
huffman@18290
    21
  "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
huffman@18290
    22
huffman@15576
    23
consts
huffman@16753
    24
  Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
huffman@15576
    25
huffman@16753
    26
primrec
huffman@16753
    27
  "Ifup f Ibottom = \<bottom>"
huffman@16753
    28
  "Ifup f (Iup x) = f\<cdot>x"
huffman@15576
    29
huffman@18290
    30
subsection {* Ordering on lifted cpo *}
huffman@15593
    31
huffman@25787
    32
instantiation u :: (cpo) sq_ord
huffman@25787
    33
begin
huffman@15576
    34
huffman@25787
    35
definition
huffman@16753
    36
  less_up_def:
huffman@16753
    37
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
huffman@16753
    38
      (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
huffman@15576
    39
huffman@25787
    40
instance ..
huffman@25787
    41
end
huffman@25787
    42
huffman@16753
    43
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
huffman@16753
    44
by (simp add: less_up_def)
huffman@15576
    45
huffman@16753
    46
lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
huffman@16753
    47
by (simp add: less_up_def)
huffman@15576
    48
huffman@16319
    49
lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
huffman@16753
    50
by (simp add: less_up_def)
huffman@15576
    51
huffman@18290
    52
subsection {* Lifted cpo is a partial order *}
huffman@15576
    53
huffman@15599
    54
instance u :: (cpo) po
huffman@25787
    55
proof
huffman@25787
    56
  fix x :: "'a u"
huffman@25787
    57
  show "x \<sqsubseteq> x"
huffman@25787
    58
    unfolding less_up_def by (simp split: u.split)
huffman@25787
    59
next
huffman@25787
    60
  fix x y :: "'a u"
huffman@25787
    61
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
huffman@25787
    62
    unfolding less_up_def
huffman@25787
    63
    by (auto split: u.split_asm intro: antisym_less)
huffman@25787
    64
next
huffman@25787
    65
  fix x y z :: "'a u"
huffman@25787
    66
  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
huffman@25787
    67
    unfolding less_up_def
huffman@25787
    68
    by (auto split: u.split_asm intro: trans_less)
huffman@25787
    69
qed
huffman@15576
    70
huffman@25827
    71
lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
huffman@25827
    72
by (auto, case_tac x, auto)
huffman@25827
    73
huffman@25827
    74
instance u :: (finite_po) finite_po
huffman@25827
    75
by (intro_classes, simp add: u_UNIV)
huffman@25827
    76
huffman@25827
    77
huffman@18290
    78
subsection {* Lifted cpo is a cpo *}
huffman@15593
    79
huffman@16319
    80
lemma is_lub_Iup:
huffman@16319
    81
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
huffman@15576
    82
apply (rule is_lubI)
huffman@15576
    83
apply (rule ub_rangeI)
huffman@16319
    84
apply (subst Iup_less)
huffman@16319
    85
apply (erule is_ub_lub)
huffman@16753
    86
apply (case_tac u)
huffman@16319
    87
apply (drule ub_rangeD)
huffman@16319
    88
apply simp
huffman@16319
    89
apply simp
huffman@16319
    90
apply (erule is_lub_lub)
huffman@15576
    91
apply (rule ub_rangeI)
huffman@16319
    92
apply (drule_tac i=i in ub_rangeD)
huffman@15593
    93
apply simp
huffman@15599
    94
done
huffman@15599
    95
huffman@25789
    96
lemma is_lub_Iup': "\<lbrakk>directed S; S <<| x\<rbrakk> \<Longrightarrow> (Iup ` S) <<| Iup x"
huffman@25789
    97
apply (rule is_lubI)
huffman@25789
    98
apply (rule ub_imageI)
huffman@25789
    99
apply (subst Iup_less)
huffman@25789
   100
apply (erule (1) is_ubD [OF is_lubD1])
huffman@25789
   101
apply (case_tac u)
huffman@25789
   102
apply (drule directedD1, erule exE)
huffman@25789
   103
apply (drule (1) ub_imageD)
huffman@25789
   104
apply simp
huffman@25789
   105
apply simp
huffman@25789
   106
apply (erule is_lub_lub)
huffman@25789
   107
apply (rule is_ubI)
huffman@25789
   108
apply (drule (1) ub_imageD)
huffman@25789
   109
apply simp
huffman@25789
   110
done
huffman@25789
   111
huffman@15599
   112
text {* Now some lemmas about chains of @{typ "'a u"} elements *}
huffman@15599
   113
huffman@16753
   114
lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
huffman@16753
   115
by (case_tac z, simp_all)
huffman@16319
   116
huffman@16319
   117
lemma up_lemma2:
huffman@16753
   118
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
huffman@16319
   119
apply (erule contrapos_nn)
huffman@15599
   120
apply (drule_tac x="j" and y="i + j" in chain_mono3)
huffman@15599
   121
apply (rule le_add2)
huffman@16753
   122
apply (case_tac "Y j")
huffman@16319
   123
apply assumption
huffman@16319
   124
apply simp
huffman@15599
   125
done
huffman@15599
   126
huffman@16319
   127
lemma up_lemma3:
huffman@16753
   128
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
huffman@16319
   129
by (rule up_lemma1 [OF up_lemma2])
huffman@15599
   130
huffman@16319
   131
lemma up_lemma4:
huffman@16753
   132
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
huffman@15599
   133
apply (rule chainI)
huffman@16319
   134
apply (rule Iup_less [THEN iffD1])
huffman@16319
   135
apply (subst up_lemma3, assumption+)+
huffman@15599
   136
apply (simp add: chainE)
huffman@15599
   137
done
huffman@15599
   138
huffman@16319
   139
lemma up_lemma5:
huffman@16753
   140
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
huffman@16319
   141
    (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
huffman@16319
   142
by (rule ext, rule up_lemma3 [symmetric])
huffman@15599
   143
huffman@16319
   144
lemma up_lemma6:
wenzelm@25131
   145
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
huffman@16319
   146
      \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
wenzelm@16933
   147
apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
huffman@16319
   148
apply assumption
huffman@16319
   149
apply (subst up_lemma5, assumption+)
huffman@16319
   150
apply (rule is_lub_Iup)
huffman@16319
   151
apply (rule thelubE [OF _ refl])
huffman@16753
   152
apply (erule (1) up_lemma4)
huffman@15599
   153
done
huffman@15599
   154
huffman@17838
   155
lemma up_chain_lemma:
huffman@16319
   156
  "chain Y \<Longrightarrow>
huffman@16319
   157
   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
huffman@16753
   158
   (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
huffman@16319
   159
apply (rule disjCI)
huffman@16319
   160
apply (simp add: expand_fun_eq)
huffman@16319
   161
apply (erule exE, rename_tac j)
huffman@16319
   162
apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
huffman@16319
   163
apply (simp add: up_lemma4)
huffman@16319
   164
apply (simp add: up_lemma6 [THEN thelubI])
huffman@16319
   165
apply (rule_tac x=j in exI)
huffman@16319
   166
apply (simp add: up_lemma3)
huffman@15599
   167
done
huffman@15599
   168
huffman@16319
   169
lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
huffman@17838
   170
apply (frule up_chain_lemma, safe)
huffman@16319
   171
apply (rule_tac x="Iup (lub (range A))" in exI)
huffman@17838
   172
apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
huffman@16319
   173
apply (simp add: is_lub_Iup thelubE)
huffman@17585
   174
apply (rule exI, rule lub_const)
huffman@15576
   175
done
huffman@15576
   176
huffman@15599
   177
instance u :: (cpo) cpo
huffman@15593
   178
by intro_classes (rule cpo_up)
huffman@15593
   179
huffman@25789
   180
lemma up_directed_lemma:
huffman@25789
   181
  "directed (S::'a::dcpo u set) \<Longrightarrow>
huffman@25789
   182
    (directed (Iup -` S) \<and> S <<| Iup (lub (Iup -` S))) \<or>
huffman@25789
   183
    S = {Ibottom}"
huffman@25789
   184
apply (case_tac "\<exists>x. Iup x \<in> S")
huffman@25789
   185
apply (rule disjI1)
huffman@25789
   186
apply (subgoal_tac "directed (Iup -` S)")
huffman@25789
   187
apply (rule conjI, assumption)
huffman@25789
   188
apply (rule is_lubI)
huffman@25789
   189
apply (rule is_ubI)
huffman@25789
   190
apply (case_tac x, simp, simp)
huffman@25789
   191
apply (erule is_ub_thelub', simp)
huffman@25789
   192
apply (case_tac u)
huffman@25789
   193
apply (erule exE)
huffman@25789
   194
apply (drule (1) is_ubD)
huffman@25789
   195
apply simp
huffman@25789
   196
apply simp
huffman@25789
   197
apply (erule is_lub_thelub')
huffman@25789
   198
apply (rule is_ubI, simp)
huffman@25789
   199
apply (drule (1) is_ubD, simp)
huffman@25789
   200
apply (rule directedI)
huffman@25789
   201
apply (erule exE)
huffman@25789
   202
apply (rule exI)
huffman@25789
   203
apply (erule vimageI2)
huffman@25789
   204
apply simp
huffman@25789
   205
apply (drule_tac x="Iup x" and y="Iup y" in directedD2, assumption+)
huffman@25789
   206
apply (erule bexE, rename_tac z)
huffman@25789
   207
apply (case_tac z)
huffman@25789
   208
apply simp
huffman@25789
   209
apply (rule_tac x=a in bexI)
huffman@25789
   210
apply simp
huffman@25789
   211
apply simp
huffman@25789
   212
apply (rule disjI2)
huffman@25789
   213
apply (simp, safe)
huffman@25789
   214
apply (case_tac x, simp, simp)
huffman@25789
   215
apply (drule directedD1)
huffman@25789
   216
apply (clarify, rename_tac x)
huffman@25789
   217
apply (case_tac x, simp, simp)
huffman@25789
   218
done
huffman@25789
   219
huffman@25789
   220
lemma dcpo_up: "directed (S::'a::dcpo u set) \<Longrightarrow> \<exists>x. S <<| x"
huffman@25789
   221
apply (frule up_directed_lemma, safe)
huffman@25789
   222
apply (erule exI)
huffman@25789
   223
apply (rule exI, rule is_lub_singleton)
huffman@25789
   224
done
huffman@25789
   225
huffman@25789
   226
instance u :: (dcpo) dcpo
huffman@25789
   227
by intro_classes (rule dcpo_up)
huffman@25789
   228
huffman@18290
   229
subsection {* Lifted cpo is pointed *}
huffman@15576
   230
huffman@17585
   231
lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
huffman@16753
   232
apply (rule_tac x = "Ibottom" in exI)
huffman@15593
   233
apply (rule minimal_up [THEN allI])
huffman@15576
   234
done
huffman@15576
   235
huffman@15599
   236
instance u :: (cpo) pcpo
huffman@15593
   237
by intro_classes (rule least_up)
huffman@15593
   238
huffman@15593
   239
text {* for compatibility with old HOLCF-Version *}
huffman@16753
   240
lemma inst_up_pcpo: "\<bottom> = Ibottom"
huffman@16319
   241
by (rule minimal_up [THEN UU_I, symmetric])
huffman@15593
   242
huffman@15593
   243
subsection {* Continuity of @{term Iup} and @{term Ifup} *}
huffman@15593
   244
huffman@15593
   245
text {* continuity for @{term Iup} *}
huffman@15576
   246
huffman@16319
   247
lemma cont_Iup: "cont Iup"
huffman@16215
   248
apply (rule contI)
huffman@15599
   249
apply (rule is_lub_Iup)
huffman@15599
   250
apply (erule thelubE [OF _ refl])
huffman@15576
   251
done
huffman@15576
   252
huffman@15593
   253
text {* continuity for @{term Ifup} *}
huffman@15576
   254
huffman@16319
   255
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
huffman@16753
   256
by (induct x, simp_all)
huffman@15576
   257
huffman@16319
   258
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
huffman@16319
   259
apply (rule monofunI)
huffman@16753
   260
apply (case_tac x, simp)
huffman@16753
   261
apply (case_tac y, simp)
huffman@16319
   262
apply (simp add: monofun_cfun_arg)
huffman@15576
   263
done
huffman@15576
   264
huffman@16319
   265
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
huffman@16319
   266
apply (rule contI)
huffman@17838
   267
apply (frule up_chain_lemma, safe)
huffman@17838
   268
apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
huffman@16319
   269
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
huffman@16319
   270
apply (simp add: cont_cfun_arg)
huffman@18078
   271
apply (simp add: lub_const)
huffman@15576
   272
done
huffman@15576
   273
huffman@15593
   274
subsection {* Continuous versions of constants *}
huffman@15576
   275
wenzelm@25131
   276
definition
wenzelm@25131
   277
  up  :: "'a \<rightarrow> 'a u" where
wenzelm@25131
   278
  "up = (\<Lambda> x. Iup x)"
huffman@16319
   279
wenzelm@25131
   280
definition
wenzelm@25131
   281
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
wenzelm@25131
   282
  "fup = (\<Lambda> f p. Ifup f p)"
huffman@15593
   283
huffman@15593
   284
translations
wenzelm@25131
   285
  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
wenzelm@25131
   286
  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
huffman@15593
   287
huffman@15593
   288
text {* continuous versions of lemmas for @{typ "('a)u"} *}
huffman@15576
   289
huffman@16753
   290
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
huffman@16753
   291
apply (induct z)
huffman@16319
   292
apply (simp add: inst_up_pcpo)
huffman@16319
   293
apply (simp add: up_def cont_Iup)
huffman@15576
   294
done
huffman@15576
   295
huffman@16753
   296
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
huffman@16319
   297
by (simp add: up_def cont_Iup)
huffman@15576
   298
huffman@16753
   299
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
huffman@16753
   300
by simp
huffman@16319
   301
huffman@17838
   302
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
huffman@16319
   303
by (simp add: up_def cont_Iup inst_up_pcpo)
huffman@15576
   304
huffman@25785
   305
lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
huffman@25785
   306
by simp
huffman@15576
   307
huffman@16326
   308
lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
huffman@16319
   309
by (simp add: up_def cont_Iup)
huffman@16319
   310
huffman@25788
   311
lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@25788
   312
apply (cases p)
huffman@16319
   313
apply (simp add: inst_up_pcpo)
huffman@16319
   314
apply (simp add: up_def cont_Iup)
huffman@15576
   315
done
huffman@15576
   316
huffman@25788
   317
lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
huffman@25788
   318
by (cases x, simp_all)
huffman@25788
   319
huffman@25827
   320
text {* lifting preserves chain-finiteness *}
huffman@25827
   321
huffman@17838
   322
lemma up_chain_cases:
huffman@17838
   323
  "chain Y \<Longrightarrow>
huffman@17838
   324
  (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
huffman@17838
   325
  (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
huffman@17838
   326
by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
huffman@17838
   327
huffman@25827
   328
instance u :: (chfin) chfin
huffman@25827
   329
apply (intro_classes, clarify)
huffman@25827
   330
apply (drule up_chain_cases, safe)
huffman@25827
   331
apply (drule chfin [rule_format])
huffman@25827
   332
apply (erule exE, rename_tac n)
huffman@25827
   333
apply (rule_tac x="n + j" in exI)
huffman@25827
   334
apply (simp only: max_in_chain_def)
huffman@25827
   335
apply (clarify, rename_tac k)
huffman@25827
   336
apply (subgoal_tac "\<exists>m. k = m + j", clarsimp)
huffman@25827
   337
apply (rule_tac x="k - j" in exI, simp)
huffman@25827
   338
apply (simp add: max_in_chain_def)
huffman@25827
   339
done
huffman@25827
   340
huffman@17838
   341
lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
huffman@17838
   342
apply (unfold compact_def)
huffman@17838
   343
apply (rule admI)
huffman@17838
   344
apply (drule up_chain_cases)
huffman@17838
   345
apply (elim disjE exE conjE)
huffman@17838
   346
apply simp
huffman@17838
   347
apply (erule (1) admD)
huffman@17838
   348
apply (rule allI, drule_tac x="i + j" in spec)
huffman@17838
   349
apply simp
huffman@18078
   350
apply simp
huffman@17838
   351
done
huffman@17838
   352
huffman@17838
   353
text {* properties of fup *}
huffman@17838
   354
huffman@16319
   355
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@16319
   356
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
huffman@15576
   357
huffman@16319
   358
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
huffman@16753
   359
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
huffman@15576
   360
huffman@16553
   361
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
huffman@25788
   362
by (cases x, simp_all)
huffman@15576
   363
huffman@15576
   364
end