# HG changeset patch # User paulson # Date 962807872 -7200 # Node ID e1dee89de0378f19d5e9a80528119c4b6de1d905 # Parent ad9f986616de30ff92416d58a1b476368df95a84 massive tidy-up: goal -> Goal, remove use of prems, etc. diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cfun1.ML --- 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cfun2.ML --- 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<'b::pcpo.!y. x< 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< f1`x1 << f2`x2"; -by (cut_facts_tac prems 1); +Goal "[|f1< 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<Abs_CFun(f)< Abs_CFun(f)< '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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cfun3.ML --- 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< x=UU | x=y; \ +Goal "!!f g.[|!x y::'a. x< x=UU | x=y; \ \ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x< 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cont.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cprod1.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cprod2.ML --- 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< 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)< 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< (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"; -by (cut_facts_tac prems 1); +Goal "[|x1< (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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Cprod3.ML --- 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=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 = "; +Goalw [cpair_def] "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 " = 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="; 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= |] ==> Q|] ==> Q"; +val prems = Goalw [cpair_def] "[|!!x y. [|p= |] ==> 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"; -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`=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] " = p"; +Goalw [cfst_def,csnd_def,cpair_def] " = 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< 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) = " *) -val prems = goalw Cprod3.thy [csplit_def] +Goalw [csplit_def] "csplit`f` = 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Fix.ML --- 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'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\ \ chain(%m. Y(Least(%j. m ! m. P(Y(LEAST j::nat. m'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\ \ lub(range(Y)) = lub(range(%m. Y(Least(%j. m'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 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Fun2.ML --- 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<'b::pcpo.!y. x<('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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Fun3.ML --- 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Lift1.ML --- 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Lift2.ML --- 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=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~Y(i)=Undef"; +Goal "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \ +\ ==> EX j. ALL i. j~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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Lift3.ML --- 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/One.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Pcpo.ML --- 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~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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Porder.ML --- 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 F x< x F x< 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< 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< 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< 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< 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Porder0.ML --- 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< uu=(@u.!y. u< 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Sprod0.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Sprod1.ML --- 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Sprod2.ML --- 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< 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Sprod3.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Ssum0.ML --- 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]; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Ssum1.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Ssum2.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Ssum3.ML --- 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Up1.ML --- 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< 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/Up3.ML --- 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<\ \ 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); diff -r ad9f986616de -r e1dee89de037 src/HOLCF/ex/Loop.ML --- 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/ex/Stream.ML --- 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< 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< 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"; diff -r ad9f986616de -r e1dee89de037 src/HOLCF/ex/loeckx.ML --- 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";