Theory Lift

Up to index of Isabelle/HOLCF

theory Lift
imports Discrete Up Cprod
uses [Lift.ML]
begin

(*  Title:      HOLCF/Lift.thy
    ID:         $Id: Lift.thy,v 1.22 2005/09/23 20:21:52 wenzelm Exp $
    Author:     Olaf Mueller
*)

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

theory Lift
imports Discrete Up Cprod
begin

defaultsort type

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

lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]

constdefs
  Def :: "'a => 'a lift"
  "Def x ≡ Abs_lift (up·(Discr x))"

subsection {* Lift as a datatype *}

lemma lift_distinct1: "⊥ ≠ Def x"
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)

lemma lift_distinct2: "Def x ≠ ⊥"
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)

lemma Def_inject: "(Def x = Def y) = (x = y)"
by (simp add: Def_def Abs_lift_inject lift_def)

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 lift
  distinct lift_distinct1 lift_distinct2
  inject Def_inject
  induction lift_induct

lemma Def_not_UU: "Def a ≠ UU"
  by simp


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

lemma Lift_exhaust: "x = ⊥ ∨ (∃y. x = Def y)"
  by (induct x) simp_all

lemma Lift_cases: "[|x = ⊥ ==> P; ∃a. x = Def a ==> P|] ==> P"
  by (insert Lift_exhaust) blast

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

ML {*
  local val lift_definedE = thm "lift_definedE"
  in val def_tac = SIMPSET' (fn ss =>
    etac lift_definedE THEN' asm_simp_tac ss)
  end;
*}

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

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

lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y = (x = y)"
by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)

lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
apply (induct y)
apply (simp add: eq_UU_iff)
apply (simp add: Def_inject_less_eq)
done


subsection {* Lift is flat *}

lemma less_lift: "(x::'a lift) \<sqsubseteq> y = (x = y ∨ x = ⊥)"
by (induct x, simp_all)

instance lift :: (type) flat
by (intro_classes, simp add: less_lift)

text {*
  \medskip Two specific lemmas for the combination of LCF and HOL
  terms.
*}

lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(λx. ((f x)·(g x)) s)"
by (rule cont2cont_Rep_CFun [THEN cont2cont_CF1L])

lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(λx. ((f x)·(g x)) s t)"
by (rule cont_Rep_CFun_app [THEN cont2cont_CF1L])

subsection {* Further operations *}

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

  flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
  "flift2 f ≡ FLIFT x. Def (f x)"

  liftpair :: "'a lift × 'b lift => ('a × 'b) lift"
  "liftpair x ≡ csplit·(FLIFT x y. Def (x, y))·x"

subsection {* Continuity Proofs for flift1, flift2 *}

text {* Need the instance of @{text flat}. *}

lemma cont_lift_case1: "cont (λf. lift_case a f x)"
apply (induct x)
apply simp
apply simp
apply (rule cont_id [THEN cont2cont_CF1L])
done

lemma cont_lift_case2: "cont (λx. lift_case ⊥ f x)"
apply (rule flatdom_strict2cont)
apply simp
done

lemma cont_flift1: "cont flift1"
apply (unfold flift1_def)
apply (rule cont2cont_LAM)
apply (rule cont_lift_case2)
apply (rule cont_lift_case1)
done

lemma cont2cont_flift1:
  "[|!!y. cont (λx. f x y)|] ==> cont (λx. FLIFT y. f x y)"
apply (rule cont_flift1 [THEN cont2cont_app3])
apply (simp add: cont2cont_lambda)
done

lemma cont2cont_lift_case:
  "[|!!y. cont (λx. f x y); cont g|] ==> cont (λx. lift_case UU (f x) (g x))"
apply (subgoal_tac "cont (λx. (FLIFT y. f x y)·(g x))")
apply (simp add: flift1_def cont_lift_case2)
apply (simp add: cont2cont_flift1)
done

text {* rewrites for @{term flift1}, @{term flift2} *}

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

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

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

lemma flift2_defined [simp]: "x ≠ ⊥ ==> (flift2 f)·x ≠ ⊥"
by (erule lift_definedE, simp)

text {*
  \medskip Extension of @{text cont_tac} and installation of simplifier.
*}

lemmas cont_lemmas_ext [simp] =
  cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
  cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if

ML {*
val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";

fun cont_tac  i = resolve_tac cont_lemmas2 i;
fun cont_tacR i = REPEAT (cont_tac i);

local val flift1_def = thm "flift1_def"
in fun cont_tacRs ss i =
  simp_tac ss i THEN
  REPEAT (cont_tac i)
end;
*}

end

lemmas inst_lift_pcpo:

  UU = Abs_lift UU

lemmas inst_lift_pcpo:

  UU = Abs_lift UU

Lift as a datatype

lemma lift_distinct1:

  UU ≠ Def x

lemma lift_distinct2:

  Def x ≠ UU

lemma Def_inject:

  (Def x = Def y) = (x = y)

lemma lift_induct:

  [| P UU; !!x. P (Def x) |] ==> P y

lemma Def_not_UU:

  Def a ≠ UU

lemma Lift_exhaust:

  x = UU ∨ (∃y. x = Def y)

lemma Lift_cases:

  [| x = UU ==> P; ∃a. x = Def a ==> P |] ==> P

lemma not_Undef_is_Def:

  (x ≠ UU) = (∃y. x = Def y)

lemma lift_definedE:

  [| x ≠ UU; !!a. x = Def a ==> R |] ==> R

lemma DefE:

  Def x = UU ==> R

lemma DefE2:

  [| x = Def s; x = UU |] ==> R

lemma Def_inject_less_eq:

  Def x << Def y = (x = y)

lemma Def_less_is_eq:

  Def x << y = (Def x = y)

Lift is flat

lemma less_lift:

  x << y = (x = yx = UU)

lemma cont_Rep_CFun_app:

  [| cont g; cont f |] ==> cont (%x. (f x·(g x)) s)

lemma cont_Rep_CFun_app_app:

  [| cont g; cont f |] ==> cont (%x. (f x·(g x)) s t)

Further operations

Continuity Proofs for flift1, flift2

lemma cont_lift_case1:

  cont (%f. lift_case a f x)

lemma cont_lift_case2:

  cont (lift_case UU f)

lemma cont_flift1:

  cont flift1

lemma cont2cont_flift1:

  (!!y. cont (%x. f x y)) ==> cont (%x. FLIFT y. f x y)

lemma cont2cont_lift_case:

  [| !!y. cont (%x. f x y); cont g |] ==> cont (%x. lift_case UU (f x) (g x))

lemma flift1_Def:

  flift1 f·(Def x) = f x

lemma flift2_Def:

  flift2 f·(Def x) = Def (f x)

lemma flift1_strict:

  flift1 f·UU = UU

lemma flift2_strict:

  flift2 f·UU = UU

lemma flift2_defined:

  x ≠ UU ==> flift2 f·x ≠ UU

lemmas cont_lemmas_ext:

  (!!y. cont (%x. f x y)) ==> cont (%x. FLIFT y. f x y)
  [| !!y. cont (%x. f x y); cont g |] ==> cont (%x. lift_case UU (f x) (g x))
  (!!y. cont (%x. f x y)) ==> cont f
  [| cont g; cont f |] ==> cont (%x. (f x·(g x)) s)
  [| cont g; cont f |] ==> cont (%x. (f x·(g x)) s t)
  [| cont f; cont g |] ==> cont (%x. if b then f x else g x)

lemmas cont_lemmas_ext:

  (!!y. cont (%x. f x y)) ==> cont (%x. FLIFT y. f x y)
  [| !!y. cont (%x. f x y); cont g |] ==> cont (%x. lift_case UU (f x) (g x))
  (!!y. cont (%x. f x y)) ==> cont f
  [| cont g; cont f |] ==> cont (%x. (f x·(g x)) s)
  [| cont g; cont f |] ==> cont (%x. (f x·(g x)) s t)
  [| cont f; cont g |] ==> cont (%x. if b then f x else g x)