author huffman Tue, 15 Jan 2008 02:20:47 +0100 changeset 25914 ff835e25ae87 parent 25913 e1b6521c1f94 child 25915 f1bce5261dec
clean up some proofs; add lemmas spair_strict_iff, spair_less_iff, spair_eq_iff; add instance for class bifinite
 src/HOLCF/Sprod.thy file | annotate | diff | comparison | revisions
--- a/src/HOLCF/Sprod.thy	Tue Jan 15 02:18:01 2008 +0100
+++ b/src/HOLCF/Sprod.thy	Tue Jan 15 02:20:47 2008 +0100
@@ -32,7 +32,7 @@

lemma spair_lemma:
"<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
-by (simp add: Sprod_def strictify_conv_if cpair_strict)

subsection {* Definitions of constants *}

@@ -64,23 +64,23 @@

subsection {* Case analysis *}

-lemma spair_Abs_Sprod:
-  "(:a, b:) = Abs_Sprod <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
-apply (unfold spair_def)
-done
+lemma Rep_Sprod_spair:
+  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
+unfolding spair_def
+by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
+
+lemmas Rep_Sprod_simps =
+  Rep_Sprod_inject [symmetric] less_Sprod_def
+  Rep_Sprod_strict Rep_Sprod_spair

lemma Exh_Sprod2:
"z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
-apply (cases z rule: Abs_Sprod_cases)
+apply (insert Rep_Sprod [of z])
-apply (erule disjE)
-apply (rule disjI2)
-apply (rule_tac x="cfst\<cdot>y" in exI)
-apply (rule_tac x="csnd\<cdot>y" in exI)
-apply (simp add: spair_Abs_Sprod Abs_Sprod_inject spair_lemma)
+apply (erule disjE, simp)
+apply fast
done

lemma sprodE [cases type: **]:
@@ -94,30 +94,38 @@
subsection {* Properties of @{term spair} *}

lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)

lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
+
+lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
+
+lemma spair_less_iff:
+  "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
+
+lemma spair_eq_iff:
+  "((:a, b:) = (:c, d:)) =
+    (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"

lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
-by auto
+by simp

lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
-by (erule contrapos_np, auto)
+by simp

-lemma spair_defined [simp]:
-  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
-by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def)
+lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
+by simp

lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
-by (erule contrapos_pp, simp)
+by simp

lemma spair_eq:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
-apply (simp add: Abs_Sprod_inject [OF _ spair_lemma] Sprod_def)
-done

lemma spair_inject:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
@@ -126,12 +134,6 @@
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
by simp

-lemma Rep_Sprod_spair:
-  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
-apply (unfold spair_def)
-apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
-done
-
subsection {* Properties of @{term sfst} and @{term ssnd} *}

lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
@@ -226,4 +228,40 @@
done

+subsection {* Strict product is a bifinite domain *}
+
+instance "**" :: (bifinite, bifinite) approx ..
+
+  approx_sprod_def:
+    "approx \<equiv> \<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:)"
+
+instance "**" :: (bifinite, bifinite) bifinite
+proof
+  fix i :: nat and x :: "'a \<otimes> 'b"
+  show "chain (\<lambda>i. approx i\<cdot>x)"
+    unfolding approx_sprod_def by simp
+  show "(\<Squnion>i. approx i\<cdot>x) = x"
+    unfolding approx_sprod_def
+    by (simp add: lub_distribs eta_cfun)
+  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+    unfolding approx_sprod_def
+    by (simp add: ssplit_def strictify_conv_if)
+  have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
+    unfolding approx_sprod_def
+    apply (clarify, rule_tac p=x in sprodE)
+    apply (simp add: Rep_Sprod_spair spair_eq_iff)
+    done
+  hence "finite (Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x})"
+    using finite_fixes_approx by (rule finite_subset)
+  thus "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
+    by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
+qed
+
+lemma approx_spair [simp]:
+  "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
+unfolding approx_sprod_def