# HG changeset patch
# User huffman
# Date 1120183767 -7200
# Node ID 83bf468b1dc797ee49e6187e7b5646258216606d
# Parent  91a179d4b0d509d01690ec1dda7a18d899d3dfa8
added theorem lift_definedE; moved cont_if to Cont.thy

diff -r 91a179d4b0d5 -r 83bf468b1dc7 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Fri Jul 01 04:02:22 2005 +0200
+++ b/src/HOLCF/Lift.thy	Fri Jul 01 04:09:27 2005 +0200
@@ -161,14 +161,17 @@
 lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)"
   by (cases x) simp_all
 
+lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by (cases x) simp_all
+
 text {*
   For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
   x} by @{text "Def a"} in conclusion. *}
 
 ML {*
-  local val not_Undef_is_Def = thm "not_Undef_is_Def"
+  local val lift_definedE = thm "lift_definedE"
   in val def_tac = SIMPSET' (fn ss =>
-    etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
+    etac lift_definedE THEN' asm_simp_tac ss)
   end;
 *}
 
@@ -216,12 +219,6 @@
   apply assumption
   done
 
-text {* Continuity of if-then-else. *}
-
-lemma cont_if: "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)"
-  by (cases b) simp_all
-
-
 subsection {* Continuity Proofs for flift1, flift2, if *}
 
 text {* Need the instance of @{text flat}. *}