# Theory Up

Up to index of Isabelle/HOL/HOLCF

theory Up
imports Cfun
(*  Title:      HOL/HOLCF/Up.thy    Author:     Franz Regensburger    Author:     Brian Huffman*)header {* The type of lifted values *}theory Upimports Cfunbegindefault_sort cposubsection {* Definition of new type for lifting *}datatype 'a u = Ibottom | Iup 'atype_notation (xsymbols)  u  ("(_⇩⊥)" [1000] 999)primrec Ifup :: "('a -> 'b::pcpo) => 'a u => 'b" where    "Ifup f Ibottom = ⊥" |  "Ifup f (Iup x) = f·x"subsection {* Ordering on lifted cpo *}instantiation u :: (cpo) belowbegindefinition  below_up_def:    "(op \<sqsubseteq>) ≡ (λx y. case x of Ibottom => True | Iup a =>      (case y of Ibottom => False | Iup b => a \<sqsubseteq> b))"instance ..endlemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"by (simp add: below_up_def)lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"by (simp add: below_up_def)lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"by (simp add: below_up_def)subsection {* Lifted cpo is a partial order *}instance u :: (cpo) poproof  fix x :: "'a u"  show "x \<sqsubseteq> x"    unfolding below_up_def by (simp split: u.split)next  fix x y :: "'a u"  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"    unfolding below_up_def    by (auto split: u.split_asm intro: below_antisym)next  fix x y z :: "'a u"  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"    unfolding below_up_def    by (auto split: u.split_asm intro: below_trans)qedsubsection {* Lifted cpo is a cpo *}lemma is_lub_Iup:  "range S <<| x ==> range (λi. Iup (S i)) <<| Iup x"unfolding is_lub_def is_ub_def ball_simpsby (auto simp add: below_up_def split: u.split)lemma up_chain_lemma:  assumes Y: "chain Y" obtains "∀i. Y i = Ibottom"  | A k where "∀i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"proof (cases "∃k. Y k ≠ Ibottom")  case True  then obtain k where k: "Y k ≠ Ibottom" ..  def A ≡ "λi. THE a. Iup a = Y (i + k)"  have Iup_A: "∀i. Iup (A i) = Y (i + k)"  proof    fix i :: nat    from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono)    with k have "Y (i + k) ≠ Ibottom" by (cases "Y k", auto)    thus "Iup (A i) = Y (i + k)"      by (cases "Y (i + k)", simp_all add: A_def)  qed  from Y have chain_A: "chain A"    unfolding chain_def Iup_below [symmetric]    by (simp add: Iup_A)  hence "range A <<| (\<Squnion>i. A i)"    by (rule cpo_lubI)  hence "range (λi. Iup (A i)) <<| Iup (\<Squnion>i. A i)"    by (rule is_lub_Iup)  hence "range (λi. Y (i + k)) <<| Iup (\<Squnion>i. A i)"    by (simp only: Iup_A)  hence "range (λi. Y i) <<| Iup (\<Squnion>i. A i)"    by (simp only: is_lub_range_shift [OF Y])  with Iup_A chain_A show ?thesis ..next  case False  then have "∀i. Y i = Ibottom" by simp  then show ?thesis ..qedinstance u :: (cpo) cpoproof  fix S :: "nat => 'a u"  assume S: "chain S"  thus "∃x. range (λi. S i) <<| x"  proof (rule up_chain_lemma)    assume "∀i. S i = Ibottom"    hence "range (λi. S i) <<| Ibottom"      by (simp add: is_lub_const)    thus ?thesis ..  next    fix A :: "nat => 'a"    assume "range S <<| Iup (\<Squnion>i. A i)"    thus ?thesis ..  qedqedsubsection {* Lifted cpo is pointed *}instance u :: (cpo) pcpoby intro_classes fasttext {* for compatibility with old HOLCF-Version *}lemma inst_up_pcpo: "⊥ = Ibottom"by (rule minimal_up [THEN bottomI, symmetric])subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}text {* continuity for @{term Iup} *}lemma cont_Iup: "cont Iup"apply (rule contI)apply (rule is_lub_Iup)apply (erule cpo_lubI)donetext {* continuity for @{term Ifup} *}lemma cont_Ifup1: "cont (λf. Ifup f x)"by (induct x, simp_all)lemma monofun_Ifup2: "monofun (λx. Ifup f x)"apply (rule monofunI)apply (case_tac x, simp)apply (case_tac y, simp)apply (simp add: monofun_cfun_arg)donelemma cont_Ifup2: "cont (λx. Ifup f x)"proof (rule contI2)  fix Y assume Y: "chain Y" and Y': "chain (λi. Ifup f (Y i))"  from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))"  proof (rule up_chain_lemma)    fix A and k    assume A: "∀i. Iup (A i) = Y (i + k)"    assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"    hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"      by (simp add: lub_eqI contlub_cfun_arg)    also have "… = (\<Squnion>i. Ifup f (Y (i + k)))"      by (simp add: A)    also have "… = (\<Squnion>i. Ifup f (Y i))"      using Y' by (rule lub_range_shift)    finally show ?thesis by simp  qed simpqed (rule monofun_Ifup2)subsection {* Continuous versions of constants *}definition  up  :: "'a -> 'a u" where  "up = (Λ x. Iup x)"definition  fup :: "('a -> 'b::pcpo) -> 'a u -> 'b" where  "fup = (Λ f p. Ifup f p)"translations  "case l of XCONST up·x => t" == "CONST fup·(Λ x. t)·l"  "case l of (XCONST up :: 'a)·x => t" => "CONST fup·(Λ x. t)·l"  "Λ(XCONST up·x). t" == "CONST fup·(Λ x. t)"text {* continuous versions of lemmas for @{typ "('a)u"} *}lemma Exh_Up: "z = ⊥ ∨ (∃x. z = up·x)"apply (induct z)apply (simp add: inst_up_pcpo)apply (simp add: up_def cont_Iup)donelemma up_eq [simp]: "(up·x = up·y) = (x = y)"by (simp add: up_def cont_Iup)lemma up_inject: "up·x = up·y ==> x = y"by simplemma up_defined [simp]: "up·x ≠ ⊥"by (simp add: up_def cont_Iup inst_up_pcpo)lemma not_up_less_UU: "up·x \<notsqsubseteq> ⊥"by simp (* FIXME: remove? *)lemma up_below [simp]: "up·x \<sqsubseteq> up·y <-> x \<sqsubseteq> y"by (simp add: up_def cont_Iup)lemma upE [case_names bottom up, cases type: u]:  "[|p = ⊥ ==> Q; !!x. p = up·x ==> Q|] ==> Q"apply (cases p)apply (simp add: inst_up_pcpo)apply (simp add: up_def cont_Iup)donelemma up_induct [case_names bottom up, induct type: u]:  "[|P ⊥; !!x. P (up·x)|] ==> P x"by (cases x, simp_all)text {* lifting preserves chain-finiteness *}lemma up_chain_cases:  assumes Y: "chain Y" obtains "∀i. Y i = ⊥"  | A k where "∀i. up·(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up·(\<Squnion>i. A i)"apply (rule up_chain_lemma [OF Y])apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)donelemma compact_up: "compact x ==> compact (up·x)"apply (rule compactI2)apply (erule up_chain_cases)apply simpapply (drule (1) compactD2, simp)apply (erule exE)apply (drule_tac f="up" and x="x" in monofun_cfun_arg)apply (simp, erule exI)donelemma compact_upD: "compact (up·x) ==> compact x"unfolding compact_defby (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)lemma compact_up_iff [simp]: "compact (up·x) = compact x"by (safe elim!: compact_up compact_upD)instance u :: (chfin) chfinapply intro_classesapply (erule compact_imp_max_in_chain)apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)donetext {* properties of fup *}lemma fup1 [simp]: "fup·f·⊥ = ⊥"by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)lemma fup2 [simp]: "fup·f·(up·x) = f·x"by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)lemma fup3 [simp]: "fup·up·x = x"by (cases x, simp_all)end