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
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

old_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 ‹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
proof
  fix x y :: "'a lift"
  assume "x ⊑ y" thus "x = ⊥ ∨ x = y"
    by (induct x) auto
qed

subsection ‹Continuity of \<^const>‹case_lift››

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

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›

definition
  flift1 :: "('a ⇒ 'b::pcpo) ⇒ ('a lift → 'b)"  (binder "FLIFT " 10)  where
  "flift1 = (λf. (Λ x. case_lift ⊥ 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 ⊑ 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)

end