declare upE as cases rule; add new rule up_induct
authorhuffman
Wed Jan 02 19:51:29 2008 +0100 (2008-01-02)
changeset 2578830cbe0764599
parent 25787 398dec10518e
child 25789 c0506ac5b6b4
declare upE as cases rule; add new rule up_induct
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Up.thy	Wed Jan 02 19:41:12 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jan 02 19:51:29 2008 +0100
     1.3 @@ -236,12 +236,15 @@
     1.4  lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
     1.5  by (simp add: up_def cont_Iup)
     1.6  
     1.7 -lemma upE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
     1.8 -apply (case_tac p)
     1.9 +lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.10 +apply (cases p)
    1.11  apply (simp add: inst_up_pcpo)
    1.12  apply (simp add: up_def cont_Iup)
    1.13  done
    1.14  
    1.15 +lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
    1.16 +by (cases x, simp_all)
    1.17 +
    1.18  lemma up_chain_cases:
    1.19    "chain Y \<Longrightarrow>
    1.20    (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
    1.21 @@ -269,6 +272,6 @@
    1.22  by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
    1.23  
    1.24  lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
    1.25 -by (rule_tac p=x in upE, simp_all)
    1.26 +by (cases x, simp_all)
    1.27  
    1.28  end