# HG changeset patch
# User huffman
# Date 1122394975 -7200
# Node ID 1fe50b19dabae956ad992b078c8c25a9e5cd47ee
# Parent  da331e0a4a81265939ff8c60d8bd95dfeea4ff97
add theorem fix_defined_iff; cleaned up

diff -r da331e0a4a81 -r 1fe50b19daba src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Jul 26 18:22:03 2005 +0200
+++ b/src/HOLCF/Fix.thy	Tue Jul 26 18:22:55 2005 +0200
@@ -29,8 +29,8 @@
   Ifix_def:      "Ifix \<equiv> \<lambda>F. \<Squnion>i. iterate i F \<bottom>"
   fix_def:       "fix \<equiv> \<Lambda> F. Ifix F"
 
-  admw_def:      "admw P == !F. (!n. P (iterate n F UU)) -->
-                            P (lub(range (%i. iterate i F UU)))" 
+  admw_def:      "admw P \<equiv> \<forall>F. (\<forall>n. P (iterate n F \<bottom>)) \<longrightarrow>
+                            P (\<Squnion>i. iterate i F \<bottom>)" 
 
 subsection {* Binder syntax for @{term fix} *}
 
@@ -161,14 +161,18 @@
 
 text {* strictness of @{term fix} *}
 
+lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
+apply (rule iffI)
+apply (erule subst)
+apply (rule fix_eq [symmetric])
+apply (erule fix_least [THEN UU_I])
+done
+
 lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
-by (rule fix_least [THEN UU_I])
+by (simp add: fix_defined_iff)
 
 lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
-apply (erule contrapos_nn)
-apply (erule subst)
-apply (rule fix_eq [symmetric])
-done
+by (simp add: fix_defined_iff)
 
 text {* @{term fix} applied to identity and constant functions *}