--- a/src/HOLCF/Cfun3.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Cfun3.ML Tue Apr 23 17:04:23 1996 +0200
@@ -306,7 +306,7 @@
[
(rtac contlubI 1),
(strip_tac 1),
- (res_inst_tac [("Q","lub(range(Y))=(UU::'a)")] classical2 1),
+ (case_tac "lub(range(Y))=(UU::'a)" 1),
(res_inst_tac [("t","lub(range(Y))")] subst 1),
(rtac sym 1),
(atac 1),
--- a/src/HOLCF/Fix.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Fix.ML Tue Apr 23 17:04:23 1996 +0200
@@ -31,7 +31,10 @@
[
(nat_ind_tac "n" 1),
(Simp_tac 1),
- (Asm_simp_tac 1)
+ (rtac (iterate_Suc RS ssubst) 1),
+ (rtac (iterate_Suc RS ssubst) 1),
+ (etac ssubst 1),
+ (rtac refl 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -554,7 +557,7 @@
(rewtac max_in_chain_def),
(cut_facts_tac prems 1),
(strip_tac 1),
- (res_inst_tac [("Q","!i.Y(i)=UU")] classical2 1),
+ (case_tac "!i.Y(i)=UU" 1),
(res_inst_tac [("x","0")] exI 1),
(strip_tac 1),
(rtac trans 1),
@@ -708,13 +711,13 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("Q","f`(x::'a)=(UU::'b)")] classical2 1),
+ (case_tac "f`(x::'a)=(UU::'b)" 1),
(rtac disjI1 1),
(rtac UU_I 1),
(res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1),
(atac 1),
(rtac (minimal RS monofun_cfun_arg) 1),
- (res_inst_tac [("Q","f`(UU::'a)=(UU::'b)")] classical2 1),
+ (case_tac "f`(UU::'a)=(UU::'b)" 1),
(etac disjI1 1),
(rtac disjI2 1),
(rtac allI 1),
@@ -950,7 +953,8 @@
(etac (is_chainE RS spec) 1),
(hyp_subst_tac 1),
(Asm_simp_tac 1),
- (Asm_simp_tac 1)
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
]);
qed_goal "adm_disj_lemma4" Fix.thy
@@ -1035,7 +1039,7 @@
qed_goal "adm_disj_lemma7" Fix.thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
-\ is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))"
+\ is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -1043,33 +1047,33 @@
(rtac allI 1),
(rtac chain_mono3 1),
(atac 1),
- (rtac theleast2 1),
+ (rtac Least_le 1),
(rtac conjI 1),
(rtac Suc_lessD 1),
(etac allE 1),
(etac exE 1),
- (rtac (theleast1 RS conjunct1) 1),
+ (rtac (LeastI RS conjunct1) 1),
(atac 1),
(etac allE 1),
(etac exE 1),
- (rtac (theleast1 RS conjunct2) 1),
+ (rtac (LeastI RS conjunct2) 1),
(atac 1)
]);
qed_goal "adm_disj_lemma8" Fix.thy
-"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))"
+"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))"
(fn prems =>
[
(cut_facts_tac prems 1),
(strip_tac 1),
(etac allE 1),
(etac exE 1),
- (etac (theleast1 RS conjunct2) 1)
+ (etac (LeastI RS conjunct2) 1)
]);
qed_goal "adm_disj_lemma9" Fix.thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
-\ lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))"
+\ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -1084,7 +1088,7 @@
(atac 1),
(etac allE 1),
(etac exE 1),
- (rtac (theleast1 RS conjunct1) 1),
+ (rtac (LeastI RS conjunct1) 1),
(atac 1),
(rtac lub_mono3 1),
(rtac adm_disj_lemma7 1),
@@ -1104,7 +1108,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("x","%m. Y(theleast(%j. m<j & P(Y(j))))")] exI 1),
+ (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),
(rtac conjI 1),
(rtac adm_disj_lemma7 1),
(atac 1),
@@ -1172,8 +1176,37 @@
]);
+qed_goal "adm_not_conj" Fix.thy
+ "Ë adm (³x. ¿ P x); adm (³x. ¿ Q x) Ì êë adm (³x. ¿ (P x À Q x))" (fn prems =>[
+ cut_facts_tac prems 1,
+ subgoal_tac
+ "(³x. ¿ (P x À Q x)) = (³x. ¿ P x Á ¿ Q x)" 1,
+ rtac ext 2,
+ fast_tac HOL_cs 2,
+ etac ssubst 1,
+ etac adm_disj 1,
+ atac 1]);
+
+qed_goalw "admI" Fix.thy [adm_def]
+ "(ÄY. Ë is_chain Y ; Âi. P(Y i) ; Âi. Ãj. i < j À Y i Û Y j À Y i Ý Y j Ì êë \
+\ P(lub (range Y))) êë adm P"
+ (fn prems => [
+ strip_tac 1,
+ case_tac "finite_chain Y" 1,
+ rewtac finite_chain_def,
+ safe_tac HOL_cs,
+ dtac lub_finch1 1,
+ atac 1,
+ dtac thelubI 1,
+ etac ssubst 1,
+ etac spec 1,
+ etac swap 1,
+ rewtac max_in_chain_def,
+ resolve_tac prems 1, atac 1, atac 1,
+ fast_tac (HOL_cs addDs [le_imp_less_or_eq]
+ addEs [chain_mono RS mp]) 1]);
val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
- adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
+ adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less
];
--- a/src/HOLCF/Holcfb.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Holcfb.ML Tue Apr 23 17:04:23 1996 +0200
@@ -1,10 +1,10 @@
(* Title: HOLCF/holcfb.ML
ID: $Id$
Author: Franz Regensburger
+ Changed by: David von Oheimb
Copyright 1993 Technische Universitaet Muenchen
+*)
-Lemmas for Holcfb.thy
-*)
open Holcfb;
@@ -12,6 +12,7 @@
(* <::nat=>nat=>bool is a well-ordering *)
(* ------------------------------------------------------------------------ *)
+(*
qed_goal "well_ordering_nat" Nat.thy
"!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
(fn prems =>
@@ -34,12 +35,13 @@
(rtac leI 1),
(fast_tac HOL_cs 1)
]);
-
+*)
(* ------------------------------------------------------------------------ *)
(* Lemmas for selecting the least element in a nonempty set *)
(* ------------------------------------------------------------------------ *)
+(*
qed_goalw "theleast" Holcfb.thy [theleast_def]
"P(x) ==> P(theleast(P)) & (!x.P(x)--> theleast(P) <= x)"
(fn prems =>
@@ -50,10 +52,17 @@
(rtac selectI 1),
(atac 1)
]);
+*)
+
+(* val theleast1 = LeastI "?P ?k êë ?P (´x. ?P x)" *)
+(*
val theleast1= theleast RS conjunct1;
(* ?P1(?x1) ==> ?P1(theleast(?P1)) *)
+*)
+(* val theleast2 = Least_le "?P ?k êë (´x. ?P x) <= ?k" *)
+(*
qed_goal "theleast2" Holcfb.thy "P(x) ==> theleast(P) <= x"
(fn prems =>
[
@@ -61,81 +70,39 @@
(resolve_tac prems 1),
(resolve_tac prems 1)
]);
-
+*)
(* ------------------------------------------------------------------------ *)
(* Some lemmas in HOL.thy *)
(* ------------------------------------------------------------------------ *)
-qed_goal "de_morgan1" HOL.thy "(~a & ~b)=(~(a | b))"
-(fn prems =>
- [
- (rtac iffI 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
+(* val de_morgan1 = de_Morgan_disj RS sym; "(~a & ~b)=(~(a | b))" *)
-qed_goal "de_morgan2" HOL.thy "(~a | ~b)=(~(a & b))"
-(fn prems =>
- [
- (rtac iffI 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
+(* val de_morgan2 = de_Morgan_conj RS sym; "(~a | ~b)=(~(a & b))" *)
-qed_goal "notall2ex" HOL.thy "(~ (!x.P(x))) = (? x.~P(x))"
-(fn prems =>
- [
- (rtac iffI 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
+(* val notall2ex = not_all "(~ (!x.P(x))) = (? x.~P(x))" *)
-qed_goal "notex2all" HOL.thy "(~ (? x.P(x))) = (!x.~P(x))"
-(fn prems =>
- [
- (rtac iffI 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
+(* val notex2all = not_ex "(~ (? x.P(x))) = (!x.~P(x))" *)
-qed_goal "selectI3" HOL.thy "(? x. P(x)) ==> P(@ x.P(x))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (etac selectI 1)
- ]);
+(* val selectI3 = select_eq_Ex RS iffD2 "(? x. P(x)) ==> P(@ x.P(x))" *)
-qed_goal "selectE" HOL.thy "P(@ x.P(x)) ==> (? x. P(x))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exI 1)
- ]);
-
-qed_goal "select_eq_Ex" HOL.thy "(P(@ x.P(x))) = (? x. P(x))"
-(fn prems =>
- [
- (rtac (iff RS mp RS mp) 1),
- (strip_tac 1),
- (etac selectE 1),
- (strip_tac 1),
- (etac selectI3 1)
- ]);
+(* val selectE = select_eq_Ex RS iffD1 "P(@ x.P(x)) ==> (? x. P(x))" *)
+(*
qed_goal "notnotI" HOL.thy "P ==> ~~P"
(fn prems =>
[
(cut_facts_tac prems 1),
(fast_tac HOL_cs 1)
]);
+*)
-
+(* val classical2 = case_split_thm; "[|Q ==> R; ~Q ==> R|]==>R" *)
+(*
qed_goal "classical2" HOL.thy "[|Q ==> R; ~Q ==> R|]==>R"
(fn prems =>
[
@@ -144,13 +111,17 @@
(eresolve_tac prems 1),
(eresolve_tac prems 1)
]);
+*)
+(*
+fun case_tac s = res_inst_tac [("Q",s)] classical2;
+*)
val classical3 = (notE RS notI);
(* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
-
+(*
qed_goal "nat_less_cases" Nat.thy
"[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
( fn prems =>
@@ -161,10 +132,9 @@
(etac (sym RS hd (tl prems)) 1),
(etac (hd prems) 1)
]);
-
-
-
+*)
-
-
-
+(*
+qed_goal "Suc_less_mono" Nat.thy "Suc n < Suc m = (n < m)" (fn _ => [
+ fast_tac (HOL_cs addIs [Suc_mono] addDs [Suc_less_SucD]) 1]);
+*)
--- a/src/HOLCF/Holcfb.thy Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Holcfb.thy Tue Apr 23 17:04:23 1996 +0200
@@ -7,7 +7,9 @@
*)
-Holcfb = Nat +
+Holcfb = Nat
+
+(* +
consts
theleast :: "(nat=>bool)=>nat"
@@ -15,7 +17,17 @@
theleast_def "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
-(* start 8bit 1 *)
-(* end 8bit 1 *)
+(* start
+ 8bit 1 *)
+
+syntax
+ "Gmu" :: "[pttrn, bool] => nat" ("(3´_./ _)" 10)
+
+translations
+ "´x.P" == "theleast(%x.P)"
+
+(* end
+ 8bit 1 *)
end
+*)
\ No newline at end of file
--- a/src/HOLCF/Lift3.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Lift3.ML Tue Apr 23 17:04:23 1996 +0200
@@ -306,13 +306,10 @@
[
(cut_facts_tac prems 1),
(rtac allI 1),
- (rtac (notex2all RS iffD1) 1),
+ (rtac (not_ex RS iffD1) 1),
(rtac contrapos 1),
(etac (lift_lemma2 RS iffD1) 2),
- (rtac notnotI 1),
- (rtac (chain_UU_I RS spec) 1),
- (atac 1),
- (atac 1)
+ (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
]);
--- a/src/HOLCF/Makefile Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Makefile Tue Apr 23 17:04:23 1996 +0200
@@ -35,7 +35,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
case "$(COMP)" in \
- poly*) cp $(BIN)/HOL $(BIN)/HOLCF;\
+ poly*) cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
if [ "$${MAKE_HTML}" = "true" ]; \
then echo 'open PolyML; make_html := true; exit_use_dir".";' \
| $(COMP) $(BIN)/HOLCF;\
--- a/src/HOLCF/Pcpo.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Pcpo.ML Tue Apr 23 17:04:23 1996 +0200
@@ -92,7 +92,7 @@
(resolve_tac prems 1),
(rtac ub_rangeI 1),
(strip_tac 1),
- (res_inst_tac [("Q","x<i")] classical2 1),
+ (case_tac "x<i" 1),
(res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1),
(rtac sym 1),
(fast_tac HOL_cs 1),
@@ -207,7 +207,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (notall2ex RS iffD1) 1),
+ (rtac (not_all RS iffD1) 1),
(rtac swap 1),
(rtac chain_UU_I_inverse 2),
(etac notnotD 2),
--- a/src/HOLCF/Porder.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Porder.ML Tue Apr 23 17:04:23 1996 +0200
@@ -125,7 +125,7 @@
[
(cut_facts_tac prems 1),
(rtac (lub RS ssubst) 1),
- (etac selectI3 1)
+ (etac (select_eq_Ex RS iffD2) 1)
]);
qed_goal "lubE" Porder.thy " M <<| lub(M) ==> ? x. M <<| x"
@@ -329,7 +329,7 @@
(cut_facts_tac prems 1),
(rtac lub_finch1 1),
(etac conjunct1 1),
- (rtac selectI3 1),
+ (rtac (select_eq_Ex RS iffD2) 1),
(etac conjunct2 1)
]);
--- a/src/HOLCF/Sprod0.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Sprod0.ML Tue Apr 23 17:04:23 1996 +0200
@@ -50,7 +50,7 @@
"(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
(fn prems =>
[
- (res_inst_tac [("Q","a=UU|b=UU")] classical2 1),
+ (case_tac "a=UU|b=UU" 1),
(atac 1),
(rtac disjI1 1),
(rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS
@@ -124,7 +124,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (de_morgan1 RS ssubst) 1),
+ (rtac (de_Morgan_disj RS subst) 1),
(etac contrapos 1),
(etac strict_Ispair 1)
]);
@@ -148,7 +148,7 @@
(cut_facts_tac prems 1),
(rtac contrapos 1),
(etac defined_Ispair_rev 2),
- (rtac (de_morgan1 RS iffD1) 1),
+ (rtac (de_Morgan_disj RS iffD2) 1),
(etac conjI 1),
(atac 1)
]);
@@ -172,7 +172,7 @@
(rtac conjI 1),
(rtac (Rep_Sprod_inverse RS sym RS trans) 1),
(etac arg_cong 1),
- (rtac (de_morgan1 RS ssubst) 1),
+ (rtac (de_Morgan_disj RS subst) 1),
(atac 1),
(rtac disjI1 1),
(rtac (Rep_Sprod_inverse RS sym RS trans) 1),
--- a/src/HOLCF/Sprod3.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Sprod3.ML Tue Apr 23 17:04:23 1996 +0200
@@ -32,7 +32,7 @@
(rtac sym 1),
(rtac lub_chain_maxelem 1),
(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
- (rtac (notall2ex RS iffD1) 1),
+ (rtac (not_all RS iffD1) 1),
(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
(atac 1),
(rtac chain_UU_I_inverse 1),
@@ -129,7 +129,7 @@
(rtac sym 1),
(rtac lub_chain_maxelem 1),
(res_inst_tac [("P","%j.Y(j)~=UU")] exE 1),
- (rtac (notall2ex RS iffD1) 1),
+ (rtac (not_all RS iffD1) 1),
(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
(atac 1),
(rtac chain_UU_I_inverse 1),
@@ -253,13 +253,9 @@
(rtac strict_Isfst 1),
(rtac swap 1),
(etac (defined_IsfstIssnd RS conjunct2) 2),
- (rtac notnotI 1),
- (rtac (chain_UU_I RS spec) 1),
- (rtac (monofun_Issnd RS ch2ch_monofun) 1),
- (atac 1),
- (atac 1)
- ]);
-
+ (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS
+ chain_UU_I RS spec]) 1)
+ ]);
qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
(fn prems =>
@@ -281,13 +277,9 @@
(rtac strict_Issnd 1),
(rtac swap 1),
(etac (defined_IsfstIssnd RS conjunct1) 2),
- (rtac notnotI 1),
- (rtac (chain_UU_I RS spec) 1),
- (rtac (monofun_Isfst RS ch2ch_monofun) 1),
- (atac 1),
- (atac 1)
- ]);
-
+ (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
+ chain_UU_I RS spec]) 1)
+ ]);
qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)"
(fn prems =>
@@ -663,7 +655,7 @@
[
(rtac (beta_cfun RS ssubst) 1),
(cont_tacR 1),
- (res_inst_tac [("Q","z=UU")] classical2 1),
+ (case_tac "z=UU" 1),
(hyp_subst_tac 1),
(rtac strictify1 1),
(rtac trans 1),
--- a/src/HOLCF/Ssum0.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Ssum0.ML Tue Apr 23 17:04:23 1996 +0200
@@ -68,13 +68,13 @@
(fn prems =>
[
(rtac conjI 1),
- (res_inst_tac [("Q","a=UU")] classical2 1),
+ (case_tac "a=UU" 1),
(atac 1),
(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2
RS mp RS conjunct1 RS sym) 1),
(fast_tac HOL_cs 1),
(atac 1),
- (res_inst_tac [("Q","b=UU")] classical2 1),
+ (case_tac "b=UU" 1),
(atac 1),
(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1
RS mp RS conjunct1 RS sym) 1),
@@ -104,7 +104,7 @@
"(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
(fn prems =>
[
- (res_inst_tac [("Q","a=UU")] classical2 1),
+ (case_tac "a=UU" 1),
(atac 1),
(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong
RS iffD2 RS mp RS conjunct1 RS sym) 1),
@@ -116,7 +116,7 @@
"(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
(fn prems =>
[
- (res_inst_tac [("Q","b=UU")] classical2 1),
+ (case_tac "b=UU" 1),
(atac 1),
(rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong
RS iffD2 RS mp RS conjunct1 RS sym) 1),
@@ -149,11 +149,11 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("Q","a1=UU")] classical2 1),
+ (case_tac "a1=UU" 1),
(hyp_subst_tac 1),
(rtac (inject_Sinl_Rep1 RS sym) 1),
(etac sym 1),
- (res_inst_tac [("Q","a2=UU")] classical2 1),
+ (case_tac "a2=UU" 1),
(hyp_subst_tac 1),
(etac inject_Sinl_Rep1 1),
(etac inject_Sinl_Rep2 1),
@@ -166,11 +166,11 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("Q","b1=UU")] classical2 1),
+ (case_tac "b1=UU" 1),
(hyp_subst_tac 1),
(rtac (inject_Sinr_Rep1 RS sym) 1),
(etac sym 1),
- (res_inst_tac [("Q","b2=UU")] classical2 1),
+ (case_tac "b2=UU" 1),
(hyp_subst_tac 1),
(etac inject_Sinr_Rep1 1),
(etac inject_Sinr_Rep2 1),
@@ -232,7 +232,7 @@
(rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
(etac disjE 1),
(etac exE 1),
- (res_inst_tac [("Q","z= Abs_Ssum(Sinl_Rep(UU))")] classical2 1),
+ (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
(etac disjI1 1),
(rtac disjI2 1),
(rtac disjI1 1),
@@ -248,7 +248,7 @@
(etac arg_cong 1),
(etac arg_cong 1),
(etac exE 1),
- (res_inst_tac [("Q","z= Abs_Ssum(Sinl_Rep(UU))")] classical2 1),
+ (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
(etac disjI1 1),
(rtac disjI2 1),
(rtac disjI2 1),
--- a/src/HOLCF/Ssum2.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Ssum2.ML Tue Apr 23 17:04:23 1996 +0200
@@ -227,7 +227,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac classical2 1),
+ (rtac case_split_thm 1),
(etac disjI1 1),
(rtac disjI2 1),
(etac ssum_lemma3 1),
@@ -246,7 +246,7 @@
[
(cut_facts_tac prems 1),
(hyp_subst_tac 1),
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac Ssum0_ss 1),
(asm_simp_tac Ssum0_ss 1)
]);
@@ -261,7 +261,7 @@
[
(cut_facts_tac prems 1),
(hyp_subst_tac 1),
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac Ssum0_ss 1),
(asm_simp_tac Ssum0_ss 1)
]);
--- a/src/HOLCF/Ssum3.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/Ssum3.ML Tue Apr 23 17:04:23 1996 +0200
@@ -24,7 +24,7 @@
(rtac exI 3),
(rtac refl 3),
(etac (monofun_Isinl RS ch2ch_monofun) 2),
- (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+ (case_tac "lub(range(Y))=UU" 1),
(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
(atac 1),
(res_inst_tac [("f","Isinl")] arg_cong 1),
@@ -40,7 +40,7 @@
(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
(etac (monofun_Isinl RS ch2ch_monofun) 1),
(rtac allI 1),
- (res_inst_tac [("Q","Y(k)=UU")] classical2 1),
+ (case_tac "Y(k)=UU" 1),
(asm_simp_tac Ssum0_ss 1),
(asm_simp_tac Ssum0_ss 1)
]);
@@ -56,7 +56,7 @@
(rtac exI 3),
(rtac refl 3),
(etac (monofun_Isinr RS ch2ch_monofun) 2),
- (res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+ (case_tac "lub(range(Y))=UU" 1),
(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
(atac 1),
((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)),
@@ -71,7 +71,7 @@
(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
(etac (monofun_Isinr RS ch2ch_monofun) 1),
(rtac allI 1),
- (res_inst_tac [("Q","Y(k)=UU")] classical2 1),
+ (case_tac "Y(k)=UU" 1),
(asm_simp_tac Ssum0_ss 1),
(asm_simp_tac Ssum0_ss 1)
]);
--- a/src/HOLCF/ex/Hoare.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/ex/Hoare.ML Tue Apr 23 17:04:23 1996 +0200
@@ -40,7 +40,7 @@
val hoare_lemma5 = prove_goal HOLCF.thy
"[|(? k. b1`(iterate k g x) ~= TT);\
-\ k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
+\ k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
\ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU"
(fn prems =>
[
@@ -48,7 +48,7 @@
(hyp_subst_tac 1),
(rtac hoare_lemma2 1),
(etac exE 1),
- (etac theleast1 1)
+ (etac LeastI 1)
]);
val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> b~=TT"
@@ -69,7 +69,7 @@
val hoare_lemma8 = prove_goal HOLCF.thy
"[|(? k. b1`(iterate k g x) ~= TT);\
-\ k=theleast(%n. b1`(iterate n g x) ~= TT)|] ==> \
+\ k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
\ !m. m < k --> b1`(iterate m g x)=TT"
(fn prems =>
[
@@ -81,11 +81,11 @@
(atac 2),
(rtac (le_less_trans RS less_irrefl) 1),
(atac 2),
- (rtac theleast2 1),
+ (rtac Least_le 1),
(etac hoare_lemma6 1),
(rtac (le_less_trans RS less_irrefl) 1),
(atac 2),
- (rtac theleast2 1),
+ (rtac Least_le 1),
(etac hoare_lemma7 1)
]);
@@ -143,8 +143,8 @@
(fn prems =>
[
(nat_ind_tac "k" 1),
- (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
- (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+ (Simp_tac 1),
+ (Simp_tac 1),
(strip_tac 1),
(res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
(rtac trans 1),
@@ -152,7 +152,7 @@
(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
(rtac mp 1),
(etac spec 1),
- (Simp_tac 1),
+ (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
(simp_tac HOLCF_ss 1),
(etac mp 1),
(strip_tac 1),
@@ -168,24 +168,18 @@
(fn prems =>
[
(nat_ind_tac "k" 1),
- (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
- (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+ (Simp_tac 1),
+(simp_tac (!simpset addsimps [less_Suc_eq]) 1),
(strip_tac 1),
(res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
(rtac trans 1),
(rtac (q_def3 RS sym) 2),
(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
- (rtac mp 1),
- (etac spec 1),
- (Simp_tac 1),
+ (fast_tac HOL_cs 1),
(simp_tac HOLCF_ss 1),
(etac mp 1),
(strip_tac 1),
- (rtac mp 1),
- (etac spec 1),
- (etac less_trans 1),
- (Simp_tac 1)
- ]);
+ (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
(* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
@@ -193,14 +187,14 @@
val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
(*
val hoare_lemma10 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
- Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
+ Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
p`(iterate ?k3 g ?x1) = p`?x1" : thm
*)
val hoare_lemma11 = prove_goal Hoare.thy
"(? n.b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+\ k=Least(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
\ --> p`x = iterate k g x"
(fn prems =>
[
@@ -214,7 +208,7 @@
(rtac p_def3 1),
(asm_simp_tac HOLCF_ss 1),
(eres_inst_tac
- [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] subst 1),
+ [("s","0"),("t","Least(%n. b1`(iterate n g x) ~= TT)")] subst 1),
(Simp_tac 1),
(hyp_subst_tac 1),
(strip_tac 1),
@@ -240,7 +234,7 @@
val hoare_lemma12 = prove_goal Hoare.thy
"(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
+\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
\ --> p`x = UU"
(fn prems =>
[
@@ -398,13 +392,13 @@
val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
(*
val hoare_lemma25 = "[| ? k. b1`(iterate k g ?x1) ~= TT;
- Suc ?k3 = theleast (%n. b1`(iterate n g ?x1) ~= TT) |] ==>
+ Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
q`(iterate ?k3 g ?x1) = q`?x1" : thm
*)
val hoare_lemma26 = prove_goal Hoare.thy
"(? n. b1`(iterate n g x)~=TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
+\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
\ --> q`x = q`(iterate k g x)"
(fn prems =>
[
@@ -433,7 +427,7 @@
val hoare_lemma27 = prove_goal Hoare.thy
"(? n. b1`(iterate n g x) ~= TT) ==>\
-\ k=theleast(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
+\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
\ --> q`x = UU"
(fn prems =>
[
--- a/src/HOLCF/explicit_domains/Coind.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Coind.ML Tue Apr 23 17:04:23 1996 +0200
@@ -84,7 +84,7 @@
(rewtac stream_bisim_def),
(strip_tac 1),
(etac exE 1),
- (res_inst_tac [("Q","n=UU")] classical2 1),
+ (case_tac "n=UU" 1),
(rtac disjI1 1),
(asm_simp_tac (!simpset addsimps coind_rews) 1),
(rtac disjI2 1),
@@ -112,7 +112,7 @@
(rtac stream_coind_lemma2 1),
(strip_tac 1),
(etac exE 1),
- (res_inst_tac [("Q","n=UU")] classical2 1),
+ (case_tac "n=UU" 1),
(asm_simp_tac (!simpset addsimps coind_rews) 1),
(res_inst_tac [("x","UU::dnat")] exI 1),
(simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1),
--- a/src/HOLCF/explicit_domains/Dlist.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dlist.ML Tue Apr 23 17:04:23 1996 +0200
@@ -50,7 +50,7 @@
(cut_facts_tac prems 1),
(asm_simp_tac (!simpset addsimps
(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(Asm_simp_tac 1),
(asm_simp_tac (!simpset addsimps [defined_spair]) 1)
]);
@@ -229,9 +229,9 @@
(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
+ (case_tac "(x::'a)=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
+ (case_tac "(xl ::'a dlist)=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
@@ -255,9 +255,9 @@
val temp = prove_goal Dlist.thy "dnil ~= dcons`x`xl"
(fn prems =>
[
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (case_tac "xl=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("P1","TT = FF")] classical3 1),
(resolve_tac dist_eq_tr 1),
@@ -345,7 +345,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
@@ -354,7 +354,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (case_tac "xl=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
@@ -398,10 +398,10 @@
"dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)"
(fn prems =>
[
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(Asm_simp_tac 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("Q","xl=UU")] classical2 1),
+ (case_tac "xl=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(Asm_simp_tac 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
@@ -498,7 +498,7 @@
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(resolve_tac prems 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("Q","dlist_take n1`xl=UU")] classical2 1),
+ (case_tac "dlist_take n1`xl=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
@@ -527,7 +527,7 @@
qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
(fn prems =>
[
- (res_inst_tac [("Q","l=UU")] classical2 1),
+ (case_tac "l=UU" 1),
(asm_simp_tac (!simpset addsimps dlist_rews) 1),
(subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
(etac disjE 1),
--- a/src/HOLCF/explicit_domains/Dnat.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dnat.ML Tue Apr 23 17:04:23 1996 +0200
@@ -179,7 +179,7 @@
(dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
(etac box_less 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (res_inst_tac [("Q","n=UU")] classical2 1),
+ (case_tac "n=UU" 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
@@ -203,7 +203,7 @@
val temp = prove_goal Dnat.thy "dzero ~= dsucc`n"
(fn prems =>
[
- (res_inst_tac [("Q","n=UU")] classical2 1),
+ (case_tac "n=UU" 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(res_inst_tac [("P1","TT = FF")] classical3 1),
(resolve_tac dist_eq_tr 1),
@@ -312,7 +312,7 @@
"dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)"
(fn prems =>
[
- (res_inst_tac [("Q","xs=UU")] classical2 1),
+ (case_tac "xs=UU" 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(Asm_simp_tac 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
@@ -418,7 +418,7 @@
(asm_simp_tac (!simpset addsimps dnat_copy) 1),
(resolve_tac prems 1),
(asm_simp_tac (!simpset addsimps dnat_copy) 1),
- (res_inst_tac [("Q","x`xb=UU")] classical2 1),
+ (case_tac "x`xb=UU" 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
(eresolve_tac prems 1),
@@ -442,7 +442,7 @@
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (res_inst_tac [("Q","dnat_take n1`x=UU")] classical2 1),
+ (case_tac "dnat_take n1`x=UU" 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
@@ -470,7 +470,7 @@
qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
(fn prems =>
[
- (res_inst_tac [("Q","s=UU")] classical2 1),
+ (case_tac "s=UU" 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
(etac disjE 1),
--- a/src/HOLCF/explicit_domains/Stream.ML Tue Apr 23 17:01:51 1996 +0200
+++ b/src/HOLCF/explicit_domains/Stream.ML Tue Apr 23 17:04:23 1996 +0200
@@ -273,7 +273,7 @@
"stream_copy`f`(scons`x`xs) = scons`x`(f`xs)"
(fn prems =>
[
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
@@ -281,7 +281,7 @@
qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
(fn prems =>
[
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
@@ -290,7 +290,7 @@
"stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
(fn prems =>
[
- (res_inst_tac [("Q","x=UU")] classical2 1),
+ (case_tac "x=UU" 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
@@ -489,7 +489,7 @@
(dtac mp 1),
(atac 1),
(etac conjE 1),
- (res_inst_tac [("Q","s1 = UU & s2 = UU")] classical2 1),
+ (case_tac "s1 = UU & s2 = UU" 1),
(rtac disjI1 1),
(fast_tac HOL_cs 1),
(rtac disjI2 1),