35 ssnd :: "('a ** 'b) \<rightarrow> 'b" where |
35 ssnd :: "('a ** 'b) \<rightarrow> 'b" where |
36 "ssnd = (\<Lambda> p. snd (Rep_sprod p))" |
36 "ssnd = (\<Lambda> p. snd (Rep_sprod p))" |
37 |
37 |
38 definition |
38 definition |
39 spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where |
39 spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where |
40 "spair = (\<Lambda> a b. Abs_sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b))" |
40 "spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))" |
41 |
41 |
42 definition |
42 definition |
43 ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where |
43 ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where |
44 "ssplit = (\<Lambda> f p. strict\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" |
44 "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" |
45 |
45 |
46 syntax |
46 syntax |
47 "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") |
47 "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") |
48 translations |
48 translations |
49 "(:x, y, z:)" == "(:x, (:y, z:):)" |
49 "(:x, y, z:)" == "(:x, (:y, z:):)" |
52 translations |
52 translations |
53 "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)" |
53 "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)" |
54 |
54 |
55 subsection {* Case analysis *} |
55 subsection {* Case analysis *} |
56 |
56 |
57 lemma spair_sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> sprod" |
57 lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod" |
58 by (simp add: sprod_def strict_conv_if) |
58 by (simp add: sprod_def seq_conv_if) |
59 |
59 |
60 lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)" |
60 lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)" |
61 by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) |
61 by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) |
62 |
62 |
63 lemmas Rep_sprod_simps = |
63 lemmas Rep_sprod_simps = |
64 Rep_sprod_inject [symmetric] below_sprod_def |
64 Rep_sprod_inject [symmetric] below_sprod_def |
65 Pair_fst_snd_eq below_prod_def |
65 Pair_fst_snd_eq below_prod_def |
80 |
80 |
81 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
81 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
82 by (simp add: Rep_sprod_simps) |
82 by (simp add: Rep_sprod_simps) |
83 |
83 |
84 lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)" |
84 lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)" |
85 by (simp add: Rep_sprod_simps strict_conv_if) |
85 by (simp add: Rep_sprod_simps seq_conv_if) |
86 |
86 |
87 lemma spair_below_iff: |
87 lemma spair_below_iff: |
88 "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))" |
88 "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))" |
89 by (simp add: Rep_sprod_simps strict_conv_if) |
89 by (simp add: Rep_sprod_simps seq_conv_if) |
90 |
90 |
91 lemma spair_eq_iff: |
91 lemma spair_eq_iff: |
92 "((:a, b:) = (:c, d:)) = |
92 "((:a, b:) = (:c, d:)) = |
93 (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))" |
93 (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))" |
94 by (simp add: Rep_sprod_simps strict_conv_if) |
94 by (simp add: Rep_sprod_simps seq_conv_if) |
95 |
95 |
96 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" |
96 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" |
97 by simp |
97 by simp |
98 |
98 |
99 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
99 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
175 |
175 |
176 lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)" |
176 lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)" |
177 by (rule compactI, simp add: ssnd_below_iff) |
177 by (rule compactI, simp add: ssnd_below_iff) |
178 |
178 |
179 lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)" |
179 lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)" |
180 by (rule compact_sprod, simp add: Rep_sprod_spair strict_conv_if) |
180 by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if) |
181 |
181 |
182 lemma compact_spair_iff: |
182 lemma compact_spair_iff: |
183 "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))" |
183 "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))" |
184 apply (safe elim!: compact_spair) |
184 apply (safe elim!: compact_spair) |
185 apply (drule compact_sfst, simp) |
185 apply (drule compact_sfst, simp) |