src/HOLCF/Up.thy
author huffman
Fri Jul 08 02:41:19 2005 +0200 (2005-07-08)
changeset 16753 fb6801c926d2
parent 16553 aa36d41e4263
child 16933 91ded127f5f7
permissions -rw-r--r--
define 'a u with datatype package;
removed obsolete lemmas;
renamed upE1 to upE and Exh_Up1 to Exh_Up;
cleaned up
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@16753
    18
datatype 'a u = Ibottom | Iup 'a
huffman@15576
    19
huffman@15576
    20
consts
huffman@16753
    21
  Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
huffman@15576
    22
huffman@16753
    23
primrec
huffman@16753
    24
  "Ifup f Ibottom = \<bottom>"
huffman@16753
    25
  "Ifup f (Iup x) = f\<cdot>x"
huffman@15576
    26
huffman@15593
    27
subsection {* Ordering on type @{typ "'a u"} *}
huffman@15593
    28
huffman@15593
    29
instance u :: (sq_ord) sq_ord ..
huffman@15576
    30
huffman@15593
    31
defs (overloaded)
huffman@16753
    32
  less_up_def:
huffman@16753
    33
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
huffman@16753
    34
      (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
huffman@15576
    35
huffman@16753
    36
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
huffman@16753
    37
by (simp add: less_up_def)
huffman@15576
    38
huffman@16753
    39
lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
huffman@16753
    40
by (simp add: less_up_def)
huffman@15576
    41
huffman@16319
    42
lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
huffman@16753
    43
by (simp add: less_up_def)
huffman@15576
    44
huffman@15593
    45
subsection {* Type @{typ "'a u"} is a partial order *}
huffman@15576
    46
huffman@16753
    47
lemma refl_less_up: "(x::'a u) \<sqsubseteq> x"
huffman@16753
    48
by (simp add: less_up_def split: u.split)
huffman@15576
    49
huffman@16753
    50
lemma antisym_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
huffman@16753
    51
apply (simp add: less_up_def split: u.split_asm)
huffman@16753
    52
apply (erule (1) antisym_less)
huffman@15576
    53
done
huffman@15576
    54
huffman@16753
    55
lemma trans_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
huffman@16753
    56
apply (simp add: less_up_def split: u.split_asm)
huffman@16753
    57
apply (erule (1) trans_less)
huffman@15576
    58
done
huffman@15576
    59
huffman@15599
    60
instance u :: (cpo) po
huffman@15593
    61
by intro_classes
huffman@15593
    62
  (assumption | rule refl_less_up antisym_less_up trans_less_up)+
huffman@15576
    63
huffman@15593
    64
subsection {* Type @{typ "'a u"} is a cpo *}
huffman@15593
    65
huffman@16319
    66
lemma is_lub_Iup:
huffman@16319
    67
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
huffman@15576
    68
apply (rule is_lubI)
huffman@15576
    69
apply (rule ub_rangeI)
huffman@16319
    70
apply (subst Iup_less)
huffman@16319
    71
apply (erule is_ub_lub)
huffman@16753
    72
apply (case_tac u)
huffman@16319
    73
apply (drule ub_rangeD)
huffman@16319
    74
apply simp
huffman@16319
    75
apply simp
huffman@16319
    76
apply (erule is_lub_lub)
huffman@15576
    77
apply (rule ub_rangeI)
huffman@16319
    78
apply (drule_tac i=i in ub_rangeD)
huffman@15593
    79
apply simp
huffman@15599
    80
done
huffman@15599
    81
huffman@15599
    82
text {* Now some lemmas about chains of @{typ "'a u"} elements *}
huffman@15599
    83
huffman@16753
    84
lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
huffman@16753
    85
by (case_tac z, simp_all)
huffman@16319
    86
huffman@16319
    87
lemma up_lemma2:
huffman@16753
    88
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
huffman@16319
    89
apply (erule contrapos_nn)
huffman@15599
    90
apply (drule_tac x="j" and y="i + j" in chain_mono3)
huffman@15599
    91
apply (rule le_add2)
huffman@16753
    92
apply (case_tac "Y j")
huffman@16319
    93
apply assumption
huffman@16319
    94
apply simp
huffman@15599
    95
done
huffman@15599
    96
huffman@16319
    97
lemma up_lemma3:
huffman@16753
    98
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
huffman@16319
    99
by (rule up_lemma1 [OF up_lemma2])
huffman@15599
   100
huffman@16319
   101
lemma up_lemma4:
huffman@16753
   102
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
huffman@15599
   103
apply (rule chainI)
huffman@16319
   104
apply (rule Iup_less [THEN iffD1])
huffman@16319
   105
apply (subst up_lemma3, assumption+)+
huffman@15599
   106
apply (simp add: chainE)
huffman@15599
   107
done
huffman@15599
   108
huffman@16319
   109
lemma up_lemma5:
huffman@16753
   110
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
huffman@16319
   111
    (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
huffman@16319
   112
by (rule ext, rule up_lemma3 [symmetric])
huffman@15599
   113
huffman@16319
   114
lemma up_lemma6:
huffman@16753
   115
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
huffman@16319
   116
      \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
huffman@16319
   117
apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
huffman@16319
   118
apply assumption
huffman@16319
   119
apply (subst up_lemma5, assumption+)
huffman@16319
   120
apply (rule is_lub_Iup)
huffman@16319
   121
apply (rule thelubE [OF _ refl])
huffman@16753
   122
apply (erule (1) up_lemma4)
huffman@15599
   123
done
huffman@15599
   124
huffman@16319
   125
lemma up_chain_cases:
huffman@16319
   126
  "chain Y \<Longrightarrow>
huffman@16319
   127
   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
huffman@16753
   128
   (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
huffman@16319
   129
apply (rule disjCI)
huffman@16319
   130
apply (simp add: expand_fun_eq)
huffman@16319
   131
apply (erule exE, rename_tac j)
huffman@16319
   132
apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
huffman@16319
   133
apply (rule conjI)
huffman@16319
   134
apply (simp add: up_lemma4)
huffman@16319
   135
apply (rule conjI)
huffman@16319
   136
apply (simp add: up_lemma6 [THEN thelubI])
huffman@16319
   137
apply (rule_tac x=j in exI)
huffman@16319
   138
apply (simp add: up_lemma3)
huffman@15599
   139
done
huffman@15599
   140
huffman@16319
   141
lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
huffman@16319
   142
apply (frule up_chain_cases, safe)
huffman@16319
   143
apply (rule_tac x="Iup (lub (range A))" in exI)
huffman@16319
   144
apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
huffman@16319
   145
apply (simp add: is_lub_Iup thelubE)
huffman@16753
   146
apply (rule_tac x="Ibottom" in exI)
huffman@16319
   147
apply (rule lub_const)
huffman@15576
   148
done
huffman@15576
   149
huffman@15599
   150
instance u :: (cpo) cpo
huffman@15593
   151
by intro_classes (rule cpo_up)
huffman@15593
   152
huffman@15593
   153
subsection {* Type @{typ "'a u"} is pointed *}
huffman@15576
   154
huffman@16319
   155
lemma least_up: "EX x::'a u. ALL y. x\<sqsubseteq>y"
huffman@16753
   156
apply (rule_tac x = "Ibottom" in exI)
huffman@15593
   157
apply (rule minimal_up [THEN allI])
huffman@15576
   158
done
huffman@15576
   159
huffman@15599
   160
instance u :: (cpo) pcpo
huffman@15593
   161
by intro_classes (rule least_up)
huffman@15593
   162
huffman@15593
   163
text {* for compatibility with old HOLCF-Version *}
huffman@16753
   164
lemma inst_up_pcpo: "\<bottom> = Ibottom"
huffman@16319
   165
by (rule minimal_up [THEN UU_I, symmetric])
huffman@15593
   166
huffman@15593
   167
subsection {* Continuity of @{term Iup} and @{term Ifup} *}
huffman@15593
   168
huffman@15593
   169
text {* continuity for @{term Iup} *}
huffman@15576
   170
huffman@16319
   171
lemma cont_Iup: "cont Iup"
huffman@16215
   172
apply (rule contI)
huffman@15599
   173
apply (rule is_lub_Iup)
huffman@15599
   174
apply (erule thelubE [OF _ refl])
huffman@15576
   175
done
huffman@15576
   176
huffman@15593
   177
text {* continuity for @{term Ifup} *}
huffman@15576
   178
huffman@16319
   179
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
huffman@16753
   180
by (induct x, simp_all)
huffman@15576
   181
huffman@16319
   182
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
huffman@16319
   183
apply (rule monofunI)
huffman@16753
   184
apply (case_tac x, simp)
huffman@16753
   185
apply (case_tac y, simp)
huffman@16319
   186
apply (simp add: monofun_cfun_arg)
huffman@15576
   187
done
huffman@15576
   188
huffman@16319
   189
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
huffman@16319
   190
apply (rule contI)
huffman@16319
   191
apply (frule up_chain_cases, safe)
huffman@16319
   192
apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
huffman@16319
   193
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
huffman@16319
   194
apply (simp add: cont_cfun_arg)
huffman@16319
   195
apply (simp add: thelub_const lub_const)
huffman@15576
   196
done
huffman@15576
   197
huffman@15593
   198
subsection {* Continuous versions of constants *}
huffman@15576
   199
huffman@15593
   200
constdefs  
huffman@16319
   201
  up  :: "'a \<rightarrow> 'a u"
huffman@16319
   202
  "up \<equiv> \<Lambda> x. Iup x"
huffman@16319
   203
huffman@16319
   204
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
huffman@16319
   205
  "fup \<equiv> \<Lambda> f p. Ifup f p"
huffman@15593
   206
huffman@15593
   207
translations
huffman@16753
   208
"case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
huffman@15593
   209
huffman@15593
   210
text {* continuous versions of lemmas for @{typ "('a)u"} *}
huffman@15576
   211
huffman@16753
   212
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
huffman@16753
   213
apply (induct z)
huffman@16319
   214
apply (simp add: inst_up_pcpo)
huffman@16319
   215
apply (simp add: up_def cont_Iup)
huffman@15576
   216
done
huffman@15576
   217
huffman@16753
   218
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
huffman@16319
   219
by (simp add: up_def cont_Iup)
huffman@15576
   220
huffman@16753
   221
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
huffman@16753
   222
by simp
huffman@16319
   223
huffman@16319
   224
lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
huffman@16319
   225
by (simp add: up_def cont_Iup inst_up_pcpo)
huffman@15576
   226
huffman@16319
   227
lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
huffman@16319
   228
by (simp add: eq_UU_iff [symmetric])
huffman@15576
   229
huffman@16326
   230
lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
huffman@16319
   231
by (simp add: up_def cont_Iup)
huffman@16319
   232
huffman@16753
   233
lemma upE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@16753
   234
apply (case_tac p)
huffman@16319
   235
apply (simp add: inst_up_pcpo)
huffman@16319
   236
apply (simp add: up_def cont_Iup)
huffman@15576
   237
done
huffman@15576
   238
huffman@16319
   239
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@16319
   240
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
huffman@15576
   241
huffman@16319
   242
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
huffman@16753
   243
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
huffman@15576
   244
huffman@16553
   245
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
huffman@16753
   246
by (rule_tac p=x in upE, simp_all)
huffman@15576
   247
huffman@15576
   248
end