# HG changeset patch
# User nipkow
# Date 859481184 -3600
# Node ID 53c76f9d95fdb79a48609b6abc418edabf05fa43
# Parent  b4f8df0efa6c9716e7b9df55351d5b6898dc6a57
Optimized proofs.

diff -r b4f8df0efa6c -r 53c76f9d95fd src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Thu Mar 27 10:08:31 1997 +0100
+++ b/src/HOLCF/IMP/Denotational.ML	Thu Mar 27 17:46:24 1997 +0100
@@ -16,10 +16,11 @@
 qed "cont_dlift";
 AddIffs [cont_dlift];
 
-goalw thy [dlift_def] "dlift f`l = Def y --> (? x. l = Def x)";
+goalw thy [dlift_def]
+ "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
 by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
-qed_spec_mp "dlift_DefD";
-
+qed "dlift_is_Def";
+Addsimps [dlift_is_Def];
 
 goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
 be evalc.induct 1;
@@ -31,13 +32,7 @@
 by (com.induct_tac "c" 1);
     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
-  by (Simp_tac 1);
-  by (strip_tac 1);
-  by (forward_tac [dlift_DefD] 1);
-  be exE 1;
-  by (rotate_tac ~1 1);
-  by (Asm_full_simp_tac 1);
-  by (fast_tac (HOL_cs addSIs evalc.intrs) 1);
+  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
 by (Simp_tac 1);
@@ -46,13 +41,7 @@
  by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (safe_tac HOL_cs);
-  (* case bexp s *)
-  by (forward_tac [dlift_DefD] 1);
-  be exE 1;
-  by (rotate_tac ~1 1);
-  by (Asm_full_simp_tac 1);
   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
- (* case ~bexp s *)
  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
 qed_spec_mp "D_implies_eval";