# HG changeset patch
# User oheimb
# Date 850745063 -3600
# Node ID a07181dd2118723693f57c2f8126b2c7ace91a0d
# Parent  cb21eef657044d6fa6bf189b46f891ffe200769c
repaired several proofs

diff -r cb21eef65704 -r a07181dd2118 src/HOLCF/explicit_domains/Dlist.ML
--- a/src/HOLCF/explicit_domains/Dlist.ML	Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dlist.ML	Mon Dec 16 15:04:23 1996 +0100
@@ -8,6 +8,8 @@
 
 open Dlist;
 
+Delsimps (ex_simps @ all_simps);
+
 (* ------------------------------------------------------------------------*)
 (* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict             *)
 (* ------------------------------------------------------------------------*)
@@ -226,7 +228,7 @@
         [
         (res_inst_tac [("P1","TT << FF")] classical3 1),
         (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (case_tac "(x::'a)=UU" 1),
@@ -244,7 +246,7 @@
         (cut_facts_tac prems 1),
         (res_inst_tac [("P1","TT << FF")] classical3 1),
         (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1),
         (asm_simp_tac (!simpset addsimps dlist_rews) 1)
@@ -281,11 +283,11 @@
         [
         (cut_facts_tac prems 1),
         (rtac conjI 1),
-        (dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dlist_when) 1),
         (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dlist_when) 1),
         (asm_simp_tac (!simpset addsimps dlist_when) 1)
diff -r cb21eef65704 -r a07181dd2118 src/HOLCF/explicit_domains/Dnat.ML
--- a/src/HOLCF/explicit_domains/Dnat.ML	Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.ML	Mon Dec 16 15:04:23 1996 +0100
@@ -176,7 +176,7 @@
         [
         (res_inst_tac [("P1","TT << FF")] classical3 1),
         (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (case_tac "n=UU" 1),
@@ -192,7 +192,7 @@
         (cut_facts_tac prems 1),
         (res_inst_tac [("P1","TT << FF")] classical3 1),
         (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1)
@@ -228,7 +228,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1),
         (asm_simp_tac (!simpset addsimps dnat_rews) 1)
diff -r cb21eef65704 -r a07181dd2118 src/HOLCF/explicit_domains/Focus_ex.ML
--- a/src/HOLCF/explicit_domains/Focus_ex.ML	Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Focus_ex.ML	Mon Dec 16 15:04:23 1996 +0100
@@ -7,6 +7,8 @@
 
 open Focus_ex;
 
+	Delsimps (ex_simps @ all_simps);
+
 (* first some logical trading *)
 
 val prems = goal Focus_ex.thy
diff -r cb21eef65704 -r a07181dd2118 src/HOLCF/explicit_domains/Stream.ML
--- a/src/HOLCF/explicit_domains/Stream.ML	Mon Dec 16 13:10:02 1996 +0100
+++ b/src/HOLCF/explicit_domains/Stream.ML	Mon Dec 16 15:04:23 1996 +0100
@@ -53,11 +53,11 @@
         (asm_simp_tac (!simpset addsimps stream_rews) 1),
         (Asm_simp_tac  1),
         (res_inst_tac [("p","y")] upE1 1),
-        (contr_tac 1),
+         (contr_tac 1),
         (rtac disjI2 1),
         (rtac exI 1),
-        (rtac exI 1),
         (etac conjI 1),
+	(rtac exI 1),
         (Asm_simp_tac  1)
         ]);
 
@@ -174,11 +174,11 @@
         [
         (cut_facts_tac prems 1),
         (rtac conjI 1),
-        (dres_inst_tac [("fo5","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps stream_when) 1),
         (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (dres_inst_tac [("fo5","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
+        (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
         (etac box_less 1),
         (asm_simp_tac (!simpset addsimps stream_when) 1),
         (asm_simp_tac (!simpset addsimps stream_when) 1)
@@ -323,7 +323,7 @@
         (rtac (is_chain_iterate RS ch2ch_fappL) 1),
         (rtac (is_chain_iterate RS ch2ch_fappL) 1),
         (rtac allI 1),
-        (resolve_tac prems 1),
+        (resolve_tac prems 1)
         ]);
 
 val stream_take_lemma = prover stream_reach  [stream_take_def]
@@ -494,7 +494,7 @@
         (fast_tac HOL_cs 1),
         (rtac disjI2 1),
         (rtac disjE 1),
-        (etac (de_morgan2 RS ssubst) 1),
+        (etac (de_Morgan_conj RS subst) 1),
         (res_inst_tac [("x","shd`s1")] exI 1),
         (res_inst_tac [("x","stl`s1")] exI 1),
         (res_inst_tac [("x","stl`s2")] exI 1),
@@ -582,19 +582,17 @@
         [
         (nat_ind_tac "n" 1),
         (simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1 ),
-        (hyp_subst_tac  1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (rtac allI 1),
+        (strip_tac 1),
         (res_inst_tac [("s","s2")] streamE 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1 ),
+         (asm_simp_tac (!simpset addsimps stream_rews) 1),
+	(hyp_subst_tac 1),
+	(rotate_tac ~1 1),
+        (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
         (subgoal_tac "stream_take n1`xs = xs" 1),
-        (rtac ((hd stream_inject) RS conjunct2) 2),
-        (atac 4),
-        (atac 2),
-        (atac 2),
+         (rtac ((hd stream_inject) RS conjunct2) 2),
+           (atac 4),
+          (atac 2),
+         (atac 2),
         (rtac cfun_arg_cong 1),
         (fast_tac HOL_cs 1)
         ]);