# Theory Ssum

Up to index of Isabelle/HOLCF

theory Ssum
imports Cprod
uses [Ssum.ML]
begin

    (*  Title:      HOLCF/Ssum.thy
        ID:         $Id: Ssum.thy,v 1.15 2005/07/26 16:28:11 huffman Exp $
        Author:     Franz Regensburger and Brian Huffman

    Strict sum with typedef.
    *)

    header {* The type of strict sums *}

    theory Ssum
    imports Cprod
    begin

    defaultsort pcpo

    subsection {* Definition of strict sum type *}

    pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) =
            "{p::'a × 'b. cfst·p = ⊥ ∨ csnd·p = ⊥}"
    by simp

    syntax (xsymbols)
      "++"          :: "[type, type] => type"       ("(_ ⊕/ _)" [21, 20] 20)
    syntax (HTML output)
      "++"          :: "[type, type] => type"       ("(_ ⊕/ _)" [21, 20] 20)

    subsection {* Definitions of constructors *}

    constdefs
      sinl :: "'a -> ('a ++ 'b)"
      "sinl ≡ Λ a. Abs_Ssum <a, ⊥>"

      sinr :: "'b -> ('a ++ 'b)"
      "sinr ≡ Λ b. Abs_Ssum <⊥, b>"

    subsection {* Properties of @{term sinl} and @{term sinr} *}

    lemma sinl_Abs_Ssum: "sinl·a = Abs_Ssum <a, ⊥>"
    by (unfold sinl_def, simp add: cont_Abs_Ssum Ssum_def)

    lemma sinr_Abs_Ssum: "sinr·b = Abs_Ssum <⊥, b>"
    by (unfold sinr_def, simp add: cont_Abs_Ssum Ssum_def)

    lemma Rep_Ssum_sinl: "Rep_Ssum (sinl·a) = <a, ⊥>"
    by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)

    lemma Rep_Ssum_sinr: "Rep_Ssum (sinr·b) = <⊥, b>"
    by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)

    lemma sinl_strict [simp]: "sinl·⊥ = ⊥"
    by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)

    lemma sinr_strict [simp]: "sinr·⊥ = ⊥"
    by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict)

    lemma sinl_eq [simp]: "(sinl·x = sinl·y) = (x = y)"
    by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)

    lemma sinr_eq [simp]: "(sinr·x = sinr·y) = (x = y)"
    by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)

    lemma sinl_inject: "sinl·x = sinl·y ==> x = y"
    by (rule sinl_eq [THEN iffD1])

    lemma sinr_inject: "sinr·x = sinr·y ==> x = y"
    by (rule sinr_eq [THEN iffD1])

    lemma sinl_defined_iff [simp]: "(sinl·x = ⊥) = (x = ⊥)"
    apply (rule sinl_strict [THEN subst])
    apply (rule sinl_eq)
    done

    lemma sinr_defined_iff [simp]: "(sinr·x = ⊥) = (x = ⊥)"
    apply (rule sinr_strict [THEN subst])
    apply (rule sinr_eq)
    done

    lemma sinl_defined [intro!]: "x ≠ ⊥ ==> sinl·x ≠ ⊥"
    by simp

    lemma sinr_defined [intro!]: "x ≠ ⊥ ==> sinr·x ≠ ⊥"
    by simp

    subsection {* Case analysis *}

    lemma Exh_Ssum:
      "z = ⊥ ∨ (∃a. z = sinl·a ∧ a ≠ ⊥) ∨ (∃b. z = sinr·b ∧ b ≠ ⊥)"
    apply (rule_tac x=z in Abs_Ssum_induct)
    apply (rule_tac p=y in cprodE)
    apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
    apply (simp add: Abs_Ssum_inject Ssum_def)
    apply (auto simp add: cpair_strict Abs_Ssum_strict)
    done

    lemma ssumE:
      "[|p = ⊥ ==> Q;
       !!x. [|p = sinl·x; x ≠ ⊥|] ==> Q;
       !!y. [|p = sinr·y; y ≠ ⊥|] ==> Q|] ==> Q"
    by (cut_tac z=p in Exh_Ssum, auto)

    lemma ssumE2:
      "[|!!x. p = sinl·x ==> Q; !!y. p = sinr·y ==> Q|] ==> Q"
    apply (rule_tac p=p in ssumE)
    apply (simp only: sinl_strict [symmetric])
    apply simp
    apply simp
    done

    subsection {* Ordering properties of @{term sinl} and @{term sinr} *}

    lemma sinl_less [simp]: "(sinl·x \<sqsubseteq> sinl·y) = (x \<sqsubseteq> y)"
    by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)

    lemma sinr_less [simp]: "(sinr·x \<sqsubseteq> sinr·y) = (x \<sqsubseteq> y)"
    by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)

    lemma sinl_less_sinr [simp]: "(sinl·x \<sqsubseteq> sinr·y) = (x = ⊥)"
    by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)

    lemma sinr_less_sinl [simp]: "(sinr·x \<sqsubseteq> sinl·y) = (x = ⊥)"
    by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)

    lemma sinl_eq_sinr [simp]: "(sinl·x = sinr·y) = (x = ⊥ ∧ y = ⊥)"
    by (simp add: po_eq_conv)

    lemma sinr_eq_sinl [simp]: "(sinr·x = sinl·y) = (x = ⊥ ∧ y = ⊥)"
    by (simp add: po_eq_conv)

    subsection {* Chains of strict sums *}

    lemma less_sinlD: "p \<sqsubseteq> sinl·x ==> ∃y. p = sinl·y ∧ y \<sqsubseteq> x"
    apply (rule_tac p=p in ssumE)
    apply (rule_tac x="⊥" in exI, simp)
    apply simp
    apply simp
    done

    lemma less_sinrD: "p \<sqsubseteq> sinr·x ==> ∃y. p = sinr·y ∧ y \<sqsubseteq> x"
    apply (rule_tac p=p in ssumE)
    apply (rule_tac x="⊥" in exI, simp)
    apply simp
    apply simp
    done

    lemma ssum_chain_lemma:
    "chain Y ==> (∃A. chain A ∧ Y = (λi. sinl·(A i))) ∨
                 (∃B. chain B ∧ Y = (λi. sinr·(B i)))"
     apply (rule_tac p="lub (range Y)" in ssumE2)
      apply (rule disjI1)
      apply (rule_tac x="λi. cfst·(Rep_Ssum (Y i))" in exI)
      apply (rule conjI)
       apply (rule chain_monofun)
       apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
      apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
      apply (drule less_sinlD, clarify)
      apply (simp add: Rep_Ssum_sinl)
     apply (rule disjI2)
     apply (rule_tac x="λi. csnd·(Rep_Ssum (Y i))" in exI)
     apply (rule conjI)
      apply (rule chain_monofun)
      apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
     apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
     apply (drule less_sinrD, clarify)
     apply (simp add: Rep_Ssum_sinr)
    done

    subsection {* Definitions of constants *}

    constdefs
      Iwhen :: "['a -> 'c, 'b -> 'c, 'a ++ 'b] => 'c"
      "Iwhen ≡ λf g s.
        if cfst·(Rep_Ssum s) ≠ ⊥ then f·(cfst·(Rep_Ssum s)) else
        if csnd·(Rep_Ssum s) ≠ ⊥ then g·(csnd·(Rep_Ssum s)) else ⊥"

    text {* rewrites for @{term Iwhen} *}

    lemma Iwhen1 [simp]: "Iwhen f g ⊥ = ⊥"
    by (simp add: Iwhen_def Rep_Ssum_strict)

    lemma Iwhen2 [simp]: "x ≠ ⊥ ==> Iwhen f g (sinl·x) = f·x"
    by (simp add: Iwhen_def Rep_Ssum_sinl)

    lemma Iwhen3 [simp]: "y ≠ ⊥ ==> Iwhen f g (sinr·y) = g·y"
    by (simp add: Iwhen_def Rep_Ssum_sinr)

    lemma Iwhen4: "Iwhen f g (sinl·x) = strictify·f·x"
    by (simp add: strictify_conv_if)

    lemma Iwhen5: "Iwhen f g (sinr·y) = strictify·g·y"
    by (simp add: strictify_conv_if)

    subsection {* Continuity of @{term Iwhen} *}

    text {* @{term Iwhen} is continuous in all arguments *}

    lemma cont_Iwhen1: "cont (λf. Iwhen f g s)"
    by (rule_tac p=s in ssumE, simp_all)

    lemma cont_Iwhen2: "cont (λg. Iwhen f g s)"
    by (rule_tac p=s in ssumE, simp_all)

    lemma cont_Iwhen3: "cont (λs. Iwhen f g s)"
    apply (rule contI)
    apply (drule ssum_chain_lemma, safe)
    apply (simp add: contlub_cfun_arg [symmetric])
    apply (simp add: Iwhen4 cont_cfun_arg)
    apply (simp add: contlub_cfun_arg [symmetric])
    apply (simp add: Iwhen5 cont_cfun_arg)
    done

    subsection {* Continuous versions of constants *}

    constdefs
      sscase :: "('a -> 'c) -> ('b -> 'c) -> ('a ++ 'b) -> 'c"
      "sscase ≡ Λ f g s. Iwhen f g s"

    translations
    "case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"

    text {* continuous versions of lemmas for @{term sscase} *}

    lemma beta_sscase: "sscase·f·g·s = Iwhen f g s"
    by (simp add: sscase_def cont_Iwhen1 cont_Iwhen2 cont_Iwhen3)

    lemma sscase1 [simp]: "sscase·f·g·⊥ = ⊥"
    by (simp add: beta_sscase)

    lemma sscase2 [simp]: "x ≠ ⊥ ==> sscase·f·g·(sinl·x) = f·x"
    by (simp add: beta_sscase)

    lemma sscase3 [simp]: "y ≠ ⊥ ==> sscase·f·g·(sinr·y) = g·y"
    by (simp add: beta_sscase)

    lemma sscase4 [simp]: "sscase·sinl·sinr·z = z"
    by (rule_tac p=z in ssumE, simp_all)

    end

### Definition of strict sum type

### Definitions of constructors

### Properties of @{term sinl} and @{term sinr}

lemma sinl_Abs_Ssum:

      sinl·a = Abs_Ssum <a, UU>

lemma sinr_Abs_Ssum:

      sinr·b = Abs_Ssum <UU, b>

lemma Rep_Ssum_sinl:

      Rep_Ssum (sinl·a) = <a, UU>

lemma Rep_Ssum_sinr:

      Rep_Ssum (sinr·b) = <UU, b>

lemma sinl_strict:

      sinl·UU = UU

lemma sinr_strict:

      sinr·UU = UU

lemma sinl_eq:

      (sinl·x = sinl·y) = (x = y)

lemma sinr_eq:

      (sinr·x = sinr·y) = (x = y)

lemma sinl_inject:

      sinl·x = sinl·y ==> x = y

lemma sinr_inject:

      sinr·x = sinr·y ==> x = y

lemma sinl_defined_iff:

      (sinl·x = UU) = (x = UU)

lemma sinr_defined_iff:

      (sinr·x = UU) = (x = UU)

lemma sinl_defined:

      x ≠ UU ==> sinl·x ≠ UU

lemma sinr_defined:

      x ≠ UU ==> sinr·x ≠ UU

### Case analysis

lemma Exh_Ssum:

      z = UU ∨ (∃a. z = sinl·a ∧ a ≠ UU) ∨ (∃b. z = sinr·b ∧ b ≠ UU)

lemma ssumE:

      [| p = UU ==> Q; !!x. [| p = sinl·x; x ≠ UU |] ==> Q;
         !!y. [| p = sinr·y; y ≠ UU |] ==> Q |]
      ==> Q

lemma ssumE2:

      [| !!x. p = sinl·x ==> Q; !!y. p = sinr·y ==> Q |] ==> Q

### Ordering properties of @{term sinl} and @{term sinr}

lemma sinl_less:

      sinl·x << sinl·y = x << y

lemma sinr_less:

      sinr·x << sinr·y = x << y

lemma sinl_less_sinr:

      sinl·x << sinr·y = (x = UU)

lemma sinr_less_sinl:

      sinr·x << sinl·y = (x = UU)

lemma sinl_eq_sinr:

      (sinl·x = sinr·y) = (x = UU ∧ y = UU)

lemma sinr_eq_sinl:

      (sinr·x = sinl·y) = (x = UU ∧ y = UU)

### Chains of strict sums

lemma less_sinlD:

      p << sinl·x ==> ∃y. p = sinl·y ∧ y << x

lemma less_sinrD:

      p << sinr·x ==> ∃y. p = sinr·y ∧ y << x

lemma ssum_chain_lemma:

      chain Y
      ==> (∃A. chain A ∧ Y = (%i. sinl·(A i))) ∨ (∃B. chain B ∧ Y = (%i. sinr·(B i)))

### Definitions of constants

lemma Iwhen1:

      Iwhen f g UU = UU

lemma Iwhen2:

      x ≠ UU ==> Iwhen f g (sinl·x) = f·x

lemma Iwhen3:

      y ≠ UU ==> Iwhen f g (sinr·y) = g·y

lemma Iwhen4:

      Iwhen f g (sinl·x) = strictify·f·x

lemma Iwhen5:

      Iwhen f g (sinr·y) = strictify·g·y

### Continuity of @{term Iwhen}

lemma cont_Iwhen1:

      cont (%f. Iwhen f g s)

lemma cont_Iwhen2:

      cont (%g. Iwhen f g s)

lemma cont_Iwhen3:

      cont (Iwhen f g)

### Continuous versions of constants

lemma beta_sscase:

      sscase·f·g·s = Iwhen f g s

lemma sscase1:

      sscase·f·g·UU = UU

lemma sscase2:

      x ≠ UU ==> sscase·f·g·(sinl·x) = f·x

lemma sscase3:

      y ≠ UU ==> sscase·f·g·(sinr·y) = g·y

lemma sscase4:

      sscase·sinl·sinr·z = z