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