Theory Sprod

(*  Title:      HOL/HOLCF/Sprod.thy
    Author:     Franz Regensburger
    Author:     Brian Huffman

section ‹The type of strict products›

theory Sprod
  imports Cfun

default_sort pcpo

subsection ‹Definition of strict product type›

definition "sprod = {p::'a × 'b. p =   (fst p    snd p  )}"

pcpodef ('a, 'b) sprod  ("(_ / _)" [21,20] 20) = "sprod :: ('a × 'b) set"
  by (simp_all add: sprod_def)

instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
  by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])

type_notation (ASCII)
  sprod  (infixr "**" 20)

subsection ‹Definitions of constants›

definition sfst :: "('a ** 'b)  'a"
  where "sfst = (Λ p. fst (Rep_sprod p))"

definition ssnd :: "('a ** 'b)  'b"
  where "ssnd = (Λ p. snd (Rep_sprod p))"

definition spair :: "'a  'b  ('a ** 'b)"
  where "spair = (Λ a b. Abs_sprod (seqba, seqab))"

definition ssplit :: "('a  'b  'c)  ('a ** 'b)  'c"
  where "ssplit = (Λ f p. seqp(f(sfstp)(ssndp)))"

syntax "_stuple" :: "[logic, args]  logic"  ("(1'(:_,/ _:'))")
  "(:x, y, z:)"  "(:x, (:y, z:):)"
  "(:x, y:)"  "CONST spairxy"

  "Λ(CONST spairxy). t"  "CONST ssplit(Λ x y. t)"

subsection ‹Case analysis›

lemma spair_sprod: "(seqba, seqab)  sprod"
  by (simp add: sprod_def seq_conv_if)

lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seqba, seqab)"
  by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod)

lemmas Rep_sprod_simps =
  Rep_sprod_inject [symmetric] below_sprod_def
  prod_eq_iff below_prod_def
  Rep_sprod_strict Rep_sprod_spair

lemma sprodE [case_names bottom spair, cases type: sprod]:
  obtains "p = " | x y where "p = (:x, y:)" and "x  " and "y  "
  using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps)

lemma sprod_induct [case_names bottom spair, induct type: sprod]:
  "P ; x y. x  ; y    P (:x, y:)  P x"
  by (cases x) simp_all

subsection ‹Properties of \emph{spair}›

lemma spair_strict1 [simp]: "(:, y:) = "
  by (simp add: Rep_sprod_simps)

lemma spair_strict2 [simp]: "(:x, :) = "
  by (simp add: Rep_sprod_simps)

lemma spair_bottom_iff [simp]: "(:x, y:) =   x =   y = "
  by (simp add: Rep_sprod_simps seq_conv_if)

lemma spair_below_iff: "(:a, b:)  (:c, d:)  a =   b =   (a  c  b  d)"
  by (simp add: Rep_sprod_simps seq_conv_if)

lemma spair_eq_iff: "(:a, b:) = (:c, d:)  a = c  b = d  (a =   b = )  (c =   d = )"
  by (simp add: Rep_sprod_simps seq_conv_if)

lemma spair_strict: "x =   y =   (:x, y:) = "
  by simp

lemma spair_strict_rev: "(:x, y:)    x    y  "
  by simp

lemma spair_defined: "x  ; y    (:x, y:)  "
  by simp

lemma spair_defined_rev: "(:x, y:) =   x =   y = "
  by simp

lemma spair_below: "x    y    (:x, y:)  (:a, b:)  x  a  y  b"
  by (simp add: spair_below_iff)

lemma spair_eq: "x    y    (:x, y:) = (:a, b:)  x = a  y = b"
  by (simp add: spair_eq_iff)

lemma spair_inject: "x    y    (:x, y:) = (:a, b:)  x = a  y = b"
  by (rule spair_eq [THEN iffD1])

lemma inst_sprod_pcpo2: " = (:, :)"
  by simp

lemma sprodE2: "(x y. p = (:x, y:)  Q)  Q"
  by (cases p) (simp only: inst_sprod_pcpo2, simp)

subsection ‹Properties of \emph{sfst} and \emph{ssnd}›

lemma sfst_strict [simp]: "sfst = "
  by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict)

lemma ssnd_strict [simp]: "ssnd = "
  by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict)

lemma sfst_spair [simp]: "y    sfst(:x, y:) = x"
  by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair)

lemma ssnd_spair [simp]: "x    ssnd(:x, y:) = y"
  by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)

lemma sfst_bottom_iff [simp]: "sfstp =   p = "
  by (cases p) simp_all

lemma ssnd_bottom_iff [simp]: "ssndp =   p = "
  by (cases p) simp_all

lemma sfst_defined: "p    sfstp  "
  by simp

lemma ssnd_defined: "p    ssndp  "
  by simp

lemma spair_sfst_ssnd: "(:sfstp, ssndp:) = p"
  by (cases p) simp_all

lemma below_sprod: "x  y  sfstx  sfsty  ssndx  ssndy"
  by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)

lemma eq_sprod: "x = y  sfstx = sfsty  ssndx = ssndy"
  by (auto simp add: po_eq_conv below_sprod)

lemma sfst_below_iff: "sfstx  y  x  (:y, ssndx:)"
  by (cases "x = ", simp, cases "y = ", simp, simp add: below_sprod)

lemma ssnd_below_iff: "ssndx  y  x  (:sfstx, y:)"
  by (cases "x = ", simp, cases "y = ", simp, simp add: below_sprod)

subsection ‹Compactness›

lemma compact_sfst: "compact x  compact (sfstx)"
  by (rule compactI) (simp add: sfst_below_iff)

lemma compact_ssnd: "compact x  compact (ssndx)"
  by (rule compactI) (simp add: ssnd_below_iff)

lemma compact_spair: "compact x  compact y  compact (:x, y:)"
  by (rule compact_sprod) (simp add: Rep_sprod_spair seq_conv_if)

lemma compact_spair_iff: "compact (:x, y:)  x =   y =   (compact x  compact y)"
  apply (safe elim!: compact_spair)
     apply (drule compact_sfst, simp)
    apply (drule compact_ssnd, simp)
   apply simp
  apply simp

subsection ‹Properties of \emph{ssplit}›

lemma ssplit1 [simp]: "ssplitf = "
  by (simp add: ssplit_def)

lemma ssplit2 [simp]: "x    y    ssplitf(:x, y:) = fxy"
  by (simp add: ssplit_def)

lemma ssplit3 [simp]: "ssplitspairz = z"
  by (cases z) simp_all

subsection ‹Strict product preserves flatness›

instance sprod :: (flat, flat) flat
  fix x y :: "'a  'b"
  assume "x  y"
  then show "x =   x = y"
    apply (induct x, simp)
    apply (induct y, simp)
    apply (simp add: spair_below_iff flat_below_iff)