added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
authorhuffman
Fri Jul 08 02:39:53 2005 +0200 (2005-07-08)
changeset 16752270ec60cc9e8
parent 16751 7af6723ad741
child 16753 fb6801c926d2
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
src/HOLCF/Ssum.ML
src/HOLCF/Ssum.thy
     1.1 --- a/src/HOLCF/Ssum.ML	Fri Jul 08 02:38:05 2005 +0200
     1.2 +++ b/src/HOLCF/Ssum.ML	Fri Jul 08 02:39:53 2005 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4  val cont_Iwhen3 = thm "cont_Iwhen3";
     1.5  val sinl_strict = thm "sinl_strict";
     1.6  val sinr_strict = thm "sinr_strict";
     1.7 -val noteq_sinlsinr = thm "noteq_sinlsinr";
     1.8  val sinl_inject = thm "sinl_inject";
     1.9  val sinr_inject = thm "sinr_inject";
    1.10  val sinl_eq = thm "sinl_eq";
     2.1 --- a/src/HOLCF/Ssum.thy	Fri Jul 08 02:38:05 2005 +0200
     2.2 +++ b/src/HOLCF/Ssum.thy	Fri Jul 08 02:39:53 2005 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4    "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
     2.5  
     2.6  lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>"
     2.7 -by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric])
     2.8 +by (simp add: Abs_Ssum_strict cpair_strict)
     2.9  
    2.10  
    2.11  subsection {* Definitions of constructors *}
    2.12 @@ -52,47 +52,46 @@
    2.13  by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
    2.14  
    2.15  lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
    2.16 -by (simp add: sinl_Abs_Ssum UU_Abs_Ssum)
    2.17 +by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)
    2.18  
    2.19  lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
    2.20 -by (simp add: sinr_Abs_Ssum UU_Abs_Ssum)
    2.21 +by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict)
    2.22  
    2.23 -lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
    2.24 -apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
    2.25 -apply (simp add: Abs_Ssum_inject Ssum_def)
    2.26 -done
    2.27 -
    2.28 -lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
    2.29 +lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
    2.30  by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
    2.31  
    2.32 -lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
    2.33 +lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
    2.34  by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
    2.35  
    2.36 -lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
    2.37 -by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
    2.38 +lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
    2.39 +by (rule sinl_eq [THEN iffD1])
    2.40  
    2.41 -lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
    2.42 -by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
    2.43 +lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
    2.44 +by (rule sinr_eq [THEN iffD1])
    2.45  
    2.46 -lemma sinl_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
    2.47 -apply (erule contrapos_nn)
    2.48 -apply (rule sinl_inject)
    2.49 -apply auto
    2.50 +lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
    2.51 +apply (rule sinl_strict [THEN subst])
    2.52 +apply (rule sinl_eq)
    2.53  done
    2.54  
    2.55 -lemma sinr_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
    2.56 -apply (erule contrapos_nn)
    2.57 -apply (rule sinr_inject)
    2.58 -apply auto
    2.59 +lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
    2.60 +apply (rule sinr_strict [THEN subst])
    2.61 +apply (rule sinr_eq)
    2.62  done
    2.63  
    2.64 +lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
    2.65 +by simp
    2.66 +
    2.67 +lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
    2.68 +by simp
    2.69 +
    2.70  subsection {* Case analysis *}
    2.71  
    2.72  lemma Exh_Ssum1: 
    2.73    "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"
    2.74 +apply (rule_tac x=z in Abs_Ssum_induct)
    2.75 +apply (rule_tac p=y in cprodE)
    2.76  apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum)
    2.77 -apply (rule_tac x=z in Abs_Ssum_cases)
    2.78 -apply (rule_tac p=y in cprodE)
    2.79  apply (auto simp add: Ssum_def)
    2.80  done
    2.81  
    2.82 @@ -112,32 +111,38 @@
    2.83  
    2.84  subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
    2.85  
    2.86 -lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
    2.87 +lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
    2.88  by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
    2.89  
    2.90 -lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
    2.91 +lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
    2.92  by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
    2.93  
    2.94 -lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
    2.95 +lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
    2.96 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    2.97 +
    2.98 +lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
    2.99  by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
   2.100  
   2.101 -lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
   2.102 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
   2.103 +lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
   2.104 +by (simp add: po_eq_conv)
   2.105 +
   2.106 +lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
   2.107 +by (simp add: po_eq_conv)
   2.108  
   2.109  subsection {* Chains of strict sums *}
   2.110  
   2.111  lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
   2.112  apply (rule_tac p=p in ssumE)
   2.113  apply (rule_tac x="\<bottom>" in exI, simp)
   2.114 -apply (simp add: sinl_less sinl_eq)
   2.115 -apply (simp add: sinr_less_sinl)
   2.116 +apply simp
   2.117 +apply simp
   2.118  done
   2.119  
   2.120  lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
   2.121  apply (rule_tac p=p in ssumE)
   2.122  apply (rule_tac x="\<bottom>" in exI, simp)
   2.123 -apply (simp add: sinl_less_sinr)
   2.124 -apply (simp add: sinr_less sinr_eq)
   2.125 +apply simp
   2.126 +apply simp
   2.127  done
   2.128  
   2.129  lemma ssum_chain_lemma:
   2.130 @@ -151,7 +156,7 @@
   2.131     apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
   2.132    apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
   2.133    apply (drule less_sinlD, clarify)
   2.134 -  apply (simp add: sinl_eq Rep_Ssum_sinl)
   2.135 +  apply (simp add: Rep_Ssum_sinl)
   2.136   apply (rule disjI2)
   2.137   apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI)
   2.138   apply (rule conjI)
   2.139 @@ -159,7 +164,7 @@
   2.140    apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
   2.141   apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
   2.142   apply (drule less_sinrD, clarify)
   2.143 - apply (simp add: sinr_eq Rep_Ssum_sinr)
   2.144 + apply (simp add: Rep_Ssum_sinr)
   2.145  done
   2.146  
   2.147  subsection {* Definitions of constants *}