Theory Lift

(*  Title:      HOL/HOLCF/Lift.thy
    Author:     Olaf Mueller
*)

header {* Lifting types of class type to flat pcpo's *}

theory Lift
imports Discrete Up
begin

default_sort type

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

lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]

definition
  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)
done

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

text {* @{term bottom} and @{term Def} *}

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 @{term "x ~= ⊥"} in assumptions @{text defined} replaces @{text
  x} by @{text "Def a"} in conclusion. *}

method_setup defined = {*
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
    (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
*}

lemma DefE: "Def x = ⊥ ==> R"
  by simp

lemma DefE2: "[|x = Def s; x = ⊥|] ==> R"
  by simp

lemma Def_below_Def: "Def x \<sqsubseteq> Def y <-> x = y"
by (simp add: below_lift_def Def_def Abs_lift_inverse)

lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y <-> Def x = y"
by (induct y, simp, simp add: Def_below_Def)


subsection {* Lift is flat *}

instance lift :: (type) flat
proof
  fix x y :: "'a lift"
  assume "x \<sqsubseteq> y" thus "x = ⊥ ∨ x = y"
    by (induct x) auto
qed

subsection {* Continuity of @{const lift_case} *}

lemma lift_case_eq: "lift_case ⊥ f x = fup·(Λ y. f (undiscr y))·(Rep_lift x)"
apply (induct x, unfold lift.cases)
apply (simp add: Rep_lift_strict)
apply (simp add: Def_def Abs_lift_inverse)
done

lemma cont2cont_lift_case [simp]:
  "[|!!y. cont (λx. f x y); cont g|] ==> cont (λx. lift_case ⊥ (f x) (g x))"
unfolding lift_case_eq by (simp add: cont_Rep_lift)

subsection {* Further operations *}

definition
  flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"  (binder "FLIFT " 10)  where
  "flift1 = (λf. (Λ x. lift_case ⊥ f x))"

translations
  "Λ(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"

definition
  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 f·x = ⊥) = (x = ⊥)"
by (cases x, simp_all)

lemma FLIFT_mono:
  "(!!x. f x \<sqsubseteq> g x) ==> (FLIFT x. f x) \<sqsubseteq> (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)

end