src/HOLCF/Up.thy
author huffman
Thu Jun 23 22:07:30 2005 +0200 (2005-06-23)
changeset 16553 aa36d41e4263
parent 16326 50a613925c4e
child 16753 fb6801c926d2
permissions -rw-r--r--
add csplit3, ssplit3, fup3 as simp rules
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@15577
    11
imports Cfun Sum_Type Datatype
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@16319
    18
typedef (Up) 'a u = "UNIV :: 'a option set" ..
huffman@15576
    19
huffman@15576
    20
consts
huffman@16319
    21
  Iup         :: "'a \<Rightarrow> 'a u"
huffman@16319
    22
  Ifup        :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
huffman@15576
    23
huffman@15576
    24
defs
huffman@16319
    25
  Iup_def:     "Iup x \<equiv> Abs_Up (Some x)"
huffman@16319
    26
  Ifup_def:    "Ifup f x \<equiv> case Rep_Up x of None \<Rightarrow> \<bottom> | Some z \<Rightarrow> f\<cdot>z"
huffman@15576
    27
huffman@15576
    28
lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
huffman@15593
    29
by (simp add: Up_def Abs_Up_inverse)
huffman@15576
    30
huffman@16319
    31
lemma Exh_Up: "z = Abs_Up None \<or> (\<exists>x. z = Iup x)"
huffman@15576
    32
apply (unfold Iup_def)
huffman@15576
    33
apply (rule Rep_Up_inverse [THEN subst])
huffman@16319
    34
apply (case_tac "Rep_Up z")
huffman@16319
    35
apply auto
huffman@15576
    36
done
huffman@15576
    37
huffman@16319
    38
lemma inj_Abs_Up: "inj Abs_Up" (* worthless *)
huffman@15576
    39
apply (rule inj_on_inverseI)
huffman@15576
    40
apply (rule Abs_Up_inverse2)
huffman@15576
    41
done
huffman@15576
    42
huffman@16319
    43
lemma inj_Rep_Up: "inj Rep_Up" (* worthless *)
huffman@15576
    44
apply (rule inj_on_inverseI)
huffman@15576
    45
apply (rule Rep_Up_inverse)
huffman@15576
    46
done
huffman@15576
    47
huffman@16319
    48
lemma Iup_eq [simp]: "(Iup x = Iup y) = (x = y)"
huffman@16319
    49
by (simp add: Iup_def Abs_Up_inject Up_def)
huffman@15576
    50
huffman@16319
    51
lemma Iup_defined [simp]: "Iup x \<noteq> Abs_Up None"
huffman@16319
    52
by (simp add: Iup_def Abs_Up_inject Up_def)
huffman@15576
    53
huffman@16319
    54
lemma upE: "\<lbrakk>p = Abs_Up None \<Longrightarrow> Q; \<And>x. p = Iup x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@16319
    55
by (rule Exh_Up [THEN disjE], auto)
huffman@15576
    56
huffman@16319
    57
lemma Ifup1 [simp]: "Ifup f (Abs_Up None) = \<bottom>"
huffman@16319
    58
by (simp add: Ifup_def Abs_Up_inverse2)
huffman@15576
    59
huffman@16319
    60
lemma Ifup2 [simp]: "Ifup f (Iup x) = f\<cdot>x"
huffman@16319
    61
by (simp add: Ifup_def Iup_def Abs_Up_inverse2)
huffman@15576
    62
huffman@15593
    63
subsection {* Ordering on type @{typ "'a u"} *}
huffman@15593
    64
huffman@15593
    65
instance u :: (sq_ord) sq_ord ..
huffman@15576
    66
huffman@15593
    67
defs (overloaded)
huffman@16319
    68
  less_up_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>x1 x2. case Rep_Up x1 of
huffman@16319
    69
               None \<Rightarrow> True
huffman@16319
    70
             | Some y1 \<Rightarrow> (case Rep_Up x2 of None \<Rightarrow> False
huffman@16319
    71
                                           | Some y2 \<Rightarrow> y1 \<sqsubseteq> y2))"
huffman@15576
    72
huffman@16319
    73
lemma minimal_up [iff]: "Abs_Up None \<sqsubseteq> z"
huffman@15593
    74
by (simp add: less_up_def Abs_Up_inverse2)
huffman@15576
    75
huffman@16319
    76
lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Abs_Up None"
huffman@15593
    77
by (simp add: Iup_def less_up_def Abs_Up_inverse2)
huffman@15576
    78
huffman@16319
    79
lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
huffman@15593
    80
by (simp add: Iup_def less_up_def Abs_Up_inverse2)
huffman@15576
    81
huffman@15593
    82
subsection {* Type @{typ "'a u"} is a partial order *}
huffman@15576
    83
huffman@16319
    84
lemma refl_less_up: "(p::'a u) \<sqsubseteq> p"
huffman@16319
    85
by (rule_tac p = "p" in upE, auto)
huffman@15576
    86
huffman@16319
    87
lemma antisym_less_up: "\<lbrakk>(p1::'a u) \<sqsubseteq> p2; p2 \<sqsubseteq> p1\<rbrakk> \<Longrightarrow> p1 = p2"
huffman@15576
    88
apply (rule_tac p = "p1" in upE)
huffman@16319
    89
apply (rule_tac p = "p2" in upE)
huffman@15576
    90
apply simp
huffman@15576
    91
apply simp
huffman@15576
    92
apply (rule_tac p = "p2" in upE)
huffman@15576
    93
apply simp
huffman@15576
    94
apply simp
huffman@15576
    95
apply (drule antisym_less, assumption)
huffman@15576
    96
apply simp
huffman@15576
    97
done
huffman@15576
    98
huffman@16319
    99
lemma trans_less_up: "\<lbrakk>(p1::'a u) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3"
huffman@15576
   100
apply (rule_tac p = "p1" in upE)
huffman@15576
   101
apply simp
huffman@15576
   102
apply (rule_tac p = "p2" in upE)
huffman@15576
   103
apply simp
huffman@15576
   104
apply (rule_tac p = "p3" in upE)
huffman@16319
   105
apply simp
huffman@16319
   106
apply (auto elim: trans_less)
huffman@15576
   107
done
huffman@15576
   108
huffman@15599
   109
instance u :: (cpo) po
huffman@15593
   110
by intro_classes
huffman@15593
   111
  (assumption | rule refl_less_up antisym_less_up trans_less_up)+
huffman@15576
   112
huffman@15593
   113
subsection {* Type @{typ "'a u"} is a cpo *}
huffman@15593
   114
huffman@16319
   115
lemma is_lub_Iup:
huffman@16319
   116
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
huffman@15576
   117
apply (rule is_lubI)
huffman@15576
   118
apply (rule ub_rangeI)
huffman@16319
   119
apply (subst Iup_less)
huffman@16319
   120
apply (erule is_ub_lub)
huffman@16319
   121
apply (rule_tac p="u" in upE)
huffman@16319
   122
apply (drule ub_rangeD)
huffman@16319
   123
apply simp
huffman@16319
   124
apply simp
huffman@16319
   125
apply (erule is_lub_lub)
huffman@15576
   126
apply (rule ub_rangeI)
huffman@16319
   127
apply (drule_tac i=i in ub_rangeD)
huffman@15593
   128
apply simp
huffman@15599
   129
done
huffman@15599
   130
huffman@15599
   131
text {* Now some lemmas about chains of @{typ "'a u"} elements *}
huffman@15599
   132
huffman@16319
   133
lemma up_lemma1: "z \<noteq> Abs_Up None \<Longrightarrow> Iup (THE a. Iup a = z) = z"
huffman@16319
   134
by (rule_tac p="z" in upE, simp_all)
huffman@16319
   135
huffman@16319
   136
lemma up_lemma2:
huffman@16319
   137
  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Abs_Up None"
huffman@16319
   138
apply (erule contrapos_nn)
huffman@15599
   139
apply (drule_tac x="j" and y="i + j" in chain_mono3)
huffman@15599
   140
apply (rule le_add2)
huffman@16319
   141
apply (rule_tac p="Y j" in upE)
huffman@16319
   142
apply assumption
huffman@16319
   143
apply simp
huffman@15599
   144
done
huffman@15599
   145
huffman@16319
   146
lemma up_lemma3:
huffman@16319
   147
  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
huffman@16319
   148
by (rule up_lemma1 [OF up_lemma2])
huffman@15599
   149
huffman@16319
   150
lemma up_lemma4:
huffman@16319
   151
  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
huffman@15599
   152
apply (rule chainI)
huffman@16319
   153
apply (rule Iup_less [THEN iffD1])
huffman@16319
   154
apply (subst up_lemma3, assumption+)+
huffman@15599
   155
apply (simp add: chainE)
huffman@15599
   156
done
huffman@15599
   157
huffman@16319
   158
lemma up_lemma5:
huffman@16319
   159
  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk> \<Longrightarrow>
huffman@16319
   160
    (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
huffman@16319
   161
by (rule ext, rule up_lemma3 [symmetric])
huffman@15599
   162
huffman@16319
   163
lemma up_lemma6:
huffman@16319
   164
  "\<lbrakk>chain Y; Y j \<noteq> Abs_Up None\<rbrakk>  
huffman@16319
   165
      \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
huffman@16319
   166
apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
huffman@16319
   167
apply assumption
huffman@16319
   168
apply (subst up_lemma5, assumption+)
huffman@16319
   169
apply (rule is_lub_Iup)
huffman@16319
   170
apply (rule thelubE [OF _ refl])
huffman@16319
   171
apply (rule up_lemma4, assumption+)
huffman@15599
   172
done
huffman@15599
   173
huffman@16319
   174
lemma up_chain_cases:
huffman@16319
   175
  "chain Y \<Longrightarrow>
huffman@16319
   176
   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
huffman@16319
   177
   (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Abs_Up None))"
huffman@16319
   178
apply (rule disjCI)
huffman@16319
   179
apply (simp add: expand_fun_eq)
huffman@16319
   180
apply (erule exE, rename_tac j)
huffman@16319
   181
apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
huffman@16319
   182
apply (rule conjI)
huffman@16319
   183
apply (simp add: up_lemma4)
huffman@16319
   184
apply (rule conjI)
huffman@16319
   185
apply (simp add: up_lemma6 [THEN thelubI])
huffman@16319
   186
apply (rule_tac x=j in exI)
huffman@16319
   187
apply (simp add: up_lemma3)
huffman@15599
   188
done
huffman@15599
   189
huffman@16319
   190
lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
huffman@16319
   191
apply (frule up_chain_cases, safe)
huffman@16319
   192
apply (rule_tac x="Iup (lub (range A))" in exI)
huffman@16319
   193
apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
huffman@16319
   194
apply (simp add: is_lub_Iup thelubE)
huffman@16319
   195
apply (rule_tac x="Abs_Up None" in exI)
huffman@16319
   196
apply (rule lub_const)
huffman@15576
   197
done
huffman@15576
   198
huffman@15599
   199
instance u :: (cpo) cpo
huffman@15593
   200
by intro_classes (rule cpo_up)
huffman@15593
   201
huffman@15593
   202
subsection {* Type @{typ "'a u"} is pointed *}
huffman@15576
   203
huffman@16319
   204
lemma least_up: "EX x::'a u. ALL y. x\<sqsubseteq>y"
huffman@16319
   205
apply (rule_tac x = "Abs_Up None" in exI)
huffman@15593
   206
apply (rule minimal_up [THEN allI])
huffman@15576
   207
done
huffman@15576
   208
huffman@15599
   209
instance u :: (cpo) pcpo
huffman@15593
   210
by intro_classes (rule least_up)
huffman@15593
   211
huffman@15593
   212
text {* for compatibility with old HOLCF-Version *}
huffman@16319
   213
lemma inst_up_pcpo: "\<bottom> = Abs_Up None"
huffman@16319
   214
by (rule minimal_up [THEN UU_I, symmetric])
huffman@15593
   215
huffman@15593
   216
text {* some lemmas restated for class pcpo *}
huffman@15576
   217
huffman@16319
   218
lemma less_up3b: "~ Iup(x) \<sqsubseteq> \<bottom>"
huffman@15576
   219
apply (subst inst_up_pcpo)
huffman@16319
   220
apply simp
huffman@15576
   221
done
huffman@15576
   222
huffman@16319
   223
lemma defined_Iup2 [iff]: "Iup(x) ~= \<bottom>"
huffman@15576
   224
apply (subst inst_up_pcpo)
huffman@16319
   225
apply (rule Iup_defined)
huffman@15576
   226
done
huffman@15576
   227
huffman@15593
   228
subsection {* Continuity of @{term Iup} and @{term Ifup} *}
huffman@15593
   229
huffman@15593
   230
text {* continuity for @{term Iup} *}
huffman@15576
   231
huffman@16319
   232
lemma cont_Iup: "cont Iup"
huffman@16215
   233
apply (rule contI)
huffman@15599
   234
apply (rule is_lub_Iup)
huffman@15599
   235
apply (erule thelubE [OF _ refl])
huffman@15576
   236
done
huffman@15576
   237
huffman@15593
   238
text {* continuity for @{term Ifup} *}
huffman@15576
   239
huffman@16319
   240
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
huffman@16319
   241
apply (rule contI)
huffman@16319
   242
apply (rule_tac p="x" in upE)
huffman@16319
   243
apply (simp add: lub_const)
huffman@16319
   244
apply (simp add: cont_cfun_fun)
huffman@15576
   245
done
huffman@15576
   246
huffman@16319
   247
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
huffman@16319
   248
apply (rule monofunI)
huffman@16319
   249
apply (rule_tac p="x" in upE)
huffman@15576
   250
apply simp
huffman@16319
   251
apply (rule_tac p="y" in upE)
huffman@15599
   252
apply simp
huffman@16319
   253
apply (simp add: monofun_cfun_arg)
huffman@15576
   254
done
huffman@15576
   255
huffman@16319
   256
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
huffman@16319
   257
apply (rule contI)
huffman@16319
   258
apply (frule up_chain_cases, safe)
huffman@16319
   259
apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
huffman@16319
   260
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
huffman@16319
   261
apply (simp add: cont_cfun_arg)
huffman@16319
   262
apply (simp add: thelub_const lub_const)
huffman@15576
   263
done
huffman@15576
   264
huffman@15593
   265
subsection {* Continuous versions of constants *}
huffman@15576
   266
huffman@15593
   267
constdefs  
huffman@16319
   268
  up  :: "'a \<rightarrow> 'a u"
huffman@16319
   269
  "up \<equiv> \<Lambda> x. Iup x"
huffman@16319
   270
huffman@16319
   271
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
huffman@16319
   272
  "fup \<equiv> \<Lambda> f p. Ifup f p"
huffman@15593
   273
huffman@15593
   274
translations
huffman@16319
   275
"case l of up\<cdot>x => t1" == "fup\<cdot>(LAM x. t1)\<cdot>l"
huffman@15593
   276
huffman@15593
   277
text {* continuous versions of lemmas for @{typ "('a)u"} *}
huffman@15576
   278
huffman@16319
   279
lemma Exh_Up1: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
huffman@16319
   280
apply (rule_tac p="z" in upE)
huffman@16319
   281
apply (simp add: inst_up_pcpo)
huffman@16319
   282
apply (simp add: up_def cont_Iup)
huffman@15576
   283
done
huffman@15576
   284
huffman@16319
   285
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
huffman@16319
   286
by (simp add: up_def cont_Iup)
huffman@15576
   287
huffman@16326
   288
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
huffman@16319
   289
by (rule iffI, erule up_inject, simp)
huffman@16319
   290
huffman@16319
   291
lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
huffman@16319
   292
by (simp add: up_def cont_Iup inst_up_pcpo)
huffman@15576
   293
huffman@16319
   294
lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
huffman@16319
   295
by (simp add: eq_UU_iff [symmetric])
huffman@15576
   296
huffman@16326
   297
lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
huffman@16319
   298
by (simp add: up_def cont_Iup)
huffman@16319
   299
huffman@16319
   300
lemma upE1: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@16319
   301
apply (rule_tac p="p" in upE)
huffman@16319
   302
apply (simp add: inst_up_pcpo)
huffman@16319
   303
apply (simp add: up_def cont_Iup)
huffman@15576
   304
done
huffman@15576
   305
huffman@16319
   306
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@16319
   307
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
huffman@15576
   308
huffman@16319
   309
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
huffman@16319
   310
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 )
huffman@15576
   311
huffman@16553
   312
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
huffman@16319
   313
by (rule_tac p=x in upE1, simp_all)
huffman@15576
   314
huffman@15576
   315
end