renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
authorhuffman
Fri Jun 03 23:29:48 2005 +0200 (2005-06-03)
changeset 16212422f836f6b39
parent 16211 faa9691da2bc
child 16213 88ddef269510
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
src/HOLCF/Sprod.ML
src/HOLCF/Sprod.thy
     1.1 --- a/src/HOLCF/Sprod.ML	Fri Jun 03 23:28:21 2005 +0200
     1.2 +++ b/src/HOLCF/Sprod.ML	Fri Jun 03 23:29:48 2005 +0200
     1.3 @@ -6,21 +6,21 @@
     1.4  val sfst_def = thm "sfst_def";
     1.5  val ssnd_def = thm "ssnd_def";
     1.6  val ssplit_def = thm "ssplit_def";
     1.7 -val inject_spair = thm "inject_spair";
     1.8 +val spair_inject = thm "spair_inject";
     1.9  val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
    1.10 -val strict_spair = thm "strict_spair";
    1.11 -val strict_spair1 = thm "strict_spair1";
    1.12 -val strict_spair2 = thm "strict_spair2";
    1.13 -val strict_spair_rev = thm "strict_spair_rev";
    1.14 -val defined_spair_rev = thm "defined_spair_rev";
    1.15 -val defined_spair = thm "defined_spair";
    1.16 +val spair_strict = thm "spair_strict";
    1.17 +val spair_strict1 = thm "spair_strict1";
    1.18 +val spair_strict2 = thm "spair_strict2";
    1.19 +val spair_strict_rev = thm "spair_strict_rev";
    1.20 +val spair_defined_rev = thm "spair_defined_rev";
    1.21 +val spair_defined = thm "spair_defined";
    1.22  val Exh_Sprod2 = thm "Exh_Sprod2";
    1.23  val sprodE = thm "sprodE";
    1.24 -val strict_sfst = thm "strict_sfst";
    1.25 -val strict_ssnd = thm "strict_ssnd";
    1.26 -val sfst2 = thm "sfst2";
    1.27 -val ssnd2 = thm "ssnd2";
    1.28 -val defined_sfstssnd = thm "defined_sfstssnd";
    1.29 +val sfst_strict = thm "sfst_strict";
    1.30 +val ssnd_strict = thm "ssnd_strict";
    1.31 +val sfst_spair = thm "sfst_spair";
    1.32 +val ssnd_spair = thm "ssnd_spair";
    1.33 +val sfstssnd_defined = thm "sfstssnd_defined";
    1.34  val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
    1.35  val ssplit1 = thm "ssplit1";
    1.36  val ssplit2 = thm "ssplit2";
     2.1 --- a/src/HOLCF/Sprod.thy	Fri Jun 03 23:28:21 2005 +0200
     2.2 +++ b/src/HOLCF/Sprod.thy	Fri Jun 03 23:29:48 2005 +0200
     2.3 @@ -51,20 +51,18 @@
     2.4  lemmas cont_Abs_Sprod = 
     2.5    typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod]
     2.6  
     2.7 -lemmas strict_Rep_Sprod =
     2.8 -  typedef_strict_Rep [OF type_definition_Sprod less_sprod_def UU_Sprod]
     2.9 +lemmas Rep_Sprod_strict =
    2.10 +  typedef_Rep_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
    2.11  
    2.12 -lemmas strict_Abs_Sprod =
    2.13 -  typedef_strict_Abs [OF type_definition_Sprod less_sprod_def UU_Sprod]
    2.14 +lemmas Abs_Sprod_strict =
    2.15 +  typedef_Abs_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
    2.16  
    2.17  lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
    2.18 -by (simp add: strict_Abs_Sprod inst_cprod_pcpo2 [symmetric])
    2.19 +by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
    2.20  
    2.21  lemma spair_lemma:
    2.22    "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
    2.23 -apply (simp add: Sprod_def inst_cprod_pcpo2)
    2.24 -apply (case_tac "a = \<bottom>", case_tac [!] "b = \<bottom>", simp_all)
    2.25 -done
    2.26 +by (simp add: Sprod_def strictify_conv_if cpair_strict)
    2.27  
    2.28  subsection {* Definitions of constants *}
    2.29  
    2.30 @@ -101,7 +99,7 @@
    2.31  apply (rule_tac x=z in Abs_Sprod_cases)
    2.32  apply (simp add: Sprod_def)
    2.33  apply (erule disjE)
    2.34 -apply (simp add: strict_Abs_Sprod)
    2.35 +apply (simp add: Abs_Sprod_strict)
    2.36  apply (rule disjI2)
    2.37  apply (rule_tac x="cfst\<cdot>y" in exI)
    2.38  apply (rule_tac x="csnd\<cdot>y" in exI)
    2.39 @@ -115,23 +113,19 @@
    2.40  
    2.41  subsection {* Properties of @{term spair} *}
    2.42  
    2.43 -lemma strict_spair1 [simp]: "(:\<bottom>, b:) = \<bottom>"
    2.44 -apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
    2.45 -apply (case_tac "b = \<bottom>", simp_all)
    2.46 -done
    2.47 +lemma spair_strict1 [simp]: "(:\<bottom>, b:) = \<bottom>"
    2.48 +by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
    2.49  
    2.50 -lemma strict_spair2 [simp]: "(:a, \<bottom>:) = \<bottom>"
    2.51 -apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
    2.52 -apply (case_tac "a = \<bottom>", simp_all)
    2.53 -done
    2.54 +lemma spair_strict2 [simp]: "(:a, \<bottom>:) = \<bottom>"
    2.55 +by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
    2.56  
    2.57 -lemma strict_spair: "a = \<bottom> \<or> b = \<bottom> \<Longrightarrow> (:a, b:) = \<bottom>"
    2.58 +lemma spair_strict: "a = \<bottom> \<or> b = \<bottom> \<Longrightarrow> (:a, b:) = \<bottom>"
    2.59  by auto
    2.60  
    2.61 -lemma strict_spair_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
    2.62 +lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
    2.63  by (erule contrapos_np, auto)
    2.64  
    2.65 -lemma defined_spair [simp]: 
    2.66 +lemma spair_defined [simp]: 
    2.67    "\<lbrakk>a \<noteq> \<bottom>; b \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:a, b:) \<noteq> \<bottom>"
    2.68  apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
    2.69  apply (subst Abs_Sprod_inject)
    2.70 @@ -140,15 +134,14 @@
    2.71  apply simp
    2.72  done
    2.73  
    2.74 -lemma defined_spair_rev: "(:a, b:) = \<bottom> \<Longrightarrow> a = \<bottom> \<or> b = \<bottom>"
    2.75 +lemma spair_defined_rev: "(:a, b:) = \<bottom> \<Longrightarrow> a = \<bottom> \<or> b = \<bottom>"
    2.76  by (erule contrapos_pp, simp)
    2.77  
    2.78 -lemma inject_spair: 
    2.79 +lemma spair_inject:
    2.80    "\<lbrakk>aa \<noteq> \<bottom>; ba \<noteq> \<bottom>; (:a,b:) = (:aa,ba:)\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba"
    2.81  apply (simp add: spair_Abs_Sprod)
    2.82  apply (simp add: Abs_Sprod_inject [OF spair_lemma] Sprod_def)
    2.83 -apply (case_tac "a = \<bottom>", simp_all)
    2.84 -apply (case_tac "b = \<bottom>", simp_all)
    2.85 +apply (simp add: strictify_conv_if split: split_if_asm)
    2.86  done
    2.87  
    2.88  lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
    2.89 @@ -156,11 +149,11 @@
    2.90  
    2.91  subsection {* Properties of @{term sfst} and @{term ssnd} *}
    2.92  
    2.93 -lemma strict_sfst [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
    2.94 -by (simp add: sfst_def cont_Rep_Sprod strict_Rep_Sprod)
    2.95 +lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
    2.96 +by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
    2.97  
    2.98 -lemma strict_ssnd [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
    2.99 -by (simp add: ssnd_def cont_Rep_Sprod strict_Rep_Sprod)
   2.100 +lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
   2.101 +by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
   2.102  
   2.103  lemma Rep_Sprod_spair:
   2.104    "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
   2.105 @@ -168,13 +161,13 @@
   2.106  apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
   2.107  done
   2.108  
   2.109 -lemma sfst2 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
   2.110 +lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
   2.111  by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
   2.112  
   2.113 -lemma ssnd2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
   2.114 +lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
   2.115  by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
   2.116  
   2.117 -lemma defined_sfstssnd: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
   2.118 +lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
   2.119  by (rule_tac p=p in sprodE, simp_all)
   2.120   
   2.121  lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"