src/HOLCF/Lift.thy
author huffman
Tue Jul 05 23:14:48 2005 +0200 (2005-07-05)
changeset 16695 dc8c868e910b
parent 16630 83bf468b1dc7
child 16748 58b9ce4fac54
permissions -rw-r--r--
simplified definitions of flift1, flift2, liftpair;
added theorem cont2cont_flift1;
renamed strictness and definedness theorems
slotosch@2640
     1
(*  Title:      HOLCF/Lift.thy
slotosch@2640
     2
    ID:         $Id$
wenzelm@12026
     3
    Author:     Olaf Mueller
slotosch@2640
     4
*)
slotosch@2640
     5
wenzelm@12338
     6
header {* Lifting types of class type to flat pcpo's *}
wenzelm@12026
     7
huffman@15577
     8
theory Lift
huffman@15577
     9
imports Cprod
huffman@15577
    10
begin
wenzelm@12026
    11
wenzelm@12338
    12
defaultsort type
wenzelm@12026
    13
wenzelm@12026
    14
wenzelm@12026
    15
typedef 'a lift = "UNIV :: 'a option set" ..
wenzelm@12026
    16
wenzelm@12026
    17
constdefs
wenzelm@12026
    18
  Undef :: "'a lift"
wenzelm@12026
    19
  "Undef == Abs_lift None"
wenzelm@12026
    20
  Def :: "'a => 'a lift"
wenzelm@12026
    21
  "Def x == Abs_lift (Some x)"
wenzelm@12026
    22
wenzelm@12338
    23
instance lift :: (type) sq_ord ..
wenzelm@12026
    24
wenzelm@12026
    25
defs (overloaded)
wenzelm@12026
    26
  less_lift_def: "x << y == (x=y | x=Undef)"
wenzelm@12026
    27
wenzelm@12338
    28
instance lift :: (type) po
wenzelm@12026
    29
proof
wenzelm@12026
    30
  fix x y z :: "'a lift"
wenzelm@12026
    31
  show "x << x" by (unfold less_lift_def) blast
wenzelm@12026
    32
  { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast }
wenzelm@12026
    33
  { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast }
wenzelm@12026
    34
qed
wenzelm@12026
    35
wenzelm@12026
    36
lemma inst_lift_po: "(op <<) = (\<lambda>x y. x = y | x = Undef)"
wenzelm@12026
    37
  -- {* For compatibility with old HOLCF-Version. *}
wenzelm@12026
    38
  by (simp only: less_lift_def [symmetric])
wenzelm@12026
    39
wenzelm@12026
    40
wenzelm@12026
    41
subsection {* Type lift is pointed *}
wenzelm@12026
    42
wenzelm@12026
    43
lemma minimal_lift [iff]: "Undef << x"
wenzelm@12026
    44
  by (simp add: inst_lift_po)
wenzelm@12026
    45
huffman@15930
    46
lemma UU_lift_def: "(THE u. \<forall>y. u \<sqsubseteq> y) = Undef"
wenzelm@12026
    47
  apply (rule minimal2UU [symmetric])
wenzelm@12026
    48
  apply (rule minimal_lift)
wenzelm@12026
    49
  done
wenzelm@12026
    50
wenzelm@12026
    51
lemma least_lift: "EX x::'a lift. ALL y. x << y"
wenzelm@12026
    52
  apply (rule_tac x = Undef in exI)
wenzelm@12026
    53
  apply (rule minimal_lift [THEN allI])
wenzelm@12026
    54
  done
wenzelm@12026
    55
wenzelm@12026
    56
wenzelm@12026
    57
subsection {* Type lift is a cpo *}
wenzelm@12026
    58
wenzelm@12026
    59
text {*
wenzelm@12026
    60
  The following lemmas have already been proved in @{text Pcpo.ML} and
wenzelm@12026
    61
  @{text Fix.ML}, but there class @{text pcpo} is assumed, although
wenzelm@12026
    62
  only @{text po} is necessary and a least element. Therefore they are
wenzelm@12026
    63
  redone here for the @{text po} lift with least element @{text
wenzelm@12026
    64
  Undef}.
wenzelm@12026
    65
*}
wenzelm@12026
    66
wenzelm@12026
    67
lemma flat_imp_chfin_poo: "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))"
wenzelm@12026
    68
  -- {* Tailoring @{text flat_imp_chfin} of @{text Fix.ML} to @{text lift} *}
wenzelm@12026
    69
  apply (unfold max_in_chain_def)
huffman@16067
    70
  apply clarify
huffman@16067
    71
  apply (case_tac "ALL i. Y i = Undef")
huffman@16067
    72
   apply simp
huffman@16067
    73
  apply simp
huffman@16067
    74
  apply (erule exE)
huffman@16067
    75
  apply (rule_tac x=i in exI)
huffman@16067
    76
  apply clarify
huffman@16067
    77
  apply (drule chain_mono3, assumption)
huffman@16067
    78
  apply (simp add: less_lift_def)
wenzelm@12026
    79
  done
wenzelm@12026
    80
huffman@16067
    81
instance lift :: (type) chfin
huffman@16067
    82
  apply intro_classes
huffman@16067
    83
  apply (rule flat_imp_chfin_poo)
wenzelm@12026
    84
  done
wenzelm@12026
    85
wenzelm@12338
    86
instance lift :: (type) pcpo
wenzelm@12026
    87
  apply intro_classes
wenzelm@12026
    88
  apply (rule least_lift)
wenzelm@12026
    89
  done
wenzelm@12026
    90
wenzelm@12026
    91
lemma inst_lift_pcpo: "UU = Undef"
wenzelm@12026
    92
  -- {* For compatibility with old HOLCF-Version. *}
wenzelm@12026
    93
  by (simp add: UU_def UU_lift_def)
wenzelm@12026
    94
wenzelm@12026
    95
wenzelm@12026
    96
subsection {* Lift as a datatype *}
wenzelm@12026
    97
wenzelm@12026
    98
lemma lift_distinct1: "UU ~= Def x"
wenzelm@12026
    99
  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
   100
wenzelm@12026
   101
lemma lift_distinct2: "Def x ~= UU"
wenzelm@12026
   102
  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
   103
wenzelm@12026
   104
lemma Def_inject: "(Def x = Def x') = (x = x')"
wenzelm@12026
   105
  by (simp add: Def_def Abs_lift_inject lift_def)
wenzelm@12026
   106
wenzelm@12026
   107
lemma lift_induct: "P UU ==> (!!x. P (Def x)) ==> P y"
wenzelm@12026
   108
  apply (induct y)
wenzelm@12026
   109
  apply (induct_tac y)
wenzelm@12026
   110
   apply (simp_all add: Undef_def Def_def inst_lift_pcpo)
wenzelm@12026
   111
  done
wenzelm@12026
   112
wenzelm@12026
   113
rep_datatype lift
wenzelm@12026
   114
  distinct lift_distinct1 lift_distinct2
wenzelm@12026
   115
  inject Def_inject
wenzelm@12026
   116
  induction lift_induct
wenzelm@12026
   117
wenzelm@12026
   118
lemma Def_not_UU: "Def a ~= UU"
wenzelm@12026
   119
  by simp
wenzelm@12026
   120
wenzelm@12026
   121
declare inst_lift_pcpo [symmetric, simp]
wenzelm@12026
   122
wenzelm@12026
   123
lemma less_lift: "(x::'a lift) << y = (x=y | x=UU)"
wenzelm@12026
   124
  by (simp add: inst_lift_po)
wenzelm@12026
   125
wenzelm@12026
   126
wenzelm@12026
   127
text {* @{text UU} and @{text Def} *}
wenzelm@12026
   128
wenzelm@12026
   129
lemma Lift_exhaust: "x = UU | (EX y. x = Def y)"
wenzelm@12026
   130
  by (induct x) simp_all
wenzelm@12026
   131
wenzelm@12026
   132
lemma Lift_cases: "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"
wenzelm@12026
   133
  by (insert Lift_exhaust) blast
wenzelm@12026
   134
wenzelm@12026
   135
lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)"
wenzelm@12026
   136
  by (cases x) simp_all
wenzelm@12026
   137
huffman@16630
   138
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@16630
   139
  by (cases x) simp_all
huffman@16630
   140
wenzelm@12026
   141
text {*
wenzelm@12026
   142
  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
wenzelm@12026
   143
  x} by @{text "Def a"} in conclusion. *}
wenzelm@12026
   144
wenzelm@16121
   145
ML {*
huffman@16630
   146
  local val lift_definedE = thm "lift_definedE"
wenzelm@12026
   147
  in val def_tac = SIMPSET' (fn ss =>
huffman@16630
   148
    etac lift_definedE THEN' asm_simp_tac ss)
wenzelm@12026
   149
  end;
wenzelm@12026
   150
*}
wenzelm@12026
   151
wenzelm@12026
   152
lemma Undef_eq_UU: "Undef = UU"
wenzelm@12026
   153
  by (rule inst_lift_pcpo [symmetric])
wenzelm@12026
   154
wenzelm@12026
   155
lemma DefE: "Def x = UU ==> R"
wenzelm@12026
   156
  by simp
wenzelm@12026
   157
wenzelm@12026
   158
lemma DefE2: "[| x = Def s; x = UU |] ==> R"
wenzelm@12026
   159
  by simp
wenzelm@12026
   160
wenzelm@12026
   161
lemma Def_inject_less_eq: "Def x << Def y = (x = y)"
wenzelm@12026
   162
  by (simp add: less_lift_def)
wenzelm@12026
   163
wenzelm@12026
   164
lemma Def_less_is_eq [simp]: "Def x << y = (Def x = y)"
wenzelm@12026
   165
  by (simp add: less_lift)
wenzelm@12026
   166
wenzelm@12026
   167
wenzelm@12026
   168
subsection {* Lift is flat *}
wenzelm@12026
   169
wenzelm@12338
   170
instance lift :: (type) flat
wenzelm@12026
   171
proof
wenzelm@12026
   172
  show "ALL x y::'a lift. x << y --> x = UU | x = y"
wenzelm@12026
   173
    by (simp add: less_lift)
wenzelm@12026
   174
qed
wenzelm@12026
   175
wenzelm@12026
   176
text {*
wenzelm@12026
   177
  \medskip Two specific lemmas for the combination of LCF and HOL
wenzelm@12026
   178
  terms.
wenzelm@12026
   179
*}
wenzelm@12026
   180
wenzelm@12026
   181
lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"
wenzelm@12026
   182
  apply (rule cont2cont_CF1L)
wenzelm@12026
   183
  apply (tactic "resolve_tac cont_lemmas1 1")+
wenzelm@12026
   184
   apply auto
wenzelm@12026
   185
  done
wenzelm@12026
   186
wenzelm@12026
   187
lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"
wenzelm@12026
   188
  apply (rule cont2cont_CF1L)
wenzelm@12026
   189
  apply (erule cont_Rep_CFun_app)
wenzelm@12026
   190
  apply assumption
wenzelm@12026
   191
  done
slotosch@2640
   192
huffman@16695
   193
subsection {* Further operations *}
huffman@16695
   194
huffman@16695
   195
constdefs
huffman@16695
   196
  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10)
huffman@16695
   197
  "flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)"
huffman@16695
   198
huffman@16695
   199
  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)"
huffman@16695
   200
  "flift2 f \<equiv> FLIFT x. Def (f x)"
huffman@16695
   201
huffman@16695
   202
  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift"
huffman@16695
   203
  "liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
huffman@16695
   204
huffman@16695
   205
subsection {* Continuity Proofs for flift1, flift2 *}
wenzelm@12026
   206
wenzelm@12026
   207
text {* Need the instance of @{text flat}. *}
wenzelm@12026
   208
huffman@16695
   209
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
huffman@16695
   210
apply (induct x)
huffman@16695
   211
apply simp
huffman@16695
   212
apply simp
huffman@16695
   213
apply (rule cont_id [THEN cont2cont_CF1L])
huffman@16695
   214
done
huffman@16695
   215
huffman@16695
   216
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
huffman@16695
   217
apply (rule flatdom_strict2cont)
huffman@16695
   218
apply simp
huffman@16695
   219
done
huffman@16695
   220
huffman@16695
   221
lemma cont_flift1: "cont flift1"
huffman@16695
   222
apply (unfold flift1_def)
huffman@16695
   223
apply (rule cont2cont_LAM)
huffman@16695
   224
apply (rule cont_lift_case2)
huffman@16695
   225
apply (rule cont_lift_case1)
huffman@16695
   226
done
huffman@16695
   227
huffman@16695
   228
lemma cont2cont_flift1:
huffman@16695
   229
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
huffman@16695
   230
apply (rule cont_flift1 [THEN cont2cont_app3])
huffman@16695
   231
apply (simp add: cont2cont_lambda)
huffman@16695
   232
done
huffman@16695
   233
huffman@16695
   234
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
huffman@16695
   235
by (simp add: flift1_def cont_lift_case2)
huffman@16695
   236
huffman@16695
   237
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
huffman@16695
   238
by (simp add: flift2_def)
huffman@16695
   239
huffman@16695
   240
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   241
by (simp add: flift1_def cont_lift_case2)
huffman@16695
   242
huffman@16695
   243
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   244
by (simp add: flift2_def)
huffman@16695
   245
huffman@16695
   246
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
huffman@16695
   247
by (erule lift_definedE, simp)
huffman@16695
   248
huffman@16695
   249
text {* old continuity rules *}
huffman@16695
   250
wenzelm@12026
   251
lemma cont_flift1_arg: "cont (lift_case UU f)"
wenzelm@12026
   252
  -- {* @{text flift1} is continuous in its argument itself. *}
wenzelm@12026
   253
  apply (rule flatdom_strict2cont)
wenzelm@12026
   254
  apply simp
wenzelm@12026
   255
  done
wenzelm@12026
   256
wenzelm@12026
   257
lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==>
wenzelm@12026
   258
           cont (%y. lift_case UU (f y))"
wenzelm@12026
   259
  -- {* @{text flift1} is continuous in a variable that occurs only
wenzelm@12026
   260
    in the @{text Def} branch. *}
wenzelm@12026
   261
  apply (rule cont2cont_CF1L_rev)
wenzelm@12026
   262
  apply (intro strip)
wenzelm@12026
   263
  apply (case_tac y)
wenzelm@12026
   264
   apply simp
wenzelm@12026
   265
  apply simp
wenzelm@12026
   266
  done
wenzelm@12026
   267
wenzelm@12026
   268
lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==>
wenzelm@12026
   269
    cont (%y. lift_case UU (f y) (g y))"
wenzelm@12026
   270
  -- {* @{text flift1} is continuous in a variable that occurs either
wenzelm@12026
   271
    in the @{text Def} branch or in the argument. *}
huffman@16216
   272
  apply (rule_tac t=g in cont2cont_app)
wenzelm@12026
   273
    apply (rule cont_flift1_not_arg)
wenzelm@12026
   274
    apply auto
wenzelm@12026
   275
  apply (rule cont_flift1_arg)
wenzelm@12026
   276
  done
wenzelm@12026
   277
wenzelm@12026
   278
lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))"
wenzelm@12026
   279
  -- {* @{text flift2} is continuous in its argument itself. *}
wenzelm@12026
   280
  apply (rule flatdom_strict2cont)
wenzelm@12026
   281
  apply simp
wenzelm@12026
   282
  done
wenzelm@12026
   283
wenzelm@12026
   284
text {*
oheimb@14096
   285
  \medskip Extension of @{text cont_tac} and installation of simplifier.
wenzelm@12026
   286
*}
wenzelm@12026
   287
wenzelm@12026
   288
lemmas cont_lemmas_ext [simp] =
wenzelm@12026
   289
  cont_flift1_arg cont_flift2_arg
huffman@16388
   290
  cont_flift1_arg_and_not_arg cont2cont_lambda
wenzelm@12026
   291
  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
wenzelm@12026
   292
wenzelm@16121
   293
ML {*
wenzelm@12026
   294
val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
wenzelm@12026
   295
wenzelm@12026
   296
fun cont_tac  i = resolve_tac cont_lemmas2 i;
wenzelm@12026
   297
fun cont_tacR i = REPEAT (cont_tac i);
wenzelm@12026
   298
wenzelm@12026
   299
local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def"
wenzelm@12026
   300
in fun cont_tacRs i =
wenzelm@12026
   301
  simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
wenzelm@12026
   302
  REPEAT (cont_tac i)
wenzelm@12026
   303
end;
huffman@15651
   304
*}
wenzelm@12026
   305
slotosch@2640
   306
end