src/HOLCF/Lift.thy
author wenzelm
Sat Nov 03 01:38:11 2001 +0100 (2001-11-03)
changeset 12026 0b1d80ada4ab
parent 2640 ee4dfce170a0
child 12338 de0f4a63baa5
permissions -rw-r--r--
rep_datatype lift;
converted to new-style theory;
slotosch@2640
     1
(*  Title:      HOLCF/Lift.thy
slotosch@2640
     2
    ID:         $Id$
wenzelm@12026
     3
    Author:     Olaf Mueller
wenzelm@12026
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
slotosch@2640
     5
*)
slotosch@2640
     6
wenzelm@12026
     7
header {* Lifting types of class term to flat pcpo's *}
wenzelm@12026
     8
wenzelm@12026
     9
theory Lift = Cprod3:
wenzelm@12026
    10
wenzelm@12026
    11
defaultsort "term"
wenzelm@12026
    12
wenzelm@12026
    13
wenzelm@12026
    14
typedef 'a lift = "UNIV :: 'a option set" ..
wenzelm@12026
    15
wenzelm@12026
    16
constdefs
wenzelm@12026
    17
  Undef :: "'a lift"
wenzelm@12026
    18
  "Undef == Abs_lift None"
wenzelm@12026
    19
  Def :: "'a => 'a lift"
wenzelm@12026
    20
  "Def x == Abs_lift (Some x)"
wenzelm@12026
    21
wenzelm@12026
    22
instance lift :: ("term") sq_ord ..
wenzelm@12026
    23
wenzelm@12026
    24
defs (overloaded)
wenzelm@12026
    25
  less_lift_def: "x << y == (x=y | x=Undef)"
wenzelm@12026
    26
wenzelm@12026
    27
instance lift :: ("term") po
wenzelm@12026
    28
proof
wenzelm@12026
    29
  fix x y z :: "'a lift"
wenzelm@12026
    30
  show "x << x" by (unfold less_lift_def) blast
wenzelm@12026
    31
  { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast }
wenzelm@12026
    32
  { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast }
wenzelm@12026
    33
qed
wenzelm@12026
    34
wenzelm@12026
    35
lemma inst_lift_po: "(op <<) = (\<lambda>x y. x = y | x = Undef)"
wenzelm@12026
    36
  -- {* For compatibility with old HOLCF-Version. *}
wenzelm@12026
    37
  by (simp only: less_lift_def [symmetric])
wenzelm@12026
    38
wenzelm@12026
    39
wenzelm@12026
    40
subsection {* Type lift is pointed *}
wenzelm@12026
    41
wenzelm@12026
    42
lemma minimal_lift [iff]: "Undef << x"
wenzelm@12026
    43
  by (simp add: inst_lift_po)
wenzelm@12026
    44
wenzelm@12026
    45
lemma UU_lift_def: "(SOME u. \<forall>y. u \<sqsubseteq> y) = Undef"
wenzelm@12026
    46
  apply (rule minimal2UU [symmetric])
wenzelm@12026
    47
  apply (rule minimal_lift)
wenzelm@12026
    48
  done
wenzelm@12026
    49
wenzelm@12026
    50
lemma least_lift: "EX x::'a lift. ALL y. x << y"
wenzelm@12026
    51
  apply (rule_tac x = Undef in exI)
wenzelm@12026
    52
  apply (rule minimal_lift [THEN allI])
wenzelm@12026
    53
  done
wenzelm@12026
    54
wenzelm@12026
    55
wenzelm@12026
    56
subsection {* Type lift is a cpo *}
wenzelm@12026
    57
wenzelm@12026
    58
text {*
wenzelm@12026
    59
  The following lemmas have already been proved in @{text Pcpo.ML} and
wenzelm@12026
    60
  @{text Fix.ML}, but there class @{text pcpo} is assumed, although
wenzelm@12026
    61
  only @{text po} is necessary and a least element. Therefore they are
wenzelm@12026
    62
  redone here for the @{text po} lift with least element @{text
wenzelm@12026
    63
  Undef}.
wenzelm@12026
    64
*}
wenzelm@12026
    65
wenzelm@12026
    66
lemma notUndef_I: "[| x<<y; x ~= Undef |] ==> y ~= Undef"
wenzelm@12026
    67
  -- {* Tailoring @{text notUU_I} of @{text Pcpo.ML} to @{text Undef} *}
wenzelm@12026
    68
  by (blast intro: antisym_less)
wenzelm@12026
    69
wenzelm@12026
    70
lemma chain_mono2_po: "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |]
wenzelm@12026
    71
         ==> EX j. ALL i. j<i-->~Y(i)=Undef"
wenzelm@12026
    72
  -- {* Tailoring @{text chain_mono2} of @{text Pcpo.ML} to @{text Undef} *}
wenzelm@12026
    73
  apply safe
wenzelm@12026
    74
  apply (rule exI)
wenzelm@12026
    75
  apply (intro strip)
wenzelm@12026
    76
  apply (rule notUndef_I)
wenzelm@12026
    77
   apply (erule (1) chain_mono)
wenzelm@12026
    78
  apply assumption
wenzelm@12026
    79
  done
wenzelm@12026
    80
wenzelm@12026
    81
lemma flat_imp_chfin_poo: "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))"
wenzelm@12026
    82
  -- {* Tailoring @{text flat_imp_chfin} of @{text Fix.ML} to @{text lift} *}
wenzelm@12026
    83
  apply (unfold max_in_chain_def)
wenzelm@12026
    84
  apply (intro strip)
wenzelm@12026
    85
  apply (rule_tac P = "ALL i. Y (i) = Undef" in case_split)
wenzelm@12026
    86
   apply (rule_tac x = 0 in exI)
wenzelm@12026
    87
   apply (intro strip)
wenzelm@12026
    88
   apply (rule trans)
wenzelm@12026
    89
    apply (erule spec)
wenzelm@12026
    90
   apply (rule sym)
wenzelm@12026
    91
   apply (erule spec)
wenzelm@12026
    92
  apply (subgoal_tac "ALL x y. x << (y:: ('a) lift) --> x=Undef | x=y")
wenzelm@12026
    93
   prefer 2 apply (simp add: inst_lift_po)
wenzelm@12026
    94
  apply (rule chain_mono2_po [THEN exE])
wenzelm@12026
    95
    apply fast
wenzelm@12026
    96
   apply assumption
wenzelm@12026
    97
  apply (rule_tac x = "Suc x" in exI)
wenzelm@12026
    98
  apply (intro strip)
wenzelm@12026
    99
  apply (rule disjE)
wenzelm@12026
   100
    prefer 3 apply assumption
wenzelm@12026
   101
   apply (rule mp)
wenzelm@12026
   102
    apply (drule spec)
wenzelm@12026
   103
    apply (erule spec)
wenzelm@12026
   104
   apply (erule le_imp_less_or_eq [THEN disjE])
wenzelm@12026
   105
    apply (erule chain_mono)
wenzelm@12026
   106
    apply auto
wenzelm@12026
   107
  done
wenzelm@12026
   108
wenzelm@12026
   109
theorem cpo_lift: "chain (Y::nat => 'a lift) ==> EX x. range Y <<| x"
wenzelm@12026
   110
  apply (cut_tac flat_imp_chfin_poo)
wenzelm@12026
   111
  apply (blast intro: lub_finch1)
wenzelm@12026
   112
  done
wenzelm@12026
   113
wenzelm@12026
   114
instance lift :: ("term") pcpo
wenzelm@12026
   115
  apply intro_classes
wenzelm@12026
   116
   apply (erule cpo_lift)
wenzelm@12026
   117
  apply (rule least_lift)
wenzelm@12026
   118
  done
wenzelm@12026
   119
wenzelm@12026
   120
lemma inst_lift_pcpo: "UU = Undef"
wenzelm@12026
   121
  -- {* For compatibility with old HOLCF-Version. *}
wenzelm@12026
   122
  by (simp add: UU_def UU_lift_def)
wenzelm@12026
   123
wenzelm@12026
   124
wenzelm@12026
   125
subsection {* Lift as a datatype *}
wenzelm@12026
   126
wenzelm@12026
   127
lemma lift_distinct1: "UU ~= Def x"
wenzelm@12026
   128
  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
   129
wenzelm@12026
   130
lemma lift_distinct2: "Def x ~= UU"
wenzelm@12026
   131
  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
   132
wenzelm@12026
   133
lemma Def_inject: "(Def x = Def x') = (x = x')"
wenzelm@12026
   134
  by (simp add: Def_def Abs_lift_inject lift_def)
wenzelm@12026
   135
wenzelm@12026
   136
lemma lift_induct: "P UU ==> (!!x. P (Def x)) ==> P y"
wenzelm@12026
   137
  apply (induct y)
wenzelm@12026
   138
  apply (induct_tac y)
wenzelm@12026
   139
   apply (simp_all add: Undef_def Def_def inst_lift_pcpo)
wenzelm@12026
   140
  done
wenzelm@12026
   141
wenzelm@12026
   142
rep_datatype lift
wenzelm@12026
   143
  distinct lift_distinct1 lift_distinct2
wenzelm@12026
   144
  inject Def_inject
wenzelm@12026
   145
  induction lift_induct
wenzelm@12026
   146
wenzelm@12026
   147
lemma Def_not_UU: "Def a ~= UU"
wenzelm@12026
   148
  by simp
wenzelm@12026
   149
wenzelm@12026
   150
wenzelm@12026
   151
subsection {* Further operations *}
wenzelm@12026
   152
wenzelm@12026
   153
consts
wenzelm@12026
   154
 flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
wenzelm@12026
   155
 flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
wenzelm@12026
   156
 liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
slotosch@2640
   157
wenzelm@12026
   158
defs
wenzelm@12026
   159
 flift1_def:
wenzelm@12026
   160
  "flift1 f == (LAM x. (case x of
wenzelm@12026
   161
                   UU => UU
wenzelm@12026
   162
                 | Def y => (f y)))"
wenzelm@12026
   163
 flift2_def:
wenzelm@12026
   164
  "flift2 f == (LAM x. (case x of
wenzelm@12026
   165
                   UU => UU
wenzelm@12026
   166
                 | Def y => Def (f y)))"
wenzelm@12026
   167
 liftpair_def:
wenzelm@12026
   168
  "liftpair x  == (case (cfst$x) of
wenzelm@12026
   169
                  UU  => UU
wenzelm@12026
   170
                | Def x1 => (case (csnd$x) of
wenzelm@12026
   171
                               UU => UU
wenzelm@12026
   172
                             | Def x2 => Def (x1,x2)))"
wenzelm@12026
   173
wenzelm@12026
   174
wenzelm@12026
   175
declare inst_lift_pcpo [symmetric, simp]
wenzelm@12026
   176
wenzelm@12026
   177
wenzelm@12026
   178
lemma less_lift: "(x::'a lift) << y = (x=y | x=UU)"
wenzelm@12026
   179
  by (simp add: inst_lift_po)
wenzelm@12026
   180
wenzelm@12026
   181
wenzelm@12026
   182
text {* @{text UU} and @{text Def} *}
wenzelm@12026
   183
wenzelm@12026
   184
lemma Lift_exhaust: "x = UU | (EX y. x = Def y)"
wenzelm@12026
   185
  by (induct x) simp_all
wenzelm@12026
   186
wenzelm@12026
   187
lemma Lift_cases: "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"
wenzelm@12026
   188
  by (insert Lift_exhaust) blast
wenzelm@12026
   189
wenzelm@12026
   190
lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)"
wenzelm@12026
   191
  by (cases x) simp_all
wenzelm@12026
   192
wenzelm@12026
   193
text {*
wenzelm@12026
   194
  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
wenzelm@12026
   195
  x} by @{text "Def a"} in conclusion. *}
wenzelm@12026
   196
wenzelm@12026
   197
ML {*
wenzelm@12026
   198
  local val not_Undef_is_Def = thm "not_Undef_is_Def"
wenzelm@12026
   199
  in val def_tac = SIMPSET' (fn ss =>
wenzelm@12026
   200
    etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
wenzelm@12026
   201
  end;
wenzelm@12026
   202
*}
wenzelm@12026
   203
wenzelm@12026
   204
lemma Undef_eq_UU: "Undef = UU"
wenzelm@12026
   205
  by (rule inst_lift_pcpo [symmetric])
wenzelm@12026
   206
wenzelm@12026
   207
lemma DefE: "Def x = UU ==> R"
wenzelm@12026
   208
  by simp
wenzelm@12026
   209
wenzelm@12026
   210
lemma DefE2: "[| x = Def s; x = UU |] ==> R"
wenzelm@12026
   211
  by simp
wenzelm@12026
   212
wenzelm@12026
   213
lemma Def_inject_less_eq: "Def x << Def y = (x = y)"
wenzelm@12026
   214
  by (simp add: less_lift_def)
wenzelm@12026
   215
wenzelm@12026
   216
lemma Def_less_is_eq [simp]: "Def x << y = (Def x = y)"
wenzelm@12026
   217
  by (simp add: less_lift)
wenzelm@12026
   218
wenzelm@12026
   219
wenzelm@12026
   220
subsection {* Lift is flat *}
wenzelm@12026
   221
wenzelm@12026
   222
instance lift :: ("term") flat
wenzelm@12026
   223
proof
wenzelm@12026
   224
  show "ALL x y::'a lift. x << y --> x = UU | x = y"
wenzelm@12026
   225
    by (simp add: less_lift)
wenzelm@12026
   226
qed
wenzelm@12026
   227
wenzelm@12026
   228
defaultsort pcpo
wenzelm@12026
   229
wenzelm@12026
   230
wenzelm@12026
   231
text {*
wenzelm@12026
   232
  \medskip Two specific lemmas for the combination of LCF and HOL
wenzelm@12026
   233
  terms.
wenzelm@12026
   234
*}
wenzelm@12026
   235
wenzelm@12026
   236
lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"
wenzelm@12026
   237
  apply (rule cont2cont_CF1L)
wenzelm@12026
   238
  apply (tactic "resolve_tac cont_lemmas1 1")+
wenzelm@12026
   239
   apply auto
wenzelm@12026
   240
  done
wenzelm@12026
   241
wenzelm@12026
   242
lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"
wenzelm@12026
   243
  apply (rule cont2cont_CF1L)
wenzelm@12026
   244
  apply (erule cont_Rep_CFun_app)
wenzelm@12026
   245
  apply assumption
wenzelm@12026
   246
  done
slotosch@2640
   247
wenzelm@12026
   248
text {* Continuity of if-then-else. *}
wenzelm@12026
   249
wenzelm@12026
   250
lemma cont_if: "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)"
wenzelm@12026
   251
  by (cases b) simp_all
wenzelm@12026
   252
wenzelm@12026
   253
wenzelm@12026
   254
subsection {* Continuity Proofs for flift1, flift2, if *}
wenzelm@12026
   255
wenzelm@12026
   256
text {* Need the instance of @{text flat}. *}
wenzelm@12026
   257
wenzelm@12026
   258
lemma cont_flift1_arg: "cont (lift_case UU f)"
wenzelm@12026
   259
  -- {* @{text flift1} is continuous in its argument itself. *}
wenzelm@12026
   260
  apply (rule flatdom_strict2cont)
wenzelm@12026
   261
  apply simp
wenzelm@12026
   262
  done
wenzelm@12026
   263
wenzelm@12026
   264
lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==>
wenzelm@12026
   265
           cont (%y. lift_case UU (f y))"
wenzelm@12026
   266
  -- {* @{text flift1} is continuous in a variable that occurs only
wenzelm@12026
   267
    in the @{text Def} branch. *}
wenzelm@12026
   268
  apply (rule cont2cont_CF1L_rev)
wenzelm@12026
   269
  apply (intro strip)
wenzelm@12026
   270
  apply (case_tac y)
wenzelm@12026
   271
   apply simp
wenzelm@12026
   272
  apply simp
wenzelm@12026
   273
  done
wenzelm@12026
   274
wenzelm@12026
   275
lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==>
wenzelm@12026
   276
    cont (%y. lift_case UU (f y) (g y))"
wenzelm@12026
   277
  -- {* @{text flift1} is continuous in a variable that occurs either
wenzelm@12026
   278
    in the @{text Def} branch or in the argument. *}
wenzelm@12026
   279
  apply (rule_tac tt = g in cont2cont_app)
wenzelm@12026
   280
    apply (rule cont_flift1_not_arg)
wenzelm@12026
   281
    apply auto
wenzelm@12026
   282
  apply (rule cont_flift1_arg)
wenzelm@12026
   283
  done
wenzelm@12026
   284
wenzelm@12026
   285
lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))"
wenzelm@12026
   286
  -- {* @{text flift2} is continuous in its argument itself. *}
wenzelm@12026
   287
  apply (rule flatdom_strict2cont)
wenzelm@12026
   288
  apply simp
wenzelm@12026
   289
  done
wenzelm@12026
   290
wenzelm@12026
   291
text {*
wenzelm@12026
   292
  \medskip Extension of cont_tac and installation of simplifier.
wenzelm@12026
   293
*}
wenzelm@12026
   294
wenzelm@12026
   295
lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1"
wenzelm@12026
   296
  apply (rule cont2cont_CF1L_rev)
wenzelm@12026
   297
  apply simp
wenzelm@12026
   298
  done
wenzelm@12026
   299
wenzelm@12026
   300
lemmas cont_lemmas_ext [simp] =
wenzelm@12026
   301
  cont_flift1_arg cont_flift2_arg
wenzelm@12026
   302
  cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
wenzelm@12026
   303
  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
wenzelm@12026
   304
wenzelm@12026
   305
ML_setup {*
wenzelm@12026
   306
val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
wenzelm@12026
   307
wenzelm@12026
   308
fun cont_tac  i = resolve_tac cont_lemmas2 i;
wenzelm@12026
   309
fun cont_tacR i = REPEAT (cont_tac i);
wenzelm@12026
   310
wenzelm@12026
   311
local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def"
wenzelm@12026
   312
in fun cont_tacRs i =
wenzelm@12026
   313
  simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
wenzelm@12026
   314
  REPEAT (cont_tac i)
wenzelm@12026
   315
end;
wenzelm@12026
   316
wenzelm@12026
   317
simpset_ref() := simpset() addSolver
wenzelm@12026
   318
  (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
wenzelm@12026
   319
*}
wenzelm@12026
   320
wenzelm@12026
   321
wenzelm@12026
   322
subsection {* flift1, flift2 *}
wenzelm@12026
   323
wenzelm@12026
   324
lemma flift1_Def [simp]: "flift1 f$(Def x) = (f x)"
wenzelm@12026
   325
  by (simp add: flift1_def)
wenzelm@12026
   326
wenzelm@12026
   327
lemma flift2_Def [simp]: "flift2 f$(Def x) = Def (f x)"
wenzelm@12026
   328
  by (simp add: flift2_def)
wenzelm@12026
   329
wenzelm@12026
   330
lemma flift1_UU [simp]: "flift1 f$UU = UU"
wenzelm@12026
   331
  by (simp add: flift1_def)
wenzelm@12026
   332
wenzelm@12026
   333
lemma flift2_UU [simp]: "flift2 f$UU = UU"
wenzelm@12026
   334
  by (simp add: flift2_def)
wenzelm@12026
   335
wenzelm@12026
   336
lemma flift2_nUU [simp]: "x~=UU ==> (flift2 f)$x~=UU"
wenzelm@12026
   337
  by (tactic "def_tac 1")
slotosch@2640
   338
slotosch@2640
   339
end