# HG changeset patch
# User huffman
# Date 1213977655 -7200
# Node ID de9a2fd0eab448144a5478bfb957194f91021dc9
# Parent  7be07972600980118c9a49f0760c36a4ecc2a950
added some lemmas; tuned proofs

diff -r 7be079726009 -r de9a2fd0eab4 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Fri Jun 20 17:58:16 2008 +0200
+++ b/src/HOLCF/One.thy	Fri Jun 20 18:00:55 2008 +0200
@@ -22,29 +22,34 @@
 text {* Exhaustion and Elimination for type @{typ one} *}
 
 lemma Exh_one: "t = \<bottom> \<or> t = ONE"
-apply (unfold ONE_def)
-apply (induct t)
-apply simp
-apply simp
-done
+unfolding ONE_def by (induct t) simp_all
 
 lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-apply (rule Exh_one [THEN disjE])
-apply fast
-apply fast
-done
+unfolding ONE_def by (induct p) simp_all
+
+lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
+by (cases x rule: oneE) simp_all
 
 lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
-apply (unfold ONE_def)
-apply simp
-done
+unfolding ONE_def by simp
+
+lemma less_ONE [simp]: "x \<sqsubseteq> ONE"
+by (induct x rule: one_induct) simp_all
+
+lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
+by (induct x rule: one_induct) simp_all
 
 lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
-apply (unfold ONE_def)
-apply simp_all
-done
+unfolding ONE_def by simp_all
 
-lemma compact_ONE [simp]: "compact ONE"
+lemma one_neq_iffs [simp]:
+  "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
+  "ONE \<noteq> x \<longleftrightarrow> x = \<bottom>"
+  "x \<noteq> \<bottom> \<longleftrightarrow> x = ONE"
+  "\<bottom> \<noteq> x \<longleftrightarrow> x = ONE"
+by (induct x rule: one_induct) simp_all
+
+lemma compact_ONE: "compact ONE"
 by (rule compact_chfin)
 
 text {* Case analysis function for type @{typ one} *}
@@ -54,8 +59,8 @@
   "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
 
 translations
-  "case x of CONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
-  "\<Lambda> (CONST ONE). t" == "CONST one_when\<cdot>t"
+  "case x of XCONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
+  "\<Lambda> (XCONST ONE). t" == "CONST one_when\<cdot>t"
 
 lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
 by (simp add: one_when_def)
@@ -64,6 +69,6 @@
 by (simp add: one_when_def)
 
 lemma one_when3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
-by (rule_tac p=x in oneE, simp_all)
+by (induct x rule: one_induct) simp_all
 
 end