42 spair_def: "spair \<equiv> \<Lambda> a b. Abs_Sprod |
42 spair_def: "spair \<equiv> \<Lambda> a b. Abs_Sprod |
43 <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
43 <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
44 ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p))" |
44 ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. 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 |
48 |
49 translations |
49 translations |
50 "(:x, y, z:)" == "(:x, (:y, z:):)" |
50 "(:x, y, z:)" == "(:x, (:y, z:):)" |
51 "(:x, y:)" == "spair$x$y" |
51 "(:x, y:)" == "spair\<cdot>x\<cdot>y" |
|
52 |
|
53 translations |
|
54 "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)" |
52 |
55 |
53 subsection {* Case analysis *} |
56 subsection {* Case analysis *} |
54 |
57 |
55 lemma spair_Abs_Sprod: |
58 lemma spair_Abs_Sprod: |
56 "(:a, b:) = Abs_Sprod <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
59 "(:a, b:) = Abs_Sprod <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
89 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
92 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
90 by (erule contrapos_np, auto) |
93 by (erule contrapos_np, auto) |
91 |
94 |
92 lemma spair_defined [simp]: |
95 lemma spair_defined [simp]: |
93 "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
96 "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
94 by (simp add: spair_Abs_Sprod Abs_Sprod_defined cpair_defined_iff Sprod_def) |
97 by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def) |
95 |
98 |
96 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" |
99 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" |
97 by (erule contrapos_pp, simp) |
100 by (erule contrapos_pp, simp) |
98 |
101 |
99 lemma spair_eq: |
102 lemma spair_eq: |