# 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 = y ∨ x = 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)