Quelle Sprod.thy Sprache: Isabelle

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

section \<open>The type of strict products\<close>

theory Sprod
  imports Cfun
begin

subsection \<open>Definition of strict product type\<close>

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

pcpodef ('a::pcpo, 'b::pcpo) sprod  (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [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 \<open>**\<close> 20)

subsection \<open>Definitions of constants\<close>

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

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

definition spair :: "'a::pcpo \ 'b::pcpo \ ('a ** 'b)"
  where "spair = (\ a b. Abs_sprod (seq\b\a, seq\a\b))"

definition ssplit :: "('a::pcpo \ 'b::pcpo \ 'c::pcpo) \ ('a ** 'b) \ 'c"
  where "ssplit = (\ f p. seq\p\(f\(sfst\p)\(ssnd\p)))"

syntax
  "_stuple" :: "[logic, args] \ logic" (\(\indent=1 notation=\mixfix strict tuple\\'(:_,/ _:'))\)
syntax_consts
  "_stuple" \<rightleftharpoons> spair
translations
  "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
  "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"

translations
  "\(CONST spair\x\y). t" \ "CONST ssplit\(\ x y. t)"

subsection \<open>Case analysis\<close>

lemma spair_sprod: "(seq\b\a, seq\a\b) \ sprod"
  by (simp add: sprod_def seq_conv_if)

lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\b\a, seq\a\b)"
  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 \<open>Properties of \emph{spair}\<close>

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 \<open>Properties of \emph{sfst} and \emph{ssnd}\<close>

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]: "sfst\p = \ \ p = \"
  by (cases p) simp_all

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

lemma sfst_defined: "p \ \ \ sfst\p \ \"
  by simp

lemma ssnd_defined: "p \ \ \ ssnd\p \ \"
  by simp

lemma spair_sfst_ssnd: "(:sfst\p, ssnd\p:) = p"
  by (cases p) simp_all

lemma below_sprod: "x \ y \ sfst\x \ sfst\y \ ssnd\x \ ssnd\y"
  by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)

lemma eq_sprod: "x = y \ sfst\x = sfst\y \ ssnd\x = ssnd\y"
  by (auto simp add: po_eq_conv below_sprod)

lemma sfst_below_iff: "sfst\x \ y \ x \ (:y, ssnd\x:)"
  by (cases "x = \", simp, cases "y = \", simp, simp add: below_sprod)

lemma ssnd_below_iff: "ssnd\x \ y \ x \ (:sfst\x, y:)"
  by (cases "x = \", simp, cases "y = \", simp, simp add: below_sprod)

subsection \<open>Compactness\<close>

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

lemma compact_ssnd: "compact x \ compact (ssnd\x)"
  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
  done

subsection \<open>Properties of \emph{ssplit}\<close>

lemma ssplit1 [simp]: "ssplit\f\\ = \"
  by (simp add: ssplit_def)

lemma ssplit2 [simp]: "x \ \ \ y \ \ \ ssplit\f\(:x, y:) = f\x\y"
  by (simp add: ssplit_def)

lemma ssplit3 [simp]: "ssplit\spair\z = z"
  by (cases z) simp_all

subsection \<open>Strict product preserves flatness\<close>

instance sprod :: (flat, flat) flat
proof
  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)
    done
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.