(* Title: HOLCF/Up.thy ID: $Id: Up.thy,v 1.12 2005/09/22 17:06:06 huffman Exp $ Author: Franz Regensburger and Brian Huffman Lifting. *) header {* The type of lifted values *} theory Up imports Cfun Sum_Type Datatype begin defaultsort cpo subsection {* Definition of new type for lifting *} datatype 'a u = Ibottom | Iup 'a consts Ifup :: "('a -> 'b::pcpo) => 'a u => 'b" primrec "Ifup f Ibottom = ⊥" "Ifup f (Iup x) = f·x" subsection {* Ordering on type @{typ "'a u"} *} instance u :: (sq_ord) sq_ord .. defs (overloaded) less_up_def: "(op \<sqsubseteq>) ≡ (λx y. case x of Ibottom => True | Iup a => (case y of Ibottom => False | Iup b => a \<sqsubseteq> b))" lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" by (simp add: less_up_def) lemma not_Iup_less [iff]: "¬ Iup x \<sqsubseteq> Ibottom" by (simp add: less_up_def) lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)" by (simp add: less_up_def) subsection {* Type @{typ "'a u"} is a partial order *} lemma refl_less_up: "(x::'a u) \<sqsubseteq> x" by (simp add: less_up_def split: u.split) lemma antisym_less_up: "[|(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> x|] ==> x = y" apply (simp add: less_up_def split: u.split_asm) apply (erule (1) antisym_less) done lemma trans_less_up: "[|(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> z|] ==> x \<sqsubseteq> z" apply (simp add: less_up_def split: u.split_asm) apply (erule (1) trans_less) done instance u :: (cpo) po by intro_classes (assumption | rule refl_less_up antisym_less_up trans_less_up)+ subsection {* Type @{typ "'a u"} is a cpo *} lemma is_lub_Iup: "range S <<| x ==> range (λi. Iup (S i)) <<| Iup x" apply (rule is_lubI) apply (rule ub_rangeI) apply (subst Iup_less) apply (erule is_ub_lub) apply (case_tac u) apply (drule ub_rangeD) apply simp apply simp apply (erule is_lub_lub) apply (rule ub_rangeI) apply (drule_tac i=i in ub_rangeD) apply simp done text {* Now some lemmas about chains of @{typ "'a u"} elements *} lemma up_lemma1: "z ≠ Ibottom ==> Iup (THE a. Iup a = z) = z" by (case_tac z, simp_all) lemma up_lemma2: "[|chain Y; Y j ≠ Ibottom|] ==> Y (i + j) ≠ Ibottom" apply (erule contrapos_nn) apply (drule_tac x="j" and y="i + j" in chain_mono3) apply (rule le_add2) apply (case_tac "Y j") apply assumption apply simp done lemma up_lemma3: "[|chain Y; Y j ≠ Ibottom|] ==> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)" by (rule up_lemma1 [OF up_lemma2]) lemma up_lemma4: "[|chain Y; Y j ≠ Ibottom|] ==> chain (λi. THE a. Iup a = Y (i + j))" apply (rule chainI) apply (rule Iup_less [THEN iffD1]) apply (subst up_lemma3, assumption+)+ apply (simp add: chainE) done lemma up_lemma5: "[|chain Y; Y j ≠ Ibottom|] ==> (λi. Y (i + j)) = (λi. Iup (THE a. Iup a = Y (i + j)))" by (rule ext, rule up_lemma3 [symmetric]) lemma up_lemma6: "[|chain Y; Y j ≠ Ibottom|] ==> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))" apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1]) apply assumption apply (subst up_lemma5, assumption+) apply (rule is_lub_Iup) apply (rule thelubE [OF _ refl]) apply (erule (1) up_lemma4) done lemma up_chain_cases: "chain Y ==> (∃A. chain A ∧ lub (range Y) = Iup (lub (range A)) ∧ (∃j. ∀i. Y (i + j) = Iup (A i))) ∨ (Y = (λi. Ibottom))" apply (rule disjCI) apply (simp add: expand_fun_eq) apply (erule exE, rename_tac j) apply (rule_tac x="λi. THE a. Iup a = Y (i + j)" in exI) apply (simp add: up_lemma4) apply (simp add: up_lemma6 [THEN thelubI]) apply (rule_tac x=j in exI) apply (simp add: up_lemma3) done lemma cpo_up: "chain (Y::nat => 'a u) ==> ∃x. range Y <<| x" apply (frule up_chain_cases, safe) apply (rule_tac x="Iup (lub (range A))" in exI) apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1]) apply (simp add: is_lub_Iup thelubE) apply (rule exI, rule lub_const) done instance u :: (cpo) cpo by intro_classes (rule cpo_up) subsection {* Type @{typ "'a u"} is pointed *} lemma least_up: "∃x::'a u. ∀y. x \<sqsubseteq> y" apply (rule_tac x = "Ibottom" in exI) apply (rule minimal_up [THEN allI]) done instance u :: (cpo) pcpo by intro_classes (rule least_up) text {* for compatibility with old HOLCF-Version *} lemma inst_up_pcpo: "⊥ = Ibottom" by (rule minimal_up [THEN UU_I, symmetric]) subsection {* Continuity of @{term Iup} and @{term Ifup} *} text {* continuity for @{term Iup} *} lemma cont_Iup: "cont Iup" apply (rule contI) apply (rule is_lub_Iup) apply (erule thelubE [OF _ refl]) done text {* 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) done lemma cont_Ifup2: "cont (λx. Ifup f x)" apply (rule contI) apply (frule up_chain_cases, safe) apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1]) apply (erule monofun_Ifup2 [THEN ch2ch_monofun]) apply (simp add: cont_cfun_arg) apply (simp add: thelub_const lub_const) done subsection {* Continuous versions of constants *} constdefs up :: "'a -> 'a u" "up ≡ Λ x. Iup x" fup :: "('a -> 'b::pcpo) -> 'a u -> 'b" "fup ≡ Λ f p. Ifup f p" translations "case l of up·x => t" == "fup·(LAM x. t)·l" 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) done lemma 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 simp lemma up_defined [simp]: " up·x ≠ ⊥" by (simp add: up_def cont_Iup inst_up_pcpo) lemma not_up_less_UU [simp]: "¬ up·x \<sqsubseteq> ⊥" by (simp add: eq_UU_iff [symmetric]) lemma up_less [simp]: "(up·x \<sqsubseteq> up·y) = (x \<sqsubseteq> y)" by (simp add: up_def cont_Iup) lemma upE: "[|p = ⊥ ==> Q; !!x. p = up·x ==> Q|] ==> Q" apply (case_tac p) apply (simp add: inst_up_pcpo) apply (simp add: up_def cont_Iup) done lemma fup1 [simp]: "fup·f·⊥ = ⊥" by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo) lemma fup2 [simp]: "fup·f·(up·x) = f·x" by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2) lemma fup3 [simp]: "fup·up·x = x" by (rule_tac p=x in upE, simp_all) end
lemma minimal_up:
Ibottom << z
lemma not_Iup_less:
¬ Iup x << Ibottom
lemma Iup_less:
Iup x << Iup y = x << y
lemma refl_less_up:
x << x
lemma antisym_less_up:
[| x << y; y << x |] ==> x = y
lemma trans_less_up:
[| x << y; y << z |] ==> x << z
lemma is_lub_Iup:
range S <<| x ==> range (%i. Iup (S i)) <<| Iup x
lemma up_lemma1:
z ≠ Ibottom ==> Iup (THE a. Iup a = z) = z
lemma up_lemma2:
[| chain Y; Y j ≠ Ibottom |] ==> Y (i + j) ≠ Ibottom
lemma up_lemma3:
[| chain Y; Y j ≠ Ibottom |] ==> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)
lemma up_lemma4:
[| chain Y; Y j ≠ Ibottom |] ==> chain (%i. THE a. Iup a = Y (i + j))
lemma up_lemma5:
[| chain Y; Y j ≠ Ibottom |] ==> (%i. Y (i + j)) = (%i. Iup (THE a. Iup a = Y (i + j)))
lemma up_lemma6:
[| chain Y; Y j ≠ Ibottom |] ==> range Y <<| Iup (LUB i. THE a. Iup a = Y (i + j))
lemma up_chain_cases:
chain Y ==> (∃A. chain A ∧ lub (range Y) = Iup (lub (range A)) ∧ (∃j. ∀i. Y (i + j) = Iup (A i))) ∨ Y = (%i. Ibottom)
lemma cpo_up:
chain Y ==> ∃x. range Y <<| x
lemma least_up:
∃x. ∀y. x << y
lemma inst_up_pcpo:
UU = Ibottom
lemma cont_Iup:
cont Iup
lemma cont_Ifup1:
cont (%f. Ifup f x)
lemma monofun_Ifup2:
monofun (Ifup f)
lemma cont_Ifup2:
cont (Ifup f)
lemma Exh_Up:
z = UU ∨ (∃x. z = up·x)
lemma up_eq:
(up·x = up·y) = (x = y)
lemma up_inject:
up·x = up·y ==> x = y
lemma up_defined:
up·x ≠ UU
lemma not_up_less_UU:
¬ up·x << UU
lemma up_less:
up·x << up·y = x << y
lemma upE:
[| p = UU ==> Q; !!x. p = up·x ==> Q |] ==> Q
lemma fup1:
fup·f·UU = UU
lemma fup2:
fup·f·(up·x) = f·x
lemma fup3:
fup·up·x = x