(* Title: HOL/HOLCF/Sprod.thy Author: Franz Regensburger Author: Brian Huffman *) header {* The type of strict products *} theory Sprod imports Cfun begin default_sort pcpo subsection {* Definition of strict product type *} definition "sprod = {p::'a \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \ 'b) set" unfolding sprod_def by simp_all instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) type_notation (xsymbols) sprod ("(_ \/ _)" [21,20] 20) type_notation (HTML output) sprod ("(_ \/ _)" [21,20] 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 (seq\b\a, seq\a\b))" definition ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" where "ssplit = (\ f p. seq\p\(f\(sfst\p)\(ssnd\p)))" syntax "_stuple" :: "[logic, args] \ logic" ("(1'(:_,/ _:'))") translations "(:x, y, z:)" == "(:x, (:y, z:):)" "(:x, y:)" == "CONST spair\x\y" translations "\(CONST spair\x\y). t" == "CONST ssplit\(\ x y. t)" subsection {* Case analysis *} 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 {* 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]: "(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:)" apply (cases "x = \", simp, cases "y = \", simp) apply (simp add: below_sprod) done lemma ssnd_below_iff: "ssnd\x \ y \ x \ (:sfst\x, y:)" apply (cases "x = \", simp, cases "y = \", simp) apply (simp add: below_sprod) done subsection {* Compactness *} 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 {* Properties of \emph{ssplit} *} 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 {* Strict product preserves flatness *} instance sprod :: (flat, flat) flat proof fix x y :: "'a \ 'b" assume "x \ y" thus "x = \ \ x = y" apply (induct x, simp) apply (induct y, simp) apply (simp add: spair_below_iff flat_below_iff) done qed end