# HG changeset patch
# User huffman
# Date 1199299889 -3600
# Node ID 30cbe076459902b9d9da32f15478086907b9470b
# Parent  398dec10518ed7fd248e3be96be2eeb54ff25a18
declare upE as cases rule; add new rule up_induct

diff -r 398dec10518e -r 30cbe0764599 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Jan 02 19:41:12 2008 +0100
+++ b/src/HOLCF/Up.thy	Wed Jan 02 19:51:29 2008 +0100
@@ -236,12 +236,15 @@
 lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: up_def cont_Iup)
 
-lemma upE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-apply (case_tac p)
+lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+apply (cases p)
 apply (simp add: inst_up_pcpo)
 apply (simp add: up_def cont_Iup)
 done
 
+lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
+by (cases x, simp_all)
+
 lemma up_chain_cases:
   "chain Y \<Longrightarrow>
   (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
@@ -269,6 +272,6 @@
 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
 
 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
-by (rule_tac p=x in upE, simp_all)
+by (cases x, simp_all)
 
 end