src/HOLCF/Lift.thy
author wenzelm
Sun Oct 21 14:21:48 2007 +0200 (2007-10-21)
changeset 25131 2c8caac48ade
parent 19764 372065f34795
child 25701 73fbe868b4e7
permissions -rw-r--r--
modernized specifications ('definition', 'abbreviation', 'notation');
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@16748
     9
imports Discrete Up Cprod
huffman@15577
    10
begin
wenzelm@12026
    11
wenzelm@12338
    12
defaultsort type
wenzelm@12026
    13
huffman@16748
    14
pcpodef 'a lift = "UNIV :: 'a discr u set"
huffman@16748
    15
by simp
wenzelm@12026
    16
huffman@16748
    17
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
wenzelm@12026
    18
wenzelm@25131
    19
definition
wenzelm@25131
    20
  Def :: "'a \<Rightarrow> 'a lift" where
wenzelm@25131
    21
  "Def x = Abs_lift (up\<cdot>(Discr x))"
wenzelm@12026
    22
wenzelm@12026
    23
subsection {* Lift as a datatype *}
wenzelm@12026
    24
huffman@16748
    25
lemma lift_distinct1: "\<bottom> \<noteq> Def x"
huffman@16748
    26
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
    27
huffman@16748
    28
lemma lift_distinct2: "Def x \<noteq> \<bottom>"
huffman@16748
    29
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
    30
huffman@16748
    31
lemma Def_inject: "(Def x = Def y) = (x = y)"
huffman@16748
    32
by (simp add: Def_def Abs_lift_inject lift_def)
wenzelm@12026
    33
huffman@16748
    34
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
huffman@16748
    35
apply (induct y)
huffman@16755
    36
apply (rule_tac p=y in upE)
huffman@16748
    37
apply (simp add: Abs_lift_strict)
huffman@16748
    38
apply (case_tac x)
huffman@16748
    39
apply (simp add: Def_def)
huffman@16748
    40
done
wenzelm@12026
    41
wenzelm@12026
    42
rep_datatype lift
wenzelm@12026
    43
  distinct lift_distinct1 lift_distinct2
wenzelm@12026
    44
  inject Def_inject
wenzelm@12026
    45
  induction lift_induct
wenzelm@12026
    46
huffman@16748
    47
lemma Def_not_UU: "Def a \<noteq> UU"
wenzelm@12026
    48
  by simp
wenzelm@12026
    49
wenzelm@12026
    50
huffman@16748
    51
text {* @{term UU} and @{term Def} *}
wenzelm@12026
    52
huffman@16748
    53
lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
wenzelm@12026
    54
  by (induct x) simp_all
wenzelm@12026
    55
huffman@16748
    56
lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
wenzelm@12026
    57
  by (insert Lift_exhaust) blast
wenzelm@12026
    58
huffman@16748
    59
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
wenzelm@12026
    60
  by (cases x) simp_all
wenzelm@12026
    61
huffman@16630
    62
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@16630
    63
  by (cases x) simp_all
huffman@16630
    64
wenzelm@12026
    65
text {*
wenzelm@12026
    66
  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
wenzelm@12026
    67
  x} by @{text "Def a"} in conclusion. *}
wenzelm@12026
    68
wenzelm@16121
    69
ML {*
huffman@16630
    70
  local val lift_definedE = thm "lift_definedE"
wenzelm@12026
    71
  in val def_tac = SIMPSET' (fn ss =>
huffman@16630
    72
    etac lift_definedE THEN' asm_simp_tac ss)
wenzelm@12026
    73
  end;
wenzelm@12026
    74
*}
wenzelm@12026
    75
huffman@16748
    76
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
huffman@16748
    77
  by simp
wenzelm@12026
    78
huffman@16748
    79
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
wenzelm@12026
    80
  by simp
wenzelm@12026
    81
huffman@16748
    82
lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y = (x = y)"
huffman@16748
    83
by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
wenzelm@12026
    84
huffman@16748
    85
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
huffman@16748
    86
apply (induct y)
huffman@19440
    87
apply simp
huffman@16748
    88
apply (simp add: Def_inject_less_eq)
huffman@16748
    89
done
wenzelm@12026
    90
wenzelm@12026
    91
wenzelm@12026
    92
subsection {* Lift is flat *}
wenzelm@12026
    93
huffman@16748
    94
lemma less_lift: "(x::'a lift) \<sqsubseteq> y = (x = y \<or> x = \<bottom>)"
huffman@16748
    95
by (induct x, simp_all)
huffman@16748
    96
wenzelm@12338
    97
instance lift :: (type) flat
huffman@16748
    98
by (intro_classes, simp add: less_lift)
wenzelm@12026
    99
wenzelm@12026
   100
text {*
wenzelm@12026
   101
  \medskip Two specific lemmas for the combination of LCF and HOL
wenzelm@12026
   102
  terms.
wenzelm@12026
   103
*}
wenzelm@12026
   104
huffman@16748
   105
lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
huffman@18092
   106
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
wenzelm@12026
   107
huffman@16748
   108
lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
huffman@18092
   109
by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
slotosch@2640
   110
huffman@16695
   111
subsection {* Further operations *}
huffman@16695
   112
wenzelm@25131
   113
definition
wenzelm@25131
   114
  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
wenzelm@25131
   115
  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
huffman@16695
   116
wenzelm@25131
   117
definition
wenzelm@25131
   118
  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
wenzelm@25131
   119
  "flift2 f = (FLIFT x. Def (f x))"
huffman@16695
   120
wenzelm@25131
   121
definition
wenzelm@25131
   122
  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where
wenzelm@25131
   123
  "liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
huffman@16695
   124
huffman@16695
   125
subsection {* Continuity Proofs for flift1, flift2 *}
wenzelm@12026
   126
wenzelm@12026
   127
text {* Need the instance of @{text flat}. *}
wenzelm@12026
   128
huffman@16695
   129
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
huffman@16695
   130
apply (induct x)
huffman@16695
   131
apply simp
huffman@16695
   132
apply simp
huffman@18092
   133
apply (rule cont_id [THEN cont2cont_fun])
huffman@16695
   134
done
huffman@16695
   135
huffman@16695
   136
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
huffman@16695
   137
apply (rule flatdom_strict2cont)
huffman@16695
   138
apply simp
huffman@16695
   139
done
huffman@16695
   140
huffman@16695
   141
lemma cont_flift1: "cont flift1"
huffman@16695
   142
apply (unfold flift1_def)
huffman@16695
   143
apply (rule cont2cont_LAM)
huffman@16695
   144
apply (rule cont_lift_case2)
huffman@16695
   145
apply (rule cont_lift_case1)
huffman@16695
   146
done
huffman@16695
   147
huffman@16695
   148
lemma cont2cont_flift1:
huffman@16695
   149
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
huffman@16695
   150
apply (rule cont_flift1 [THEN cont2cont_app3])
huffman@16695
   151
apply (simp add: cont2cont_lambda)
huffman@16695
   152
done
huffman@16695
   153
huffman@16757
   154
lemma cont2cont_lift_case:
huffman@16757
   155
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
huffman@16757
   156
apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
huffman@16757
   157
apply (simp add: flift1_def cont_lift_case2)
huffman@16757
   158
apply (simp add: cont2cont_flift1)
huffman@16757
   159
done
huffman@16757
   160
huffman@16757
   161
text {* rewrites for @{term flift1}, @{term flift2} *}
huffman@16757
   162
huffman@16695
   163
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
huffman@16695
   164
by (simp add: flift1_def cont_lift_case2)
huffman@16695
   165
huffman@16695
   166
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
huffman@16695
   167
by (simp add: flift2_def)
huffman@16695
   168
huffman@16695
   169
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   170
by (simp add: flift1_def cont_lift_case2)
huffman@16695
   171
huffman@16695
   172
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   173
by (simp add: flift2_def)
huffman@16695
   174
huffman@16695
   175
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
huffman@16695
   176
by (erule lift_definedE, simp)
huffman@16695
   177
huffman@19520
   178
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
huffman@19520
   179
by (cases x, simp_all)
huffman@19520
   180
wenzelm@12026
   181
text {*
oheimb@14096
   182
  \medskip Extension of @{text cont_tac} and installation of simplifier.
wenzelm@12026
   183
*}
wenzelm@12026
   184
wenzelm@12026
   185
lemmas cont_lemmas_ext [simp] =
huffman@16757
   186
  cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
wenzelm@12026
   187
  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
wenzelm@12026
   188
wenzelm@16121
   189
ML {*
wenzelm@19764
   190
local
wenzelm@19764
   191
  val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext";
wenzelm@19764
   192
  val flift1_def = thm "flift1_def";
wenzelm@19764
   193
in
wenzelm@12026
   194
wenzelm@12026
   195
fun cont_tac  i = resolve_tac cont_lemmas2 i;
wenzelm@12026
   196
fun cont_tacR i = REPEAT (cont_tac i);
wenzelm@12026
   197
wenzelm@19764
   198
fun cont_tacRs ss i =
wenzelm@17612
   199
  simp_tac ss i THEN
wenzelm@12026
   200
  REPEAT (cont_tac i)
wenzelm@12026
   201
end;
huffman@15651
   202
*}
wenzelm@12026
   203
slotosch@2640
   204
end