1.1 --- a/src/HOLCF/explicit_domains/Dlist.ML Mon Dec 16 13:10:02 1996 +0100
1.2 +++ b/src/HOLCF/explicit_domains/Dlist.ML Mon Dec 16 15:04:23 1996 +0100
1.3 @@ -8,6 +8,8 @@
1.4
1.5 open Dlist;
1.6
1.7 +Delsimps (ex_simps @ all_simps);
1.8 +
1.9 (* ------------------------------------------------------------------------*)
1.10 (* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict *)
1.11 (* ------------------------------------------------------------------------*)
1.12 @@ -226,7 +228,7 @@
1.13 [
1.14 (res_inst_tac [("P1","TT << FF")] classical3 1),
1.15 (resolve_tac dist_less_tr 1),
1.16 - (dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
1.17 + (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
1.18 (etac box_less 1),
1.19 (asm_simp_tac (!simpset addsimps dlist_rews) 1),
1.20 (case_tac "(x::'a)=UU" 1),
1.21 @@ -244,7 +246,7 @@
1.22 (cut_facts_tac prems 1),
1.23 (res_inst_tac [("P1","TT << FF")] classical3 1),
1.24 (resolve_tac dist_less_tr 1),
1.25 - (dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
1.26 + (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
1.27 (etac box_less 1),
1.28 (asm_simp_tac (!simpset addsimps dlist_rews) 1),
1.29 (asm_simp_tac (!simpset addsimps dlist_rews) 1)
1.30 @@ -281,11 +283,11 @@
1.31 [
1.32 (cut_facts_tac prems 1),
1.33 (rtac conjI 1),
1.34 - (dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
1.35 + (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
1.36 (etac box_less 1),
1.37 (asm_simp_tac (!simpset addsimps dlist_when) 1),
1.38 (asm_simp_tac (!simpset addsimps dlist_when) 1),
1.39 - (dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
1.40 + (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
1.41 (etac box_less 1),
1.42 (asm_simp_tac (!simpset addsimps dlist_when) 1),
1.43 (asm_simp_tac (!simpset addsimps dlist_when) 1)
2.1 --- a/src/HOLCF/explicit_domains/Dnat.ML Mon Dec 16 13:10:02 1996 +0100
2.2 +++ b/src/HOLCF/explicit_domains/Dnat.ML Mon Dec 16 15:04:23 1996 +0100
2.3 @@ -176,7 +176,7 @@
2.4 [
2.5 (res_inst_tac [("P1","TT << FF")] classical3 1),
2.6 (resolve_tac dist_less_tr 1),
2.7 - (dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
2.8 + (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
2.9 (etac box_less 1),
2.10 (asm_simp_tac (!simpset addsimps dnat_rews) 1),
2.11 (case_tac "n=UU" 1),
2.12 @@ -192,7 +192,7 @@
2.13 (cut_facts_tac prems 1),
2.14 (res_inst_tac [("P1","TT << FF")] classical3 1),
2.15 (resolve_tac dist_less_tr 1),
2.16 - (dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
2.17 + (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
2.18 (etac box_less 1),
2.19 (asm_simp_tac (!simpset addsimps dnat_rews) 1),
2.20 (asm_simp_tac (!simpset addsimps dnat_rews) 1)
2.21 @@ -228,7 +228,7 @@
2.22 (fn prems =>
2.23 [
2.24 (cut_facts_tac prems 1),
2.25 - (dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
2.26 + (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
2.27 (etac box_less 1),
2.28 (asm_simp_tac (!simpset addsimps dnat_rews) 1),
2.29 (asm_simp_tac (!simpset addsimps dnat_rews) 1)
3.1 --- a/src/HOLCF/explicit_domains/Focus_ex.ML Mon Dec 16 13:10:02 1996 +0100
3.2 +++ b/src/HOLCF/explicit_domains/Focus_ex.ML Mon Dec 16 15:04:23 1996 +0100
3.3 @@ -7,6 +7,8 @@
3.4
3.5 open Focus_ex;
3.6
3.7 + Delsimps (ex_simps @ all_simps);
3.8 +
3.9 (* first some logical trading *)
3.10
3.11 val prems = goal Focus_ex.thy
4.1 --- a/src/HOLCF/explicit_domains/Stream.ML Mon Dec 16 13:10:02 1996 +0100
4.2 +++ b/src/HOLCF/explicit_domains/Stream.ML Mon Dec 16 15:04:23 1996 +0100
4.3 @@ -53,11 +53,11 @@
4.4 (asm_simp_tac (!simpset addsimps stream_rews) 1),
4.5 (Asm_simp_tac 1),
4.6 (res_inst_tac [("p","y")] upE1 1),
4.7 - (contr_tac 1),
4.8 + (contr_tac 1),
4.9 (rtac disjI2 1),
4.10 (rtac exI 1),
4.11 - (rtac exI 1),
4.12 (etac conjI 1),
4.13 + (rtac exI 1),
4.14 (Asm_simp_tac 1)
4.15 ]);
4.16
4.17 @@ -174,11 +174,11 @@
4.18 [
4.19 (cut_facts_tac prems 1),
4.20 (rtac conjI 1),
4.21 - (dres_inst_tac [("fo5","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
4.22 + (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
4.23 (etac box_less 1),
4.24 (asm_simp_tac (!simpset addsimps stream_when) 1),
4.25 (asm_simp_tac (!simpset addsimps stream_when) 1),
4.26 - (dres_inst_tac [("fo5","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
4.27 + (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
4.28 (etac box_less 1),
4.29 (asm_simp_tac (!simpset addsimps stream_when) 1),
4.30 (asm_simp_tac (!simpset addsimps stream_when) 1)
4.31 @@ -323,7 +323,7 @@
4.32 (rtac (is_chain_iterate RS ch2ch_fappL) 1),
4.33 (rtac (is_chain_iterate RS ch2ch_fappL) 1),
4.34 (rtac allI 1),
4.35 - (resolve_tac prems 1),
4.36 + (resolve_tac prems 1)
4.37 ]);
4.38
4.39 val stream_take_lemma = prover stream_reach [stream_take_def]
4.40 @@ -494,7 +494,7 @@
4.41 (fast_tac HOL_cs 1),
4.42 (rtac disjI2 1),
4.43 (rtac disjE 1),
4.44 - (etac (de_morgan2 RS ssubst) 1),
4.45 + (etac (de_Morgan_conj RS subst) 1),
4.46 (res_inst_tac [("x","shd`s1")] exI 1),
4.47 (res_inst_tac [("x","stl`s1")] exI 1),
4.48 (res_inst_tac [("x","stl`s2")] exI 1),
4.49 @@ -582,19 +582,17 @@
4.50 [
4.51 (nat_ind_tac "n" 1),
4.52 (simp_tac (!simpset addsimps stream_rews) 1),
4.53 - (strip_tac 1 ),
4.54 - (hyp_subst_tac 1),
4.55 - (simp_tac (!simpset addsimps stream_rews) 1),
4.56 - (rtac allI 1),
4.57 + (strip_tac 1),
4.58 (res_inst_tac [("s","s2")] streamE 1),
4.59 - (asm_simp_tac (!simpset addsimps stream_rews) 1),
4.60 - (asm_simp_tac (!simpset addsimps stream_rews) 1),
4.61 - (strip_tac 1 ),
4.62 + (asm_simp_tac (!simpset addsimps stream_rews) 1),
4.63 + (hyp_subst_tac 1),
4.64 + (rotate_tac ~1 1),
4.65 + (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
4.66 (subgoal_tac "stream_take n1`xs = xs" 1),
4.67 - (rtac ((hd stream_inject) RS conjunct2) 2),
4.68 - (atac 4),
4.69 - (atac 2),
4.70 - (atac 2),
4.71 + (rtac ((hd stream_inject) RS conjunct2) 2),
4.72 + (atac 4),
4.73 + (atac 2),
4.74 + (atac 2),
4.75 (rtac cfun_arg_cong 1),
4.76 (fast_tac HOL_cs 1)
4.77 ]);