src/HOLCF/Lift.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 40002 c5b5f7a3a3b1
child 40008 58ead6f77f8e
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
slotosch@2640
     1
(*  Title:      HOLCF/Lift.thy
wenzelm@12026
     2
    Author:     Olaf Mueller
slotosch@2640
     3
*)
slotosch@2640
     4
wenzelm@12338
     5
header {* Lifting types of class type to flat pcpo's *}
wenzelm@12026
     6
huffman@15577
     7
theory Lift
huffman@27311
     8
imports Discrete Up Countable
huffman@15577
     9
begin
wenzelm@12026
    10
wenzelm@36452
    11
default_sort type
wenzelm@12026
    12
huffman@16748
    13
pcpodef 'a lift = "UNIV :: 'a discr u set"
wenzelm@29063
    14
by simp_all
wenzelm@12026
    15
huffman@25827
    16
instance lift :: (finite) finite_po
huffman@25827
    17
by (rule typedef_finite_po [OF type_definition_lift])
huffman@25827
    18
huffman@16748
    19
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
wenzelm@12026
    20
wenzelm@25131
    21
definition
wenzelm@25131
    22
  Def :: "'a \<Rightarrow> 'a lift" where
wenzelm@25131
    23
  "Def x = Abs_lift (up\<cdot>(Discr x))"
wenzelm@12026
    24
wenzelm@12026
    25
subsection {* Lift as a datatype *}
wenzelm@12026
    26
huffman@16748
    27
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
huffman@16748
    28
apply (induct y)
huffman@16755
    29
apply (rule_tac p=y in upE)
huffman@16748
    30
apply (simp add: Abs_lift_strict)
huffman@16748
    31
apply (case_tac x)
huffman@16748
    32
apply (simp add: Def_def)
huffman@16748
    33
done
wenzelm@12026
    34
haftmann@27104
    35
rep_datatype "\<bottom>\<Colon>'a lift" Def
haftmann@27104
    36
  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
wenzelm@12026
    37
haftmann@27104
    38
lemmas lift_distinct1 = lift.distinct(1)
haftmann@27104
    39
lemmas lift_distinct2 = lift.distinct(2)
haftmann@27104
    40
lemmas Def_not_UU = lift.distinct(2)
haftmann@27104
    41
lemmas Def_inject = lift.inject
wenzelm@12026
    42
wenzelm@12026
    43
huffman@16748
    44
text {* @{term UU} and @{term Def} *}
wenzelm@12026
    45
huffman@16748
    46
lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)"
wenzelm@12026
    47
  by (induct x) simp_all
wenzelm@12026
    48
huffman@16748
    49
lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
wenzelm@12026
    50
  by (insert Lift_exhaust) blast
wenzelm@12026
    51
huffman@16748
    52
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
wenzelm@12026
    53
  by (cases x) simp_all
wenzelm@12026
    54
huffman@16630
    55
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
huffman@16630
    56
  by (cases x) simp_all
huffman@16630
    57
wenzelm@12026
    58
text {*
wenzelm@30607
    59
  For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
wenzelm@12026
    60
  x} by @{text "Def a"} in conclusion. *}
wenzelm@12026
    61
wenzelm@30607
    62
method_setup defined = {*
wenzelm@30607
    63
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
wenzelm@32149
    64
    (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
wenzelm@30607
    65
*} ""
wenzelm@12026
    66
huffman@16748
    67
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
huffman@16748
    68
  by simp
wenzelm@12026
    69
huffman@16748
    70
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
wenzelm@12026
    71
  by simp
wenzelm@12026
    72
huffman@31076
    73
lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
huffman@31076
    74
by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
wenzelm@12026
    75
huffman@31076
    76
lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
huffman@31076
    77
by (induct y, simp, simp add: Def_below_Def)
wenzelm@12026
    78
wenzelm@12026
    79
wenzelm@12026
    80
subsection {* Lift is flat *}
wenzelm@12026
    81
wenzelm@12338
    82
instance lift :: (type) flat
huffman@27292
    83
proof
huffman@27292
    84
  fix x y :: "'a lift"
huffman@27292
    85
  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
huffman@27292
    86
    by (induct x) auto
huffman@27292
    87
qed
wenzelm@12026
    88
wenzelm@12026
    89
text {*
wenzelm@12026
    90
  \medskip Two specific lemmas for the combination of LCF and HOL
wenzelm@12026
    91
  terms.
wenzelm@12026
    92
*}
wenzelm@12026
    93
huffman@26452
    94
lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
huffman@18092
    95
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
wenzelm@12026
    96
huffman@26452
    97
lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
huffman@18092
    98
by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
slotosch@2640
    99
huffman@16695
   100
subsection {* Further operations *}
huffman@16695
   101
wenzelm@25131
   102
definition
wenzelm@25131
   103
  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
wenzelm@25131
   104
  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
huffman@16695
   105
wenzelm@25131
   106
definition
wenzelm@25131
   107
  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
wenzelm@25131
   108
  "flift2 f = (FLIFT x. Def (f x))"
huffman@16695
   109
huffman@16695
   110
subsection {* Continuity Proofs for flift1, flift2 *}
wenzelm@12026
   111
wenzelm@12026
   112
text {* Need the instance of @{text flat}. *}
wenzelm@12026
   113
huffman@16695
   114
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)"
huffman@16695
   115
apply (induct x)
huffman@16695
   116
apply simp
huffman@16695
   117
apply simp
huffman@18092
   118
apply (rule cont_id [THEN cont2cont_fun])
huffman@16695
   119
done
huffman@16695
   120
huffman@25723
   121
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
huffman@16695
   122
apply (rule flatdom_strict2cont)
huffman@16695
   123
apply simp
huffman@16695
   124
done
huffman@16695
   125
huffman@16695
   126
lemma cont_flift1: "cont flift1"
huffman@27292
   127
unfolding flift1_def
huffman@16695
   128
apply (rule cont2cont_LAM)
huffman@16695
   129
apply (rule cont_lift_case2)
huffman@16695
   130
apply (rule cont_lift_case1)
huffman@16695
   131
done
huffman@16695
   132
huffman@27310
   133
lemma FLIFT_mono:
huffman@27310
   134
  "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
huffman@27310
   135
apply (rule monofunE [where f=flift1])
huffman@27310
   136
apply (rule cont2mono [OF cont_flift1])
huffman@40002
   137
apply (simp add: fun_below_iff)
huffman@27310
   138
done
huffman@27310
   139
huffman@37099
   140
lemma cont2cont_flift1 [simp, cont2cont]:
huffman@16695
   141
  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
huffman@40006
   142
apply (rule cont_flift1 [THEN cont_compose])
huffman@26452
   143
apply simp
huffman@16695
   144
done
huffman@16695
   145
huffman@26452
   146
lemma cont2cont_lift_case [simp]:
huffman@25723
   147
  "\<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
   148
apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
huffman@16757
   149
apply (simp add: flift1_def cont_lift_case2)
huffman@26452
   150
apply simp
huffman@16757
   151
done
huffman@16757
   152
huffman@16757
   153
text {* rewrites for @{term flift1}, @{term flift2} *}
huffman@16757
   154
huffman@16695
   155
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
huffman@16695
   156
by (simp add: flift1_def cont_lift_case2)
huffman@16695
   157
huffman@16695
   158
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
huffman@16695
   159
by (simp add: flift2_def)
huffman@16695
   160
huffman@16695
   161
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   162
by (simp add: flift1_def cont_lift_case2)
huffman@16695
   163
huffman@16695
   164
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
huffman@16695
   165
by (simp add: flift2_def)
huffman@16695
   166
huffman@16695
   167
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
huffman@16695
   168
by (erule lift_definedE, simp)
huffman@16695
   169
huffman@19520
   170
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
huffman@19520
   171
by (cases x, simp_all)
huffman@19520
   172
slotosch@2640
   173
end