# HG changeset patch # User huffman # Date 1287916992 25200 # Node ID 9dbb01456031f41641c2813316c89708c4064a32 # Parent 429cd74f795f8781d660863204f3b1a2fda0097e use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum diff -r 429cd74f795f -r 9dbb01456031 src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Sat Oct 23 19:56:33 2010 -0700 +++ b/src/HOLCF/Sprod.thy Sun Oct 24 03:43:12 2010 -0700 @@ -12,12 +12,12 @@ subsection {* Definition of strict product type *} -pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) = +pcpodef ('a, 'b) sprod (infixr "**" 20) = "{p::'a \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" by simp_all instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin -by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def]) +by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) type_notation (xsymbols) sprod ("(_ \/ _)" [21,20] 20) @@ -28,15 +28,15 @@ definition sfst :: "('a ** 'b) \ 'a" where - "sfst = (\ p. fst (Rep_Sprod p))" + "sfst = (\ p. fst (Rep_sprod p))" definition ssnd :: "('a ** 'b) \ 'b" where - "ssnd = (\ p. snd (Rep_Sprod p))" + "ssnd = (\ p. snd (Rep_sprod p))" definition spair :: "'a \ 'b \ ('a ** 'b)" where - "spair = (\ a b. Abs_Sprod (strict\b\a, strict\a\b))" + "spair = (\ a b. Abs_sprod (strict\b\a, strict\a\b))" definition ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" where @@ -53,20 +53,20 @@ subsection {* Case analysis *} -lemma spair_Sprod: "(strict\b\a, strict\a\b) \ Sprod" -by (simp add: Sprod_def strict_conv_if) +lemma spair_sprod: "(strict\b\a, strict\a\b) \ sprod" +by (simp add: sprod_def strict_conv_if) -lemma Rep_Sprod_spair: "Rep_Sprod (:a, b:) = (strict\b\a, strict\a\b)" -by (simp add: spair_def cont_Abs_Sprod Abs_Sprod_inverse spair_Sprod) +lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\b\a, strict\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 +lemmas Rep_sprod_simps = + Rep_sprod_inject [symmetric] below_sprod_def Pair_fst_snd_eq below_prod_def - Rep_Sprod_strict Rep_Sprod_spair + 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) +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" @@ -75,22 +75,22 @@ subsection {* Properties of \emph{spair} *} lemma spair_strict1 [simp]: "(:\, y:) = \" -by (simp add: Rep_Sprod_simps) +by (simp add: Rep_sprod_simps) lemma spair_strict2 [simp]: "(:x, \:) = \" -by (simp add: Rep_Sprod_simps) +by (simp add: Rep_sprod_simps) lemma spair_strict_iff [simp]: "((:x, y:) = \) = (x = \ \ y = \)" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps strict_conv_if) lemma spair_below_iff: "((:a, b:) \ (:c, d:)) = (a = \ \ b = \ \ (a \ c \ b \ d))" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps strict_conv_if) lemma spair_eq_iff: "((:a, b:) = (:c, d:)) = (a = c \ b = d \ (a = \ \ b = \) \ (c = \ \ d = \))" -by (simp add: Rep_Sprod_simps strict_conv_if) +by (simp add: Rep_sprod_simps strict_conv_if) lemma spair_strict: "x = \ \ y = \ \ (:x, y:) = \" by simp @@ -125,16 +125,16 @@ subsection {* Properties of \emph{sfst} and \emph{ssnd} *} lemma sfst_strict [simp]: "sfst\\ = \" -by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict) +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) +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) +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) +by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair) lemma sfst_defined_iff [simp]: "(sfst\p = \) = (p = \)" by (cases p, simp_all) @@ -152,7 +152,7 @@ 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) +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) @@ -176,7 +176,7 @@ 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 strict_conv_if) +by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if) lemma compact_spair_iff: "compact (:x, y:) = (x = \ \ y = \ \ (compact x \ compact y))" diff -r 429cd74f795f -r 9dbb01456031 src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Sat Oct 23 19:56:33 2010 -0700 +++ b/src/HOLCF/Ssum.thy Sun Oct 24 03:43:12 2010 -0700 @@ -12,14 +12,14 @@ subsection {* Definition of strict sum type *} -pcpodef (Ssum) ('a, 'b) ssum (infixr "++" 10) = +pcpodef ('a, 'b) ssum (infixr "++" 10) = "{p :: tr \ ('a \ 'b). p = \ \ (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \ (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \) }" by simp_all instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin -by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def]) +by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) type_notation (xsymbols) ssum ("(_ \/ _)" [21, 20] 20) @@ -31,44 +31,44 @@ definition sinl :: "'a \ ('a ++ 'b)" where - "sinl = (\ a. Abs_Ssum (strict\a\TT, a, \))" + "sinl = (\ a. Abs_ssum (strict\a\TT, a, \))" definition sinr :: "'b \ ('a ++ 'b)" where - "sinr = (\ b. Abs_Ssum (strict\b\FF, \, b))" + "sinr = (\ b. Abs_ssum (strict\b\FF, \, b))" -lemma sinl_Ssum: "(strict\a\TT, a, \) \ Ssum" -by (simp add: Ssum_def strict_conv_if) +lemma sinl_ssum: "(strict\a\TT, a, \) \ ssum" +by (simp add: ssum_def strict_conv_if) -lemma sinr_Ssum: "(strict\b\FF, \, b) \ Ssum" -by (simp add: Ssum_def strict_conv_if) +lemma sinr_ssum: "(strict\b\FF, \, b) \ ssum" +by (simp add: ssum_def strict_conv_if) -lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\a) = (strict\a\TT, a, \)" -by (simp add: sinl_def cont_Abs_Ssum Abs_Ssum_inverse sinl_Ssum) +lemma Rep_ssum_sinl: "Rep_ssum (sinl\a) = (strict\a\TT, a, \)" +by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum) -lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\b) = (strict\b\FF, \, b)" -by (simp add: sinr_def cont_Abs_Ssum Abs_Ssum_inverse sinr_Ssum) +lemma Rep_ssum_sinr: "Rep_ssum (sinr\b) = (strict\b\FF, \, b)" +by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum) -lemmas Rep_Ssum_simps = - Rep_Ssum_inject [symmetric] below_Ssum_def +lemmas Rep_ssum_simps = + Rep_ssum_inject [symmetric] below_ssum_def Pair_fst_snd_eq below_prod_def - Rep_Ssum_strict Rep_Ssum_sinl Rep_Ssum_sinr + Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr subsection {* Properties of \emph{sinl} and \emph{sinr} *} text {* Ordering *} lemma sinl_below [simp]: "(sinl\x \ sinl\y) = (x \ y)" -by (simp add: Rep_Ssum_simps strict_conv_if) +by (simp add: Rep_ssum_simps strict_conv_if) lemma sinr_below [simp]: "(sinr\x \ sinr\y) = (x \ y)" -by (simp add: Rep_Ssum_simps strict_conv_if) +by (simp add: Rep_ssum_simps strict_conv_if) lemma sinl_below_sinr [simp]: "(sinl\x \ sinr\y) = (x = \)" -by (simp add: Rep_Ssum_simps strict_conv_if) +by (simp add: Rep_ssum_simps strict_conv_if) lemma sinr_below_sinl [simp]: "(sinr\x \ sinl\y) = (x = \)" -by (simp add: Rep_Ssum_simps strict_conv_if) +by (simp add: Rep_ssum_simps strict_conv_if) text {* Equality *} @@ -93,10 +93,10 @@ text {* Strictness *} lemma sinl_strict [simp]: "sinl\\ = \" -by (simp add: Rep_Ssum_simps) +by (simp add: Rep_ssum_simps) lemma sinr_strict [simp]: "sinr\\ = \" -by (simp add: Rep_Ssum_simps) +by (simp add: Rep_ssum_simps) lemma sinl_defined_iff [simp]: "(sinl\x = \) = (x = \)" using sinl_eq [of "x" "\"] by simp @@ -113,10 +113,10 @@ text {* Compactness *} lemma compact_sinl: "compact x \ compact (sinl\x)" -by (rule compact_Ssum, simp add: Rep_Ssum_sinl) +by (rule compact_ssum, simp add: Rep_ssum_sinl) lemma compact_sinr: "compact x \ compact (sinr\x)" -by (rule compact_Ssum, simp add: Rep_Ssum_sinr) +by (rule compact_ssum, simp add: Rep_ssum_sinr) lemma compact_sinlD: "compact (sinl\x) \ compact x" unfolding compact_def @@ -138,7 +138,7 @@ obtains "p = \" | x where "p = sinl\x" and "x \ \" | y where "p = sinr\y" and "y \ \" -using Rep_Ssum [of p] by (auto simp add: Ssum_def Rep_Ssum_simps) +using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps) lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]: "\P \; @@ -160,7 +160,7 @@ definition sscase :: "('a \ 'c) \ ('b \ 'c) \ ('a ++ 'b) \ 'c" where - "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y fi) (Rep_Ssum s))" + "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y fi) (Rep_ssum s))" translations "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" == "CONST sscase\(\ x. t1)\(\ y. t2)\s" @@ -170,17 +170,17 @@ "\(XCONST sinr\y). t" == "CONST sscase\\\(\ y. t)" lemma beta_sscase: - "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y fi) (Rep_Ssum s)" -unfolding sscase_def by (simp add: cont_Rep_Ssum [THEN cont_compose]) + "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y fi) (Rep_ssum s)" +unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose]) lemma sscase1 [simp]: "sscase\f\g\\ = \" -unfolding beta_sscase by (simp add: Rep_Ssum_strict) +unfolding beta_sscase by (simp add: Rep_ssum_strict) lemma sscase2 [simp]: "x \ \ \ sscase\f\g\(sinl\x) = f\x" -unfolding beta_sscase by (simp add: Rep_Ssum_sinl) +unfolding beta_sscase by (simp add: Rep_ssum_sinl) lemma sscase3 [simp]: "y \ \ \ sscase\f\g\(sinr\y) = g\y" -unfolding beta_sscase by (simp add: Rep_Ssum_sinr) +unfolding beta_sscase by (simp add: Rep_ssum_sinr) lemma sscase4 [simp]: "sscase\sinl\sinr\z = z" by (cases z, simp_all)