Theory Lift

(*  Title:      HOL/HOLCF/Lift.thy
    Author:     Olaf Müller

section ‹Lifting types of class type to flat pcpo's›

theory Lift
imports Discrete Up

default_sort type

pcpodef 'a lift = "UNIV :: 'a discr u set"
by simp_all

lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]

  Def :: "'a  'a lift" where
  "Def x = Abs_lift (up(Discr x))"

subsection ‹Lift as a datatype›

lemma lift_induct: "P ; x. P (Def x)  P y"
apply (induct y)
apply (rule_tac p=y in upE)
apply (simp add: Abs_lift_strict)
apply (case_tac x)
apply (simp add: Def_def)

old_rep_datatype "::'a lift" Def
  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)

text termbottom and termDef

lemma not_Undef_is_Def: "(x  ) = (y. x = Def y)"
  by (cases x) simp_all

lemma lift_definedE: "x  ; a. x = Def a  R  R"
  by (cases x) simp_all

text ‹
  For termx ~=  in assumptions defined› replaces x› by Def a› in conclusion.›

method_setup defined = Scan.succeed (fn ctxt => SIMPLE_METHOD'
    (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt))

lemma DefE: "Def x =   R"
  by simp

lemma DefE2: "x = Def s; x =   R"
  by simp

lemma Def_below_Def: "Def x  Def y  x = y"
by (simp add: below_lift_def Def_def Abs_lift_inverse)

lemma Def_below_iff [simp]: "Def x  y  Def x = y"
by (induct y, simp, simp add: Def_below_Def)

subsection ‹Lift is flat›

instance lift :: (type) flat
  fix x y :: "'a lift"
  assume "x  y" thus "x =   x = y"
    by (induct x) auto

subsection ‹Continuity of constcase_lift

lemma case_lift_eq: "case_lift  f x = fup(Λ y. f (undiscr y))(Rep_lift x)"
apply (induct x, unfold
apply (simp add: Rep_lift_strict)
apply (simp add: Def_def Abs_lift_inverse)

lemma cont2cont_case_lift [simp]:
  "y. cont (λx. f x y); cont g  cont (λx. case_lift  (f x) (g x))"
unfolding case_lift_eq by (simp add: cont_Rep_lift)

subsection ‹Further operations›

  flift1 :: "('a  'b::pcpo)  ('a lift  'b)"  (binder "FLIFT " 10)  where
  "flift1 = (λf. (Λ x. case_lift  f x))"

  "Λ(XCONST Def x). t" => "CONST flift1 (λx. t)"
  "Λ(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
  "Λ(CONST Def x). t" <= "FLIFT x. t"

  flift2 :: "('a  'b)  ('a lift  'b lift)" where
  "flift2 f = (FLIFT x. Def (f x))"

lemma flift1_Def [simp]: "flift1 f(Def x) = (f x)"
by (simp add: flift1_def)

lemma flift2_Def [simp]: "flift2 f(Def x) = Def (f x)"
by (simp add: flift2_def)

lemma flift1_strict [simp]: "flift1 f = "
by (simp add: flift1_def)

lemma flift2_strict [simp]: "flift2 f = "
by (simp add: flift2_def)

lemma flift2_defined [simp]: "x    (flift2 f)x  "
by (erule lift_definedE, simp)

lemma flift2_bottom_iff [simp]: "(flift2 fx = ) = (x = )"
by (cases x, simp_all)

lemma FLIFT_mono:
  "(x. f x  g x)  (FLIFT x. f x)  (FLIFT x. g x)"
by (rule cfun_belowI, case_tac x, simp_all)

lemma cont2cont_flift1 [simp, cont2cont]:
  "y. cont (λx. f x y)  cont (λx. FLIFT y. f x y)"
by (simp add: flift1_def cont2cont_LAM)