# HG changeset patch
# User huffman
# Date 1117834188 -7200
# Node ID 422f836f6b3988e591a10c4be187e0c9d5c3ef7d
# Parent  faa9691da2bcf2dabba3bd01dfa42540e593d846
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair

diff -r faa9691da2bc -r 422f836f6b39 src/HOLCF/Sprod.ML
--- a/src/HOLCF/Sprod.ML	Fri Jun 03 23:28:21 2005 +0200
+++ b/src/HOLCF/Sprod.ML	Fri Jun 03 23:29:48 2005 +0200
@@ -6,21 +6,21 @@
 val sfst_def = thm "sfst_def";
 val ssnd_def = thm "ssnd_def";
 val ssplit_def = thm "ssplit_def";
-val inject_spair = thm "inject_spair";
+val spair_inject = thm "spair_inject";
 val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
-val strict_spair = thm "strict_spair";
-val strict_spair1 = thm "strict_spair1";
-val strict_spair2 = thm "strict_spair2";
-val strict_spair_rev = thm "strict_spair_rev";
-val defined_spair_rev = thm "defined_spair_rev";
-val defined_spair = thm "defined_spair";
+val spair_strict = thm "spair_strict";
+val spair_strict1 = thm "spair_strict1";
+val spair_strict2 = thm "spair_strict2";
+val spair_strict_rev = thm "spair_strict_rev";
+val spair_defined_rev = thm "spair_defined_rev";
+val spair_defined = thm "spair_defined";
 val Exh_Sprod2 = thm "Exh_Sprod2";
 val sprodE = thm "sprodE";
-val strict_sfst = thm "strict_sfst";
-val strict_ssnd = thm "strict_ssnd";
-val sfst2 = thm "sfst2";
-val ssnd2 = thm "ssnd2";
-val defined_sfstssnd = thm "defined_sfstssnd";
+val sfst_strict = thm "sfst_strict";
+val ssnd_strict = thm "ssnd_strict";
+val sfst_spair = thm "sfst_spair";
+val ssnd_spair = thm "ssnd_spair";
+val sfstssnd_defined = thm "sfstssnd_defined";
 val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
 val ssplit1 = thm "ssplit1";
 val ssplit2 = thm "ssplit2";
diff -r faa9691da2bc -r 422f836f6b39 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Jun 03 23:28:21 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Fri Jun 03 23:29:48 2005 +0200
@@ -51,20 +51,18 @@
 lemmas cont_Abs_Sprod = 
   typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod]
 
-lemmas strict_Rep_Sprod =
-  typedef_strict_Rep [OF type_definition_Sprod less_sprod_def UU_Sprod]
+lemmas Rep_Sprod_strict =
+  typedef_Rep_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
 
-lemmas strict_Abs_Sprod =
-  typedef_strict_Abs [OF type_definition_Sprod less_sprod_def UU_Sprod]
+lemmas Abs_Sprod_strict =
+  typedef_Abs_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
 
 lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
-by (simp add: strict_Abs_Sprod inst_cprod_pcpo2 [symmetric])
+by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
 
 lemma spair_lemma:
   "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
-apply (simp add: Sprod_def inst_cprod_pcpo2)
-apply (case_tac "a = \<bottom>", case_tac [!] "b = \<bottom>", simp_all)
-done
+by (simp add: Sprod_def strictify_conv_if cpair_strict)
 
 subsection {* Definitions of constants *}
 
@@ -101,7 +99,7 @@
 apply (rule_tac x=z in Abs_Sprod_cases)
 apply (simp add: Sprod_def)
 apply (erule disjE)
-apply (simp add: strict_Abs_Sprod)
+apply (simp add: Abs_Sprod_strict)
 apply (rule disjI2)
 apply (rule_tac x="cfst\<cdot>y" in exI)
 apply (rule_tac x="csnd\<cdot>y" in exI)
@@ -115,23 +113,19 @@
 
 subsection {* Properties of @{term spair} *}
 
-lemma strict_spair1 [simp]: "(:\<bottom>, b:) = \<bottom>"
-apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
-apply (case_tac "b = \<bottom>", simp_all)
-done
+lemma spair_strict1 [simp]: "(:\<bottom>, b:) = \<bottom>"
+by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
 
-lemma strict_spair2 [simp]: "(:a, \<bottom>:) = \<bottom>"
-apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
-apply (case_tac "a = \<bottom>", simp_all)
-done
+lemma spair_strict2 [simp]: "(:a, \<bottom>:) = \<bottom>"
+by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
 
-lemma strict_spair: "a = \<bottom> \<or> b = \<bottom> \<Longrightarrow> (:a, b:) = \<bottom>"
+lemma spair_strict: "a = \<bottom> \<or> b = \<bottom> \<Longrightarrow> (:a, b:) = \<bottom>"
 by auto
 
-lemma strict_spair_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
+lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
 by (erule contrapos_np, auto)
 
-lemma defined_spair [simp]: 
+lemma spair_defined [simp]: 
   "\<lbrakk>a \<noteq> \<bottom>; b \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:a, b:) \<noteq> \<bottom>"
 apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
 apply (subst Abs_Sprod_inject)
@@ -140,15 +134,14 @@
 apply simp
 done
 
-lemma defined_spair_rev: "(:a, b:) = \<bottom> \<Longrightarrow> a = \<bottom> \<or> b = \<bottom>"
+lemma spair_defined_rev: "(:a, b:) = \<bottom> \<Longrightarrow> a = \<bottom> \<or> b = \<bottom>"
 by (erule contrapos_pp, simp)
 
-lemma inject_spair: 
+lemma spair_inject:
   "\<lbrakk>aa \<noteq> \<bottom>; ba \<noteq> \<bottom>; (:a,b:) = (:aa,ba:)\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba"
 apply (simp add: spair_Abs_Sprod)
 apply (simp add: Abs_Sprod_inject [OF spair_lemma] Sprod_def)
-apply (case_tac "a = \<bottom>", simp_all)
-apply (case_tac "b = \<bottom>", simp_all)
+apply (simp add: strictify_conv_if split: split_if_asm)
 done
 
 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
@@ -156,11 +149,11 @@
 
 subsection {* Properties of @{term sfst} and @{term ssnd} *}
 
-lemma strict_sfst [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
-by (simp add: sfst_def cont_Rep_Sprod strict_Rep_Sprod)
+lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
+by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
 
-lemma strict_ssnd [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
-by (simp add: ssnd_def cont_Rep_Sprod strict_Rep_Sprod)
+lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
+by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
 
 lemma Rep_Sprod_spair:
   "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
@@ -168,13 +161,13 @@
 apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
 done
 
-lemma sfst2 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
+lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
 by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
 
-lemma ssnd2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
+lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
 by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
 
-lemma defined_sfstssnd: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
+lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
 by (rule_tac p=p in sprodE, simp_all)
  
 lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"