Lift.thy   Interaktion und
PortierbarkeitIsabelle

(*  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 ‹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::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