author huffman Fri, 01 Jul 2005 04:09:27 +0200 changeset 16630 83bf468b1dc7 parent 16629 91a179d4b0d5 child 16631 58b4a689ae85
added theorem lift_definedE; moved cont_if to Cont.thy
 src/HOLCF/Lift.thy file | annotate | diff | comparison | revisions
```--- 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}. *}```