massive tidy-up: goal -> Goal, remove use of prems, etc.
--- a/src/HOLCF/Cfun1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cfun1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,16 +10,15 @@
(* derive old type definition rules for Abs_CFun & Rep_CFun *)
(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "Rep_CFun fo : CFun";
+Goal "Rep_CFun fo : CFun";
by (rtac Rep_CFun 1);
qed "Rep_Cfun";
-val prems = goal thy "Abs_CFun (Rep_CFun fo) = fo";
+Goal "Abs_CFun (Rep_CFun fo) = fo";
by (rtac Rep_CFun_inverse 1);
qed "Rep_Cfun_inverse";
-val prems = goal thy "f:CFun==>Rep_CFun(Abs_CFun f)=f";
-by (cut_facts_tac prems 1);
+Goal "f:CFun==>Rep_CFun(Abs_CFun f)=f";
by (etac Abs_CFun_inverse 1);
qed "Abs_Cfun_inverse";
@@ -27,13 +26,12 @@
(* less_cfun is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [less_cfun_def] "(f::'a->'b) << f";
+Goalw [less_cfun_def] "(f::'a->'b) << f";
by (rtac refl_less 1);
qed "refl_less_cfun";
-val prems = goalw thy [less_cfun_def]
+Goalw [less_cfun_def]
"[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
-by (cut_facts_tac prems 1);
by (rtac injD 1);
by (rtac antisym_less 2);
by (atac 3);
@@ -42,9 +40,8 @@
by (rtac Rep_Cfun_inverse 1);
qed "antisym_less_cfun";
-val prems = goalw thy [less_cfun_def]
+Goalw [less_cfun_def]
"[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
-by (cut_facts_tac prems 1);
by (etac trans_less 1);
by (atac 1);
qed "trans_less_cfun";
@@ -53,23 +50,16 @@
(* lemmas about application of continuous functions *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "[| f=g; x=y |] ==> f`x = g`y";
-by (cut_facts_tac prems 1);
-by (fast_tac HOL_cs 1);
+Goal "[| f=g; x=y |] ==> f`x = g`y";
+by (Asm_simp_tac 1);
qed "cfun_cong";
-val prems = goal thy "f=g ==> f`x = g`x";
-by (cut_facts_tac prems 1);
-by (etac cfun_cong 1);
-by (rtac refl 1);
+Goal "f=g ==> f`x = g`x";
+by (Asm_simp_tac 1);
qed "cfun_fun_cong";
-val prems = goal thy "x=y ==> f`x = f`y";
-by (cut_facts_tac prems 1);
-by (rtac cfun_cong 1);
-by (rtac refl 1);
-by (atac 1);
+Goal "x=y ==> f`x = f`y";
+by (Asm_simp_tac 1);
qed "cfun_arg_cong";
@@ -77,8 +67,7 @@
(* additional lemma about the isomorphism between -> and Cfun *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "cont f ==> Rep_CFun (Abs_CFun f) = f";
-by (cut_facts_tac prems 1);
+Goal "cont f ==> Rep_CFun (Abs_CFun f) = f";
by (rtac Abs_Cfun_inverse 1);
by (rewtac CFun_def);
by (etac (mem_Collect_eq RS ssubst) 1);
@@ -88,8 +77,7 @@
(* simplification of application *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "cont f ==> (Abs_CFun f)`x = f x";
-by (cut_facts_tac prems 1);
+Goal "cont f ==> (Abs_CFun f)`x = f x";
by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
qed "Cfunapp2";
@@ -97,9 +85,7 @@
(* beta - equality for continuous functions *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
-by (cut_facts_tac prems 1);
+Goal "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
by (rtac Cfunapp2 1);
by (atac 1);
qed "beta_cfun";
--- a/src/HOLCF/Cfun2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cfun2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
+Goal "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
by (fold_goals_tac [less_cfun_def]);
by (rtac refl 1);
qed "inst_cfun_po";
@@ -16,7 +16,7 @@
(* access to less_cfun in class po *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
+Goal "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
by (simp_tac (simpset() addsimps [inst_cfun_po]) 1);
qed "less_cfun";
@@ -24,7 +24,7 @@
(* Type 'a ->'b is pointed *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "Abs_CFun(% x. UU) << f";
+Goal "Abs_CFun(% x. UU) << f";
by (stac less_cfun 1);
by (stac Abs_Cfun_inverse2 1);
by (rtac cont_const 1);
@@ -33,7 +33,7 @@
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
-val prems = goal thy "? x::'a->'b::pcpo.!y. x<<y";
+Goal "? x::'a->'b::pcpo.!y. x<<y";
by (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1);
by (rtac (minimal_cfun RS allI) 1);
qed "least_cfun";
@@ -44,7 +44,7 @@
(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2 *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "cont(Rep_CFun(fo))";
+Goal "cont(Rep_CFun(fo))";
by (res_inst_tac [("P","cont")] CollectD 1);
by (fold_goals_tac [CFun_def]);
by (rtac Rep_Cfun 1);
@@ -73,7 +73,7 @@
(* Rep_CFun is monotone in its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun] "monofun(Rep_CFun)";
+Goalw [monofun] "monofun(Rep_CFun)";
by (strip_tac 1);
by (etac (less_cfun RS subst) 1);
qed "monofun_Rep_CFun1";
@@ -83,8 +83,7 @@
(* monotonicity of application Rep_CFun in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "f1 << f2 ==> f1`x << f2`x";
-by (cut_facts_tac prems 1);
+Goal "f1 << f2 ==> f1`x << f2`x";
by (res_inst_tac [("x","x")] spec 1);
by (rtac (less_fun RS subst) 1);
by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
@@ -98,9 +97,7 @@
(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
-by (cut_facts_tac prems 1);
+Goal "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
by (rtac trans_less 1);
by (etac monofun_cfun_arg 1);
by (etac monofun_cfun_fun 1);
@@ -119,9 +116,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "chain(Y) ==> chain(%i. f`(Y i))";
-by (cut_facts_tac prems 1);
+Goal "chain(Y) ==> chain(%i. f`(Y i))";
by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
qed "ch2ch_Rep_CFunR";
@@ -135,9 +130,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
-by (cut_facts_tac prems 1);
+Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
by (rtac lub_MF2_mono 1);
by (rtac monofun_Rep_CFun1 1);
by (rtac (monofun_Rep_CFun2 RS allI) 1);
@@ -149,11 +142,9 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "[| chain(F); chain(Y) |] ==>\
+Goal "[| chain(F); chain(Y) |] ==>\
\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))";
-by (cut_facts_tac prems 1);
by (rtac ex_lubMF2 1);
by (rtac monofun_Rep_CFun1 1);
by (rtac (monofun_Rep_CFun2 RS allI) 1);
@@ -165,9 +156,7 @@
(* the lub of a chain of cont. functions is continuous *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
-by (cut_facts_tac prems 1);
+Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
by (rtac monocontlub2cont 1);
by (etac lub_cfun_mono 1);
by (rtac contlubI 1);
@@ -182,23 +171,18 @@
(* type 'a -> 'b is chain complete *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
-by (cut_facts_tac prems 1);
+Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (stac less_cfun 1);
by (stac Abs_Cfun_inverse2 1);
by (etac cont_lubcfun 1);
-by (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1);
+by (rtac (lub_fun RS is_lubD1 RS ub_rangeD) 1);
by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
-by (strip_tac 1);
by (stac less_cfun 1);
by (stac Abs_Cfun_inverse2 1);
by (etac cont_lubcfun 1);
-by (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1);
+by (rtac (lub_fun RS is_lub_lub) 1);
by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
qed "lub_cfun";
@@ -208,9 +192,7 @@
chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
*)
-val prems = goal thy
- "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
-by (cut_facts_tac prems 1);
+Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
by (rtac exI 1);
by (etac lub_cfun 1);
qed "cpo_cfun";
@@ -220,7 +202,7 @@
(* Extensionality in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Cfun1.thy "(!!x. f`x = g`x) ==> f = g";
+val prems = Goal "(!!x. f`x = g`x) ==> f = g";
by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
@@ -232,21 +214,20 @@
(* Monotonicity of Abs_CFun *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)";
+Goal "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)";
by (rtac (less_cfun RS iffD2) 1);
by (stac Abs_Cfun_inverse2 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
by (stac Abs_Cfun_inverse2 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
qed "semi_monofun_Abs_CFun";
(* ------------------------------------------------------------------------ *)
(* Extenionality wrt. << in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "(!!x. f`x << g`x) ==> f << g";
+val prems = Goal "(!!x. f`x << g`x) ==> f << g";
by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
by (rtac semi_monofun_Abs_CFun 1);
--- a/src/HOLCF/Cfun3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cfun3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "UU = Abs_CFun(%x. UU)";
+Goal "UU = Abs_CFun(%x. UU)";
by (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1);
qed "inst_cfun_pcpo";
@@ -15,7 +15,7 @@
(* the contlub property for Rep_CFun its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "contlub(Rep_CFun)";
+Goal "contlub(Rep_CFun)";
by (rtac contlubI 1);
by (strip_tac 1);
by (rtac (expand_fun_eq RS iffD2) 1);
@@ -34,7 +34,7 @@
(* the cont property for Rep_CFun in its first argument *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "cont(Rep_CFun)";
+Goal "cont(Rep_CFun)";
by (rtac monocontlub2cont 1);
by (rtac monofun_Rep_CFun1 1);
by (rtac contlub_Rep_CFun1 1);
@@ -45,10 +45,9 @@
(* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_] *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"chain(FY) ==>\
\ lub(range FY)`x = lub(range (%i. FY(i)`x))";
-by (cut_facts_tac prems 1);
by (rtac trans 1);
by (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1);
by (stac thelub_fun 1);
@@ -57,10 +56,9 @@
qed "contlub_cfun_fun";
-val prems = goal thy
+Goal
"chain(FY) ==>\
\ range(%i. FY(i)`x) <<| lub(range FY)`x";
-by (cut_facts_tac prems 1);
by (rtac thelubE 1);
by (etac ch2ch_Rep_CFunL 1);
by (etac (contlub_cfun_fun RS sym) 1);
@@ -71,10 +69,9 @@
(* contlub, cont properties of Rep_CFun in both argument in mixfix _[_] *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"[|chain(FY);chain(TY)|] ==>\
\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))";
-by (cut_facts_tac prems 1);
by (rtac contlub_CF2 1);
by (rtac cont_Rep_CFun1 1);
by (rtac allI 1);
@@ -83,10 +80,9 @@
by (atac 1);
qed "contlub_cfun";
-val prems = goal thy
+Goal
"[|chain(FY);chain(TY)|] ==>\
\ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))";
-by (cut_facts_tac prems 1);
by (rtac thelubE 1);
by (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1);
by (rtac allI 1);
@@ -113,7 +109,7 @@
(* cont2mono Lemma for %x. LAM y. c1(x)(y) *)
(* ------------------------------------------------------------------------ *)
-val [p1,p2] = goal thy
+val [p1,p2] = Goal
"[| !!x. cont(c1 x); !!y. monofun(%x. c1 x y)|] ==> monofun(%x. LAM y. c1 x y)";
by (rtac monofunI 1);
by (strip_tac 1);
@@ -131,7 +127,7 @@
(* cont2cont Lemma for %x. LAM y. c1 x y) *)
(* ------------------------------------------------------------------------ *)
-val [p1,p2] = goal thy
+val [p1,p2] = Goal
"[| !!x. cont(c1 x); !!y. cont(%x. c1 x y) |] ==> cont(%x. LAM y. c1 x y)";
by (rtac monocontlub2cont 1);
by (rtac (p1 RS cont2mono_LAM) 1);
@@ -166,7 +162,7 @@
(* function application _[_] is strict in its first arguments *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "(UU::'a::cpo->'b)`x = (UU::'b)";
+Goal "(UU::'a::cpo->'b)`x = (UU::'b)";
by (stac inst_cfun_pcpo 1);
by (stac beta_cfun 1);
by (Simp_tac 1);
@@ -178,18 +174,17 @@
(* results about strictify *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [Istrictify_def]
+Goalw [Istrictify_def]
"Istrictify(f)(UU)= (UU)";
by (Simp_tac 1);
qed "Istrictify1";
-val prems = goalw thy [Istrictify_def]
+Goalw [Istrictify_def]
"~x=UU ==> Istrictify(f)(x)=f`x";
-by (cut_facts_tac prems 1);
by (Asm_simp_tac 1);
qed "Istrictify2";
-val prems = goal thy "monofun(Istrictify)";
+Goal "monofun(Istrictify)";
by (rtac monofunI 1);
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
@@ -207,7 +202,7 @@
by (rtac refl_less 1);
qed "monofun_Istrictify1";
-val prems = goal thy "monofun(Istrictify(f))";
+Goal "monofun(Istrictify(f))";
by (rtac monofunI 1);
by (strip_tac 1);
by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
@@ -224,7 +219,7 @@
qed "monofun_Istrictify2";
-val prems = goal thy "contlub(Istrictify)";
+Goal "contlub(Istrictify)";
by (rtac contlubI 1);
by (strip_tac 1);
by (rtac (expand_fun_eq RS iffD2) 1);
@@ -276,7 +271,7 @@
(monofun_Istrictify2 RS monocontlub2cont));
-val _ = goalw thy [strictify_def] "strictify`f`UU=UU";
+Goalw [strictify_def] "strictify`f`UU=UU";
by (stac beta_cfun 1);
by (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1, cont2cont_CF1L]) 1);
by (stac beta_cfun 1);
@@ -284,14 +279,12 @@
by (rtac Istrictify1 1);
qed "strictify1";
-val prems = goalw thy [strictify_def]
- "~x=UU ==> strictify`f`x=f`x";
+Goalw [strictify_def] "~x=UU ==> strictify`f`x=f`x";
by (stac beta_cfun 1);
by (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1, cont2cont_CF1L]) 1);
by (stac beta_cfun 1);
by (rtac cont_Istrictify2 1);
-by (rtac Istrictify2 1);
-by (resolve_tac prems 1);
+by (etac Istrictify2 1);
qed "strictify2";
@@ -326,7 +319,7 @@
(* a prove for embedding projection pairs is similar *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \
\ ==> f`UU=UU & g`UU=UU";
by (rtac conjI 1);
@@ -341,9 +334,7 @@
qed "iso_strict";
-val prems = goal thy
- "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU";
-by (cut_facts_tac prems 1);
+Goal "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU";
by (etac swap 1);
by (dtac notnotD 1);
by (dres_inst_tac [("f","ab")] cfun_arg_cong 1);
@@ -353,9 +344,7 @@
by (atac 1);
qed "isorep_defined";
-val prems = goal thy
- "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU";
-by (cut_facts_tac prems 1);
+Goal "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU";
by (etac swap 1);
by (dtac notnotD 1);
by (dres_inst_tac [("f","rep")] cfun_arg_cong 1);
@@ -369,7 +358,7 @@
(* propagation of flatness and chainfiniteness by continuous isomorphisms *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
+Goal "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
\ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)";
by (rewtac max_in_chain_def);
@@ -391,7 +380,7 @@
qed "chfin2chfin";
-val prems = goal thy "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
+Goal "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
\ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y";
by (strip_tac 1);
by (rtac disjE 1);
@@ -419,9 +408,7 @@
(* a result about functions with flat codomain *)
(* ------------------------------------------------------------------------- *)
-val prems = goal thy
-"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)";
-by (cut_facts_tac prems 1);
+Goal "f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)";
by (case_tac "f`(x::'a)=(UU::'b)" 1);
by (rtac disjI1 1);
by (rtac UU_I 1);
@@ -448,13 +435,13 @@
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [ID_def] "ID`x=x";
+Goalw [ID_def] "ID`x=x";
by (stac beta_cfun 1);
by (rtac cont_id 1);
by (rtac refl 1);
qed "ID1";
-val _ = goalw thy [oo_def] "(f oo g)=(LAM x. f`(g`x))";
+Goalw [oo_def] "(f oo g)=(LAM x. f`(g`x))";
by (stac beta_cfun 1);
by (Simp_tac 1);
by (stac beta_cfun 1);
@@ -462,7 +449,7 @@
by (rtac refl 1);
qed "cfcomp1";
-val _ = goal thy "(f oo g)`x=f`(g`x)";
+Goal "(f oo g)`x=f`(g`x)";
by (stac cfcomp1 1);
by (stac beta_cfun 1);
by (Simp_tac 1);
@@ -479,14 +466,14 @@
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "f oo ID = f ";
+Goal "f oo ID = f ";
by (rtac ext_cfun 1);
by (stac cfcomp2 1);
by (stac ID1 1);
by (rtac refl 1);
qed "ID2";
-val prems = goal thy "ID oo f = f ";
+Goal "ID oo f = f ";
by (rtac ext_cfun 1);
by (stac cfcomp2 1);
by (stac ID1 1);
@@ -494,7 +481,7 @@
qed "ID3";
-val prems = goal thy "f oo (g oo h) = (f oo g) oo h";
+Goal "f oo (g oo h) = (f oo g) oo h";
by (rtac ext_cfun 1);
by (res_inst_tac [("s","f`(g`(h`x))")] trans 1);
by (stac cfcomp2 1);
--- a/src/HOLCF/Cont.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cont.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,43 +10,37 @@
(* access to definition *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [contlub]
+Goalw [contlub]
"! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
\ contlub(f)";
-by (cut_facts_tac prems 1);
by (atac 1);
qed "contlubI";
-val prems = goalw thy [contlub]
+Goalw [contlub]
" contlub(f)==>\
\ ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))";
-by (cut_facts_tac prems 1);
by (atac 1);
qed "contlubE";
-val prems = goalw thy [cont]
+Goalw [cont]
"! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)";
-by (cut_facts_tac prems 1);
by (atac 1);
qed "contI";
-val prems = goalw thy [cont]
+Goalw [cont]
"cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))";
-by (cut_facts_tac prems 1);
by (atac 1);
qed "contE";
-val prems = goalw thy [monofun]
+Goalw [monofun]
"! x y. x << y --> f(x) << f(y) ==> monofun(f)";
-by (cut_facts_tac prems 1);
by (atac 1);
qed "monofunI";
-val prems = goalw thy [monofun]
+Goalw [monofun]
"monofun(f) ==> ! x y. x << y --> f(x) << f(y)";
-by (cut_facts_tac prems 1);
by (atac 1);
qed "monofunE";
@@ -59,35 +53,30 @@
(* monotone functions map chains to chains *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))";
-by (cut_facts_tac prems 1);
by (rtac chainI 1);
-by (rtac allI 1);
by (etac (monofunE RS spec RS spec RS mp) 1);
-by (etac (chainE RS spec) 1);
+by (etac (chainE) 1);
qed "ch2ch_monofun";
(* ------------------------------------------------------------------------ *)
(* monotone functions map upper bound to upper bounds *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"[| monofun(f); range(Y) <| u|] ==> range(%i. f(Y(i))) <| f(u)";
-by (cut_facts_tac prems 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (etac (monofunE RS spec RS spec RS mp) 1);
-by (etac (ub_rangeE RS spec) 1);
+by (etac (ub_rangeD) 1);
qed "ub2ub_monofun";
(* ------------------------------------------------------------------------ *)
(* left to right: monofun(f) & contlub(f) ==> cont(f) *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [cont]
+Goalw [cont]
"[|monofun(f);contlub(f)|] ==> cont(f)";
-by (cut_facts_tac prems 1);
by (strip_tac 1);
by (rtac thelubE 1);
by (etac ch2ch_monofun 1);
@@ -155,77 +144,70 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)";
-by (cut_facts_tac prems 1);
by (etac (ch2ch_monofun RS ch2ch_fun) 1);
by (atac 1);
qed "ch2ch_MF2L";
-val prems = goal thy
+Goal
"[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))";
-by (cut_facts_tac prems 1);
by (etac ch2ch_monofun 1);
by (atac 1);
qed "ch2ch_MF2R";
-val prems = goal thy
+Goal
"[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
\ chain(%i. MF2(F(i))(Y(i)))";
-by (cut_facts_tac prems 1);
by (rtac chainI 1);
-by (strip_tac 1 );
by (rtac trans_less 1);
-by (etac (ch2ch_MF2L RS chainE RS spec) 1);
+by (etac (ch2ch_MF2L RS chainE) 1);
by (atac 1);
by ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1));
-by (etac (chainE RS spec) 1);
+by (etac (chainE) 1);
qed "ch2ch_MF2LR";
-val prems = goal thy
+Goal
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ chain(F);chain(Y)|] ==> \
\ chain(%j. lub(range(%i. MF2 (F j) (Y i))))";
-by (cut_facts_tac prems 1);
-by (rtac (lub_mono RS allI RS chainI) 1);
+by (rtac (lub_mono RS chainI) 1);
by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
by (atac 1);
by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
by (atac 1);
by (strip_tac 1);
-by (rtac (chainE RS spec) 1);
+by (rtac (chainE) 1);
by (etac ch2ch_MF2L 1);
by (atac 1);
qed "ch2ch_lubMF2R";
-val prems = goal thy
+Goal
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ chain(F);chain(Y)|] ==> \
\ chain(%i. lub(range(%j. MF2 (F j) (Y i))))";
-by (cut_facts_tac prems 1);
-by (rtac (lub_mono RS allI RS chainI) 1);
+by (rtac (lub_mono RS chainI) 1);
by (etac ch2ch_MF2L 1);
by (atac 1);
by (etac ch2ch_MF2L 1);
by (atac 1);
by (strip_tac 1);
-by (rtac (chainE RS spec) 1);
+by (rtac (chainE) 1);
by ((rtac ch2ch_MF2R 1) THEN (etac spec 1));
by (atac 1);
qed "ch2ch_lubMF2L";
-val prems = goal thy
+Goal
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ chain(F)|] ==> \
\ monofun(% x. lub(range(% j. MF2 (F j) (x))))";
-by (cut_facts_tac prems 1);
by (rtac monofunI 1);
by (strip_tac 1);
by (rtac lub_mono 1);
@@ -238,13 +220,12 @@
by (atac 1);
qed "lub_MF2_mono";
-val prems = goal thy
+Goal
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ chain(F); chain(Y)|] ==> \
\ lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
\ lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))";
-by (cut_facts_tac prems 1);
by (rtac antisym_less 1);
by (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1);
by (etac ch2ch_lubMF2R 1);
@@ -275,13 +256,12 @@
qed "ex_lubMF2";
-val prems = goal thy
+Goal
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ chain(FY);chain(TY)|] ==>\
\ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. MF2(FY(i))(TY(i))))";
-by (cut_facts_tac prems 1);
by (rtac antisym_less 1);
by (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1);
by (etac ch2ch_lubMF2L 1);
@@ -295,7 +275,7 @@
by (rtac allI 1);
by (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1);
by (res_inst_tac [("x","ia")] exI 1);
-by (rtac (chain_mono RS mp) 1);
+by (rtac (chain_mono) 1);
by (etac allE 1);
by (etac ch2ch_MF2R 1);
by (REPEAT (atac 1));
@@ -303,7 +283,7 @@
by (res_inst_tac [("x","ia")] exI 1);
by (rtac refl_less 1);
by (res_inst_tac [("x","i")] exI 1);
-by (rtac (chain_mono RS mp) 1);
+by (rtac (chain_mono) 1);
by (etac ch2ch_MF2L 1);
by (REPEAT (atac 1));
by (rtac lub_mono 1);
@@ -317,13 +297,12 @@
by (atac 1);
qed "diag_lubMF2_1";
-val prems = goal thy
+Goal
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
\ chain(FY);chain(TY)|] ==>\
\ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. MF2(FY(i))(TY(i))))";
-by (cut_facts_tac prems 1);
by (rtac trans 1);
by (rtac ex_lubMF2 1);
by (REPEAT (atac 1));
@@ -337,46 +316,35 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
-"[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
+val [prem1,prem2,prem3,prem4] = goal thy
+"[| cont(CF2); !f. cont(CF2(f)); chain(FY); chain(TY)|] ==>\
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))";
-by (cut_facts_tac prems 1);
-by (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1);
-by (atac 1);
+by (cut_facts_tac [prem1,prem2,prem3, prem4] 1);
+by (stac (prem1 RS cont2contlub RS contlubE RS spec RS mp) 1);
+by (assume_tac 1);
by (stac thelub_fun 1);
-by (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1);
-by (atac 1);
+by (rtac (prem1 RS (cont2mono RS ch2ch_monofun)) 1);
+by (assume_tac 1);
by (rtac trans 1);
-by (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1);
-by (atac 1);
-by (rtac diag_lubMF2_2 1);
-by (etac cont2mono 1);
-by (rtac allI 1);
-by (etac allE 1);
-by (etac cont2mono 1);
-by (REPEAT (atac 1));
+by (rtac ((prem2 RS spec RS cont2contlub) RS contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1);
+by (rtac prem4 1);
+by (blast_tac (claset() addIs [diag_lubMF2_2, cont2mono]) 1);
qed "contlub_CF2";
(* ------------------------------------------------------------------------ *)
(* The following results are about application for functions in 'a=>'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "f1 << f2 ==> f1(x) << f2(x)";
-by (cut_facts_tac prems 1);
+Goal "f1 << f2 ==> f1(x) << f2(x)";
by (etac (less_fun RS iffD1 RS spec) 1);
qed "monofun_fun_fun";
-val prems = goal thy
- "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)";
-by (cut_facts_tac prems 1);
+Goal "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)";
by (etac (monofunE RS spec RS spec RS mp) 1);
by (atac 1);
qed "monofun_fun_arg";
-val prems = goal thy
-"[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)";
-by (cut_facts_tac prems 1);
+Goal "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)";
by (rtac trans_less 1);
by (etac monofun_fun_arg 1);
by (atac 1);
@@ -389,23 +357,20 @@
(* continuity *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
- "[|monofun(c1)|] ==> monofun(%x. c1 x y)";
-by (cut_facts_tac prems 1);
+Goal "[|monofun(c1)|] ==> monofun(%x. c1 x y)";
by (rtac monofunI 1);
by (strip_tac 1);
by (etac (monofun_fun_arg RS monofun_fun_fun) 1);
by (atac 1);
qed "mono2mono_MF1L";
-val prems = goal thy
- "[|cont(c1)|] ==> cont(%x. c1 x y)";
-by (cut_facts_tac prems 1);
+Goal "[|cont(c1)|] ==> cont(%x. c1 x y)";
by (rtac monocontlub2cont 1);
by (etac (cont2mono RS mono2mono_MF1L) 1);
by (rtac contlubI 1);
by (strip_tac 1);
-by (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
+by (ftac asm_rl 1);
+by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
by (atac 1);
by (stac thelub_fun 1);
by (rtac ch2ch_monofun 1);
@@ -416,20 +381,14 @@
(********* Note "(%x.%y.c1 x y) = c1" ***********)
-val prems = goal thy
- "!y. monofun(%x. c1 x y) ==> monofun(c1)";
-by (cut_facts_tac prems 1);
+Goal "!y. monofun(%x. c1 x y) ==> monofun(c1)";
by (rtac monofunI 1);
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1);
-by (atac 1);
+by (blast_tac (claset() addDs [monofunE]) 1);
qed "mono2mono_MF1L_rev";
-val prems = goal thy
- "!y. cont(%x. c1 x y) ==> cont(c1)";
-by (cut_facts_tac prems 1);
+Goal "!y. cont(%x. c1 x y) ==> cont(c1)";
by (rtac monocontlub2cont 1);
by (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1);
by (etac spec 1);
@@ -440,8 +399,7 @@
by (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1);
by (etac spec 1);
by (atac 1);
-by (rtac ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1);
-by (atac 1);
+by (blast_tac (claset() addDs [ cont2contlub RS contlubE]) 1);
qed "cont2cont_CF1L_rev";
(* ------------------------------------------------------------------------ *)
@@ -449,10 +407,9 @@
(* never used here *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
\ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))";
-by (cut_facts_tac prems 1);
by (rtac trans 1);
by (rtac (cont2contlub RS contlubE RS spec RS mp) 2);
by (atac 3);
@@ -463,10 +420,8 @@
by (atac 1);
qed "contlub_abstraction";
-val prems = goal thy
-"[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
+Goal "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
\ monofun(%x.(ft(x))(tt(x)))";
-by (cut_facts_tac prems 1);
by (rtac monofunI 1);
by (strip_tac 1);
by (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1);
@@ -479,9 +434,7 @@
qed "mono2mono_app";
-val prems = goal thy
-"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))";
-by (cut_facts_tac prems 1);
+Goal "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))";
by (rtac contlubI 1);
by (strip_tac 1);
by (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1);
@@ -509,7 +462,7 @@
(* The identity function is continuous *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "cont(% x. x)";
+Goal "cont(% x. x)";
by (rtac contI 1);
by (strip_tac 1);
by (etac thelubE 1);
@@ -520,16 +473,9 @@
(* constant functions are continuous *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [cont] "cont(%x. c)";
+Goalw [cont] "cont(%x. c)";
by (strip_tac 1);
-by (rtac is_lubI 1);
-by (rtac conjI 1);
-by (rtac ub_rangeI 1);
-by (strip_tac 1);
-by (rtac refl_less 1);
-by (strip_tac 1);
-by (dtac ub_rangeE 1);
-by (etac spec 1);
+by (blast_tac (claset() addIs [is_lubI, ub_rangeI] addDs [ub_rangeD]) 1);
qed "cont_const";
@@ -541,7 +487,7 @@
(* A non-emptyness result for Cfun *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "?x:Collect cont";
+Goal "?x:Collect cont";
by (rtac CollectI 1);
by (rtac cont_const 1);
qed "CfunI";
@@ -550,9 +496,7 @@
(* some properties of flat *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun]
- "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)";
-by (cut_facts_tac prems 1);
+Goalw [monofun] "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)";
by (strip_tac 1);
by (dtac (ax_flat RS spec RS spec RS mp) 1);
by (fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1);
--- a/src/HOLCF/Cprod1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cprod1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -11,16 +11,14 @@
(* less_cprod is a partial order on 'a * 'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Prod.thy
- "[|fst x = fst y; snd x = snd y|] ==> x = y";
-by (cut_facts_tac prems 1);
+Goal "[|fst x = fst y; snd x = snd y|] ==> x = y";
by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
by (rotate_tac ~1 1);
by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
by (asm_simp_tac (simpset_of Prod.thy) 1);
qed "Sel_injective_cprod";
-val prems = goalw Cprod1.thy [less_cprod_def] "(p::'a*'b) << p";
+Goalw [less_cprod_def] "(p::'a*'b) << p";
by (Simp_tac 1);
qed "refl_less_cprod";
@@ -30,9 +28,8 @@
by (fast_tac (HOL_cs addIs [antisym_less]) 1);
qed "antisym_less_cprod";
-val prems = goalw thy [less_cprod_def]
+Goalw [less_cprod_def]
"[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3";
-by (cut_facts_tac prems 1);
by (rtac conjI 1);
by (fast_tac (HOL_cs addIs [trans_less]) 1);
by (fast_tac (HOL_cs addIs [trans_less]) 1);
--- a/src/HOLCF/Cprod2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cprod2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,37 +7,26 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)";
+Goal "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)";
by (fold_goals_tac [less_cprod_def]);
by (rtac refl 1);
qed "inst_cprod_po";
-val prems = goalw thy [inst_cprod_po RS eq_reflection]
- "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2";
-by (cut_facts_tac prems 1);
-by (etac conjE 1);
-by (dtac (fst_conv RS subst) 1);
-by (dtac (fst_conv RS subst) 1);
-by (dtac (fst_conv RS subst) 1);
-by (dtac (snd_conv RS subst) 1);
-by (dtac (snd_conv RS subst) 1);
-by (dtac (snd_conv RS subst) 1);
-by (rtac conjI 1);
-by (atac 1);
-by (atac 1);
+Goal "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2";
+by (asm_full_simp_tac (simpset() addsimps [inst_cprod_po]) 1);
qed "less_cprod4c";
(* ------------------------------------------------------------------------ *)
(* type cprod is pointed *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "(UU,UU)<<p";
+Goal "(UU,UU)<<p";
by (simp_tac(simpset() addsimps[inst_cprod_po])1);
qed "minimal_cprod";
bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
-val prems = goal thy "? x::'a*'b.!y. x<<y";
+Goal "EX x::'a*'b. ALL y. x<<y";
by (res_inst_tac [("x","(UU,UU)")] exI 1);
by (rtac (minimal_cprod RS allI) 1);
qed "least_cprod";
@@ -46,19 +35,18 @@
(* Pair <_,_> is monotone in both arguments *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun] "monofun Pair";
+Goalw [monofun] "monofun Pair";
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
by (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1);
qed "monofun_pair1";
-val prems = goalw thy [monofun] "monofun(Pair x)";
+Goalw [monofun] "monofun(Pair x)";
by (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1);
qed "monofun_pair2";
-val prems = goal thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)";
-by (cut_facts_tac prems 1);
+Goal "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)";
by (rtac trans_less 1);
by (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS (less_fun RS iffD1 RS spec)) 1);
by (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2);
@@ -70,7 +58,7 @@
(* fst and snd are monotone *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun] "monofun fst";
+Goalw [monofun] "monofun fst";
by (strip_tac 1);
by (res_inst_tac [("p","x")] PairE 1);
by (hyp_subst_tac 1);
@@ -80,7 +68,7 @@
by (etac (less_cprod4c RS conjunct1) 1);
qed "monofun_fst";
-val prems = goalw thy [monofun] "monofun snd";
+Goalw [monofun] "monofun snd";
by (strip_tac 1);
by (res_inst_tac [("p","x")] PairE 1);
by (hyp_subst_tac 1);
@@ -94,11 +82,10 @@
(* the type 'a * 'b is a cpo *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))";
-by (cut_facts_tac prems 1);
-by (rtac (conjI RS is_lubI) 1);
-by (rtac (allI RS ub_rangeI) 1);
+by (rtac (is_lubI) 1);
+by (rtac (ub_rangeI) 1);
by (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1);
by (rtac monofun_pair 1);
by (rtac is_ub_thelub 1);
@@ -124,8 +111,7 @@
*)
-val prems = goal thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x";
-by (cut_facts_tac prems 1);
+Goal "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x";
by (rtac exI 1);
by (etac lub_cprod 1);
qed "cpo_cprod";
--- a/src/HOLCF/Cprod3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cprod3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "UU = (UU,UU)";
+Goal "UU = (UU,UU)";
by (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1);
qed "inst_cprod_pcpo";
@@ -15,11 +15,10 @@
(* continuity of (_,_) , fst, snd *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Cprod3.thy
+Goal
"chain(Y::(nat=>'a::cpo)) ==>\
\ (lub(range(Y)),(x::'b::cpo)) =\
\ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1);
by (rtac lub_equal 1);
by (atac 1);
@@ -34,7 +33,7 @@
by (rtac (lub_const RS thelubI) 1);
qed "Cprod3_lemma1";
-val prems = goal Cprod3.thy "contlub(Pair)";
+Goal "contlub(Pair)";
by (rtac contlubI 1);
by (strip_tac 1);
by (rtac (expand_fun_eq RS iffD2) 1);
@@ -48,11 +47,10 @@
by (etac Cprod3_lemma1 1);
qed "contlub_pair1";
-val prems = goal Cprod3.thy
+Goal
"chain(Y::(nat=>'a::cpo)) ==>\
\ ((x::'b::cpo),lub(range Y)) =\
\ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1);
by (rtac sym 1);
by (Simp_tac 1);
@@ -66,7 +64,7 @@
by (Simp_tac 1);
qed "Cprod3_lemma2";
-val prems = goal Cprod3.thy "contlub(Pair(x))";
+Goal "contlub(Pair(x))";
by (rtac contlubI 1);
by (strip_tac 1);
by (rtac trans 1);
@@ -75,19 +73,19 @@
by (etac Cprod3_lemma2 1);
qed "contlub_pair2";
-val prems = goal Cprod3.thy "cont(Pair)";
+Goal "cont(Pair)";
by (rtac monocontlub2cont 1);
by (rtac monofun_pair1 1);
by (rtac contlub_pair1 1);
qed "cont_pair1";
-val prems = goal Cprod3.thy "cont(Pair(x))";
+Goal "cont(Pair(x))";
by (rtac monocontlub2cont 1);
by (rtac monofun_pair2 1);
by (rtac contlub_pair2 1);
qed "cont_pair2";
-val prems = goal Cprod3.thy "contlub(fst)";
+Goal "contlub(fst)";
by (rtac contlubI 1);
by (strip_tac 1);
by (stac (lub_cprod RS thelubI) 1);
@@ -95,7 +93,7 @@
by (Simp_tac 1);
qed "contlub_fst";
-val prems = goal Cprod3.thy "contlub(snd)";
+Goal "contlub(snd)";
by (rtac contlubI 1);
by (strip_tac 1);
by (stac (lub_cprod RS thelubI) 1);
@@ -103,13 +101,13 @@
by (Simp_tac 1);
qed "contlub_snd";
-val prems = goal Cprod3.thy "cont(fst)";
+Goal "cont(fst)";
by (rtac monocontlub2cont 1);
by (rtac monofun_fst 1);
by (rtac contlub_fst 1);
qed "cont_fst";
-val prems = goal Cprod3.thy "cont(snd)";
+Goal "cont(snd)";
by (rtac monocontlub2cont 1);
by (rtac monofun_snd 1);
by (rtac contlub_snd 1);
@@ -126,7 +124,7 @@
(* convert all lemmas to the continuous versions *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Cprod3.thy [cpair_def]
+Goalw [cpair_def]
"(LAM x y.(x,y))`a`b = (a,b)";
by (stac beta_cfun 1);
by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1);
@@ -135,16 +133,15 @@
by (rtac refl 1);
qed "beta_cfun_cprod";
-val prems = goalw Cprod3.thy [cpair_def]
+Goalw [cpair_def]
" <a,b>=<aa,ba> ==> a=aa & b=ba";
-by (cut_facts_tac prems 1);
by (dtac (beta_cfun_cprod RS subst) 1);
by (dtac (beta_cfun_cprod RS subst) 1);
by (etac Pair_inject 1);
by (fast_tac HOL_cs 1);
qed "inject_cpair";
-val prems = goalw Cprod3.thy [cpair_def] "UU = <UU,UU>";
+Goalw [cpair_def] "UU = <UU,UU>";
by (rtac sym 1);
by (rtac trans 1);
by (rtac beta_cfun_cprod 1);
@@ -152,14 +149,13 @@
by (rtac inst_cprod_pcpo 1);
qed "inst_cprod_pcpo2";
-val prems = goal Cprod3.thy
+Goal
"<a,b> = UU ==> a = UU & b = UU";
-by (cut_facts_tac prems 1);
by (dtac (inst_cprod_pcpo2 RS subst) 1);
by (etac inject_cpair 1);
qed "defined_cpair_rev";
-val prems = goalw Cprod3.thy [cpair_def]
+Goalw [cpair_def]
"? a b. z=<a,b>";
by (rtac PairE 1);
by (rtac exI 1);
@@ -167,39 +163,37 @@
by (etac (beta_cfun_cprod RS ssubst) 1);
qed "Exh_Cprod2";
-val prems = goalw Cprod3.thy [cpair_def]
-"[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q";
+val prems = Goalw [cpair_def] "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q";
by (rtac PairE 1);
by (resolve_tac prems 1);
by (etac (beta_cfun_cprod RS ssubst) 1);
qed "cprodE";
-val prems = goalw Cprod3.thy [cfst_def,cpair_def]
+Goalw [cfst_def,cpair_def]
"cfst`<x,y>=x";
-by (cut_facts_tac prems 1);
by (stac beta_cfun_cprod 1);
by (stac beta_cfun 1);
by (rtac cont_fst 1);
by (Simp_tac 1);
qed "cfst2";
-val prems = goalw Cprod3.thy [csnd_def,cpair_def]
+Goalw [csnd_def,cpair_def]
"csnd`<x,y>=y";
-by (cut_facts_tac prems 1);
by (stac beta_cfun_cprod 1);
by (stac beta_cfun 1);
by (rtac cont_snd 1);
by (Simp_tac 1);
qed "csnd2";
-val _ = goal Cprod3.thy "cfst`UU = UU";
+Goal "cfst`UU = UU";
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1);
qed "cfst_strict";
-val _ = goal Cprod3.thy "csnd`UU = UU";
+
+Goal "csnd`UU = UU";
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1);
qed "csnd_strict";
-val prems = goalw Cprod3.thy [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p";
+Goalw [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p";
by (stac beta_cfun_cprod 1);
by (stac beta_cfun 1);
by (rtac cont_snd 1);
@@ -208,19 +202,17 @@
by (rtac (surjective_pairing RS sym) 1);
qed "surjective_pairing_Cprod2";
-val prems = goalw Cprod3.thy [cfst_def,csnd_def,cpair_def]
+Goalw [cfst_def,csnd_def,cpair_def]
"<xa,ya> << <x,y> ==> xa<<x & ya << y";
-by (cut_facts_tac prems 1);
by (rtac less_cprod4c 1);
by (dtac (beta_cfun_cprod RS subst) 1);
by (dtac (beta_cfun_cprod RS subst) 1);
by (atac 1);
qed "less_cprod5c";
-val prems = goalw Cprod3.thy [cfst_def,csnd_def,cpair_def]
+Goalw [cfst_def,csnd_def,cpair_def]
"[|chain(S)|] ==> range(S) <<| \
\ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>";
-by (cut_facts_tac prems 1);
by (stac beta_cfun_cprod 1);
by (stac (beta_cfun RS ext) 1);
by (rtac cont_snd 1);
@@ -236,14 +228,14 @@
lub (range ?S1) =
<lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>"
*)
-val prems = goalw Cprod3.thy [csplit_def]
+Goalw [csplit_def]
"csplit`f`<x,y> = f`x`y";
by (stac beta_cfun 1);
by (Simp_tac 1);
by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1);
qed "csplit2";
-val prems = goalw Cprod3.thy [csplit_def]
+Goalw [csplit_def]
"csplit`cpair`z=z";
by (stac beta_cfun 1);
by (Simp_tac 1);
--- a/src/HOLCF/Fix.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Fix.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,13 +10,9 @@
(* derive inductive properties of iterate from primitive recursion *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "iterate (Suc n) F x = iterate n F (F`x)";
+Goal "iterate (Suc n) F x = iterate n F (F`x)";
by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (stac iterate_Suc 1);
-by (stac iterate_Suc 1);
-by (etac ssubst 1);
-by (rtac refl 1);
+by Auto_tac;
qed "iterate_Suc2";
(* ------------------------------------------------------------------------ *)
@@ -24,20 +20,15 @@
(* This property is essential since monotonicity of iterate makes no sense *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [chain]
- " x << F`x ==> chain (%i. iterate i F x)";
-by (cut_facts_tac prems 1);
+Goalw [chain] "x << F`x ==> chain (%i. iterate i F x)";
by (strip_tac 1);
-by (Simp_tac 1);
by (induct_tac "i" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
by (etac monofun_cfun_arg 1);
qed "chain_iterate2";
-val prems = goal thy
- "chain (%i. iterate i F UU)";
+Goal "chain (%i. iterate i F UU)";
by (rtac chain_iterate2 1);
by (rtac minimal 1);
qed "chain_iterate";
@@ -49,7 +40,7 @@
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [Ifix_def] "Ifix F =F`(Ifix F)";
+Goalw [Ifix_def] "Ifix F =F`(Ifix F)";
by (stac contlub_cfun_arg 1);
by (rtac chain_iterate 1);
by (rtac antisym_less 1);
@@ -59,20 +50,18 @@
by (rtac chain_iterate 1);
by (rtac allI 1);
by (rtac (iterate_Suc RS subst) 1);
-by (rtac (chain_iterate RS chainE RS spec) 1);
+by (rtac (chain_iterate RS chainE) 1);
by (rtac is_lub_thelub 1);
by (rtac ch2ch_Rep_CFunR 1);
by (rtac chain_iterate 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (rtac (iterate_Suc RS subst) 1);
by (rtac is_ub_thelub 1);
by (rtac chain_iterate 1);
qed "Ifix_eq";
-val prems = goalw thy [Ifix_def] "F`x=x ==> Ifix(F) << x";
-by (cut_facts_tac prems 1);
+Goalw [Ifix_def] "F`x=x ==> Ifix(F) << x";
by (rtac is_lub_thelub 1);
by (rtac chain_iterate 1);
by (rtac ub_rangeI 1);
@@ -103,7 +92,7 @@
(* In this special case it is the application function Rep_CFun *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [contlub] "contlub(iterate(i))";
+Goalw [contlub] "contlub(iterate(i))";
by (strip_tac 1);
by (induct_tac "i" 1);
by (Asm_simp_tac 1);
@@ -112,10 +101,9 @@
by (rtac ext 1);
by (stac thelub_fun 1);
by (rtac chainI 1);
-by (rtac allI 1);
by (rtac (less_fun RS iffD2) 1);
by (rtac allI 1);
-by (rtac (chainE RS spec) 1);
+by (rtac (chainE) 1);
by (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1);
by (rtac allI 1);
by (rtac monofun_Rep_CFun2 1);
@@ -132,7 +120,7 @@
qed "contlub_iterate";
-val prems = goal thy "cont(iterate(i))";
+Goal "cont(iterate(i))";
by (rtac monocontlub2cont 1);
by (rtac monofun_iterate 1);
by (rtac contlub_iterate 1);
@@ -142,7 +130,7 @@
(* a lemma about continuity of iterate in its third argument *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "monofun(iterate n F)";
+Goal "monofun(iterate n F)";
by (rtac monofunI 1);
by (strip_tac 1);
by (induct_tac "n" 1);
@@ -164,7 +152,7 @@
by (etac (monofun_iterate2 RS ch2ch_monofun) 1);
qed "contlub_iterate2";
-val prems = goal thy "cont (iterate n F)";
+Goal "cont (iterate n F)";
by (rtac monocontlub2cont 1);
by (rtac monofun_iterate2 1);
by (rtac contlub_iterate2 1);
@@ -189,16 +177,15 @@
(* be derived for lubs in this argument *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))";
-by (cut_facts_tac prems 1);
by (rtac chainI 1);
by (strip_tac 1);
by (rtac lub_mono 1);
by (rtac chain_iterate 1);
by (rtac chain_iterate 1);
by (strip_tac 1);
-by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE RS spec) 1);
+by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE) 1);
qed "chain_iterate_lub";
(* ------------------------------------------------------------------------ *)
@@ -207,18 +194,16 @@
(* chains is the essential argument which is usually derived from monot. *)
(* ------------------------------------------------------------------------ *)
-Goal
- "chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))";
+Goal "chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))";
by (rtac (thelub_fun RS subst) 1);
by (etac (monofun_iterate RS ch2ch_monofun) 1);
by (asm_simp_tac (simpset() addsimps [contlub_iterate RS contlubE]) 1);
qed "contlub_Ifix_lemma1";
-val prems = goal thy "chain(Y) ==>\
+Goal "chain(Y) ==>\
\ lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
\ lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))";
-by (cut_facts_tac prems 1);
by (rtac antisym_less 1);
by (rtac is_lub_thelub 1);
by (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1);
@@ -247,7 +232,7 @@
qed "ex_lub_iterate";
-val prems = goalw thy [contlub,Ifix_def] "contlub(Ifix)";
+Goalw [contlub,Ifix_def] "contlub(Ifix)";
by (strip_tac 1);
by (stac (contlub_Ifix_lemma1 RS ext) 1);
by (atac 1);
@@ -255,7 +240,7 @@
qed "contlub_Ifix";
-val prems = goal thy "cont(Ifix)";
+Goal "cont(Ifix)";
by (rtac monocontlub2cont 1);
by (rtac monofun_Ifix 1);
by (rtac contlub_Ifix 1);
@@ -265,21 +250,19 @@
(* propagate properties of Ifix to its continuous counterpart *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [fix_def] "fix`F = F`(fix`F)";
+Goalw [fix_def] "fix`F = F`(fix`F)";
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
by (rtac Ifix_eq 1);
qed "fix_eq";
-val prems = goalw thy [fix_def] "F`x = x ==> fix`F << x";
-by (cut_facts_tac prems 1);
+Goalw [fix_def] "F`x = x ==> fix`F << x";
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
by (etac Ifix_least 1);
qed "fix_least";
-val prems = goal thy
+Goal
"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F";
-by (cut_facts_tac prems 1);
by (rtac antisym_less 1);
by (etac allE 1);
by (etac mp 1);
@@ -288,28 +271,24 @@
qed "fix_eqI";
-val prems = goal thy "f == fix`F ==> f = F`f";
-by (rewrite_goals_tac prems);
-by (rtac fix_eq 1);
+Goal "f == fix`F ==> f = F`f";
+by (asm_simp_tac (simpset() addsimps [fix_eq RS sym]) 1);
qed "fix_eq2";
-val prems = goal thy "f == fix`F ==> f`x = F`f`x";
-by (rtac trans 1);
-by (rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1);
-by (rtac refl 1);
+Goal "f == fix`F ==> f`x = F`f`x";
+by (etac (fix_eq2 RS cfun_fun_cong) 1);
qed "fix_eq3";
fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i));
-val prems = goal thy "f = fix`F ==> f = F`f";
-by (cut_facts_tac prems 1);
+Goal "f = fix`F ==> f = F`f";
by (hyp_subst_tac 1);
by (rtac fix_eq 1);
qed "fix_eq4";
-val prems = goal thy "f = fix`F ==> f`x = F`f`x";
+Goal "f = fix`F ==> f`x = F`f`x";
by (rtac trans 1);
-by (rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1);
+by (etac (fix_eq4 RS cfun_fun_cong) 1);
by (rtac refl 1);
qed "fix_eq5";
@@ -346,7 +325,7 @@
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "Ifix=(%x. lub(range(%i. iterate i x UU)))";
+Goal "Ifix=(%x. lub(range(%i. iterate i x UU)))";
by (rtac ext 1);
by (rewtac Ifix_def);
by (rtac refl 1);
@@ -356,8 +335,7 @@
(* direct connection between fix and iteration without Ifix *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [fix_def]
- "fix`F = lub(range(%i. iterate i F UU))";
+Goalw [fix_def] "fix`F = lub(range(%i. iterate i F UU))";
by (fold_goals_tac [Ifix_def]);
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
qed "fix_def2";
@@ -371,17 +349,16 @@
(* access to definitions *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [adm_def]
- "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)";
-by (fast_tac (HOL_cs addIs prems) 1);
+val prems = Goalw [adm_def]
+ "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)";
+by (blast_tac (claset() addIs prems) 1);
qed "admI";
Goalw [adm_def] "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))";
by (Blast_tac 1);
qed "admD";
-val prems = goalw thy [admw_def]
- "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
+Goalw [admw_def] "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
\ P (lub(range(%i. iterate i F UU))))";
by (rtac refl 1);
qed "admw_def2";
@@ -390,7 +367,7 @@
(* an admissible formula is also weak admissible *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [admw_def] "!!P. adm(P)==>admw(P)";
+Goalw [admw_def] "!!P. adm(P)==>admw(P)";
by (strip_tac 1);
by (etac admD 1);
by (rtac chain_iterate 1);
@@ -401,23 +378,19 @@
(* fixed point induction *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
-"[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)";
-by (cut_facts_tac prems 1);
+val major::prems = Goal
+ "[| adm(P); P(UU); !!x. P(x) ==> P(F`x)|] ==> P(fix`F)";
by (stac fix_def2 1);
-by (etac admD 1);
+by (rtac (major RS admD) 1);
by (rtac chain_iterate 1);
by (rtac allI 1);
by (induct_tac "i" 1);
-by (stac iterate_0 1);
-by (atac 1);
-by (stac iterate_Suc 1);
-by (resolve_tac prems 1);
-by (atac 1);
+by (asm_simp_tac (simpset() addsimps (iterate_0::prems)) 1);
+by (asm_simp_tac (simpset() addsimps (iterate_Suc::prems)) 1);
qed "fix_ind";
-val prems = goal thy "[| f == fix`F; adm(P); \
-\ P(UU);!!x. P(x) ==> P(F`x)|] ==> P f";
+val prems = Goal "[| f == fix`F; adm(P); \
+\ P(UU); !!x. P(x) ==> P(F`x)|] ==> P f";
by (cut_facts_tac prems 1);
by (asm_simp_tac HOL_ss 1);
by (etac fix_ind 1);
@@ -429,9 +402,7 @@
(* computational induction for weak admissible formulae *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
-"[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)";
-by (cut_facts_tac prems 1);
+Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)";
by (stac fix_def2 1);
by (rtac (admw_def2 RS iffD1 RS spec RS mp) 1);
by (atac 1);
@@ -439,9 +410,8 @@
by (etac spec 1);
qed "wfix_ind";
-val prems = goal thy "[| f == fix`F; admw(P); \
+Goal "[| f == fix`F; admw(P); \
\ !n. P(iterate n F UU) |] ==> P f";
-by (cut_facts_tac prems 1);
by (asm_simp_tac HOL_ss 1);
by (etac wfix_ind 1);
by (atac 1);
@@ -451,9 +421,8 @@
(* for chain-finite (easy) types every formula is admissible *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [adm_def]
+Goalw [adm_def]
"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)";
-by (cut_facts_tac prems 1);
by (strip_tac 1);
by (rtac exE 1);
by (rtac mp 1);
@@ -484,7 +453,7 @@
(* improved admisibility introduction *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [adm_def]
+val prems = Goalw [adm_def]
"(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
\ ==> P(lub (range Y))) ==> adm P";
by (strip_tac 1);
@@ -500,38 +469,31 @@
(* admissibility of special formulae and propagation *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [adm_def]
- "[|cont u;cont v|]==> adm(%x. u x << v x)";
-by (cut_facts_tac prems 1);
+Goalw [adm_def] "[|cont u;cont v|]==> adm(%x. u x << v x)";
by (strip_tac 1);
+by (forw_inst_tac [("f","u")] (cont2mono RS ch2ch_monofun) 1);
+by (assume_tac 1);
+by (forw_inst_tac [("f","v")] (cont2mono RS ch2ch_monofun) 1);
+by (assume_tac 1);
by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
by (atac 1);
by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
by (atac 1);
-by (rtac lub_mono 1);
-by (cut_facts_tac prems 1);
-by (etac (cont2mono RS ch2ch_monofun) 1);
-by (atac 1);
-by (cut_facts_tac prems 1);
-by (etac (cont2mono RS ch2ch_monofun) 1);
-by (atac 1);
-by (atac 1);
+by (blast_tac (claset() addIs [lub_mono]) 1);
qed "adm_less";
Addsimps [adm_less];
-val prems = goal thy
- "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)";
+Goal "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)";
by (fast_tac (HOL_cs addEs [admD] addIs [admI]) 1);
qed "adm_conj";
Addsimps [adm_conj];
-val prems = goalw thy [adm_def] "adm(%x. t)";
+Goalw [adm_def] "adm(%x. t)";
by (fast_tac HOL_cs 1);
qed "adm_not_free";
Addsimps [adm_not_free];
-val prems = goalw thy [adm_def]
- "!!t. cont t ==> adm(%x.~ (t x) << u)";
+Goalw [adm_def] "!!t. cont t ==> adm(%x.~ (t x) << u)";
by (strip_tac 1);
by (rtac contrapos 1);
by (etac spec 1);
@@ -542,15 +504,13 @@
by (atac 1);
qed "adm_not_less";
-val prems = goal thy
- "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)";
+Goal "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)";
by (fast_tac (HOL_cs addIs [admI] addEs [admD]) 1);
qed "adm_all";
bind_thm ("adm_all2", allI RS adm_all);
-val prems = goal thy
- "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))";
+Goal "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))";
by (rtac admI 1);
by (stac (cont2contlub RS contlubE RS spec RS mp) 1);
by (atac 1);
@@ -561,7 +521,7 @@
by (atac 1);
qed "adm_subst";
-val prems = goal thy "adm(%x.~ UU << t(x))";
+Goal "adm(%x.~ UU << t(x))";
by (Simp_tac 1);
qed "adm_UU_not_less";
@@ -589,32 +549,27 @@
(* ------------------------------------------------------------------------ *)
-val prems = goal HOL.thy
- "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))";
-by (cut_facts_tac prems 1);
-by (fast_tac HOL_cs 1);
+Goal "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))";
+by (Fast_tac 1);
qed "adm_disj_lemma1";
-val _ = goal thy
- "!!Q. [| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\
+Goal "[| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))";
-by (fast_tac (claset() addEs [admD] addss simpset()) 1);
+by (force_tac (claset() addEs [admD], simpset()) 1);
qed "adm_disj_lemma2";
-val _ = goalw thy [chain]
- "!!Q. chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)";
+Goalw [chain] "chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)";
by (Asm_simp_tac 1);
by (safe_tac HOL_cs);
by (subgoal_tac "ia = i" 1);
by (ALLGOALS Asm_simp_tac);
qed "adm_disj_lemma3";
-val _ = goal Arith.thy
- "!!Q. !j. i < j --> Q(Y(j)) ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)";
-by (asm_simp_tac (simpset_of Arith.thy) 1);
+Goal "!j. i < j --> Q(Y(j)) ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)";
+by (Asm_simp_tac 1);
qed "adm_disj_lemma4";
-val prems = goal thy
+Goal
"!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))";
by (safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]));
@@ -623,10 +578,9 @@
by (Asm_simp_tac 1);
qed "adm_disj_lemma5";
-val prems = goal thy
+Goal
"[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
\ ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))";
-by (cut_facts_tac prems 1);
by (etac exE 1);
by (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1);
by (rtac conjI 1);
@@ -640,12 +594,10 @@
by (atac 1);
qed "adm_disj_lemma6";
-val prems = goal thy
+Goal
"[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ chain(%m. Y(Least(%j. m<j & P(Y(j)))))";
-by (cut_facts_tac prems 1);
by (rtac chainI 1);
-by (rtac allI 1);
by (rtac chain_mono3 1);
by (atac 1);
by (rtac Least_le 1);
@@ -661,19 +613,17 @@
by (atac 1);
qed "adm_disj_lemma7";
-val prems = goal thy
+Goal
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))";
-by (cut_facts_tac prems 1);
by (strip_tac 1);
by (etac allE 1);
by (etac exE 1);
by (etac (LeastI RS conjunct2) 1);
qed "adm_disj_lemma8";
-val prems = goal thy
+Goal
"[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))";
-by (cut_facts_tac prems 1);
by (rtac antisym_less 1);
by (rtac lub_mono 1);
by (atac 1);
@@ -681,7 +631,7 @@
by (atac 1);
by (atac 1);
by (strip_tac 1);
-by (rtac (chain_mono RS mp) 1);
+by (rtac (chain_mono) 1);
by (atac 1);
by (etac allE 1);
by (etac exE 1);
@@ -694,15 +644,13 @@
by (atac 1);
by (strip_tac 1);
by (rtac exI 1);
-by (rtac (chain_mono RS mp) 1);
+by (rtac (chain_mono) 1);
by (atac 1);
by (rtac lessI 1);
qed "adm_disj_lemma9";
-val prems = goal thy
- "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
+Goal "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1);
by (rtac conjI 1);
by (rtac adm_disj_lemma7 1);
@@ -716,25 +664,21 @@
by (atac 1);
qed "adm_disj_lemma10";
-val prems = goal thy
- "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))";
-by (cut_facts_tac prems 1);
+Goal "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))";
by (etac adm_disj_lemma2 1);
by (etac adm_disj_lemma6 1);
by (atac 1);
qed "adm_disj_lemma12";
-val prems = goal thy
+Goal
"[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))";
-by (cut_facts_tac prems 1);
by (etac adm_disj_lemma2 1);
by (etac adm_disj_lemma10 1);
by (atac 1);
qed "adm_lemma11";
-val prems = goal thy
- "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)";
+Goal "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)";
by (rtac admI 1);
by (rtac (adm_disj_lemma1 RS disjE) 1);
by (atac 1);
@@ -752,8 +696,7 @@
bind_thm("adm_lemma11",adm_lemma11);
bind_thm("adm_disj",adm_disj);
-val prems = goal thy
- "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
+Goal "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
by (etac ssubst 1);
by (etac adm_disj 1);
@@ -770,9 +713,7 @@
qed"adm_iff";
-val prems= goal thy
-"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))";
-by (cut_facts_tac prems 1);
+Goal "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))";
by (subgoal_tac "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1);
by (rtac ext 2);
by (fast_tac HOL_cs 2);
--- a/src/HOLCF/Fun2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Fun2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "(op <<)=(%f g.!x. f x << g x)";
+Goal "(op <<)=(%f g.!x. f x << g x)";
by (fold_goals_tac [less_fun_def]);
by (rtac refl 1);
qed "inst_fun_po";
@@ -16,13 +16,13 @@
(* Type 'a::term => 'b::pcpo is pointed *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "(%z. UU) << x";
+Goal "(%z. UU) << x";
by (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1);
qed "minimal_fun";
bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
-val prems = goal thy "? x::'a=>'b::pcpo.!y. x<<y";
+Goal "? x::'a=>'b::pcpo.!y. x<<y";
by (res_inst_tac [("x","(%z. UU)")] exI 1);
by (rtac (minimal_fun RS allI) 1);
qed "least_fun";
@@ -31,7 +31,7 @@
(* make the symbol << accessible for type fun *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "(f1 << f2) = (! x. f1(x) << f2(x))";
+Goal "(f1 << f2) = (! x. f1(x) << f2(x))";
by (stac inst_fun_po 1);
by (rtac refl 1);
qed "less_fun";
@@ -48,29 +48,21 @@
(* upper bounds of function chains yield upper bound in the po range *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Fun2.thy
- " range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
-by (cut_facts_tac prems 1);
+Goal "range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
by (rtac ub_rangeI 1);
-by (rtac allI 1);
-by (rtac allE 1);
-by (rtac (less_fun RS subst) 1);
-by (etac (ub_rangeE RS spec) 1);
-by (atac 1);
+by (dtac ub_rangeD 1);
+by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
+by Auto_tac;
qed "ub2ub_fun";
(* ------------------------------------------------------------------------ *)
(* Type 'a::term => 'b::pcpo is chain complete *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Fun2.thy
- "chain(S::nat=>('a::term => 'b::cpo)) ==> \
+Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> \
\ range(S) <<| (% x. lub(range(% i. S(i)(x))))";
-by (cut_facts_tac prems 1);
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (stac less_fun 1);
by (rtac allI 1);
by (rtac is_ub_thelub 1);
@@ -86,9 +78,7 @@
bind_thm ("thelub_fun", lub_fun RS thelubI);
(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
-val prems = goal Fun2.thy
- "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x";
-by (cut_facts_tac prems 1);
+Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x";
by (rtac exI 1);
by (etac lub_fun 1);
qed "cpo_fun";
--- a/src/HOLCF/Fun3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Fun3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -5,6 +5,6 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "UU = (%x. UU)";
+Goal "UU = (%x. UU)";
by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
qed "inst_fun_pcpo";
--- a/src/HOLCF/Lift1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Lift1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -17,14 +17,12 @@
by (fast_tac HOL_cs 1);
qed"refl_less_lift";
-val prems = goalw thy [less_lift_def]
+Goalw [less_lift_def]
"[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
-by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"antisym_less_lift";
-val prems = goalw Lift1.thy [less_lift_def]
+Goalw [less_lift_def]
"[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
-by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"trans_less_lift";
--- a/src/HOLCF/Lift2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Lift2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "(op <<)=(%x y. x=y|x=Undef)";
+Goal "(op <<)=(%x y. x=y|x=Undef)";
by (fold_goals_tac [less_lift_def]);
by (rtac refl 1);
qed "inst_lift_po";
@@ -22,7 +22,9 @@
bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
-val prems = goal thy "? x::'a lift.!y. x<<y";
+AddIffs [minimal_lift];
+
+Goal "EX x::'a lift. ALL y. x<<y";
by (res_inst_tac [("x","Undef")] exI 1);
by (rtac (minimal_lift RS allI) 1);
qed "least_lift";
@@ -39,41 +41,37 @@
(* Tailoring notUU_I of Pcpo.ML to Undef *)
Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
-by (etac contrapos 1);
-by (hyp_subst_tac 1);
-by (rtac antisym_less 1);
-by (atac 1);
-by (rtac minimal_lift 1);
+by (blast_tac (claset() addIs [antisym_less]) 1);
qed"notUndef_I";
(* Tailoring chain_mono2 of Pcpo.ML to Undef *)
-Goal "[| ? j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \
-\ ==> ? j.!i. j<i-->~Y(i)=Undef";
+Goal "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \
+\ ==> EX j. ALL i. j<i-->~Y(i)=Undef";
by Safe_tac;
by (Step_tac 1);
by (strip_tac 1);
by (rtac notUndef_I 1);
by (atac 2);
-by (etac (chain_mono RS mp) 1);
+by (etac (chain_mono) 1);
by (atac 1);
qed"chain_mono2_po";
(* Tailoring flat_imp_chfin of Fix.ML to lift *)
-Goal "(! Y. chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
+Goal "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))";
by (rewtac max_in_chain_def);
by (strip_tac 1);
-by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm 1);
+by (res_inst_tac [("P","ALL i. Y(i)=Undef")] case_split_thm 1);
by (res_inst_tac [("x","0")] exI 1);
by (strip_tac 1);
by (rtac trans 1);
by (etac spec 1);
by (rtac sym 1);
by (etac spec 1);
-by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
+by (subgoal_tac "ALL x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
by (rtac (chain_mono2_po RS exE) 1);
by (Fast_tac 1);
@@ -86,29 +84,16 @@
by (dtac spec 1);
by (etac spec 1);
by (etac (le_imp_less_or_eq RS disjE) 1);
-by (etac (chain_mono RS mp) 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (rtac refl_less 1);
-by (res_inst_tac [("P","Y(Suc(x)) = Undef")] notE 1);
-by (atac 2);
-by (rtac mp 1);
-by (etac spec 1);
-by (Asm_simp_tac 1);
+by (etac (chain_mono) 1);
+by Auto_tac;
qed"flat_imp_chfin_poo";
(* Main Lemma: cpo_lift *)
-Goal "chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
+Goal "chain(Y::nat=>('a)lift) ==> EX x. range(Y) <<|x";
by (cut_inst_tac [] flat_imp_chfin_poo 1);
-by (Step_tac 1);
-by Safe_tac;
-by (Step_tac 1);
-by (rtac exI 1);
-by (rtac lub_finch1 1);
-by (atac 1);
-by (atac 1);
+by (blast_tac (claset() addIs [lub_finch1]) 1);
qed"cpo_lift";
--- a/src/HOLCF/Lift3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Lift3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -8,7 +8,7 @@
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "UU = Undef";
+Goal "UU = Undef";
by (simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1);
qed "inst_lift_pcpo";
@@ -86,8 +86,7 @@
by (Asm_simp_tac 1);
qed"Lift_exhaust";
-val prems = goal thy
- "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P";
+val prems = Goal "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P";
by (cut_facts_tac [Lift_exhaust] 1);
by (fast_tac (HOL_cs addSEs prems) 1);
qed"Lift_cases";
@@ -103,13 +102,11 @@
bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym);
-val prems = goal thy "Def x = UU ==> R";
-by (cut_facts_tac prems 1);
+Goal "Def x = UU ==> R";
by (asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1);
qed "DefE";
-val prems = goal thy "[| x = Def s; x = UU |] ==> R";
-by (cut_facts_tac prems 1);
+Goal "[| x = Def s; x = UU |] ==> R";
by (fast_tac (HOL_cs addSDs [DefE]) 1);
qed"DefE2";
@@ -151,10 +148,8 @@
(* continuity of if then else *)
-val prems = goal thy "[| cont f1; cont f2 |] ==> \
-\ cont (%x. if b then f1 x else f2 x)";
-by (cut_facts_tac prems 1);
+Goal "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)";
by (case_tac "b" 1);
-by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
+by Auto_tac;
qed"cont_if";
--- a/src/HOLCF/One.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/One.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,14 +10,13 @@
(* Exhaustion and Elimination for type one *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [ONE_def] "t=UU | t = ONE";
+Goalw [ONE_def] "t=UU | t = ONE";
by (lift.induct_tac "t" 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed "Exh_one";
-val prems = goal thy
- "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q";
+val prems = Goal "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q";
by (rtac (Exh_one RS disjE) 1);
by (eresolve_tac prems 1);
by (eresolve_tac prems 1);
--- a/src/HOLCF/Pcpo.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Pcpo.ML Wed Jul 05 16:37:52 2000 +0200
@@ -18,14 +18,14 @@
bind_thm("minimal", UU_least RS spec);
+AddIffs [minimal];
+
(* ------------------------------------------------------------------------ *)
(* in cpo's everthing equal to THE lub has lub properties for every chain *)
(* ------------------------------------------------------------------------ *)
-Goal "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l ";
-by (hyp_subst_tac 1);
-by (rtac lubI 1);
-by (etac cpo 1);
+Goal "[| chain(S); lub(range(S)) = (l::'a::cpo) |] ==> range(S) <<| l ";
+by (blast_tac (claset() addDs [cpo] addIs [lubI]) 1);
qed "thelubE";
(* ------------------------------------------------------------------------ *)
@@ -33,11 +33,14 @@
(* ------------------------------------------------------------------------ *)
-bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
-(* chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *)
+Goal "chain (S::nat => 'a::cpo) ==> S(x) << lub(range(S))";
+by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_ub_lub]) 1);
+qed "is_ub_thelub";
-bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
-(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *)
+Goal "[| chain (S::nat => 'a::cpo); range(S) <| x |] ==> lub(range S) << x";
+by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_lub_lub]) 1);
+qed "is_lub_thelub";
+
Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))";
by (rtac iffI 1);
@@ -58,7 +61,6 @@
\ ==> lub(range(C1)) << lub(range(C2))";
by (etac is_lub_thelub 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (rtac trans_less 1);
by (etac spec 1);
by (etac is_ub_thelub 1);
@@ -103,7 +105,7 @@
by (rtac is_ub_thelub 1);
by (assume_tac 1);
by (res_inst_tac [("y","X(Suc(j))")] trans_less 1);
-by (rtac (chain_mono RS mp) 1);
+by (rtac chain_mono 1);
by (assume_tac 1);
by (rtac (not_less_eq RS subst) 1);
by (atac 1);
@@ -164,7 +166,6 @@
Goal "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU";
by (rtac lub_chain_maxelem 1);
-by (rtac exI 1);
by (etac spec 1);
by (rtac allI 1);
by (rtac (antisym_less_inverse RS conjunct1) 1);
@@ -181,7 +182,7 @@
Goal
"[|EX j. ~Y(j)=UU;chain(Y::nat=>'a::pcpo)|] ==> EX j. ALL i. j<i-->~Y(i)=UU";
-by (blast_tac (claset() addDs [notUU_I, chain_mono RS mp]) 1);
+by (blast_tac (claset() addDs [notUU_I, chain_mono]) 1);
qed "chain_mono2";
(**************************************)
@@ -192,9 +193,10 @@
(* flat types are chfin *)
(* ------------------------------------------------------------------------ *)
+(*Used only in an "instance" declaration (Fun1.thy)*)
Goalw [max_in_chain_def]
- "ALL Y::nat=>'a::flat. chain Y-->(EX n. max_in_chain n Y)";
-by (strip_tac 1);
+ "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)";
+by (Clarify_tac 1);
by (case_tac "ALL i. Y(i)=UU" 1);
by (res_inst_tac [("x","0")] exI 1);
by (Asm_simp_tac 1);
@@ -202,11 +204,9 @@
by (etac exE 1);
by (res_inst_tac [("x","i")] exI 1);
by (strip_tac 1);
-by (dres_inst_tac [("x","i"),("y","j")] chain_mono 1);
by (etac (le_imp_less_or_eq RS disjE) 1);
by Safe_tac;
-by (dtac (ax_flat RS spec RS spec RS mp) 1);
-by (Fast_tac 1);
+by (blast_tac (claset() addDs [chain_mono, ax_flat RS spec RS spec RS mp]) 1);
qed "flat_imp_chfin";
(* flat subclass of chfin --> adm_flat not needed *)
@@ -253,5 +253,5 @@
by (rewtac finite_chain_def);
by (rewtac max_in_chain_def);
by (fast_tac (HOL_cs addIs prems
- addDs [le_imp_less_or_eq] addEs [chain_mono RS mp]) 1);
+ addDs [le_imp_less_or_eq] addEs [chain_mono]) 1);
qed "increasing_chain_adm_lemma";
--- a/src/HOLCF/Porder.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Porder.ML Wed Jul 05 16:37:52 2000 +0200
@@ -11,46 +11,25 @@
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [is_lub, is_ub]
+Goalw [is_lub, is_ub]
"[| S <<| x ; S <<| y |] ==> x=y";
-by (cut_facts_tac prems 1);
-by (etac conjE 1);
-by (etac conjE 1);
-by (rtac antisym_less 1);
-by (rtac mp 1);
-by ((etac allE 1) THEN (atac 1) THEN (atac 1));
-by (rtac mp 1);
-by ((etac allE 1) THEN (atac 1) THEN (atac 1));
+by (blast_tac (claset() addIs [antisym_less]) 1);
qed "unique_lub";
(* ------------------------------------------------------------------------ *)
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [chain] "chain F ==> x<y --> F x<<F y";
-by (cut_facts_tac prems 1);
+Goalw [chain] "chain F ==> x<y --> F x<<F y";
by (induct_tac "y" 1);
-by (rtac impI 1);
-by (etac less_zeroE 1);
-by (stac less_Suc_eq 1);
-by (strip_tac 1);
-by (etac disjE 1);
-by (rtac trans_less 1);
-by (etac allE 2);
-by (atac 2);
-by (fast_tac HOL_cs 1);
-by (hyp_subst_tac 1);
-by (etac allE 1);
-by (atac 1);
-qed "chain_mono";
+by Auto_tac;
+by (blast_tac (claset() addIs [trans_less]) 2);
+by (blast_tac (claset() addSEs [less_SucE]) 1);
+qed_spec_mp "chain_mono";
Goal "[| chain F; x <= y |] ==> F x << F y";
-by (rtac (le_imp_less_or_eq RS disjE) 1);
-by (atac 1);
-by (etac (chain_mono RS mp) 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (rtac refl_less 1);
+by (dtac le_imp_less_or_eq 1);
+by (blast_tac (claset() addIs [chain_mono]) 1);
qed "chain_mono3";
@@ -58,11 +37,10 @@
(* The range of a chain is a totally ordered << *)
(* ------------------------------------------------------------------------ *)
-val _ = goalw thy [tord]
-"!!F. chain(F) ==> tord(range(F))";
+Goalw [tord] "chain(F) ==> tord(range(F))";
by (Safe_tac);
by (rtac nat_less_cases 1);
-by (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])));
+by (ALLGOALS (fast_tac (claset() addIs [chain_mono])));
qed "chain_tord";
@@ -71,21 +49,9 @@
(* ------------------------------------------------------------------------ *)
bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
-Goal "? x. M <<| x ==> M <<| lub(M)";
-by (stac lub 1);
-by (etac (select_eq_Ex RS iffD2) 1);
-qed "lubI";
-
-Goal "M <<| lub(M) ==> ? x. M <<| x";
-by (etac exI 1);
-qed "lubE";
-
-Goal "(? x. M <<| x) = M <<| lub(M)";
-by (stac lub 1);
-by (rtac (select_eq_Ex RS subst) 1);
-by (rtac refl 1);
-qed "lub_eq";
-
+Goal "EX x. M <<| x ==> M <<| lub(M)";
+by (asm_full_simp_tac (simpset() addsimps [lub, Ex_def]) 1);
+bind_thm ("lubI", exI RS result());
Goal "M <<| l ==> lub(M) = l";
by (rtac unique_lub 1);
@@ -96,8 +62,7 @@
Goal "lub{x} = x";
-by (rtac thelubI 1);
-by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
+by (simp_tac (simpset() addsimps [thelubI,is_lub,is_ub]) 1);
qed "lub_singleton";
Addsimps [lub_singleton];
@@ -105,65 +70,51 @@
(* access to some definition as inference rule *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [is_lub]
- "S <<| x ==> S <| x & (! u. S <| u --> x << u)";
-by (cut_facts_tac prems 1);
-by (atac 1);
-qed "is_lubE";
+Goalw [is_lub] "S <<| x ==> S <| x";
+by Auto_tac;
+qed "is_lubD1";
-val prems = goalw thy [is_lub]
- "S <| x & (! u. S <| u --> x << u) ==> S <<| x";
-by (cut_facts_tac prems 1);
-by (atac 1);
+Goalw [is_lub] "[| S <<| x; S <| u |] ==> x << u";
+by Auto_tac;
+qed "is_lub_lub";
+
+val prems = Goalw [is_lub]
+ "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x";
+by (blast_tac (claset() addIs prems) 1);
qed "is_lubI";
-val prems = goalw thy [chain] "chain F ==> !i. F(i) << F(Suc(i))";
-by (cut_facts_tac prems 1);
-by (atac 1);
+Goalw [chain] "chain F ==> F(i) << F(Suc(i))";
+by Auto_tac;
qed "chainE";
-val prems = goalw thy [chain] "!i. F i << F(Suc i) ==> chain F";
-by (cut_facts_tac prems 1);
-by (atac 1);
+val prems = Goalw [chain] "(!!i. F i << F(Suc i)) ==> chain F";
+by (blast_tac (claset() addIs prems) 1);
qed "chainI";
(* ------------------------------------------------------------------------ *)
(* technical lemmas about (least) upper bounds of chains *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [is_ub] "range S <| x ==> !i. S(i) << x";
-by (cut_facts_tac prems 1);
-by (strip_tac 1);
-by (rtac mp 1);
-by (etac spec 1);
-by (rtac rangeI 1);
-qed "ub_rangeE";
+Goalw [is_ub] "range S <| x ==> S(i) << x";
+by (Blast_tac 1);
+qed "ub_rangeD";
-val prems = goalw thy [is_ub] "!i. S i << x ==> range S <| x";
-by (cut_facts_tac prems 1);
-by (strip_tac 1);
-by (etac rangeE 1);
-by (hyp_subst_tac 1);
-by (etac spec 1);
+val prems = Goalw [is_ub] "(!!i. S i << x) ==> range S <| x";
+by (blast_tac (claset() addIs prems) 1);
qed "ub_rangeI";
-bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
+bind_thm ("is_ub_lub", is_lubD1 RS ub_rangeD);
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
-bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
-(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *)
(* ------------------------------------------------------------------------ *)
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [max_in_chain_def]
+Goalw [max_in_chain_def]
"[| chain C; max_in_chain i C|] ==> range C <<| C i";
-by (cut_facts_tac prems 1);
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (res_inst_tac [("m","i")] nat_less_cases 1);
by (rtac (antisym_less_inverse RS conjunct2) 1);
by (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1);
@@ -171,37 +122,30 @@
by (rtac (antisym_less_inverse RS conjunct2) 1);
by (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1);
by (etac spec 1);
-by (etac (chain_mono RS mp) 1);
+by (etac chain_mono 1);
by (atac 1);
-by (strip_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (etac (ub_rangeD) 1);
qed "lub_finch1";
-val prems= goalw thy [finite_chain_def]
+Goalw [finite_chain_def]
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
-by (cut_facts_tac prems 1);
by (rtac lub_finch1 1);
-by (etac conjunct1 1);
-by (rtac (select_eq_Ex RS iffD2) 1);
-by (etac conjunct2 1);
+by (best_tac (claset() addIs [selectI]) 2);
+by (Blast_tac 1);
qed "lub_finch2";
Goal "x<<y ==> chain (%i. if i=0 then x else y)";
by (rtac chainI 1);
-by (rtac allI 1);
by (induct_tac "i" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
qed "bin_chain";
-val prems = goalw thy [max_in_chain_def,le_def]
+Goalw [max_in_chain_def,le_def]
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)";
-by (cut_facts_tac prems 1);
by (rtac allI 1);
by (induct_tac "j" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
qed "bin_chainmax";
Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
@@ -209,22 +153,16 @@
THEN rtac lub_finch1 2);
by (etac bin_chain 2);
by (etac bin_chainmax 2);
-by (Simp_tac 1);
+by (Simp_tac 1);
qed "lub_bin_chain";
(* ------------------------------------------------------------------------ *)
(* the maximal element in a chain is its lub *)
(* ------------------------------------------------------------------------ *)
-Goal "[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c";
-by (rtac thelubI 1);
-by (rtac is_lubI 1);
-by (rtac conjI 1);
-by (etac ub_rangeI 1);
-by (strip_tac 1);
-by (etac exE 1);
-by (hyp_subst_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+Goal "[| Y i = c; ALL i. Y i<<c |] ==> lub(range Y) = c";
+by (blast_tac (claset() addDs [ub_rangeD]
+ addIs [thelubI, is_lubI, ub_rangeI]) 1);
qed "lub_chain_maxelem";
(* ------------------------------------------------------------------------ *)
@@ -232,13 +170,7 @@
(* ------------------------------------------------------------------------ *)
Goal "range(%x. c) <<| c";
-by (rtac is_lubI 1);
-by (rtac conjI 1);
-by (rtac ub_rangeI 1);
-by (strip_tac 1);
-by (rtac refl_less 1);
-by (strip_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (blast_tac (claset() addDs [ub_rangeD] addIs [is_lubI, ub_rangeI]) 1);
qed "lub_const";
--- a/src/HOLCF/Porder0.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Porder0.ML Wed Jul 05 16:37:52 2000 +0200
@@ -12,11 +12,7 @@
(* minimal fixes least element *)
(* ------------------------------------------------------------------------ *)
Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
-by (rtac antisym_less 1);
-by (etac spec 1);
-by (res_inst_tac [("a","uu")] selectI2 1);
-by (atac 1);
-by (etac spec 1);
+by (blast_tac (claset() addIs [selectI2,antisym_less]) 1);
bind_thm ("minimal2UU", allI RS result());
(* ------------------------------------------------------------------------ *)
@@ -24,9 +20,7 @@
(* ------------------------------------------------------------------------ *)
Goal "(x::'a::po)=y ==> x << y & y << x";
-by (rtac conjI 1);
-by ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1));
-by ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1));
+by (Blast_tac 1);
qed "antisym_less_inverse";
--- a/src/HOLCF/Sprod0.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Sprod0.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,13 +10,11 @@
(* A non-emptyness result for Sprod *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod0.thy [Sprod_def]
- "(Spair_Rep a b):Sprod";
+Goalw [Sprod_def] "(Spair_Rep a b):Sprod";
by (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]);
qed "SprodI";
-val prems = goal Sprod0.thy
- "inj_on Abs_Sprod Sprod";
+Goal "inj_on Abs_Sprod Sprod";
by (rtac inj_on_inverseI 1);
by (etac Abs_Sprod_inverse 1);
qed "inj_on_Abs_Sprod";
@@ -25,9 +23,8 @@
(* Strictness and definedness of Spair_Rep *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod0.thy [Spair_Rep_def]
+Goalw [Spair_Rep_def]
"(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)";
-by (cut_facts_tac prems 1);
by (rtac ext 1);
by (rtac ext 1);
by (rtac iffI 1);
@@ -35,32 +32,28 @@
by (fast_tac HOL_cs 1);
qed "strict_Spair_Rep";
-val prems = goalw Sprod0.thy [Spair_Rep_def]
+Goalw [Spair_Rep_def]
"(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)";
by (case_tac "a=UU|b=UU" 1);
by (atac 1);
-by (rtac disjI1 1);
-by (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (fast_tac (claset() addDs [fun_cong]) 1);
qed "defined_Spair_Rep_rev";
(* ------------------------------------------------------------------------ *)
(* injectivity of Spair_Rep and Ispair *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod0.thy [Spair_Rep_def]
+Goalw [Spair_Rep_def]
"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba";
-by (cut_facts_tac prems 1);
-by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS iffD1 RS mp) 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (dtac fun_cong 1);
+by (dtac fun_cong 1);
+by (etac (iffD1 RS mp) 1);
+by Auto_tac;
qed "inject_Spair_Rep";
-val prems = goalw Sprod0.thy [Ispair_def]
+Goalw [Ispair_def]
"[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba";
-by (cut_facts_tac prems 1);
by (etac inject_Spair_Rep 1);
by (atac 1);
by (etac (inj_on_Abs_Sprod RS inj_onD) 1);
@@ -73,37 +66,33 @@
(* strictness and definedness of Ispair *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod0.thy [Ispair_def]
+Goalw [Ispair_def]
"(a=UU | b=UU) ==> Ispair a b = Ispair UU UU";
-by (cut_facts_tac prems 1);
by (etac (strict_Spair_Rep RS arg_cong) 1);
qed "strict_Ispair";
-val prems = goalw Sprod0.thy [Ispair_def]
+Goalw [Ispair_def]
"Ispair UU b = Ispair UU UU";
by (rtac (strict_Spair_Rep RS arg_cong) 1);
by (rtac disjI1 1);
by (rtac refl 1);
qed "strict_Ispair1";
-val prems = goalw Sprod0.thy [Ispair_def]
+Goalw [Ispair_def]
"Ispair a UU = Ispair UU UU";
by (rtac (strict_Spair_Rep RS arg_cong) 1);
by (rtac disjI2 1);
by (rtac refl 1);
qed "strict_Ispair2";
-val prems = goal Sprod0.thy
- "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
-by (cut_facts_tac prems 1);
+Goal "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
by (rtac (de_Morgan_disj RS subst) 1);
by (etac contrapos 1);
by (etac strict_Ispair 1);
qed "strict_Ispair_rev";
-val prems = goalw Sprod0.thy [Ispair_def]
+Goalw [Ispair_def]
"Ispair a b = Ispair UU UU ==> (a = UU | b = UU)";
-by (cut_facts_tac prems 1);
by (rtac defined_Spair_Rep_rev 1);
by (rtac (inj_on_Abs_Sprod RS inj_onD) 1);
by (atac 1);
@@ -111,9 +100,7 @@
by (rtac SprodI 1);
qed "defined_Ispair_rev";
-val prems = goal Sprod0.thy
-"[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
-by (cut_facts_tac prems 1);
+Goal "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
by (rtac contrapos 1);
by (etac defined_Ispair_rev 2);
by (rtac (de_Morgan_disj RS iffD2) 1);
@@ -126,7 +113,7 @@
(* Exhaustion of the strict product ** *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod0.thy [Ispair_def]
+Goalw [Ispair_def]
"z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)";
by (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1);
by (etac exE 1);
@@ -151,15 +138,16 @@
(* general elimination rule for strict product *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Sprod0.thy
-"[|p=Ispair UU UU ==> Q ;!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] ==> Q";
+val [prem1,prem2] = Goal
+" [| p=Ispair UU UU ==> Q ; !!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] \
+\ ==> Q";
by (rtac (Exh_Sprod RS disjE) 1);
-by (etac (hd prems) 1);
+by (etac prem1 1);
by (etac exE 1);
by (etac exE 1);
by (etac conjE 1);
by (etac conjE 1);
-by (etac (hd (tl prems)) 1);
+by (etac prem2 1);
by (atac 1);
by (atac 1);
qed "IsprodE";
@@ -169,9 +157,7 @@
(* some results about the selectors Isfst, Issnd *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod0.thy [Isfst_def]
- "p=Ispair UU UU ==> Isfst p = UU";
-by (cut_facts_tac prems 1);
+Goalw [Isfst_def] "p=Ispair UU UU ==> Isfst p = UU";
by (rtac select_equality 1);
by (rtac conjI 1);
by (fast_tac HOL_cs 1);
@@ -183,24 +169,24 @@
qed "strict_Isfst";
-val prems = goal Sprod0.thy
- "Isfst(Ispair UU y) = UU";
+Goal "Isfst(Ispair UU y) = UU";
by (stac strict_Ispair1 1);
by (rtac strict_Isfst 1);
by (rtac refl 1);
qed "strict_Isfst1";
-val prems = goal Sprod0.thy
- "Isfst(Ispair x UU) = UU";
+Addsimps [strict_Isfst1];
+
+Goal "Isfst(Ispair x UU) = UU";
by (stac strict_Ispair2 1);
by (rtac strict_Isfst 1);
by (rtac refl 1);
qed "strict_Isfst2";
+Addsimps [strict_Isfst2];
-val prems = goalw Sprod0.thy [Issnd_def]
- "p=Ispair UU UU ==>Issnd p=UU";
-by (cut_facts_tac prems 1);
+
+Goalw [Issnd_def] "p=Ispair UU UU ==>Issnd p=UU";
by (rtac select_equality 1);
by (rtac conjI 1);
by (fast_tac HOL_cs 1);
@@ -211,23 +197,23 @@
by (REPEAT (fast_tac HOL_cs 1));
qed "strict_Issnd";
-val prems = goal Sprod0.thy
- "Issnd(Ispair UU y) = UU";
+Goal "Issnd(Ispair UU y) = UU";
by (stac strict_Ispair1 1);
by (rtac strict_Issnd 1);
by (rtac refl 1);
qed "strict_Issnd1";
-val prems = goal Sprod0.thy
- "Issnd(Ispair x UU) = UU";
+Addsimps [strict_Issnd1];
+
+Goal "Issnd(Ispair x UU) = UU";
by (stac strict_Ispair2 1);
by (rtac strict_Issnd 1);
by (rtac refl 1);
qed "strict_Issnd2";
-val prems = goalw Sprod0.thy [Isfst_def]
- "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
-by (cut_facts_tac prems 1);
+Addsimps [strict_Issnd2];
+
+Goalw [Isfst_def] "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
by (rtac select_equality 1);
by (rtac conjI 1);
by (strip_tac 1);
@@ -243,9 +229,7 @@
by (fast_tac HOL_cs 1);
qed "Isfst";
-val prems = goalw Sprod0.thy [Issnd_def]
- "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
-by (cut_facts_tac prems 1);
+Goalw [Issnd_def] "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
by (rtac select_equality 1);
by (rtac conjI 1);
by (strip_tac 1);
@@ -261,8 +245,7 @@
by (fast_tac HOL_cs 1);
qed "Issnd";
-val prems = goal Sprod0.thy "y~=UU ==>Isfst(Ispair x y)=x";
-by (cut_facts_tac prems 1);
+Goal "y~=UU ==>Isfst(Ispair x y)=x";
by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
by (etac Isfst 1);
by (atac 1);
@@ -270,8 +253,7 @@
by (rtac strict_Isfst1 1);
qed "Isfst2";
-val prems = goal Sprod0.thy "~x=UU ==>Issnd(Ispair x y)=y";
-by (cut_facts_tac prems 1);
+Goal "~x=UU ==>Issnd(Ispair x y)=y";
by (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1);
by (etac Issnd 1);
by (atac 1);
@@ -289,9 +271,9 @@
addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
Isfst2,Issnd2];
-val prems = goal Sprod0.thy
- "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU";
-by (cut_facts_tac prems 1);
+Addsimps [Isfst2,Issnd2];
+
+Goal "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU";
by (res_inst_tac [("p","p")] IsprodE 1);
by (contr_tac 1);
by (hyp_subst_tac 1);
@@ -305,8 +287,7 @@
(* Surjective pairing: equivalent to Exh_Sprod *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Sprod0.thy
- "z = Ispair(Isfst z)(Issnd z)";
+Goal "z = Ispair(Isfst z)(Issnd z)";
by (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1);
by (asm_simp_tac Sprod0_ss 1);
by (etac exE 1);
@@ -314,9 +295,7 @@
by (asm_simp_tac Sprod0_ss 1);
qed "surjective_pairing_Sprod";
-val prems = goal thy
- "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
-by (cut_facts_tac prems 1);
+Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1);
by (rotate_tac ~1 1);
by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
--- a/src/HOLCF/Sprod1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Sprod1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -9,22 +9,18 @@
(* less_sprod is a partial order on Sprod *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [less_sprod_def]"(p::'a ** 'b) << p";
+Goalw [less_sprod_def]"(p::'a ** 'b) << p";
by (fast_tac (HOL_cs addIs [refl_less]) 1);
qed "refl_less_sprod";
-val prems = goalw thy [less_sprod_def]
+Goalw [less_sprod_def]
"[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2";
-by (cut_facts_tac prems 1);
by (rtac Sel_injective_Sprod 1);
by (fast_tac (HOL_cs addIs [antisym_less]) 1);
by (fast_tac (HOL_cs addIs [antisym_less]) 1);
qed "antisym_less_sprod";
-val prems = goalw thy [less_sprod_def]
+Goalw [less_sprod_def]
"[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3";
-by (cut_facts_tac prems 1);
-by (rtac conjI 1);
-by (fast_tac (HOL_cs addIs [trans_less]) 1);
-by (fast_tac (HOL_cs addIs [trans_less]) 1);
+by (blast_tac (HOL_cs addIs [trans_less]) 1);
qed "trans_less_sprod";
--- a/src/HOLCF/Sprod2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Sprod2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)";
+Goal "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)";
by (fold_goals_tac [less_sprod_def]);
by (rtac refl 1);
qed "inst_sprod_po";
@@ -16,13 +16,13 @@
(* type sprod is pointed *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy "Ispair UU UU << p";
+Goal "Ispair UU UU << p";
by (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1);
qed "minimal_sprod";
bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
-val prems = goal thy "? x::'a**'b.!y. x<<y";
+Goal "? x::'a**'b.!y. x<<y";
by (res_inst_tac [("x","Ispair UU UU")] exI 1);
by (rtac (minimal_sprod RS allI) 1);
qed "least_sprod";
@@ -31,7 +31,7 @@
(* Ispair is monotone in both arguments *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod2.thy [monofun] "monofun(Ispair)";
+Goalw [monofun] "monofun(Ispair)";
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
@@ -42,7 +42,7 @@
by (REPEAT(asm_simp_tac(Sprod0_ss addsimps[inst_sprod_po,refl_less,minimal]) 1));
qed "monofun_Ispair1";
-val prems = goalw Sprod2.thy [monofun] "monofun(Ispair(x))";
+Goalw [monofun] "monofun(Ispair(x))";
by (strip_tac 1);
by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1);
by (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1);
@@ -64,11 +64,11 @@
(* Isfst and Issnd are monotone *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Sprod2.thy [monofun] "monofun(Isfst)";
+Goalw [monofun] "monofun(Isfst)";
by (simp_tac (HOL_ss addsimps [inst_sprod_po]) 1);
qed "monofun_Isfst";
-val prems = goalw Sprod2.thy [monofun] "monofun(Issnd)";
+Goalw [monofun] "monofun(Issnd)";
by (simp_tac (HOL_ss addsimps [inst_sprod_po]) 1);
qed "monofun_Issnd";
@@ -76,12 +76,11 @@
(* the type 'a ** 'b is a cpo *)
(* ------------------------------------------------------------------------ *)
-val prems = goal Sprod2.thy
+Goal
"[|chain(S)|] ==> range(S) <<| \
\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))";
-by (cut_facts_tac prems 1);
-by (rtac (conjI RS is_lubI) 1);
-by (rtac (allI RS ub_rangeI) 1);
+by (rtac (is_lubI) 1);
+by (rtac (ub_rangeI) 1);
by (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1);
by (rtac monofun_Ispair 1);
by (rtac is_ub_thelub 1);
@@ -102,9 +101,7 @@
bind_thm ("thelub_sprod", lub_sprod RS thelubI);
-val prems = goal Sprod2.thy
- "chain(S::nat=>'a**'b)==>? x. range(S)<<| x";
-by (cut_facts_tac prems 1);
+Goal "chain(S::nat=>'a**'b)==>? x. range(S)<<| x";
by (rtac exI 1);
by (etac lub_sprod 1);
qed "cpo_sprod";
--- a/src/HOLCF/Sprod3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Sprod3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
*)
(* for compatibility with old HOLCF-Version *)
-val prems = goal thy "UU = Ispair UU UU";
+Goal "UU = Ispair UU UU";
by (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1);
qed "inst_sprod_pcpo";
@@ -17,12 +17,11 @@
(* continuity of Ispair, Isfst, Issnd *)
(* ------------------------------------------------------------------------ *)
-val prems = goal thy
+Goal
"[| chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
\ (lub(range(%i. Issnd(Ispair(Y i) x))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1);
by (rtac lub_equal 1);
by (atac 1);
@@ -31,33 +30,23 @@
by (rtac (monofun_Ispair1 RS ch2ch_monofun) 1);
by (atac 1);
by (rtac allI 1);
-by (asm_simp_tac Sprod0_ss 1);
+by (Asm_simp_tac 1);
by (rtac sym 1);
+by (dtac chain_UU_I_inverse2 1);
+by (etac exE 1);
by (rtac lub_chain_maxelem 1);
-by (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1);
-by (rtac (not_all RS iffD1) 1);
-by (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1);
-by (atac 1);
-by (rtac chain_UU_I_inverse 1);
-by (atac 1);
-by (rtac exI 1);
by (etac Issnd2 1);
by (rtac allI 1);
-by (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1);
-by (asm_simp_tac Sprod0_ss 1);
-by (rtac refl_less 1);
-by (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1);
-by (etac sym 1);
-by (asm_simp_tac Sprod0_ss 1);
-by (rtac minimal 1);
+by (rename_tac "j" 1);
+by (case_tac "Y(j)=UU" 1);
+by Auto_tac;
qed "sprod3_lemma1";
-val prems = goal thy
+Goal
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
\ (lub(range(%i. Issnd(Ispair(Y i) x))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
by (atac 1);
by (rtac trans 1);
@@ -65,21 +54,18 @@
by (rtac (strict_Ispair RS sym) 1);
by (rtac disjI1 1);
by (rtac chain_UU_I_inverse 1);
-by (rtac allI 1);
-by (asm_simp_tac Sprod0_ss 1);
+by Auto_tac;
by (etac (chain_UU_I RS spec) 1);
by (atac 1);
qed "sprod3_lemma2";
-val prems = goal thy
+Goal
"[| chain(Y); x = UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
\ (lub(range(%i. Issnd(Ispair (Y i) x))))";
-by (cut_facts_tac prems 1);
-by (res_inst_tac [("s","UU"),("t","x")] ssubst 1);
-by (atac 1);
+by (etac ssubst 1);
by (rtac trans 1);
by (rtac strict_Ispair2 1);
by (rtac (strict_Ispair RS sym) 1);
@@ -112,46 +98,28 @@
by (atac 1);
qed "contlub_Ispair1";
-val prems = goal thy
+Goal
"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
\ (lub(range(%i. Issnd (Ispair x (Y i)))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1);
by (rtac sym 1);
+by (dtac chain_UU_I_inverse2 1);
+by (etac exE 1);
by (rtac lub_chain_maxelem 1);
-by (res_inst_tac [("P","%j. Y(j)~=UU")] exE 1);
-by (rtac (not_all RS iffD1) 1);
-by (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1);
-by (atac 1);
-by (rtac chain_UU_I_inverse 1);
-by (atac 1);
-by (rtac exI 1);
by (etac Isfst2 1);
by (rtac allI 1);
-by (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1);
-by (asm_simp_tac Sprod0_ss 1);
-by (rtac refl_less 1);
-by (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1);
-by (etac sym 1);
-by (asm_simp_tac Sprod0_ss 1);
-by (rtac minimal 1);
-by (rtac lub_equal 1);
-by (atac 1);
-by (rtac (monofun_Issnd RS ch2ch_monofun) 1);
-by (rtac (monofun_Ispair2 RS ch2ch_monofun) 1);
-by (atac 1);
-by (rtac allI 1);
-by (asm_simp_tac Sprod0_ss 1);
+by (rename_tac "j" 1);
+by (case_tac "Y(j)=UU" 1);
+by Auto_tac;
qed "sprod3_lemma4";
-val prems = goal thy
+Goal
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
\ (lub(range(%i. Issnd(Ispair x (Y i)))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
by (atac 1);
by (rtac trans 1);
@@ -165,12 +133,11 @@
by (atac 1);
qed "sprod3_lemma5";
-val prems = goal thy
+Goal
"[| chain(Y); x = UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
\ (lub(range(%i. Issnd (Ispair x (Y i)))))";
-by (cut_facts_tac prems 1);
by (res_inst_tac [("s","UU"),("t","x")] ssubst 1);
by (atac 1);
by (rtac trans 1);
@@ -182,7 +149,7 @@
by (simp_tac Sprod0_ss 1);
qed "sprod3_lemma6";
-val prems = goal thy "contlub(Ispair(x))";
+Goal "contlub(Ispair(x))";
by (rtac contlubI 1);
by (strip_tac 1);
by (rtac trans 1);
@@ -200,20 +167,20 @@
by (atac 1);
qed "contlub_Ispair2";
-val prems = goal thy "cont(Ispair)";
+Goal "cont(Ispair)";
by (rtac monocontlub2cont 1);
by (rtac monofun_Ispair1 1);
by (rtac contlub_Ispair1 1);
qed "cont_Ispair1";
-val prems = goal thy "cont(Ispair(x))";
+Goal "cont(Ispair(x))";
by (rtac monocontlub2cont 1);
by (rtac monofun_Ispair2 1);
by (rtac contlub_Ispair2 1);
qed "cont_Ispair2";
-val prems = goal thy "contlub(Isfst)";
+Goal "contlub(Isfst)";
by (rtac contlubI 1);
by (strip_tac 1);
by (stac (lub_sprod RS thelubI) 1);
@@ -233,7 +200,7 @@
by (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
qed "contlub_Isfst";
-val prems = goal thy "contlub(Issnd)";
+Goal "contlub(Issnd)";
by (rtac contlubI 1);
by (strip_tac 1);
by (stac (lub_sprod RS thelubI) 1);
@@ -252,20 +219,19 @@
by (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
qed "contlub_Issnd";
-val prems = goal thy "cont(Isfst)";
+Goal "cont(Isfst)";
by (rtac monocontlub2cont 1);
by (rtac monofun_Isfst 1);
by (rtac contlub_Isfst 1);
qed "cont_Isfst";
-val prems = goal thy "cont(Issnd)";
+Goal "cont(Issnd)";
by (rtac monocontlub2cont 1);
by (rtac monofun_Issnd 1);
by (rtac contlub_Issnd 1);
qed "cont_Issnd";
-val prems = goal thy "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)";
-by (cut_facts_tac prems 1);
+Goal "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)";
by (fast_tac HOL_cs 1);
qed "spair_eq";
@@ -273,7 +239,7 @@
(* convert all lemmas to the continuous versions *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [spair_def]
+Goalw [spair_def]
"(LAM x y. Ispair x y)`a`b = Ispair a b";
by (stac beta_cfun 1);
by (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1, cont2cont_CF1L]) 1);
@@ -284,9 +250,8 @@
Addsimps [beta_cfun_sprod];
-val prems = goalw thy [spair_def]
+Goalw [spair_def]
"[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba";
-by (cut_facts_tac prems 1);
by (etac inject_Ispair 1);
by (atac 1);
by (etac box_equals 1);
@@ -294,7 +259,7 @@
by (rtac beta_cfun_sprod 1);
qed "inject_spair";
-val prems = goalw thy [spair_def] "UU = (:UU,UU:)";
+Goalw [spair_def] "UU = (:UU,UU:)";
by (rtac sym 1);
by (rtac trans 1);
by (rtac beta_cfun_sprod 1);
@@ -302,9 +267,8 @@
by (rtac inst_sprod_pcpo 1);
qed "inst_sprod_pcpo2";
-val prems = goalw thy [spair_def]
+Goalw [spair_def]
"(a=UU | b=UU) ==> (:a,b:)=UU";
-by (cut_facts_tac prems 1);
by (rtac trans 1);
by (rtac beta_cfun_sprod 1);
by (rtac trans 1);
@@ -312,14 +276,14 @@
by (etac strict_Ispair 1);
qed "strict_spair";
-val prems = goalw thy [spair_def] "(:UU,b:) = UU";
+Goalw [spair_def] "(:UU,b:) = UU";
by (stac beta_cfun_sprod 1);
by (rtac trans 1);
by (rtac (inst_sprod_pcpo RS sym) 2);
by (rtac strict_Ispair1 1);
qed "strict_spair1";
-val prems = goalw thy [spair_def] "(:a,UU:) = UU";
+Goalw [spair_def] "(:a,UU:) = UU";
by (stac beta_cfun_sprod 1);
by (rtac trans 1);
by (rtac (inst_sprod_pcpo RS sym) 2);
@@ -338,16 +302,15 @@
by Auto_tac;
qed "defined_spair_rev";
-val prems = goalw thy [spair_def]
+Goalw [spair_def]
"[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU";
-by (cut_facts_tac prems 1);
by (stac beta_cfun_sprod 1);
by (stac inst_sprod_pcpo 1);
by (etac defined_Ispair 1);
by (atac 1);
qed "defined_spair";
-val prems = goalw thy [spair_def]
+Goalw [spair_def]
"z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)";
by (rtac (Exh_Sprod RS disjE) 1);
by (rtac disjI1 1);
@@ -379,9 +342,8 @@
qed "sprodE";
-val prems = goalw thy [sfst_def]
+Goalw [sfst_def]
"p=UU==>sfst`p=UU";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by (rtac cont_Isfst 1);
by (rtac strict_Isfst 1);
@@ -389,7 +351,7 @@
by (atac 1);
qed "strict_sfst";
-val prems = goalw thy [sfst_def,spair_def]
+Goalw [sfst_def,spair_def]
"sfst`(:UU,y:) = UU";
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
@@ -397,7 +359,7 @@
by (rtac strict_Isfst1 1);
qed "strict_sfst1";
-val prems = goalw thy [sfst_def,spair_def]
+Goalw [sfst_def,spair_def]
"sfst`(:x,UU:) = UU";
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
@@ -405,9 +367,8 @@
by (rtac strict_Isfst2 1);
qed "strict_sfst2";
-val prems = goalw thy [ssnd_def]
+Goalw [ssnd_def]
"p=UU==>ssnd`p=UU";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by (rtac cont_Issnd 1);
by (rtac strict_Issnd 1);
@@ -415,7 +376,7 @@
by (atac 1);
qed "strict_ssnd";
-val prems = goalw thy [ssnd_def,spair_def]
+Goalw [ssnd_def,spair_def]
"ssnd`(:UU,y:) = UU";
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
@@ -423,7 +384,7 @@
by (rtac strict_Issnd1 1);
qed "strict_ssnd1";
-val prems = goalw thy [ssnd_def,spair_def]
+Goalw [ssnd_def,spair_def]
"ssnd`(:x,UU:) = UU";
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
@@ -431,18 +392,16 @@
by (rtac strict_Issnd2 1);
qed "strict_ssnd2";
-val prems = goalw thy [sfst_def,spair_def]
+Goalw [sfst_def,spair_def]
"y~=UU ==>sfst`(:x,y:)=x";
-by (cut_facts_tac prems 1);
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
by (rtac cont_Isfst 1);
by (etac Isfst2 1);
qed "sfst2";
-val prems = goalw thy [ssnd_def,spair_def]
+Goalw [ssnd_def,spair_def]
"x~=UU ==>ssnd`(:x,y:)=y";
-by (cut_facts_tac prems 1);
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
by (rtac cont_Issnd 1);
@@ -450,9 +409,8 @@
qed "ssnd2";
-val prems = goalw thy [sfst_def,ssnd_def,spair_def]
+Goalw [sfst_def,ssnd_def,spair_def]
"p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by (rtac cont_Issnd 1);
by (stac beta_cfun 1);
@@ -462,7 +420,7 @@
by (atac 1);
qed "defined_sfstssnd";
-val prems = goalw thy [sfst_def,ssnd_def,spair_def] "(:sfst`p , ssnd`p:) = p";
+Goalw [sfst_def,ssnd_def,spair_def] "(:sfst`p , ssnd`p:) = p";
by (stac beta_cfun_sprod 1);
by (stac beta_cfun 1);
by (rtac cont_Issnd 1);
@@ -471,17 +429,15 @@
by (rtac (surjective_pairing_Sprod RS sym) 1);
qed "surjective_pairing_Sprod2";
-val prems = goalw thy [sfst_def,ssnd_def,spair_def]
-"[|chain(S)|] ==> range(S) <<| \
-\ (: lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) :)";
-by (cut_facts_tac prems 1);
+Goalw [sfst_def,ssnd_def,spair_def]
+"chain(S) ==> range(S) <<| \
+\ (: lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) :)";
by (stac beta_cfun_sprod 1);
by (stac (beta_cfun RS ext) 1);
by (rtac cont_Issnd 1);
by (stac (beta_cfun RS ext) 1);
by (rtac cont_Isfst 1);
-by (rtac lub_sprod 1);
-by (resolve_tac prems 1);
+by (etac lub_sprod 1);
qed "lub_sprod2";
@@ -492,7 +448,7 @@
(:lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i))):)" : thm
*)
-val prems = goalw thy [ssplit_def]
+Goalw [ssplit_def]
"ssplit`f`UU=UU";
by (stac beta_cfun 1);
by (Simp_tac 1);
@@ -500,25 +456,25 @@
by (rtac refl 1);
qed "ssplit1";
-val prems = goalw thy [ssplit_def]
+Goalw [ssplit_def]
"[|x~=UU;y~=UU|] ==> ssplit`f`(:x,y:)= f`x`y";
by (stac beta_cfun 1);
by (Simp_tac 1);
by (stac strictify2 1);
by (rtac defined_spair 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (stac beta_cfun 1);
by (Simp_tac 1);
by (stac sfst2 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
by (stac ssnd2 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
by (rtac refl 1);
qed "ssplit2";
-val prems = goalw thy [ssplit_def]
+Goalw [ssplit_def]
"ssplit`spair`z=z";
by (stac beta_cfun 1);
by (Simp_tac 1);
--- a/src/HOLCF/Ssum0.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Ssum0.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,14 +10,14 @@
(* A non-emptyness result for Sssum *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum";
+Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
by (rtac CollectI 1);
by (rtac disjI1 1);
by (rtac exI 1);
by (rtac refl 1);
qed "SsumIl";
-val prems = goalw Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum";
+Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
by (rtac CollectI 1);
by (rtac disjI2 1);
by (rtac exI 1);
@@ -33,7 +33,7 @@
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
+Goalw [Sinr_Rep_def,Sinl_Rep_def]
"Sinl_Rep(UU) = Sinr_Rep(UU)";
by (rtac ext 1);
by (rtac ext 1);
@@ -41,7 +41,7 @@
by (fast_tac HOL_cs 1);
qed "strict_SinlSinr_Rep";
-val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+Goalw [Isinl_def,Isinr_def]
"Isinl(UU) = Isinr(UU)";
by (rtac (strict_SinlSinr_Rep RS arg_cong) 1);
qed "strict_IsinlIsinr";
@@ -51,25 +51,14 @@
(* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
+Goalw [Sinl_Rep_def,Sinr_Rep_def]
"(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
-by (rtac conjI 1);
-by (case_tac "a=UU" 1);
-by (atac 1);
-by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
-by (fast_tac HOL_cs 1);
-by (atac 1);
-by (case_tac "b=UU" 1);
-by (atac 1);
-by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1 RS sym) 1);
-by (fast_tac HOL_cs 1);
-by (atac 1);
+by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "noteq_SinlSinr_Rep";
-val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+Goalw [Isinl_def,Isinr_def]
"Isinl(a)=Isinr(b) ==> a=UU & b=UU";
-by (cut_facts_tac prems 1);
by (rtac noteq_SinlSinr_Rep 1);
by (etac (inj_on_Abs_Ssum RS inj_onD) 1);
by (rtac SsumIl 1);
@@ -82,36 +71,22 @@
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum0.thy [Sinl_Rep_def]
- "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
-by (case_tac "a=UU" 1);
-by (atac 1);
-by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
-by (fast_tac HOL_cs 1);
-by (atac 1);
+Goalw [Sinl_Rep_def] "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
+by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinl_Rep1";
-val prems = goalw Ssum0.thy [Sinr_Rep_def]
- "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
-by (case_tac "b=UU" 1);
-by (atac 1);
-by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1);
-by (fast_tac HOL_cs 1);
-by (atac 1);
+Goalw [Sinr_Rep_def] "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
+by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinr_Rep1";
-val prems = goalw Ssum0.thy [Sinl_Rep_def]
+Goalw [Sinl_Rep_def]
"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
-by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1) 1);
-by (fast_tac HOL_cs 1);
-by (resolve_tac prems 1);
+by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinl_Rep2";
-val prems = goalw Ssum0.thy [Sinr_Rep_def]
+Goalw [Sinr_Rep_def]
"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
-by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1) 1);
-by (fast_tac HOL_cs 1);
-by (resolve_tac prems 1);
+by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinr_Rep2";
Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
@@ -140,18 +115,14 @@
by (atac 1);
qed "inject_Sinr_Rep";
-val prems = goalw Ssum0.thy [Isinl_def]
-"Isinl(a1)=Isinl(a2)==> a1=a2";
-by (cut_facts_tac prems 1);
+Goalw [Isinl_def] "Isinl(a1)=Isinl(a2)==> a1=a2";
by (rtac inject_Sinl_Rep 1);
by (etac (inj_on_Abs_Ssum RS inj_onD) 1);
by (rtac SsumIl 1);
by (rtac SsumIl 1);
qed "inject_Isinl";
-val prems = goalw Ssum0.thy [Isinr_def]
-"Isinr(b1)=Isinr(b2) ==> b1=b2";
-by (cut_facts_tac prems 1);
+Goalw [Isinr_def] "Isinr(b1)=Isinr(b2) ==> b1=b2";
by (rtac inject_Sinr_Rep 1);
by (etac (inj_on_Abs_Ssum RS inj_onD) 1);
by (rtac SsumIr 1);
@@ -175,7 +146,7 @@
(* choice of the bottom representation is arbitrary *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum0.thy [Isinl_def,Isinr_def]
+Goalw [Isinl_def,Isinr_def]
"z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)";
by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1);
by (etac disjE 1);
@@ -250,7 +221,7 @@
(* rewrites for Iwhen *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum0.thy [Iwhen_def]
+Goalw [Iwhen_def]
"Iwhen f g (Isinl UU) = UU";
by (rtac select_equality 1);
by (rtac conjI 1);
@@ -273,9 +244,8 @@
qed "Iwhen1";
-val prems = goalw Ssum0.thy [Iwhen_def]
+Goalw [Iwhen_def]
"x~=UU ==> Iwhen f g (Isinl x) = f`x";
-by (cut_facts_tac prems 1);
by (rtac select_equality 1);
by (fast_tac HOL_cs 2);
by (rtac conjI 1);
@@ -297,9 +267,8 @@
by (fast_tac HOL_cs 1);
qed "Iwhen2";
-val prems = goalw Ssum0.thy [Iwhen_def]
+Goalw [Iwhen_def]
"y~=UU ==> Iwhen f g (Isinr y) = g`y";
-by (cut_facts_tac prems 1);
by (rtac select_equality 1);
by (fast_tac HOL_cs 2);
by (rtac conjI 1);
@@ -329,3 +298,4 @@
val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps
[(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
+Addsimps [strict_IsinlIsinr RS sym, Iwhen1, Iwhen2, Iwhen3];
--- a/src/HOLCF/Ssum1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Ssum1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -32,11 +32,10 @@
(res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1)
THEN (rtac trans 1)
THEN (atac 2)
- THEN (etac sym 1))
+ THEN (etac sym 1));
-val prems = goalw thy [less_ssum_def]
+Goalw [less_ssum_def]
"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)";
-by (cut_facts_tac prems 1);
by (rtac select_equality 1);
by (dtac conjunct1 2);
by (dtac spec 2);
@@ -73,9 +72,8 @@
qed "less_ssum1a";
-val prems = goalw thy [less_ssum_def]
+Goalw [less_ssum_def]
"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)";
-by (cut_facts_tac prems 1);
by (rtac select_equality 1);
by (dtac conjunct2 2);
by (dtac conjunct1 2);
@@ -113,9 +111,8 @@
qed "less_ssum1b";
-val prems = goalw thy [less_ssum_def]
+Goalw [less_ssum_def]
"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)";
-by (cut_facts_tac prems 1);
by (rtac select_equality 1);
by (rtac conjI 1);
by (strip_tac 1);
@@ -153,9 +150,8 @@
qed "less_ssum1c";
-val prems = goalw thy [less_ssum_def]
+Goalw [less_ssum_def]
"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)";
-by (cut_facts_tac prems 1);
by (rtac select_equality 1);
by (dtac conjunct2 2);
by (dtac conjunct2 2);
--- a/src/HOLCF/Ssum2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Ssum2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -62,12 +62,12 @@
(* Isinl, Isinr are monotone *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun] "monofun(Isinl)";
+Goalw [monofun] "monofun(Isinl)";
by (strip_tac 1);
by (etac (less_ssum3a RS iffD2) 1);
qed "monofun_Isinl";
-val prems = goalw thy [monofun] "monofun(Isinr)";
+Goalw [monofun] "monofun(Isinr)";
by (strip_tac 1);
by (etac (less_ssum3b RS iffD2) 1);
qed "monofun_Isinr";
@@ -78,7 +78,7 @@
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun] "monofun(Iwhen)";
+Goalw [monofun] "monofun(Iwhen)";
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
@@ -92,7 +92,7 @@
by (asm_simp_tac Ssum0_ss 1);
qed "monofun_Iwhen1";
-val prems = goalw thy [monofun] "monofun(Iwhen(f))";
+Goalw [monofun] "monofun(Iwhen(f))";
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
@@ -104,7 +104,7 @@
by (etac monofun_cfun_fun 1);
qed "monofun_Iwhen2";
-val prems = goalw thy [monofun] "monofun(Iwhen(f)(g))";
+Goalw [monofun] "monofun(Iwhen(f)(g))";
by (strip_tac 1);
by (res_inst_tac [("p","x")] IssumE 1);
by (hyp_subst_tac 1);
@@ -182,13 +182,13 @@
by (rtac (less_ssum3d RS iffD1) 1);
by (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1);
by (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1);
-by (etac (chain_mono RS mp) 1);
+by (etac (chain_mono) 1);
by (atac 1);
by (eres_inst_tac [("P","xa=UU")] notE 1);
by (rtac (less_ssum3c RS iffD1) 1);
by (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1);
by (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1);
-by (etac (chain_mono RS mp) 1);
+by (etac (chain_mono) 1);
by (atac 1);
qed "ssum_lemma3";
@@ -261,9 +261,7 @@
Goal "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
\ range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))";
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (etac allE 1);
by (etac exE 1);
by (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1);
@@ -290,16 +288,14 @@
by (rtac (less_ssum3c RS iffD1) 1);
by (res_inst_tac [("t","Isinl(x)")] subst 1);
by (atac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (etac (ub_rangeD) 1);
qed "lub_ssum1a";
Goal "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
\ range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))";
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (etac allE 1);
by (etac exE 1);
by (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1);
@@ -320,7 +316,7 @@
by (rtac (less_ssum3d RS iffD1) 1);
by (res_inst_tac [("t","Isinr(y)")] subst 1);
by (atac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (etac (ub_rangeD) 1);
by (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1);
by (atac 1);
by (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1);
--- a/src/HOLCF/Ssum3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Ssum3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -334,37 +334,34 @@
(* continuous versions of lemmas for 'a ++ 'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw Ssum3.thy [sinl_def] "sinl`UU =UU";
+Goalw [sinl_def] "sinl`UU =UU";
by (simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1);
by (rtac (inst_ssum_pcpo RS sym) 1);
qed "strict_sinl";
-val prems = goalw Ssum3.thy [sinr_def] "sinr`UU=UU";
+Goalw [sinr_def] "sinr`UU=UU";
by (simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1);
by (rtac (inst_ssum_pcpo RS sym) 1);
qed "strict_sinr";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"sinl`a=sinr`b ==> a=UU & b=UU";
-by (cut_facts_tac prems 1);
by (rtac noteq_IsinlIsinr 1);
by (etac box_equals 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
qed "noteq_sinlsinr";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"sinl`a1=sinl`a2==> a1=a2";
-by (cut_facts_tac prems 1);
by (rtac inject_Isinl 1);
by (etac box_equals 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
qed "inject_sinl";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"sinr`a1=sinr`a2==> a1=a2";
-by (cut_facts_tac prems 1);
by (rtac inject_Isinr 1);
by (etac box_equals 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
@@ -386,7 +383,7 @@
by (etac notnotD 1);
qed "defined_sinr";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)";
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
by (stac inst_ssum_pcpo 1);
@@ -422,7 +419,7 @@
val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont2cont_CF1L]) 1));
-val _ = goalw Ssum3.thy [sscase_def,sinl_def,sinr_def]
+Goalw [sscase_def,sinl_def,sinr_def]
"sscase`f`g`UU = UU";
by (stac inst_ssum_pcpo 1);
by (stac beta_cfun 1);
@@ -438,9 +435,8 @@
val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1));
-val prems = goalw Ssum3.thy [sscase_def,sinl_def,sinr_def]
+Goalw [sscase_def,sinl_def,sinr_def]
"x~=UU==> sscase`f`g`(sinl`x) = f`x";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by tac;
by (stac beta_cfun 1);
@@ -452,9 +448,8 @@
by (asm_simp_tac Ssum0_ss 1);
qed "sscase2";
-val prems = goalw Ssum3.thy [sscase_def,sinl_def,sinr_def]
+Goalw [sscase_def,sinl_def,sinr_def]
"x~=UU==> sscase`f`g`(sinr`x) = g`x";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by tac;
by (stac beta_cfun 1);
@@ -467,7 +462,7 @@
qed "sscase3";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"(sinl`x << sinl`y) = (x << y)";
by (stac beta_cfun 1);
by tac;
@@ -476,7 +471,7 @@
by (rtac less_ssum3a 1);
qed "less_ssum4a";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"(sinr`x << sinr`y) = (x << y)";
by (stac beta_cfun 1);
by tac;
@@ -485,7 +480,7 @@
by (rtac less_ssum3b 1);
qed "less_ssum4b";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"(sinl`x << sinr`y) = (x = UU)";
by (stac beta_cfun 1);
by tac;
@@ -494,7 +489,7 @@
by (rtac less_ssum3c 1);
qed "less_ssum4c";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"(sinr`x << sinl`y) = (x = UU)";
by (stac beta_cfun 1);
by tac;
@@ -503,18 +498,16 @@
by (rtac less_ssum3d 1);
qed "less_ssum4d";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)";
-by (cut_facts_tac prems 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
by (etac ssum_lemma4 1);
qed "ssum_chainE";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def,sscase_def]
+Goalw [sinl_def,sinr_def,sscase_def]
"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\
\ lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by tac;
by (stac beta_cfun 1);
@@ -534,10 +527,9 @@
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1);
qed "thelub_ssum2a";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def,sscase_def]
+Goalw [sinl_def,sinr_def,sscase_def]
"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\
\ lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by tac;
by (stac beta_cfun 1);
@@ -557,17 +549,15 @@
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
qed "thelub_ssum2b";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
+Goalw [sinl_def,sinr_def]
"[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x";
-by (cut_facts_tac prems 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
by (etac ssum_lemma9 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
qed "thelub_ssum2a_rev";
-val prems = goalw Ssum3.thy [sinl_def,sinr_def]
- "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x";
-by (cut_facts_tac prems 1);
+Goalw [sinl_def,sinr_def]
+ "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x";
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
by (etac ssum_lemma10 1);
by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1);
--- a/src/HOLCF/Up1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Up1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,8 +10,7 @@
by (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1);
qed "Abs_Up_inverse2";
-val prems = Goalw [Iup_def ]
- "z = Abs_Up(Inl ()) | (? x. z = Iup x)";
+Goalw [Iup_def] "z = Abs_Up(Inl ()) | (? x. z = Iup x)";
by (rtac (Rep_Up_inverse RS subst) 1);
by (res_inst_tac [("s","Rep_Up z")] sumE 1);
by (rtac disjI1 1);
@@ -34,8 +33,7 @@
by (rtac Rep_Up_inverse 1);
qed "inj_Rep_Up";
-val prems = goalw thy [Iup_def] "Iup x=Iup y ==> x=y";
-by (cut_facts_tac prems 1);
+Goalw [Iup_def] "Iup x=Iup y ==> x=y";
by (rtac (inj_Inr RS injD) 1);
by (rtac (inj_Abs_Up RS injD) 1);
by (atac 1);
@@ -43,7 +41,7 @@
AddSDs [inject_Iup];
-val prems = goalw thy [Iup_def] "Iup x~=Abs_Up(Inl ())";
+Goalw [Iup_def] "Iup x~=Abs_Up(Inl ())";
by (rtac notI 1);
by (rtac notE 1);
by (rtac Inl_not_Inr 1);
@@ -59,14 +57,13 @@
by (eresolve_tac prems 1);
qed "upE";
-val prems = goalw thy [Ifup_def]
- "Ifup(f)(Abs_Up(Inl ()))=UU";
+Goalw [Ifup_def] "Ifup(f)(Abs_Up(Inl ()))=UU";
by (stac Abs_Up_inverse2 1);
by (stac sum_case_Inl 1);
by (rtac refl 1);
qed "Ifup1";
-val prems = goalw thy [Ifup_def,Iup_def]
+Goalw [Ifup_def,Iup_def]
"Ifup(f)(Iup(x))=f`x";
by (stac Abs_Up_inverse2 1);
by (stac sum_case_Inr 1);
@@ -78,14 +75,14 @@
Addsimps [Ifup1,Ifup2];
-val prems = goalw thy [less_up_def]
+Goalw [less_up_def]
"Abs_Up(Inl ())<< z";
by (stac Abs_Up_inverse2 1);
by (stac sum_case_Inl 1);
by (rtac TrueI 1);
qed "less_up1a";
-val prems = goalw thy [Iup_def,less_up_def]
+Goalw [Iup_def,less_up_def]
"~(Iup x) << (Abs_Up(Inl ()))";
by (rtac notI 1);
by (rtac iffD1 1);
@@ -97,7 +94,7 @@
by (rtac refl 1);
qed "less_up1b";
-val prems = goalw thy [Iup_def,less_up_def]
+Goalw [Iup_def,less_up_def]
"(Iup x) << (Iup y)=(x<<y)";
by (stac Abs_Up_inverse2 1);
by (stac Abs_Up_inverse2 1);
--- a/src/HOLCF/Up2.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Up2.ML Wed Jul 05 16:37:52 2000 +0200
@@ -25,7 +25,7 @@
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
-Goal "? x::'a u.!y. x<<y";
+Goal "EX x::'a u. ALL y. x<<y";
by (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1);
by (rtac (minimal_up RS allI) 1);
qed "least_up";
@@ -46,12 +46,12 @@
(* Iup and Ifup are monotone *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [monofun] "monofun(Iup)";
+Goalw [monofun] "monofun(Iup)";
by (strip_tac 1);
by (etac (less_up2c RS iffD2) 1);
qed "monofun_Iup";
-val prems = goalw thy [monofun] "monofun(Ifup)";
+Goalw [monofun] "monofun(Ifup)";
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
@@ -61,7 +61,7 @@
by (etac monofun_cfun_fun 1);
qed "monofun_Ifup1";
-val prems = goalw thy [monofun] "monofun(Ifup(f))";
+Goalw [monofun] "monofun(Ifup(f))";
by (strip_tac 1);
by (res_inst_tac [("p","x")] upE 1);
by (asm_simp_tac Up0_ss 1);
@@ -89,12 +89,10 @@
(* ('a)u is a cpo *)
(* ------------------------------------------------------------------------ *)
-Goal "[|chain(Y);? i x. Y(i)=Iup(x)|] \
+Goal "[|chain(Y);EX i x. Y(i)=Iup(x)|] \
\ ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))";
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (res_inst_tac [("p","Y(i)")] upE 1);
by (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1);
by (etac sym 1);
@@ -113,7 +111,7 @@
by (atac 1);
by (rtac less_up2b 1);
by (hyp_subst_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (etac ub_rangeD 1);
by (res_inst_tac [("t","u")] (up_lemma1 RS subst) 1);
by (atac 1);
by (rtac (less_up2c RS iffD2) 1);
@@ -122,11 +120,9 @@
by (etac (monofun_Ifup2 RS ub2ub_monofun) 1);
qed "lub_up1a";
-Goal "[|chain(Y);!i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())";
+Goal "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())";
by (rtac is_lubI 1);
-by (rtac conjI 1);
by (rtac ub_rangeI 1);
-by (rtac allI 1);
by (res_inst_tac [("p","Y(i)")] upE 1);
by (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1);
by (atac 1);
@@ -142,7 +138,7 @@
bind_thm ("thelub_up1a", lub_up1a RS thelubI);
(*
-[| chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
+[| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==>
lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
*)
@@ -152,7 +148,7 @@
lub (range ?Y1) = UU_up
*)
-Goal "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x";
+Goal "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x";
by (rtac disjE 1);
by (rtac exI 2);
by (etac lub_up1a 2);
--- a/src/HOLCF/Up3.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Up3.ML Wed Jul 05 16:37:52 2000 +0200
@@ -132,26 +132,25 @@
(* continuous versions of lemmas for ('a)u *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [up_def] "z = UU | (? x. z = up`x)";
+Goalw [up_def] "z = UU | (? x. z = up`x)";
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
by (stac inst_up_pcpo 1);
by (rtac Exh_Up 1);
qed "Exh_Up1";
-val prems = goalw thy [up_def] "up`x=up`y ==> x=y";
-by (cut_facts_tac prems 1);
+Goalw [up_def] "up`x=up`y ==> x=y";
by (rtac inject_Iup 1);
by (etac box_equals 1);
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
qed "inject_up";
-val prems = goalw thy [up_def] " up`x ~= UU";
+Goalw [up_def] " up`x ~= UU";
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
by (rtac defined_Iup2 1);
qed "defined_up";
-val prems = goalw thy [up_def]
+val prems = Goalw [up_def]
"[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q";
by (rtac upE 1);
by (resolve_tac prems 1);
@@ -163,7 +162,7 @@
val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
cont_Ifup2,cont2cont_CF1L]) 1);
-val prems = goalw thy [up_def,fup_def] "fup`f`UU=UU";
+Goalw [up_def,fup_def] "fup`f`UU=UU";
by (stac inst_up_pcpo 1);
by (stac beta_cfun 1);
by tac;
@@ -172,7 +171,7 @@
by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1);
qed "fup1";
-val prems = goalw thy [up_def,fup_def] "fup`f`(up`x)=f`x";
+Goalw [up_def,fup_def] "fup`f`(up`x)=f`x";
by (stac beta_cfun 1);
by (rtac cont_Iup 1);
by (stac beta_cfun 1);
@@ -182,21 +181,20 @@
by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1);
qed "fup2";
-val prems = goalw thy [up_def,fup_def] "~ up`x << UU";
+Goalw [up_def,fup_def] "~ up`x << UU";
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
by (rtac less_up3b 1);
qed "less_up4b";
-val prems = goalw thy [up_def,fup_def]
+Goalw [up_def,fup_def]
"(up`x << up`y) = (x<<y)";
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
by (rtac less_up2c 1);
qed "less_up4c";
-val prems = goalw thy [up_def,fup_def]
+Goalw [up_def,fup_def]
"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
-by (cut_facts_tac prems 1);
by (stac beta_cfun 1);
by tac;
by (stac beta_cfun 1);
@@ -216,9 +214,8 @@
-val prems = goalw thy [up_def,fup_def]
+Goalw [up_def,fup_def]
"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU";
-by (cut_facts_tac prems 1);
by (stac inst_up_pcpo 1);
by (rtac thelub_up1b 1);
by (atac 1);
--- a/src/HOLCF/ex/Loop.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/ex/Loop.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,275 +10,179 @@
(* access to definitions *)
(* ------------------------------------------------------------------------- *)
-val step_def2 = prove_goalw Loop.thy [step_def]
-"step`b`g`x = If b`x then g`x else x fi"
- (fn prems =>
- [
- (Simp_tac 1)
- ]);
-val while_def2 = prove_goalw Loop.thy [while_def]
-"while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)"
- (fn prems =>
- [
- (Simp_tac 1)
- ]);
+Goalw [step_def] "step`b`g`x = If b`x then g`x else x fi";
+by (Simp_tac 1);
+qed "step_def2";
+
+Goalw [while_def] "while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)";
+by (Simp_tac 1);
+qed "while_def2";
(* ------------------------------------------------------------------------- *)
(* rekursive properties of while *)
(* ------------------------------------------------------------------------- *)
-val while_unfold = prove_goal Loop.thy
-"while`b`g`x = If b`x then while`b`g`(g`x) else x fi"
- (fn prems =>
- [
- (fix_tac5 while_def2 1),
- (Simp_tac 1)
- ]);
+Goal "while`b`g`x = If b`x then while`b`g`(g`x) else x fi";
+by (fix_tac5 while_def2 1);
+by (Simp_tac 1);
+qed "while_unfold";
-val while_unfold2 = prove_goal Loop.thy
- "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
- (fn prems =>
- [
- (nat_ind_tac "k" 1),
- (simp_tac HOLCF_ss 1),
- (rtac allI 1),
- (rtac trans 1),
- (stac while_unfold 1),
- (rtac refl 2),
- (stac iterate_Suc2 1),
- (rtac trans 1),
- (etac spec 2),
- (stac step_def2 1),
- (res_inst_tac [("p","b`x")] trE 1),
- (asm_simp_tac HOLCF_ss 1),
- (stac while_unfold 1),
- (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
- (etac (flat_codom RS disjE) 1),
- (atac 1),
- (etac spec 1),
- (simp_tac HOLCF_ss 1),
- (asm_simp_tac HOLCF_ss 1),
- (asm_simp_tac HOLCF_ss 1),
- (stac while_unfold 1),
- (asm_simp_tac HOLCF_ss 1)
- ]);
+Goal "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)";
+by (nat_ind_tac "k" 1);
+by (simp_tac HOLCF_ss 1);
+by (rtac allI 1);
+by (rtac trans 1);
+by (stac while_unfold 1);
+by (rtac refl 2);
+by (stac iterate_Suc2 1);
+by (rtac trans 1);
+by (etac spec 2);
+by (stac step_def2 1);
+by (res_inst_tac [("p","b`x")] trE 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (stac while_unfold 1);
+by (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1);
+by (etac (flat_codom RS disjE) 1);
+by (atac 1);
+by (etac spec 1);
+by (simp_tac HOLCF_ss 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (stac while_unfold 1);
+by (asm_simp_tac HOLCF_ss 1);
+qed "while_unfold2";
-val while_unfold3 = prove_goal Loop.thy
- "while`b`g`x = while`b`g`(step`b`g`x)"
- (fn prems =>
- [
- (res_inst_tac [("s",
- "while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1),
- (rtac (while_unfold2 RS spec) 1),
- (Simp_tac 1)
- ]);
+Goal "while`b`g`x = while`b`g`(step`b`g`x)";
+by (res_inst_tac [("s", "while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1);
+by (rtac (while_unfold2 RS spec) 1);
+by (Simp_tac 1);
+qed "while_unfold3";
(* ------------------------------------------------------------------------- *)
(* properties of while and iterations *)
(* ------------------------------------------------------------------------- *)
-val loop_lemma1 = prove_goal Loop.thy
- "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \
-\ ==>iterate(Suc k) (step`b`g) x=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (Simp_tac 1),
- (rtac trans 1),
- (rtac step_def2 1),
- (asm_simp_tac HOLCF_ss 1),
- (etac exE 1),
- (etac (flat_codom RS disjE) 1),
- (asm_simp_tac HOLCF_ss 1),
- (asm_simp_tac HOLCF_ss 1)
- ]);
+Goal "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \
+\ ==>iterate(Suc k) (step`b`g) x=UU";
+by (Simp_tac 1);
+by (rtac trans 1);
+by (rtac step_def2 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (etac exE 1);
+by (etac (flat_codom RS disjE) 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (asm_simp_tac HOLCF_ss 1);
+qed "loop_lemma1";
+
+Goal "[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
+\ iterate k (step`b`g) x ~=UU";
+
+by (blast_tac (claset() addIs [loop_lemma1]) 1);
+qed "loop_lemma2";
-val loop_lemma2 = prove_goal Loop.thy
-"[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
-\iterate k (step`b`g) x ~=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac contrapos 1),
- (etac loop_lemma1 2),
- (atac 1),
- (atac 1)
- ]);
+Goal "[| ALL x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
+\ EX y. b`y=FF; INV x |] \
+\ ==> iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)";
+by (nat_ind_tac "k" 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (simp_tac (simpset() addsimps [step_def2]) 1);
+by (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1);
+by (etac notE 1);
+by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac mp 1);
+by (etac spec 1);
+by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
+by (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"),
+ ("t","g`(iterate k (step`b`g) x)")] ssubst 1);
+by (atac 2);
+by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
+by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
+qed_spec_mp "loop_lemma3";
-val loop_lemma3 = prove_goal Loop.thy
-"[| ALL x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
-\ EX y. b`y=FF; INV x |] \
-\==> iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (nat_ind_tac "k" 1),
- (Asm_simp_tac 1),
- (strip_tac 1),
- (simp_tac (simpset() addsimps [step_def2]) 1),
- (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1),
- (etac notE 1),
- (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
- (asm_simp_tac HOLCF_ss 1),
- (rtac mp 1),
- (etac spec 1),
- (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
- addsimps [loop_lemma2] ) 1),
- (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"),
- ("t","g`(iterate k (step`b`g) x)")] ssubst 1),
- (atac 2),
- (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
- (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
- addsimps [loop_lemma2] ) 1)
- ]);
+Goal "ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x";
+by (nat_ind_tac "k" 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (stac while_unfold 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (rtac allI 1);
+by (stac iterate_Suc2 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac while_unfold3 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "loop_lemma4";
+
+Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\
+\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU";
+by (stac while_def2 1);
+by (rtac fix_ind 1);
+by (rtac (allI RS adm_all) 1);
+by (rtac adm_eq 1);
+by (cont_tacR 1);
+by (Simp_tac 1);
+by (rtac allI 1);
+by (Simp_tac 1);
+by (res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1);
+by (etac spec 2);
+by (rtac cfun_arg_cong 1);
+by (rtac trans 1);
+by (rtac (iterate_Suc RS sym) 2);
+by (asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1);
+by (Blast_tac 1);
+qed_spec_mp "loop_lemma5";
-val loop_lemma4 = prove_goal Loop.thy
-"ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x"
- (fn prems =>
- [
- (nat_ind_tac "k" 1),
- (Simp_tac 1),
- (strip_tac 1),
- (stac while_unfold 1),
- (asm_simp_tac HOLCF_ss 1),
- (rtac allI 1),
- (stac iterate_Suc2 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac while_unfold3 1),
- (asm_simp_tac HOLCF_ss 1)
- ]);
+Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU";
+by (res_inst_tac [("t","x")] (iterate_0 RS subst) 1);
+by (etac (loop_lemma5) 1);
+qed "loop_lemma6";
-val loop_lemma5 = prove_goal Loop.thy
-"ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\
-\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (stac while_def2 1),
- (rtac fix_ind 1),
- (rtac (allI RS adm_all) 1),
- (rtac adm_eq 1),
- (cont_tacR 1),
- (Simp_tac 1),
- (rtac allI 1),
- (Simp_tac 1),
- (res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1),
- (asm_simp_tac HOLCF_ss 1),
- (asm_simp_tac HOLCF_ss 1),
- (res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1),
- (etac spec 2),
- (rtac cfun_arg_cong 1),
- (rtac trans 1),
- (rtac (iterate_Suc RS sym) 2),
- (asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1),
- (dtac spec 1),
- (contr_tac 1)
- ]);
-
-
-val loop_lemma6 = prove_goal Loop.thy
-"ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU"
- (fn prems =>
- [
- (res_inst_tac [("t","x")] (iterate_0 RS subst) 1),
- (rtac (loop_lemma5 RS spec) 1),
- (resolve_tac prems 1)
- ]);
-
-val loop_lemma7 = prove_goal Loop.thy
-"while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac swap 1),
- (rtac loop_lemma6 1),
- (fast_tac HOL_cs 1)
- ]);
-
-val loop_lemma8 = prove_goal Loop.thy
-"while`b`g`x ~= UU ==> EX y. b`y=FF"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (dtac loop_lemma7 1),
- (fast_tac HOL_cs 1)
- ]);
+Goal "while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF";
+by (blast_tac (claset() addIs [loop_lemma6]) 1);
+qed "loop_lemma7";
(* ------------------------------------------------------------------------- *)
(* an invariant rule for loops *)
(* ------------------------------------------------------------------------- *)
-val loop_inv2 = prove_goal Loop.thy
+Goal
"[| (ALL y. INV y & b`y=TT & g`y ~= UU --> INV (g`y));\
\ (ALL y. INV y & b`y=FF --> Q y);\
-\ INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)"
- (fn prems =>
- [
- (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1),
- (rtac loop_lemma7 1),
- (resolve_tac prems 1),
- (stac (loop_lemma4 RS spec RS mp) 1),
- (atac 1),
- (rtac (nth_elem (1,prems) RS spec RS mp) 1),
- (rtac conjI 1),
- (atac 2),
- (rtac (loop_lemma3 RS mp) 1),
- (resolve_tac prems 1),
- (rtac loop_lemma8 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (rtac notI2 1),
- (resolve_tac prems 1),
- (etac box_equals 1),
- (rtac (loop_lemma4 RS spec RS mp RS sym) 1),
- (atac 1),
- (rtac refl 1)
- ]);
+\ INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)";
+by (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1);
+by (etac loop_lemma7 1);
+by (stac (loop_lemma4) 1);
+by (atac 1);
+by (dtac spec 1 THEN etac mp 1);
+by (rtac conjI 1);
+by (atac 2);
+by (rtac (loop_lemma3) 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [loop_lemma6]) 1);
+by (assume_tac 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset() addsimps [loop_lemma4]) 1);
+qed "loop_inv2";
-val loop_inv3 = prove_goal Loop.thy
-"[| !!y.[| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
-\ !!y.[| INV y; b`y=FF|]==> Q y;\
-\ INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)"
- (fn prems =>
- [
- (rtac loop_inv2 1),
- (rtac allI 1),
- (rtac impI 1),
- (resolve_tac prems 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1),
- (rtac allI 1),
- (rtac impI 1),
- (resolve_tac prems 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
-
-val loop_inv = prove_goal Loop.thy
-"[| P(x);\
+val [premP,premI,premTT,premFF,premW] = Goal
+"[| P(x); \
\ !!y. P y ==> INV y;\
-\ !!y.[| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
-\ !!y.[| INV y; b`y=FF|]==> Q y;\
-\ while`b`g`x ~= UU |] ==> Q (while`b`g`x)"
- (fn prems =>
- [
- (rtac loop_inv3 1),
- (eresolve_tac prems 1),
- (atac 1),
- (atac 1),
- (resolve_tac prems 1),
- (atac 1),
- (atac 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
+\ !!y. [| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
+\ !!y. [| INV y; b`y=FF|] ==> Q y;\
+\ while`b`g`x ~= UU |] ==> Q (while`b`g`x)";
+by (rtac loop_inv2 1);
+by (rtac (premP RS premI) 3);
+by (rtac premW 3);
+by (blast_tac (claset() addIs [premTT]) 1);
+by (blast_tac (claset() addIs [premFF]) 1);
+qed "loop_inv";
--- a/src/HOLCF/ex/Stream.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/ex/Stream.ML Wed Jul 05 16:37:52 2000 +0200
@@ -12,65 +12,60 @@
val [stream_con_rew1,stream_con_rew2] = stream.con_rews;
+Addsimps stream.take_rews;
+Addsimps stream.when_rews;
+Addsimps stream.sel_rews;
+
(* ----------------------------------------------------------------------- *)
(* theorems about scons *)
(* ----------------------------------------------------------------------- *)
section "scons";
-qed_goal "scons_eq_UU" thy "a && s = UU = (a = UU)" (fn _ => [
- safe_tac HOL_cs,
- etac contrapos2 1,
- safe_tac (HOL_cs addSIs stream.con_rews)]);
+Goal "a && s = UU = (a = UU)";
+by Safe_tac;
+by (etac contrapos2 1);
+by (safe_tac (claset() addSIs stream.con_rews));
+qed "scons_eq_UU";
-qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R"
- (fn prems => [
- cut_facts_tac prems 1,
- dresolve_tac [stream_con_rew2] 1,
- contr_tac 1]);
+Goal "[| a && x = UU; a ~= UU |] ==> R";
+by (dresolve_tac [stream_con_rew2] 1);
+by (contr_tac 1);
+qed "scons_not_empty";
-qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU & x = a && y)"
- (fn _ =>[
- cut_facts_tac [stream.exhaust] 1,
- safe_tac HOL_cs,
- contr_tac 1,
- fast_tac (HOL_cs addDs [stream_con_rew2]) 1,
- fast_tac HOL_cs 1,
- fast_tac (HOL_cs addDs [stream_con_rew2]) 1]);
+Goal "x ~= UU = (EX a y. a ~= UU & x = a && y)";
+by (cut_facts_tac [stream.exhaust] 1);
+by (best_tac (claset() addDs [stream_con_rew2]) 1);
+qed "stream_exhaust_eq";
-qed_goal "stream_prefix" thy
-"[| a && s << t; a ~= UU |] ==> ? b tt. t = b && tt & b ~= UU & s << tt"
- (fn prems => [
- cut_facts_tac prems 1,
- stream_case_tac "t" 1,
- fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1,
- fast_tac (HOL_cs addDs stream.inverts) 1]);
+Goal
+"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt";
+by (stream_case_tac "t" 1);
+by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1);
+by (fast_tac (claset() addDs stream.inverts) 1);
+qed "stream_prefix";
-qed_goal "stream_flat_prefix" thy
-"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
-(fn prems=>[
- cut_facts_tac prems 1,
- (cut_facts_tac [read_instantiate[("x1","x::'a::flat"),
- ("x","y::'a::flat")]
- (ax_flat RS spec RS spec)] 1),
- (forward_tac stream.inverts 1),
- (safe_tac HOL_cs),
- (dtac (hd stream.con_rews RS subst) 1),
- (fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1)]);
+Goal "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys";
+by (cut_inst_tac [("x1","x::'a::flat"), ("x","y::'a::flat")]
+ (ax_flat RS spec RS spec) 1);
+by (forward_tac stream.inverts 1);
+by Safe_tac;
+by (dtac (hd stream.con_rews RS subst) 1);
+by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1);
+qed "stream_flat_prefix";
-qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \
-\(x = UU | (? a y. x = a && y & a ~= UU & a << b & y << z))" (fn prems => [
- cut_facts_tac prems 1,
- safe_tac HOL_cs,
- stream_case_tac "x" 1,
- safe_tac (HOL_cs addSDs stream.inverts
- addSIs [minimal, monofun_cfun, monofun_cfun_arg]),
- fast_tac HOL_cs 1]);
+Goal "b ~= UU ==> x << b && z = \
+\ (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))";
+by Safe_tac;
+by (stream_case_tac "x" 1);
+by (safe_tac (claset() addSDs stream.inverts
+ addSIs [minimal, monofun_cfun, monofun_cfun_arg]));
+by (Fast_tac 1);
+qed "stream_prefix'";
-qed_goal "stream_inject_eq" thy
- "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)" (fn prems => [
- cut_facts_tac prems 1,
- safe_tac (HOL_cs addSEs stream.injects)]);
+Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)";
+by (best_tac (claset() addSEs stream.injects) 1);
+qed "stream_inject_eq";
(* ----------------------------------------------------------------------- *)
@@ -79,10 +74,10 @@
section "stream_when";
-qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [
- stream_case_tac "s" 1,
- ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_Rep_CFun1::stream.when_rews))
- ]);
+Goal "stream_when`UU`s=UU";
+by (stream_case_tac "s" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1])));
+qed "stream_when_strictf";
(* ----------------------------------------------------------------------- *)
@@ -92,39 +87,38 @@
section "ft & rt";
(*
-qed_goal "stream_ft_lemma1" thy "ft`s=UU --> s=UU" (fn prems => [
- stream_case_tac "s" 1,
- REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)]);
+Goal "ft`s=UU --> s=UU";
+by (stream_case_tac "s" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1));
+qed "stream_ft_lemma1";
*)
-qed_goal "ft_defin" thy "s~=UU ==> ft`s~=UU" (fn prems => [
- cut_facts_tac prems 1,
- stream_case_tac "s" 1,
- fast_tac HOL_cs 1,
- asm_simp_tac (HOLCF_ss addsimps stream.rews) 1]);
+Goal "s~=UU ==> ft`s~=UU";
+by (stream_case_tac "s" 1);
+by (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps stream.rews) 1);
+qed "ft_defin";
-qed_goal "rt_strict_rev" thy "rt`s~=UU ==> s~=UU" (fn prems => [
- cut_facts_tac prems 1,
- etac contrapos 1,
- asm_simp_tac (HOLCF_ss addsimps stream.sel_rews) 1]);
+Goal "rt`s~=UU ==> s~=UU";
+by Auto_tac;
+qed "rt_strict_rev";
-qed_goal "surjectiv_scons" thy "(ft`s)&&(rt`s)=s"
- (fn prems =>
- [
- stream_case_tac "s" 1,
- REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)
- ]);
+Goal "(ft`s)&&(rt`s)=s";
+by (stream_case_tac "s" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews)));
+qed "surjectiv_scons";
-qed_goal_spec_mp "monofun_rt_mult" thy
-"!x s. x << s --> iterate i rt x << iterate i rt s" (fn _ => [
- nat_ind_tac "i" 1,
- simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
- strip_tac 1,
- stream_case_tac "x" 1,
- rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1,
- dtac stream_prefix 1,
- safe_tac HOL_cs,
- asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1]);
+Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s";
+by (induct_tac "i" 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (stream_case_tac "x" 1);
+by (rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1);
+by (dtac stream_prefix 1);
+by Safe_tac;
+by (asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1);
+qed_spec_mp "monofun_rt_mult";
+
(* ----------------------------------------------------------------------- *)
@@ -133,88 +127,84 @@
section "stream_take";
-qed_goal "stream_reach2" thy "(LUB i. stream_take i`s) = s"
- (fn prems =>
- [
- (res_inst_tac [("t","s")] (stream.reach RS subst) 1),
- (stac fix_def2 1),
- (rewrite_goals_tac [stream.take_def]),
- (stac contlub_cfun_fun 1),
- (rtac chain_iterate 1),
- (rtac refl 1)
- ]);
+Goal "(LUB i. stream_take i`s) = s";
+by (subgoal_tac "(LUB i. stream_take i`s) = fix`stream_copy`s" 1);
+by (simp_tac (simpset() addsimps [fix_def2, stream.take_def,
+ contlub_cfun_fun, chain_iterate]) 2);
+by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
+qed "stream_reach2";
-qed_goal "chain_stream_take" thy "chain (%i. stream_take i`s)" (fn _ => [
- rtac chainI 1,
- subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
- fast_tac HOL_cs 1,
- rtac allI 1,
- nat_ind_tac "i" 1,
- simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
- rtac allI 1,
- stream_case_tac "s" 1,
- simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
- asm_simp_tac (HOLCF_ss addsimps monofun_cfun_arg::stream.take_rews) 1]);
+Goal "chain (%i. stream_take i`s)";
+by (rtac chainI 1);
+by (subgoal_tac "ALL i s. stream_take i`s << stream_take (Suc i)`s" 1);
+by (Fast_tac 1);
+by (rtac allI 1);
+by (induct_tac "ia" 1);
+by (Simp_tac 1);
+by (rtac allI 1);
+by (stream_case_tac "s" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [monofun_cfun_arg]) 1);
+qed "chain_stream_take";
-qed_goalw "stream_take_more" thy [stream.take_def]
- "stream_take n`x = x ==> stream_take (Suc n)`x = x" (fn prems => [
- cut_facts_tac prems 1,
- rtac antisym_less 1,
- rtac (stream.reach RS subst) 1, (* 1*back(); *)
- rtac monofun_cfun_fun 1,
- stac fix_def2 1,
- rtac is_ub_thelub 1,
- rtac chain_iterate 1,
- etac subst 1, (* 2*back(); *)
- rtac monofun_cfun_fun 1,
- rtac (rewrite_rule [chain] chain_iterate RS spec) 1]);
+
+Goalw [stream.take_def]
+ "stream_take n`x = x ==> stream_take (Suc n)`x = x";
+by (rtac antisym_less 1);
+by (subgoal_tac "iterate (Suc n) stream_copy UU`x << fix`stream_copy`x" 1);
+by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
+by (rtac monofun_cfun_fun 1);
+by (stac fix_def2 1);
+by (rtac is_ub_thelub 1);
+by (rtac chain_iterate 1);
+by (etac subst 1 THEN rtac monofun_cfun_fun 1);
+by (rtac (rewrite_rule [chain] chain_iterate RS spec) 1);
+qed "stream_take_more";
(*
-val stream_take_lemma2 = prove_goal thy
- "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2" (fn prems => [
- (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),
- (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 ),
- (subgoal_tac "stream_take n1`xs = xs" 1),
- (rtac ((hd stream_inject) RS conjunct2) 2),
- (atac 4),
- (atac 2),
- (atac 2),
- (rtac cfun_arg_cong 1),
- (fast_tac HOL_cs 1)
- ]);
+Goal
+ "ALL s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2";
+by (induct_tac "n" 1);
+by (simp_tac (simpset() addsimps stream_rews) 1);
+by (strip_tac 1);
+by (hyp_subst_tac 1);
+by (simp_tac (simpset() addsimps stream_rews) 1);
+by (rtac allI 1);
+by (res_inst_tac [("s","s2")] streamE 1);
+by (asm_simp_tac (simpset() addsimps stream_rews) 1);
+by (asm_simp_tac (simpset() addsimps stream_rews) 1);
+by (strip_tac 1 );
+by (subgoal_tac "stream_take n1`xs = xs" 1);
+by (rtac ((hd stream_inject) RS conjunct2) 2);
+by (atac 4);
+by (atac 2);
+by (atac 2);
+by (rtac cfun_arg_cong 1);
+by (Blast_tac 1);
+qed "stream_take_lemma2";
*)
-val stream_take_lemma3 = prove_goal thy
- "!x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
- (fn prems => [
- (nat_ind_tac "n" 1),
- (asm_simp_tac (HOL_ss addsimps stream.take_rews) 1),
- (strip_tac 1),
- (res_inst_tac [("P","x && xs=UU")] notE 1),
- (eresolve_tac stream.con_rews 1),
- (etac sym 1),
- (strip_tac 1),
- (rtac stream_take_more 1),
- (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1),
- (etac (hd(tl(tl(stream.take_rews))) RS subst) 1),
- (atac 1),
- (atac 1)]) RS spec RS spec RS mp RS mp;
+Goal
+ "ALL x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (res_inst_tac [("P","x && xs=UU")] notE 1);
+by (eresolve_tac stream.con_rews 1);
+by (etac sym 1);
+by (strip_tac 1);
+by (rtac stream_take_more 1);
+by (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1);
+by (assume_tac 3);
+by (etac (hd(tl(tl(stream.take_rews))) RS subst) 1);
+by (atac 1);
+qed_spec_mp "stream_take_lemma3";
-val stream_take_lemma4 = prove_goal thy
- "!x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs"
- (fn _ => [
- (nat_ind_tac "n" 1),
- (simp_tac (HOL_ss addsimps stream.take_rews) 1),
- (simp_tac (HOL_ss addsimps stream.take_rews) 1)
- ]) RS spec RS spec RS mp;
+Goal
+ "ALL x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "stream_take_lemma4";
(* ------------------------------------------------------------------------- *)
@@ -223,50 +213,58 @@
section "induction";
-qed_goalw "stream_finite_ind" thy [stream.finite_def]
- "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x"
- (fn prems => [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (etac subst 1),
- (rtac stream.finite_ind 1),
- (atac 1),
- (eresolve_tac prems 1),
- (atac 1)]);
-qed_goal "stream_finite_ind2" thy
+val prems = Goalw [stream.finite_def]
+ "[| stream_finite x; \
+\ P UU; \
+\ !!a s. [| a ~= UU; P s |] \
+\ ==> P (a && s) |] ==> P x";
+by (cut_facts_tac prems 1);
+by (etac exE 1);
+by (etac subst 1);
+by (rtac stream.finite_ind 1);
+by (atac 1);
+by (eresolve_tac prems 1);
+by (atac 1);
+qed "stream_finite_ind";
+
+val major::prems = Goal
"[| P UU;\
\ !! x . x ~= UU ==> P (x && UU); \
\ !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s ) \
-\ |] ==> !s. P (stream_take n`s)" (fn prems => [
- res_inst_tac [("n","n")] nat_induct2 1,
- asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
- rtac allI 1,
- stream_case_tac "s" 1,
- asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
- asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
- rtac allI 1,
- stream_case_tac "s" 1,
- asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
- res_inst_tac [("x","sa")] stream.casedist 1,
- asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
- asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1]);
+\ |] ==> !s. P (stream_take n`s)";
+by (res_inst_tac [("n","n")] nat_induct2 1);
+by (asm_simp_tac (simpset() addsimps [major]) 1);
+by (rtac allI 1);
+by (stream_case_tac "s" 1);
+by (asm_simp_tac (simpset() addsimps [major]) 1);
+by (asm_simp_tac (simpset() addsimps prems) 1);
+by (rtac allI 1);
+by (stream_case_tac "s" 1);
+by (asm_simp_tac (simpset() addsimps [major]) 1);
+by (res_inst_tac [("x","sa")] stream.casedist 1);
+by (asm_simp_tac (simpset() addsimps prems) 1);
+by (asm_simp_tac (simpset() addsimps prems) 1);
+qed "stream_finite_ind2";
-qed_goal "stream_ind2" thy
+val prems = Goal
"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \
\ !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\
-\ |] ==> P x" (fn prems => [
- rtac (stream.reach RS subst) 1,
- rtac (adm_impl_admw RS wfix_ind) 1,
- rtac adm_subst 1,
- cont_tacR 1,
- resolve_tac prems 1,
- rtac allI 1,
- rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1,
- resolve_tac prems 1,
- eresolve_tac prems 1,
- eresolve_tac prems 1, atac 1, atac 1]);
+\ |] ==> P x";
+by (rtac (stream.reach RS subst) 1);
+by (rtac (adm_impl_admw RS wfix_ind) 1);
+by (rtac adm_subst 1);
+by (cont_tacR 1);
+by (resolve_tac prems 1);
+by (rtac allI 1);
+by (rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1);
+by (resolve_tac prems 1);
+by (eresolve_tac prems 1);
+by (eresolve_tac prems 1);
+by (atac 1);
+by (atac 1);
+qed "stream_ind2";
(* ----------------------------------------------------------------------- *)
@@ -275,41 +273,39 @@
section "coinduction";
-qed_goalw "stream_coind_lemma2" thy [stream.bisim_def]
-"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (etac allE 1),
- (etac allE 1),
- (dtac mp 1),
- (atac 1),
- (etac conjE 1),
- (case_tac "x = UU & x' = UU" 1),
- (rtac disjI1 1),
- (fast_tac HOL_cs 1),
- (rtac disjI2 1),
- (rtac disjE 1),
- (etac (de_Morgan_conj RS subst) 1),
- (res_inst_tac [("x","ft`x")] exI 1),
- (res_inst_tac [("x","rt`x")] exI 1),
- (res_inst_tac [("x","rt`x'")] exI 1),
- (rtac conjI 1),
- (etac ft_defin 1),
- (asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
- (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1),
- (simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
- (res_inst_tac [("x","ft`x'")] exI 1),
- (res_inst_tac [("x","rt`x")] exI 1),
- (res_inst_tac [("x","rt`x'")] exI 1),
- (rtac conjI 1),
- (etac ft_defin 1),
- (asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
- (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1),
- (etac sym 1),
- (simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1)
- ]);
+
+Goalw [stream.bisim_def]
+"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R";
+by (strip_tac 1);
+by (etac allE 1);
+by (etac allE 1);
+by (dtac mp 1);
+by (atac 1);
+by (etac conjE 1);
+by (case_tac "x = UU & x' = UU" 1);
+by (rtac disjI1 1);
+by (Blast_tac 1);
+by (rtac disjI2 1);
+by (rtac disjE 1);
+by (etac (de_Morgan_conj RS subst) 1);
+by (res_inst_tac [("x","ft`x")] exI 1);
+by (res_inst_tac [("x","rt`x")] exI 1);
+by (res_inst_tac [("x","rt`x'")] exI 1);
+by (rtac conjI 1);
+by (etac ft_defin 1);
+by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
+by (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1);
+by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
+by (res_inst_tac [("x","ft`x'")] exI 1);
+by (res_inst_tac [("x","rt`x")] exI 1);
+by (res_inst_tac [("x","rt`x'")] exI 1);
+by (rtac conjI 1);
+by (etac ft_defin 1);
+by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
+by (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1);
+by (etac sym 1);
+by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
+qed "stream_coind_lemma2";
(* ----------------------------------------------------------------------- *)
(* theorems about stream_finite *)
@@ -317,59 +313,44 @@
section "stream_finite";
-qed_goalw "stream_finite_UU" thy [stream.finite_def] "stream_finite UU"
- (fn prems => [
- (rtac exI 1),
- (simp_tac (HOLCF_ss addsimps stream.rews) 1)]);
+
+Goalw [stream.finite_def] "stream_finite UU";
+by (rtac exI 1);
+by (simp_tac (simpset() addsimps stream.rews) 1);
+qed "stream_finite_UU";
-qed_goal "stream_finite_UU_rev" thy "~ stream_finite s ==> s ~= UU" (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac contrapos 1),
- (hyp_subst_tac 1),
- (rtac stream_finite_UU 1)
- ]);
+Goal "~ stream_finite s ==> s ~= UU";
+by (blast_tac (claset() addIs [stream_finite_UU]) 1);
+qed "stream_finite_UU_rev";
-qed_goalw "stream_finite_lemma1" thy [stream.finite_def]
- "stream_finite xs ==> stream_finite (x && xs)" (fn prems => [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (rtac exI 1),
- (etac stream_take_lemma4 1)
- ]);
+Goalw [stream.finite_def] "stream_finite xs ==> stream_finite (x && xs)";
+by (blast_tac (claset() addIs [stream_take_lemma4]) 1);
+qed "stream_finite_lemma1";
+
+Goalw [stream.finite_def]
+ "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs";
+by (blast_tac (claset() addIs [stream_take_lemma3]) 1);
+qed "stream_finite_lemma2";
-qed_goalw "stream_finite_lemma2" thy [stream.finite_def]
- "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (rtac exI 1),
- (etac stream_take_lemma3 1),
- (atac 1)
- ]);
-
-qed_goal "stream_finite_rt_eq" thy "stream_finite (rt`s) = stream_finite s"
- (fn _ => [
- stream_case_tac "s" 1,
- simp_tac (HOL_ss addsimps stream_finite_UU::stream.sel_rews) 1,
- asm_simp_tac (HOL_ss addsimps stream.sel_rews) 1,
- fast_tac (HOL_cs addIs [stream_finite_lemma1]
- addDs [stream_finite_lemma2]) 1]);
+Goal "stream_finite (rt`s) = stream_finite s";
+by (stream_case_tac "s" 1);
+by (simp_tac (simpset() addsimps [stream_finite_UU]) 1);
+by (Asm_simp_tac 1);
+by (fast_tac (claset() addIs [stream_finite_lemma1]
+ addDs [stream_finite_lemma2]) 1);
+qed "stream_finite_rt_eq";
-qed_goal_spec_mp "stream_finite_less" thy
- "stream_finite s ==> !t. t<<s --> stream_finite t" (fn prems => [
- cut_facts_tac prems 1,
- eres_inst_tac [("x","s")] stream_finite_ind 1,
- strip_tac 1, dtac UU_I 1,
- asm_simp_tac (HOLCF_ss addsimps [stream_finite_UU]) 1,
- strip_tac 1,
- asm_full_simp_tac (HOL_ss addsimps [stream_prefix']) 1,
- fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]);
+Goal "stream_finite s ==> !t. t<<s --> stream_finite t";
+by (eres_inst_tac [("x","s")] stream_finite_ind 1);
+by (strip_tac 1);
+by (dtac UU_I 1);
+by (asm_simp_tac (simpset() addsimps [stream_finite_UU]) 1);
+by (strip_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [stream_prefix']) 1);
+by (fast_tac (claset() addSIs [stream_finite_UU, stream_finite_lemma1]) 1);
+qed_spec_mp "stream_finite_less";
-qed_goal "adm_not_stream_finite" thy "adm (%x. ~ stream_finite x)" (fn _ => [
- rtac admI2 1,
- dtac spec 1,
- etac contrapos 1,
- dtac stream_finite_less 1,
- etac is_ub_thelub 1,
- atac 1]);
+Goal "adm (%x. ~ stream_finite x)";
+by (rtac admI2 1);
+by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1);
+qed "adm_not_stream_finite";
--- a/src/HOLCF/ex/loeckx.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/ex/loeckx.ML Wed Jul 05 16:37:52 2000 +0200
@@ -2,20 +2,12 @@
(* Elegant proof for continuity of fixed-point operator *)
(* Loeckx & Sieber S.88 *)
-val prems = goalw Fix.thy [Ifix_def]
-"Ifix F= lub (range (%i.%G. iterate i G UU)) F";
+Goalw [Ifix_def] "Ifix F= lub (range (%i.%G. iterate i G UU)) F";
by (stac thelub_fun 1);
-by (rtac ch2ch_fun 1);
-back();
by (rtac refl 2);
-by (rtac chainI 1);
-by (strip_tac 1);
-by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (rtac (less_fun RS iffD2) 1);
-by (strip_tac 1);
-by (rtac (chain_iterate RS chainE RS spec) 1);
-val loeckx_sieber = result();
+by (blast_tac (claset() addIs [ch2ch_fun, chainI, less_fun RS iffD2,
+ chain_iterate RS chainE]) 1);
+qed "loeckx_sieber";
(*
@@ -46,7 +38,7 @@
*)
-val prems = goal Fix.thy "cont(Ifix)";
+Goal "cont(Ifix)";
by (res_inst_tac
[("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
ssubst 1);
@@ -73,27 +65,20 @@
by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
-by (rtac (chain_iterate RS chainE RS spec) 1);
-val cont_Ifix2 = result();
+by (rtac (chain_iterate RS chainE) 1);
+qed "cont_Ifix2";
(* the proof in little steps *)
-val prems = goal Fix.thy
-"(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
+Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
by (rtac ext 1);
-by (stac beta_cfun 1);
-by (rtac cont2cont_CF1L 1);
-by (rtac cont_iterate 1);
-by (rtac refl 1);
-val fix_lemma1 = result();
+by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1);
+qed "fix_lemma1";
-val prems = goal Fix.thy
-" Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
+Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
by (rtac ext 1);
-by (rewtac Ifix_def );
-by (stac fix_lemma1 1);
-by (rtac refl 1);
-val fix_lemma2 = result();
+by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1);
+qed "fix_lemma2";
(*
- cont_lubcfun;
@@ -101,11 +86,10 @@
*)
-val prems = goal Fix.thy "cont Ifix";
+Goal "cont Ifix";
by (stac fix_lemma2 1);
by (rtac cont_lubcfun 1);
by (rtac chainI 1);
-by (strip_tac 1);
by (rtac less_cfun2 1);
by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
@@ -113,6 +97,6 @@
by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
-by (rtac (chain_iterate RS chainE RS spec) 1);
-val cont_Ifix2 = result();
+by (rtac (chain_iterate RS chainE) 1);
+qed "cont_Ifix2";