# Theory Cprod

Up to index of Isabelle/HOLCF

theory Cprod
imports Cfun
uses [Cprod.ML]
begin

    (*  Title:      HOLCF/Cprod.thy
        ID:         $Id: Cprod.thy,v 1.15 2005/07/26 16:22:03 huffman Exp $
        Author:     Franz Regensburger

    Partial ordering for cartesian product of HOL products.
    *)

    header {* The cpo of cartesian products *}

    theory Cprod
    imports Cfun
    begin

    defaultsort cpo

    subsection {* Type @{typ unit} is a pcpo *}

    instance unit :: sq_ord ..

    defs (overloaded)
      less_unit_def [simp]: "x \<sqsubseteq> (y::unit) ≡ True"

    instance unit :: po
    by intro_classes simp_all

    instance unit :: cpo
    by intro_classes (simp add: is_lub_def is_ub_def)

    instance unit :: pcpo
    by intro_classes simp

    subsection {* Type @{typ "'a * 'b"} is a partial order *}

    instance "*" :: (sq_ord, sq_ord) sq_ord ..

    defs (overloaded)
      less_cprod_def: "(op \<sqsubseteq>) ≡ λp1 p2. (fst p1 \<sqsubseteq> fst p2 ∧ snd p1 \<sqsubseteq> snd p2)"

    lemma refl_less_cprod: "(p::'a * 'b) \<sqsubseteq> p"
    by (simp add: less_cprod_def)

    lemma antisym_less_cprod: "[|(p1::'a * 'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p1|] ==> p1 = p2"
    apply (unfold less_cprod_def)
    apply (rule injective_fst_snd)
    apply (fast intro: antisym_less)
    apply (fast intro: antisym_less)
    done

    lemma trans_less_cprod: "[|(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3|] ==> p1 \<sqsubseteq> p3"
    apply (unfold less_cprod_def)
    apply (fast intro: trans_less)
    done

    instance "*" :: (cpo, cpo) po
    by intro_classes
      (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+

    subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}

    text {* Pair @{text "(_,_)"}  is monotone in both arguments *}

    lemma monofun_pair1: "monofun (λx. (x, y))"
    by (simp add: monofun_def less_cprod_def)

    lemma monofun_pair2: "monofun (λy. (x, y))"
    by (simp add: monofun_def less_cprod_def)

    lemma monofun_pair:
      "[|x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2|] ==> (x1, y1) \<sqsubseteq> (x2, y2)"
    by (simp add: less_cprod_def)

    text {* @{term fst} and @{term snd} are monotone *}

    lemma monofun_fst: "monofun fst"
    by (simp add: monofun_def less_cprod_def)

    lemma monofun_snd: "monofun snd"
    by (simp add: monofun_def less_cprod_def)

    subsection {* Type @{typ "'a * 'b"} is a cpo *}

    lemma lub_cprod:
      "chain S ==> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    apply (rule is_lubI)
    apply (rule ub_rangeI)
    apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
    apply (rule monofun_pair)
    apply (rule is_ub_thelub)
    apply (erule monofun_fst [THEN ch2ch_monofun])
    apply (rule is_ub_thelub)
    apply (erule monofun_snd [THEN ch2ch_monofun])
    apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
    apply (rule monofun_pair)
    apply (rule is_lub_thelub)
    apply (erule monofun_fst [THEN ch2ch_monofun])
    apply (erule monofun_fst [THEN ub2ub_monofun])
    apply (rule is_lub_thelub)
    apply (erule monofun_snd [THEN ch2ch_monofun])
    apply (erule monofun_snd [THEN ub2ub_monofun])
    done

    lemma thelub_cprod:
      "chain S ==> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    by (rule lub_cprod [THEN thelubI])

    lemma cpo_cprod:
      "chain (S::nat => 'a::cpo * 'b::cpo) ==> ∃x. range S <<| x"
    by (rule exI, erule lub_cprod)

    instance "*" :: (cpo, cpo) cpo
    by intro_classes (rule cpo_cprod)

    subsection {* Type @{typ "'a * 'b"} is pointed *}

    lemma minimal_cprod: "(⊥, ⊥) \<sqsubseteq> p"
    by (simp add: less_cprod_def)

    lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y"
    apply (rule_tac x = "(⊥, ⊥)" in exI)
    apply (rule minimal_cprod [THEN allI])
    done

    instance "*" :: (pcpo, pcpo) pcpo
    by intro_classes (rule least_cprod)

    text {* for compatibility with old HOLCF-Version *}
    lemma inst_cprod_pcpo: "UU = (UU,UU)"
    by (rule minimal_cprod [THEN UU_I, symmetric])

    subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}

    lemma contlub_pair1: "contlub (λx. (x, y))"
    apply (rule contlubI)
    apply (subst thelub_cprod)
    apply (erule monofun_pair1 [THEN ch2ch_monofun])
    apply (simp add: thelub_const)
    done

    lemma contlub_pair2: "contlub (λy. (x, y))"
    apply (rule contlubI)
    apply (subst thelub_cprod)
    apply (erule monofun_pair2 [THEN ch2ch_monofun])
    apply (simp add: thelub_const)
    done

    lemma cont_pair1: "cont (λx. (x, y))"
    apply (rule monocontlub2cont)
    apply (rule monofun_pair1)
    apply (rule contlub_pair1)
    done

    lemma cont_pair2: "cont (λy. (x, y))"
    apply (rule monocontlub2cont)
    apply (rule monofun_pair2)
    apply (rule contlub_pair2)
    done

    lemma contlub_fst: "contlub fst"
    apply (rule contlubI)
    apply (simp add: thelub_cprod)
    done

    lemma contlub_snd: "contlub snd"
    apply (rule contlubI)
    apply (simp add: thelub_cprod)
    done

    lemma cont_fst: "cont fst"
    apply (rule monocontlub2cont)
    apply (rule monofun_fst)
    apply (rule contlub_fst)
    done

    lemma cont_snd: "cont snd"
    apply (rule monocontlub2cont)
    apply (rule monofun_snd)
    apply (rule contlub_snd)
    done

    subsection {* Continuous versions of constants *}

    consts
      cpair  :: "'a -> 'b -> ('a * 'b)" (* continuous pairing *)
      cfst   :: "('a * 'b) -> 'a"
      csnd   :: "('a * 'b) -> 'b"
      csplit :: "('a -> 'b -> 'c) -> ('a * 'b) -> 'c"

    syntax
      "@ctuple" :: "['a, args] => 'a * 'b"  ("(1<_,/ _>)")

    translations
      "<x, y, z>" == "<x, <y, z>>"
      "<x, y>"    == "cpair$x$y"

    defs
      cpair_def:  "cpair  ≡ (Λ x y. (x, y))"
      cfst_def:   "cfst   ≡ (Λ p. fst p)"
      csnd_def:   "csnd   ≡ (Λ p. snd p)"
      csplit_def: "csplit ≡ (Λ f p. f·(cfst·p)·(csnd·p))"

    subsection {* Syntax *}

    text {* syntax for @{text "LAM <x,y,z>.e"} *}

    syntax
      "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)

    translations
      "LAM <x,y,zs>. b"       == "csplit$(LAM x. LAM <y,zs>. b)"
      "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
      "LAM <x,y>.b"           == "csplit$(LAM x y. b)"

    syntax (xsymbols)
      "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3Λ()<_>./ _)" [0, 10] 10)

    text {* syntax for Let *}

    constdefs
      CLet :: "'a -> ('a -> 'b) -> 'b"
      "CLet ≡ Λ s f. f·s"

    nonterminals
      Cletbinds  Cletbind

    syntax
      "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
      "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
      ""        :: "Cletbind => Cletbinds"               ("_")
      "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
      "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)

    translations
      "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
      "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
      "Let x = a in e"          == "CLet$a$(LAM x. e)"
      "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"

    subsection {* Convert all lemmas to the continuous versions *}

    lemma cpair_eq_pair: "<x, y> = (x, y)"
    by (simp add: cpair_def cont_pair1 cont_pair2)

    lemma inject_cpair: "<a,b> = <aa,ba> ==> a = aa ∧ b = ba"
    by (simp add: cpair_eq_pair)

    lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' ∧ b = b')"
    by (simp add: cpair_eq_pair)

    lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' ∧ b \<sqsubseteq> b')"
    by (simp add: cpair_eq_pair less_cprod_def)

    lemma cpair_defined_iff: "(<x, y> = ⊥) = (x = ⊥ ∧ y = ⊥)"
    by (simp add: inst_cprod_pcpo cpair_eq_pair)

    lemma cpair_strict: "<⊥, ⊥> = ⊥"
    by (simp add: cpair_defined_iff)

    lemma inst_cprod_pcpo2: "⊥ = <⊥, ⊥>"
    by (rule cpair_strict [symmetric])

    lemma defined_cpair_rev:
     "<a,b> = ⊥ ==> a = ⊥ ∧ b = ⊥"
    by (simp add: inst_cprod_pcpo cpair_eq_pair)

    lemma Exh_Cprod2: "∃a b. z = <a, b>"
    by (simp add: cpair_eq_pair)

    lemma cprodE: "[|!!x y. p = <x, y> ==> Q|] ==> Q"
    by (cut_tac Exh_Cprod2, auto)

    lemma cfst_cpair [simp]: "cfst·<x, y> = x"
    by (simp add: cpair_eq_pair cfst_def cont_fst)

    lemma csnd_cpair [simp]: "csnd·<x, y> = y"
    by (simp add: cpair_eq_pair csnd_def cont_snd)

    lemma cfst_strict [simp]: "cfst·⊥ = ⊥"
    by (simp add: inst_cprod_pcpo2)

    lemma csnd_strict [simp]: "csnd·⊥ = ⊥"
    by (simp add: inst_cprod_pcpo2)

    lemma surjective_pairing_Cprod2: "<cfst·p, csnd·p> = p"
    apply (unfold cfst_def csnd_def)
    apply (simp add: cont_fst cont_snd cpair_eq_pair)
    done

    lemma less_cprod: "x \<sqsubseteq> y = (cfst·x \<sqsubseteq> cfst·y ∧ csnd·x \<sqsubseteq> csnd·y)"
    by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)

    lemma eq_cprod: "(x = y) = (cfst·x = cfst·y ∧ csnd·x = csnd·y)"
    by (auto simp add: po_eq_conv less_cprod)

    lemma lub_cprod2:
      "chain S ==> range S <<| <\<Squnion>i. cfst·(S i), \<Squnion>i. csnd·(S i)>"
    apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
    apply (erule lub_cprod)
    done

    lemma thelub_cprod2:
      "chain S ==> lub (range S) = <\<Squnion>i. cfst·(S i), \<Squnion>i. csnd·(S i)>"
    by (rule lub_cprod2 [THEN thelubI])

    lemma csplit2 [simp]: "csplit·f·<x,y> = f·x·y"
    by (simp add: csplit_def)

    lemma csplit3 [simp]: "csplit·cpair·z = z"
    by (simp add: csplit_def surjective_pairing_Cprod2)

    lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2

    end

### Type @{typ unit} is a pcpo

### Type @{typ "'a * 'b"} is a partial order

lemma refl_less_cprod:

      p << p

lemma antisym_less_cprod:

      [| p1.0 << p2.0; p2.0 << p1.0 |] ==> p1.0 = p2.0

lemma trans_less_cprod:

      [| p1.0 << p2.0; p2.0 << p3.0 |] ==> p1.0 << p3.0

### Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd}

lemma monofun_pair1:

      monofun (%x. (x, y))

lemma monofun_pair2:

      monofun (Pair x)

lemma monofun_pair:

      [| x1.0 << x2.0; y1.0 << y2.0 |] ==> (x1.0, y1.0) << (x2.0, y2.0)

lemma monofun_fst:

      monofun fst

lemma monofun_snd:

      monofun snd

### Type @{typ "'a * 'b"} is a cpo

lemma lub_cprod:

      chain S ==> range S <<| (LUB i. fst (S i), LUB i. snd (S i))

lemma thelub_cprod:

      chain S ==> lub (range S) = (LUB i. fst (S i), LUB i. snd (S i))

lemma cpo_cprod:

      chain S ==> ∃x. range S <<| x

### Type @{typ "'a * 'b"} is pointed

lemma minimal_cprod:

      (UU, UU) << p

lemma least_cprod:

      ∃x. ∀y. x << y

lemma inst_cprod_pcpo:

      UU = (UU, UU)

### Continuity of @{text "(_,_)"}, @{term fst}, @{term snd}

lemma contlub_pair1:

      contlub (%x. (x, y))

lemma contlub_pair2:

      contlub (Pair x)

lemma cont_pair1:

      cont (%x. (x, y))

lemma cont_pair2:

      cont (Pair x)

lemma contlub_fst:

      contlub fst

lemma contlub_snd:

      contlub snd

lemma cont_fst:

      cont fst

lemma cont_snd:

      cont snd

### Continuous versions of constants

### Syntax

### Convert all lemmas to the continuous versions

lemma cpair_eq_pair:

      <x, y> = (x, y)

lemma inject_cpair:

      <a, b> = <aa, ba> ==> a = aa ∧ b = ba

lemma cpair_eq:

      (<a, b> = <a', b'>) = (a = a' ∧ b = b')

lemma cpair_less:

      <a, b> << <a', b'> = (a << a' ∧ b << b')

lemma cpair_defined_iff:

      (<x, y> = UU) = (x = UU ∧ y = UU)

lemma cpair_strict:

      <UU, UU> = UU

lemma inst_cprod_pcpo2:

      UU = <UU, UU>

lemma defined_cpair_rev:

      <a, b> = UU ==> a = UU ∧ b = UU

lemma Exh_Cprod2:

      ∃a b. z = <a, b>

lemma cprodE:

      (!!x y. p = <x, y> ==> Q) ==> Q

lemma cfst_cpair:

      cfst·<x, y> = x

lemma csnd_cpair:

      csnd·<x, y> = y

lemma cfst_strict:

      cfst·UU = UU

lemma csnd_strict:

      csnd·UU = UU

lemma surjective_pairing_Cprod2:

      <cfst·p, csnd·p> = p

lemma less_cprod:

      x << y = (cfst·x << cfst·y ∧ csnd·x << csnd·y)

lemma eq_cprod:

      (x = y) = (cfst·x = cfst·y ∧ csnd·x = csnd·y)

lemma lub_cprod2:

      chain S ==> range S <<| <LUB i. cfst·(S i), LUB i. csnd·(S i)>

lemma thelub_cprod2:

      chain S ==> lub (range S) = <LUB i. cfst·(S i), LUB i. csnd·(S i)>

lemma csplit2:

      csplit·f·<x, y> = f·x·y

lemma csplit3:

      csplit·cpair·z = z

lemmas Cprod_rews:

      cfst·<x, y> = x

      csnd·<x, y> = y

      csplit·f·<x, y> = f·x·y

lemmas Cprod_rews:

      cfst·<x, y> = x

      csnd·<x, y> = y

      csplit·f·<x, y> = f·x·y