Quelle  Lift.thy   Sprache: Isabelle

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

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

theory Lift
imports Up
begin

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

lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]

definition
  Def :: "'a::type \ '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::type lift" Def
  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)

text ‹🍋‹bottom› and 🍋‹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 🍋‹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 🍋‹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::type \ '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::type \ 'b::type) \ ('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