src/HOLCF/Lift.thy
changeset 12026 0b1d80ada4ab
parent 2640 ee4dfce170a0
child 12338 de0f4a63baa5
     1.1 --- a/src/HOLCF/Lift.thy	Sat Nov 03 01:36:19 2001 +0100
     1.2 +++ b/src/HOLCF/Lift.thy	Sat Nov 03 01:38:11 2001 +0100
     1.3 @@ -1,16 +1,339 @@
     1.4  (*  Title:      HOLCF/Lift.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Oscar Slotosch
     1.7 -    Copyright   1997 Technische Universitaet Muenchen
     1.8 +    Author:     Olaf Mueller
     1.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  *)
    1.11  
    1.12 -Lift = Lift3 + 
    1.13 +header {* Lifting types of class term to flat pcpo's *}
    1.14 +
    1.15 +theory Lift = Cprod3:
    1.16 +
    1.17 +defaultsort "term"
    1.18 +
    1.19 +
    1.20 +typedef 'a lift = "UNIV :: 'a option set" ..
    1.21 +
    1.22 +constdefs
    1.23 +  Undef :: "'a lift"
    1.24 +  "Undef == Abs_lift None"
    1.25 +  Def :: "'a => 'a lift"
    1.26 +  "Def x == Abs_lift (Some x)"
    1.27 +
    1.28 +instance lift :: ("term") sq_ord ..
    1.29 +
    1.30 +defs (overloaded)
    1.31 +  less_lift_def: "x << y == (x=y | x=Undef)"
    1.32 +
    1.33 +instance lift :: ("term") po
    1.34 +proof
    1.35 +  fix x y z :: "'a lift"
    1.36 +  show "x << x" by (unfold less_lift_def) blast
    1.37 +  { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast }
    1.38 +  { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast }
    1.39 +qed
    1.40 +
    1.41 +lemma inst_lift_po: "(op <<) = (\<lambda>x y. x = y | x = Undef)"
    1.42 +  -- {* For compatibility with old HOLCF-Version. *}
    1.43 +  by (simp only: less_lift_def [symmetric])
    1.44 +
    1.45 +
    1.46 +subsection {* Type lift is pointed *}
    1.47 +
    1.48 +lemma minimal_lift [iff]: "Undef << x"
    1.49 +  by (simp add: inst_lift_po)
    1.50 +
    1.51 +lemma UU_lift_def: "(SOME u. \<forall>y. u \<sqsubseteq> y) = Undef"
    1.52 +  apply (rule minimal2UU [symmetric])
    1.53 +  apply (rule minimal_lift)
    1.54 +  done
    1.55 +
    1.56 +lemma least_lift: "EX x::'a lift. ALL y. x << y"
    1.57 +  apply (rule_tac x = Undef in exI)
    1.58 +  apply (rule minimal_lift [THEN allI])
    1.59 +  done
    1.60 +
    1.61 +
    1.62 +subsection {* Type lift is a cpo *}
    1.63 +
    1.64 +text {*
    1.65 +  The following lemmas have already been proved in @{text Pcpo.ML} and
    1.66 +  @{text Fix.ML}, but there class @{text pcpo} is assumed, although
    1.67 +  only @{text po} is necessary and a least element. Therefore they are
    1.68 +  redone here for the @{text po} lift with least element @{text
    1.69 +  Undef}.
    1.70 +*}
    1.71 +
    1.72 +lemma notUndef_I: "[| x<<y; x ~= Undef |] ==> y ~= Undef"
    1.73 +  -- {* Tailoring @{text notUU_I} of @{text Pcpo.ML} to @{text Undef} *}
    1.74 +  by (blast intro: antisym_less)
    1.75 +
    1.76 +lemma chain_mono2_po: "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |]
    1.77 +         ==> EX j. ALL i. j<i-->~Y(i)=Undef"
    1.78 +  -- {* Tailoring @{text chain_mono2} of @{text Pcpo.ML} to @{text Undef} *}
    1.79 +  apply safe
    1.80 +  apply (rule exI)
    1.81 +  apply (intro strip)
    1.82 +  apply (rule notUndef_I)
    1.83 +   apply (erule (1) chain_mono)
    1.84 +  apply assumption
    1.85 +  done
    1.86 +
    1.87 +lemma flat_imp_chfin_poo: "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))"
    1.88 +  -- {* Tailoring @{text flat_imp_chfin} of @{text Fix.ML} to @{text lift} *}
    1.89 +  apply (unfold max_in_chain_def)
    1.90 +  apply (intro strip)
    1.91 +  apply (rule_tac P = "ALL i. Y (i) = Undef" in case_split)
    1.92 +   apply (rule_tac x = 0 in exI)
    1.93 +   apply (intro strip)
    1.94 +   apply (rule trans)
    1.95 +    apply (erule spec)
    1.96 +   apply (rule sym)
    1.97 +   apply (erule spec)
    1.98 +  apply (subgoal_tac "ALL x y. x << (y:: ('a) lift) --> x=Undef | x=y")
    1.99 +   prefer 2 apply (simp add: inst_lift_po)
   1.100 +  apply (rule chain_mono2_po [THEN exE])
   1.101 +    apply fast
   1.102 +   apply assumption
   1.103 +  apply (rule_tac x = "Suc x" in exI)
   1.104 +  apply (intro strip)
   1.105 +  apply (rule disjE)
   1.106 +    prefer 3 apply assumption
   1.107 +   apply (rule mp)
   1.108 +    apply (drule spec)
   1.109 +    apply (erule spec)
   1.110 +   apply (erule le_imp_less_or_eq [THEN disjE])
   1.111 +    apply (erule chain_mono)
   1.112 +    apply auto
   1.113 +  done
   1.114 +
   1.115 +theorem cpo_lift: "chain (Y::nat => 'a lift) ==> EX x. range Y <<| x"
   1.116 +  apply (cut_tac flat_imp_chfin_poo)
   1.117 +  apply (blast intro: lub_finch1)
   1.118 +  done
   1.119 +
   1.120 +instance lift :: ("term") pcpo
   1.121 +  apply intro_classes
   1.122 +   apply (erule cpo_lift)
   1.123 +  apply (rule least_lift)
   1.124 +  done
   1.125 +
   1.126 +lemma inst_lift_pcpo: "UU = Undef"
   1.127 +  -- {* For compatibility with old HOLCF-Version. *}
   1.128 +  by (simp add: UU_def UU_lift_def)
   1.129 +
   1.130 +
   1.131 +subsection {* Lift as a datatype *}
   1.132 +
   1.133 +lemma lift_distinct1: "UU ~= Def x"
   1.134 +  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
   1.135 +
   1.136 +lemma lift_distinct2: "Def x ~= UU"
   1.137 +  by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo)
   1.138 +
   1.139 +lemma Def_inject: "(Def x = Def x') = (x = x')"
   1.140 +  by (simp add: Def_def Abs_lift_inject lift_def)
   1.141 +
   1.142 +lemma lift_induct: "P UU ==> (!!x. P (Def x)) ==> P y"
   1.143 +  apply (induct y)
   1.144 +  apply (induct_tac y)
   1.145 +   apply (simp_all add: Undef_def Def_def inst_lift_pcpo)
   1.146 +  done
   1.147 +
   1.148 +rep_datatype lift
   1.149 +  distinct lift_distinct1 lift_distinct2
   1.150 +  inject Def_inject
   1.151 +  induction lift_induct
   1.152 +
   1.153 +lemma Def_not_UU: "Def a ~= UU"
   1.154 +  by simp
   1.155 +
   1.156 +
   1.157 +subsection {* Further operations *}
   1.158 +
   1.159 +consts
   1.160 + flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
   1.161 + flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
   1.162 + liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
   1.163  
   1.164 -instance lift :: (term)flat (ax_flat_lift)
   1.165 +defs
   1.166 + flift1_def:
   1.167 +  "flift1 f == (LAM x. (case x of
   1.168 +                   UU => UU
   1.169 +                 | Def y => (f y)))"
   1.170 + flift2_def:
   1.171 +  "flift2 f == (LAM x. (case x of
   1.172 +                   UU => UU
   1.173 +                 | Def y => Def (f y)))"
   1.174 + liftpair_def:
   1.175 +  "liftpair x  == (case (cfst$x) of
   1.176 +                  UU  => UU
   1.177 +                | Def x1 => (case (csnd$x) of
   1.178 +                               UU => UU
   1.179 +                             | Def x2 => Def (x1,x2)))"
   1.180 +
   1.181 +
   1.182 +declare inst_lift_pcpo [symmetric, simp]
   1.183 +
   1.184 +
   1.185 +lemma less_lift: "(x::'a lift) << y = (x=y | x=UU)"
   1.186 +  by (simp add: inst_lift_po)
   1.187 +
   1.188 +
   1.189 +text {* @{text UU} and @{text Def} *}
   1.190 +
   1.191 +lemma Lift_exhaust: "x = UU | (EX y. x = Def y)"
   1.192 +  by (induct x) simp_all
   1.193 +
   1.194 +lemma Lift_cases: "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"
   1.195 +  by (insert Lift_exhaust) blast
   1.196 +
   1.197 +lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)"
   1.198 +  by (cases x) simp_all
   1.199 +
   1.200 +text {*
   1.201 +  For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
   1.202 +  x} by @{text "Def a"} in conclusion. *}
   1.203 +
   1.204 +ML {*
   1.205 +  local val not_Undef_is_Def = thm "not_Undef_is_Def"
   1.206 +  in val def_tac = SIMPSET' (fn ss =>
   1.207 +    etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
   1.208 +  end;
   1.209 +*}
   1.210 +
   1.211 +lemma Undef_eq_UU: "Undef = UU"
   1.212 +  by (rule inst_lift_pcpo [symmetric])
   1.213 +
   1.214 +lemma DefE: "Def x = UU ==> R"
   1.215 +  by simp
   1.216 +
   1.217 +lemma DefE2: "[| x = Def s; x = UU |] ==> R"
   1.218 +  by simp
   1.219 +
   1.220 +lemma Def_inject_less_eq: "Def x << Def y = (x = y)"
   1.221 +  by (simp add: less_lift_def)
   1.222 +
   1.223 +lemma Def_less_is_eq [simp]: "Def x << y = (Def x = y)"
   1.224 +  by (simp add: less_lift)
   1.225 +
   1.226 +
   1.227 +subsection {* Lift is flat *}
   1.228 +
   1.229 +instance lift :: ("term") flat
   1.230 +proof
   1.231 +  show "ALL x y::'a lift. x << y --> x = UU | x = y"
   1.232 +    by (simp add: less_lift)
   1.233 +qed
   1.234 +
   1.235 +defaultsort pcpo
   1.236 +
   1.237 +
   1.238 +text {*
   1.239 +  \medskip Two specific lemmas for the combination of LCF and HOL
   1.240 +  terms.
   1.241 +*}
   1.242 +
   1.243 +lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"
   1.244 +  apply (rule cont2cont_CF1L)
   1.245 +  apply (tactic "resolve_tac cont_lemmas1 1")+
   1.246 +   apply auto
   1.247 +  done
   1.248 +
   1.249 +lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"
   1.250 +  apply (rule cont2cont_CF1L)
   1.251 +  apply (erule cont_Rep_CFun_app)
   1.252 +  apply assumption
   1.253 +  done
   1.254  
   1.255 -default pcpo
   1.256 +text {* Continuity of if-then-else. *}
   1.257 +
   1.258 +lemma cont_if: "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)"
   1.259 +  by (cases b) simp_all
   1.260 +
   1.261 +
   1.262 +subsection {* Continuity Proofs for flift1, flift2, if *}
   1.263 +
   1.264 +text {* Need the instance of @{text flat}. *}
   1.265 +
   1.266 +lemma cont_flift1_arg: "cont (lift_case UU f)"
   1.267 +  -- {* @{text flift1} is continuous in its argument itself. *}
   1.268 +  apply (rule flatdom_strict2cont)
   1.269 +  apply simp
   1.270 +  done
   1.271 +
   1.272 +lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==>
   1.273 +           cont (%y. lift_case UU (f y))"
   1.274 +  -- {* @{text flift1} is continuous in a variable that occurs only
   1.275 +    in the @{text Def} branch. *}
   1.276 +  apply (rule cont2cont_CF1L_rev)
   1.277 +  apply (intro strip)
   1.278 +  apply (case_tac y)
   1.279 +   apply simp
   1.280 +  apply simp
   1.281 +  done
   1.282 +
   1.283 +lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==>
   1.284 +    cont (%y. lift_case UU (f y) (g y))"
   1.285 +  -- {* @{text flift1} is continuous in a variable that occurs either
   1.286 +    in the @{text Def} branch or in the argument. *}
   1.287 +  apply (rule_tac tt = g in cont2cont_app)
   1.288 +    apply (rule cont_flift1_not_arg)
   1.289 +    apply auto
   1.290 +  apply (rule cont_flift1_arg)
   1.291 +  done
   1.292 +
   1.293 +lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))"
   1.294 +  -- {* @{text flift2} is continuous in its argument itself. *}
   1.295 +  apply (rule flatdom_strict2cont)
   1.296 +  apply simp
   1.297 +  done
   1.298 +
   1.299 +text {*
   1.300 +  \medskip Extension of cont_tac and installation of simplifier.
   1.301 +*}
   1.302 +
   1.303 +lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1"
   1.304 +  apply (rule cont2cont_CF1L_rev)
   1.305 +  apply simp
   1.306 +  done
   1.307 +
   1.308 +lemmas cont_lemmas_ext [simp] =
   1.309 +  cont_flift1_arg cont_flift2_arg
   1.310 +  cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2
   1.311 +  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
   1.312 +
   1.313 +ML_setup {*
   1.314 +val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
   1.315 +
   1.316 +fun cont_tac  i = resolve_tac cont_lemmas2 i;
   1.317 +fun cont_tacR i = REPEAT (cont_tac i);
   1.318 +
   1.319 +local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def"
   1.320 +in fun cont_tacRs i =
   1.321 +  simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN
   1.322 +  REPEAT (cont_tac i)
   1.323 +end;
   1.324 +
   1.325 +simpset_ref() := simpset() addSolver
   1.326 +  (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
   1.327 +*}
   1.328 +
   1.329 +
   1.330 +subsection {* flift1, flift2 *}
   1.331 +
   1.332 +lemma flift1_Def [simp]: "flift1 f$(Def x) = (f x)"
   1.333 +  by (simp add: flift1_def)
   1.334 +
   1.335 +lemma flift2_Def [simp]: "flift2 f$(Def x) = Def (f x)"
   1.336 +  by (simp add: flift2_def)
   1.337 +
   1.338 +lemma flift1_UU [simp]: "flift1 f$UU = UU"
   1.339 +  by (simp add: flift1_def)
   1.340 +
   1.341 +lemma flift2_UU [simp]: "flift2 f$UU = UU"
   1.342 +  by (simp add: flift2_def)
   1.343 +
   1.344 +lemma flift2_nUU [simp]: "x~=UU ==> (flift2 f)$x~=UU"
   1.345 +  by (tactic "def_tac 1")
   1.346  
   1.347  end
   1.348 -
   1.349 -
   1.350 -