# HG changeset patch
# User huffman
# Date 1119557515 -7200
# Node ID a0c8d0499b5f30142af4afe9ae1a1758ef19b51a
# Parent  cec3fbf9832bbffd9b959582fe2b0857f685d449
added theorems fix_strict, fix_defined, fix_id, fix_const

diff -r cec3fbf9832b -r a0c8d0499b5f src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Thu Jun 23 22:10:29 2005 +0200
+++ b/src/HOLCF/Fix.thy	Thu Jun 23 22:11:55 2005 +0200
@@ -159,6 +159,25 @@
 apply (simp add: Ifix_def)
 done
 
+text {* strictness of @{term fix} *}
+
+lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
+by (rule fix_least [THEN UU_I])
+
+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
+
+text {* @{term fix} applied to identity and constant functions *}
+
+lemma fix_id: "(\<mu> x. x) = \<bottom>"
+by (simp add: fix_strict)
+
+lemma fix_const: "(\<mu> x. c) = c"
+by (rule fix_eq [THEN trans], simp)
+
 subsection {* Admissibility and fixed point induction *}
 
 text {* an admissible formula is also weak admissible *}