src/HOLCF/Lift.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40323 4cce7c708402
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     1 (*  Title:      HOLCF/Lift.thy
     2     Author:     Olaf Mueller
     3 *)
     4 
     5 header {* Lifting types of class type to flat pcpo's *}
     6 
     7 theory Lift
     8 imports Discrete Up
     9 begin
    10 
    11 default_sort type
    12 
    13 pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
    14 by simp_all
    15 
    16 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
    17 
    18 definition
    19   Def :: "'a \<Rightarrow> 'a lift" where
    20   "Def x = Abs_lift (up\<cdot>(Discr x))"
    21 
    22 subsection {* Lift as a datatype *}
    23 
    24 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
    25 apply (induct y)
    26 apply (rule_tac p=y in upE)
    27 apply (simp add: Abs_lift_strict)
    28 apply (case_tac x)
    29 apply (simp add: Def_def)
    30 done
    31 
    32 rep_datatype "\<bottom>\<Colon>'a lift" Def
    33   by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
    34 
    35 lemmas lift_distinct1 = lift.distinct(1)
    36 lemmas lift_distinct2 = lift.distinct(2)
    37 lemmas Def_not_UU = lift.distinct(2)
    38 lemmas Def_inject = lift.inject
    39 
    40 
    41 text {* @{term UU} and @{term Def} *}
    42 
    43 lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
    44   by (cases x) simp_all
    45 
    46 lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    47   by (cases x) simp_all
    48 
    49 text {*
    50   For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
    51   x} by @{text "Def a"} in conclusion. *}
    52 
    53 method_setup defined = {*
    54   Scan.succeed (fn ctxt => SIMPLE_METHOD'
    55     (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
    56 *} ""
    57 
    58 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
    59   by simp
    60 
    61 lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
    62   by simp
    63 
    64 lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
    65 by (simp add: below_lift_def Def_def Abs_lift_inverse)
    66 
    67 lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
    68 by (induct y, simp, simp add: Def_below_Def)
    69 
    70 
    71 subsection {* Lift is flat *}
    72 
    73 instance lift :: (type) flat
    74 proof
    75   fix x y :: "'a lift"
    76   assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
    77     by (induct x) auto
    78 qed
    79 
    80 subsection {* Continuity of @{const lift_case} *}
    81 
    82 lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
    83 apply (induct x, unfold lift.cases)
    84 apply (simp add: Rep_lift_strict)
    85 apply (simp add: Def_def Abs_lift_inverse)
    86 done
    87 
    88 lemma cont2cont_lift_case [simp]:
    89   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
    90 unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
    91 
    92 subsection {* Further operations *}
    93 
    94 definition
    95   flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
    96   "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
    97 
    98 translations
    99   "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
   100   "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
   101   "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
   102 
   103 definition
   104   flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   105   "flift2 f = (FLIFT x. Def (f x))"
   106 
   107 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)"
   108 by (simp add: flift1_def)
   109 
   110 lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)"
   111 by (simp add: flift2_def)
   112 
   113 lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>"
   114 by (simp add: flift1_def)
   115 
   116 lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>"
   117 by (simp add: flift2_def)
   118 
   119 lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
   120 by (erule lift_definedE, simp)
   121 
   122 lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
   123 by (cases x, simp_all)
   124 
   125 lemma FLIFT_mono:
   126   "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
   127 by (rule cfun_belowI, case_tac x, simp_all)
   128 
   129 lemma cont2cont_flift1 [simp, cont2cont]:
   130   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
   131 by (simp add: flift1_def cont2cont_LAM)
   132 
   133 end