--- a/src/HOLCF/Cfun1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cfun1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* A non-emptyness result for Cfun *)
(* ------------------------------------------------------------------------ *)
-val CfunI = prove_goalw Cfun1.thy [Cfun_def] "(% x.x):Cfun"
+qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
(fn prems =>
[
(rtac (mem_Collect_eq RS ssubst) 1),
@@ -24,13 +24,13 @@
(* less_cfun is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val refl_less_cfun = prove_goalw Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
+qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
(fn prems =>
[
(rtac refl_less 1)
]);
-val antisym_less_cfun = prove_goalw Cfun1.thy [less_cfun_def]
+qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def]
"[|less_cfun(f1,f2); less_cfun(f2,f1)|] ==> f1 = f2"
(fn prems =>
[
@@ -43,7 +43,7 @@
(rtac Rep_Cfun_inverse 1)
]);
-val trans_less_cfun = prove_goalw Cfun1.thy [less_cfun_def]
+qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def]
"[|less_cfun(f1,f2); less_cfun(f2,f3)|] ==> less_cfun(f1,f3)"
(fn prems =>
[
@@ -56,7 +56,7 @@
(* lemmas about application of continuous functions *)
(* ------------------------------------------------------------------------ *)
-val cfun_cong = prove_goal Cfun1.thy
+qed_goal "cfun_cong" Cfun1.thy
"[| f=g; x=y |] ==> f[x] = g[y]"
(fn prems =>
[
@@ -64,7 +64,7 @@
(fast_tac HOL_cs 1)
]);
-val cfun_fun_cong = prove_goal Cfun1.thy "f=g ==> f[x] = g[x]"
+qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f[x] = g[x]"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -72,7 +72,7 @@
(rtac refl 1)
]);
-val cfun_arg_cong = prove_goal Cfun1.thy "x=y ==> f[x] = f[y]"
+qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f[x] = f[y]"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -86,7 +86,7 @@
(* additional lemma about the isomorphism between -> and Cfun *)
(* ------------------------------------------------------------------------ *)
-val Abs_Cfun_inverse2 = prove_goal Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
+qed_goal "Abs_Cfun_inverse2" Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -99,7 +99,7 @@
(* simplification of application *)
(* ------------------------------------------------------------------------ *)
-val Cfunapp2 = prove_goal Cfun1.thy
+qed_goal "Cfunapp2" Cfun1.thy
"contX(f) ==> (fabs(f))[x] = f(x)"
(fn prems =>
[
@@ -111,7 +111,7 @@
(* beta - equality for continuous functions *)
(* ------------------------------------------------------------------------ *)
-val beta_cfun = prove_goal Cfun1.thy
+qed_goal "beta_cfun" Cfun1.thy
"contX(c1) ==> (LAM x .c1(x))[u] = c1(u)"
(fn prems =>
[
--- a/src/HOLCF/Cfun2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cfun2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* access to less_cfun in class po *)
(* ------------------------------------------------------------------------ *)
-val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
+qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
(fn prems =>
[
(rtac (inst_cfun_po RS ssubst) 1),
@@ -24,7 +24,7 @@
(* Type 'a ->'b is pointed *)
(* ------------------------------------------------------------------------ *)
-val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
+qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
(fn prems =>
[
(rtac (less_cfun RS ssubst) 1),
@@ -40,7 +40,7 @@
(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2 *)
(* ------------------------------------------------------------------------ *)
-val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
+qed_goal "contX_fapp2" Cfun2.thy "contX(fapp(fo))"
(fn prems =>
[
(res_inst_tac [("P","contX")] CollectD 1),
@@ -72,7 +72,7 @@
(* fapp is monotone in its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
+qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
(fn prems =>
[
(strip_tac 1),
@@ -84,7 +84,7 @@
(* monotonicity of application fapp in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-val monofun_cfun_fun = prove_goal Cfun2.thy "f1 << f2 ==> f1[x] << f2[x]"
+qed_goal "monofun_cfun_fun" Cfun2.thy "f1 << f2 ==> f1[x] << f2[x]"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -101,7 +101,7 @@
(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-val monofun_cfun = prove_goal Cfun2.thy
+qed_goal "monofun_cfun" Cfun2.thy
"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
(fn prems =>
[
@@ -117,7 +117,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-val ch2ch_fappR = prove_goal Cfun2.thy
+qed_goal "ch2ch_fappR" Cfun2.thy
"is_chain(Y) ==> is_chain(%i. f[Y(i)])"
(fn prems =>
[
@@ -135,7 +135,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-val lub_cfun_mono = prove_goal Cfun2.thy
+qed_goal "lub_cfun_mono" Cfun2.thy
"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
(fn prems =>
[
@@ -151,7 +151,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-val ex_lubcfun = prove_goal Cfun2.thy
+qed_goal "ex_lubcfun" Cfun2.thy
"[| is_chain(F); is_chain(Y) |] ==>\
\ lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
\ lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
@@ -169,7 +169,7 @@
(* the lub of a chain of cont. functions is continuous *)
(* ------------------------------------------------------------------------ *)
-val contX_lubcfun = prove_goal Cfun2.thy
+qed_goal "contX_lubcfun" Cfun2.thy
"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
(fn prems =>
[
@@ -188,7 +188,7 @@
(* type 'a -> 'b is chain complete *)
(* ------------------------------------------------------------------------ *)
-val lub_cfun = prove_goal Cfun2.thy
+qed_goal "lub_cfun" Cfun2.thy
"is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
(fn prems =>
[
@@ -216,7 +216,7 @@
is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
*)
-val cpo_cfun = prove_goal Cfun2.thy
+qed_goal "cpo_cfun" Cfun2.thy
"is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
@@ -230,7 +230,7 @@
(* Extensionality in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
+qed_goal "ext_cfun" Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
(fn prems =>
[
(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
@@ -244,7 +244,7 @@
(* Monotonicity of fabs *)
(* ------------------------------------------------------------------------ *)
-val semi_monofun_fabs = prove_goal Cfun2.thy
+qed_goal "semi_monofun_fabs" Cfun2.thy
"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
(fn prems =>
[
@@ -260,7 +260,7 @@
(* Extenionality wrt. << in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
+qed_goal "less_cfun2" Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
(fn prems =>
[
(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
--- a/src/HOLCF/Cfun3.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cfun3.ML Tue Feb 07 11:59:32 1995 +0100
@@ -10,7 +10,7 @@
(* the contlub property for fapp its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-val contlub_fapp1 = prove_goal Cfun3.thy "contlub(fapp)"
+qed_goal "contlub_fapp1" Cfun3.thy "contlub(fapp)"
(fn prems =>
[
(rtac contlubI 1),
@@ -31,7 +31,7 @@
(* the contX property for fapp in its first argument *)
(* ------------------------------------------------------------------------ *)
-val contX_fapp1 = prove_goal Cfun3.thy "contX(fapp)"
+qed_goal "contX_fapp1" Cfun3.thy "contX(fapp)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -44,7 +44,7 @@
(* contlub, contX properties of fapp in its first argument in mixfix _[_] *)
(* ------------------------------------------------------------------------ *)
-val contlub_cfun_fun = prove_goal Cfun3.thy
+qed_goal "contlub_cfun_fun" Cfun3.thy
"is_chain(FY) ==>\
\ lub(range(FY))[x] = lub(range(%i.FY(i)[x]))"
(fn prems =>
@@ -58,7 +58,7 @@
]);
-val contX_cfun_fun = prove_goal Cfun3.thy
+qed_goal "contX_cfun_fun" Cfun3.thy
"is_chain(FY) ==>\
\ range(%i.FY(i)[x]) <<| lub(range(FY))[x]"
(fn prems =>
@@ -74,7 +74,7 @@
(* contlub, contX properties of fapp in both argument in mixfix _[_] *)
(* ------------------------------------------------------------------------ *)
-val contlub_cfun = prove_goal Cfun3.thy
+qed_goal "contlub_cfun" Cfun3.thy
"[|is_chain(FY);is_chain(TY)|] ==>\
\ lub(range(FY))[lub(range(TY))] = lub(range(%i.FY(i)[TY(i)]))"
(fn prems =>
@@ -88,7 +88,7 @@
(atac 1)
]);
-val contX_cfun = prove_goal Cfun3.thy
+qed_goal "contX_cfun" Cfun3.thy
"[|is_chain(FY);is_chain(TY)|] ==>\
\ range(%i.FY(i)[TY(i)]) <<| lub(range(FY))[lub(range(TY))]"
(fn prems =>
@@ -109,7 +109,7 @@
(* contX2contX lemma for fapp *)
(* ------------------------------------------------------------------------ *)
-val contX2contX_fapp = prove_goal Cfun3.thy
+qed_goal "contX2contX_fapp" Cfun3.thy
"[|contX(%x.ft(x));contX(%x.tt(x))|] ==> contX(%x.(ft(x))[tt(x)])"
(fn prems =>
[
@@ -129,7 +129,7 @@
(* contX2mono Lemma for %x. LAM y. c1(x,y) *)
(* ------------------------------------------------------------------------ *)
-val contX2mono_LAM = prove_goal Cfun3.thy
+qed_goal "contX2mono_LAM" Cfun3.thy
"[|!x.contX(c1(x)); !y.monofun(%x.c1(x,y))|] ==>\
\ monofun(%x. LAM y. c1(x,y))"
(fn prems =>
@@ -151,7 +151,7 @@
(* contX2contX Lemma for %x. LAM y. c1(x,y) *)
(* ------------------------------------------------------------------------ *)
-val contX2contX_LAM = prove_goal Cfun3.thy
+qed_goal "contX2contX_LAM" Cfun3.thy
"[| !x.contX(c1(x)); !y.contX(%x.c1(x,y)) |] ==> contX(%x. LAM y. c1(x,y))"
(fn prems =>
[
@@ -205,7 +205,7 @@
(* function application _[_] is strict in its first arguments *)
(* ------------------------------------------------------------------------ *)
-val strict_fapp1 = prove_goal Cfun3.thy "UU[x] = UU"
+qed_goal "strict_fapp1" Cfun3.thy "UU[x] = UU"
(fn prems =>
[
(rtac (inst_cfun_pcpo RS ssubst) 1),
@@ -220,7 +220,7 @@
(* results about strictify *)
(* ------------------------------------------------------------------------ *)
-val Istrictify1 = prove_goalw Cfun3.thy [Istrictify_def]
+qed_goalw "Istrictify1" Cfun3.thy [Istrictify_def]
"Istrictify(f)(UU)=UU"
(fn prems =>
[
@@ -229,7 +229,7 @@
(fast_tac HOL_cs 1)
]);
-val Istrictify2 = prove_goalw Cfun3.thy [Istrictify_def]
+qed_goalw "Istrictify2" Cfun3.thy [Istrictify_def]
"~x=UU ==> Istrictify(f)(x)=f[x]"
(fn prems =>
[
@@ -239,7 +239,7 @@
(fast_tac HOL_cs 1)
]);
-val monofun_Istrictify1 = prove_goal Cfun3.thy "monofun(Istrictify)"
+qed_goal "monofun_Istrictify1" Cfun3.thy "monofun(Istrictify)"
(fn prems =>
[
(rtac monofunI 1),
@@ -259,7 +259,7 @@
(rtac refl_less 1)
]);
-val monofun_Istrictify2 = prove_goal Cfun3.thy "monofun(Istrictify(f))"
+qed_goal "monofun_Istrictify2" Cfun3.thy "monofun(Istrictify(f))"
(fn prems =>
[
(rtac monofunI 1),
@@ -278,7 +278,7 @@
]);
-val contlub_Istrictify1 = prove_goal Cfun3.thy "contlub(Istrictify)"
+qed_goal "contlub_Istrictify1" Cfun3.thy "contlub(Istrictify)"
(fn prems =>
[
(rtac contlubI 1),
@@ -305,7 +305,7 @@
(rtac (refl RS allI) 1)
]);
-val contlub_Istrictify2 = prove_goal Cfun3.thy "contlub(Istrictify(f))"
+qed_goal "contlub_Istrictify2" Cfun3.thy "contlub(Istrictify(f))"
(fn prems =>
[
(rtac contlubI 1),
@@ -354,7 +354,7 @@
(monofun_Istrictify2 RS monocontlub2contX));
-val strictify1 = prove_goalw Cfun3.thy [strictify_def]
+qed_goalw "strictify1" Cfun3.thy [strictify_def]
"strictify[f][UU]=UU"
(fn prems =>
[
@@ -368,7 +368,7 @@
(rtac Istrictify1 1)
]);
-val strictify2 = prove_goalw Cfun3.thy [strictify_def]
+qed_goalw "strictify2" Cfun3.thy [strictify_def]
"~x=UU ==> strictify[f][x]=f[x]"
(fn prems =>
[
--- a/src/HOLCF/Cont.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cont.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* access to definition *)
(* ------------------------------------------------------------------------ *)
-val contlubI = prove_goalw Cont.thy [contlub]
+qed_goalw "contlubI" Cont.thy [contlub]
"! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
\ contlub(f)"
(fn prems =>
@@ -21,7 +21,7 @@
(atac 1)
]);
-val contlubE = prove_goalw Cont.thy [contlub]
+qed_goalw "contlubE" Cont.thy [contlub]
" contlub(f)==>\
\ ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
(fn prems =>
@@ -31,7 +31,7 @@
]);
-val contXI = prove_goalw Cont.thy [contX]
+qed_goalw "contXI" Cont.thy [contX]
"! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> contX(f)"
(fn prems =>
[
@@ -39,7 +39,7 @@
(atac 1)
]);
-val contXE = prove_goalw Cont.thy [contX]
+qed_goalw "contXE" Cont.thy [contX]
"contX(f) ==> ! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y)))"
(fn prems =>
[
@@ -48,7 +48,7 @@
]);
-val monofunI = prove_goalw Cont.thy [monofun]
+qed_goalw "monofunI" Cont.thy [monofun]
"! x y. x << y --> f(x) << f(y) ==> monofun(f)"
(fn prems =>
[
@@ -56,7 +56,7 @@
(atac 1)
]);
-val monofunE = prove_goalw Cont.thy [monofun]
+qed_goalw "monofunE" Cont.thy [monofun]
"monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
(fn prems =>
[
@@ -73,7 +73,7 @@
(* monotone functions map chains to chains *)
(* ------------------------------------------------------------------------ *)
-val ch2ch_monofun= prove_goal Cont.thy
+qed_goal "ch2ch_monofun" Cont.thy
"[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
(fn prems =>
[
@@ -88,7 +88,7 @@
(* monotone functions map upper bound to upper bounds *)
(* ------------------------------------------------------------------------ *)
-val ub2ub_monofun = prove_goal Cont.thy
+qed_goal "ub2ub_monofun" Cont.thy
"[| monofun(f); range(Y) <| u|] ==> range(%i.f(Y(i))) <| f(u)"
(fn prems =>
[
@@ -103,7 +103,7 @@
(* left to right: monofun(f) & contlub(f) ==> contX(f) *)
(* ------------------------------------------------------------------------ *)
-val monocontlub2contX = prove_goalw Cont.thy [contX]
+qed_goalw "monocontlub2contX" Cont.thy [contX]
"[|monofun(f);contlub(f)|] ==> contX(f)"
(fn prems =>
[
@@ -120,7 +120,7 @@
(* first a lemma about binary chains *)
(* ------------------------------------------------------------------------ *)
-val binchain_contX = prove_goal Cont.thy
+qed_goal "binchain_contX" Cont.thy
"[| contX(f); x << y |] ==> range(%i. f(if(i = 0,x,y))) <<| f(y)"
(fn prems =>
[
@@ -137,7 +137,7 @@
(* part1: contX(f) ==> monofun(f *)
(* ------------------------------------------------------------------------ *)
-val contX2mono = prove_goalw Cont.thy [monofun]
+qed_goalw "contX2mono" Cont.thy [monofun]
"contX(f) ==> monofun(f)"
(fn prems =>
[
@@ -155,7 +155,7 @@
(* part2: contX(f) ==> contlub(f) *)
(* ------------------------------------------------------------------------ *)
-val contX2contlub = prove_goalw Cont.thy [contlub]
+qed_goalw "contX2contlub" Cont.thy [contlub]
"contX(f) ==> contlub(f)"
(fn prems =>
[
@@ -171,7 +171,7 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-val ch2ch_MF2L = prove_goal Cont.thy
+qed_goal "ch2ch_MF2L" Cont.thy
"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
(fn prems =>
[
@@ -181,7 +181,7 @@
]);
-val ch2ch_MF2R = prove_goal Cont.thy
+qed_goal "ch2ch_MF2R" Cont.thy
"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
(fn prems =>
[
@@ -190,7 +190,7 @@
(atac 1)
]);
-val ch2ch_MF2LR = prove_goal Cont.thy
+qed_goal "ch2ch_MF2LR" Cont.thy
"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
\ is_chain(%i. MF2(F(i))(Y(i)))"
(fn prems =>
@@ -206,7 +206,7 @@
]);
-val ch2ch_lubMF2R = prove_goal Cont.thy
+qed_goal "ch2ch_lubMF2R" Cont.thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F);is_chain(Y)|] ==> \
@@ -226,7 +226,7 @@
]);
-val ch2ch_lubMF2L = prove_goal Cont.thy
+qed_goal "ch2ch_lubMF2L" Cont.thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F);is_chain(Y)|] ==> \
@@ -246,7 +246,7 @@
]);
-val lub_MF2_mono = prove_goal Cont.thy
+qed_goal "lub_MF2_mono" Cont.thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F)|] ==> \
@@ -266,7 +266,7 @@
(atac 1)
]);
-val ex_lubMF2 = prove_goal Cont.thy
+qed_goal "ex_lubMF2" Cont.thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F); is_chain(Y)|] ==> \
@@ -305,7 +305,7 @@
]);
-val diag_lubMF2_1 = prove_goal Cont.thy
+qed_goal "diag_lubMF2_1" Cont.thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
@@ -349,7 +349,7 @@
(atac 1)
]);
-val diag_lubMF2_2 = prove_goal Cont.thy
+qed_goal "diag_lubMF2_2" Cont.thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
@@ -373,7 +373,7 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-val contlub_CF2 = prove_goal Cont.thy
+qed_goal "contlub_CF2" Cont.thy
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
(fn prems =>
@@ -399,7 +399,7 @@
(* The following results are about application for functions in 'a=>'b *)
(* ------------------------------------------------------------------------ *)
-val monofun_fun_fun = prove_goal Cont.thy
+qed_goal "monofun_fun_fun" Cont.thy
"f1 << f2 ==> f1(x) << f2(x)"
(fn prems =>
[
@@ -407,7 +407,7 @@
(etac (less_fun RS iffD1 RS spec) 1)
]);
-val monofun_fun_arg = prove_goal Cont.thy
+qed_goal "monofun_fun_arg" Cont.thy
"[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
(fn prems =>
[
@@ -416,7 +416,7 @@
(atac 1)
]);
-val monofun_fun = prove_goal Cont.thy
+qed_goal "monofun_fun" Cont.thy
"[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
(fn prems =>
[
@@ -433,7 +433,7 @@
(* continuity *)
(* ------------------------------------------------------------------------ *)
-val mono2mono_MF1L = prove_goal Cont.thy
+qed_goal "mono2mono_MF1L" Cont.thy
"[|monofun(c1)|] ==> monofun(%x. c1(x,y))"
(fn prems =>
[
@@ -444,7 +444,7 @@
(atac 1)
]);
-val contX2contX_CF1L = prove_goal Cont.thy
+qed_goal "contX2contX_CF1L" Cont.thy
"[|contX(c1)|] ==> contX(%x. c1(x,y))"
(fn prems =>
[
@@ -465,7 +465,7 @@
(********* Note "(%x.%y.c1(x,y)) = c1" ***********)
-val mono2mono_MF1L_rev = prove_goal Cont.thy
+qed_goal "mono2mono_MF1L_rev" Cont.thy
"!y.monofun(%x.c1(x,y)) ==> monofun(c1)"
(fn prems =>
[
@@ -478,7 +478,7 @@
(atac 1)
]);
-val contX2contX_CF1L_rev = prove_goal Cont.thy
+qed_goal "contX2contX_CF1L_rev" Cont.thy
"!y.contX(%x.c1(x,y)) ==> contX(c1)"
(fn prems =>
[
@@ -504,7 +504,7 @@
(* never used here *)
(* ------------------------------------------------------------------------ *)
-val contlub_abstraction = prove_goal Cont.thy
+qed_goal "contlub_abstraction" Cont.thy
"[|is_chain(Y::nat=>'a);!y.contX(%x.(c::'a=>'b=>'c)(x,y))|] ==>\
\ (%y.lub(range(%i.c(Y(i),y)))) = (lub(range(%i.%y.c(Y(i),y))))"
(fn prems =>
@@ -521,7 +521,7 @@
]);
-val mono2mono_app = prove_goal Cont.thy
+qed_goal "mono2mono_app" Cont.thy
"[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
\ monofun(%x.(ft(x))(tt(x)))"
(fn prems =>
@@ -539,7 +539,7 @@
]);
-val contX2contlub_app = prove_goal Cont.thy
+qed_goal "contX2contlub_app" Cont.thy
"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
(fn prems =>
[
@@ -556,7 +556,7 @@
]);
-val contX2contX_app = prove_goal Cont.thy
+qed_goal "contX2contX_app" Cont.thy
"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
\ contX(%x.(ft(x))(tt(x)))"
(fn prems =>
@@ -587,7 +587,7 @@
(* The identity function is continuous *)
(* ------------------------------------------------------------------------ *)
-val contX_id = prove_goal Cont.thy "contX(% x.x)"
+qed_goal "contX_id" Cont.thy "contX(% x.x)"
(fn prems =>
[
(rtac contXI 1),
@@ -602,7 +602,7 @@
(* constant functions are continuous *)
(* ------------------------------------------------------------------------ *)
-val contX_const = prove_goalw Cont.thy [contX] "contX(%x.c)"
+qed_goalw "contX_const" Cont.thy [contX] "contX(%x.c)"
(fn prems =>
[
(strip_tac 1),
@@ -617,7 +617,7 @@
]);
-val contX2contX_app3 = prove_goal Cont.thy
+qed_goal "contX2contX_app3" Cont.thy
"[|contX(f);contX(t) |] ==> contX(%x. f(t(x)))"
(fn prems =>
[
--- a/src/HOLCF/Cprod1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cprod1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -8,14 +8,14 @@
open Cprod1;
-val less_cprod1b = prove_goalw Cprod1.thy [less_cprod_def]
+qed_goalw "less_cprod1b" Cprod1.thy [less_cprod_def]
"less_cprod(p1,p2) = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))"
(fn prems =>
[
(rtac refl 1)
]);
-val less_cprod2a = prove_goalw Cprod1.thy [less_cprod_def]
+qed_goalw "less_cprod2a" Cprod1.thy [less_cprod_def]
"less_cprod(<x,y>,<UU,UU>) ==> x = UU & y = UU"
(fn prems =>
[
@@ -32,7 +32,7 @@
(etac UU_I 1)
]);
-val less_cprod2b = prove_goal Cprod1.thy
+qed_goal "less_cprod2b" Cprod1.thy
"less_cprod(p,<UU,UU>) ==> p=<UU,UU>"
(fn prems =>
[
@@ -43,7 +43,7 @@
(asm_simp_tac HOL_ss 1)
]);
-val less_cprod2c = prove_goalw Cprod1.thy [less_cprod_def]
+qed_goalw "less_cprod2c" Cprod1.thy [less_cprod_def]
"less_cprod(<x1,y1>,<x2,y2>) ==> x1 << x2 & y1 << y2"
(fn prems =>
[
@@ -64,7 +64,7 @@
(* less_cprod is a partial order on 'a * 'b *)
(* ------------------------------------------------------------------------ *)
-val refl_less_cprod = prove_goalw Cprod1.thy [less_cprod_def] "less_cprod(p,p)"
+qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod(p,p)"
(fn prems =>
[
(res_inst_tac [("p","p")] PairE 1),
@@ -73,7 +73,7 @@
(simp_tac Cfun_ss 1)
]);
-val antisym_less_cprod = prove_goal Cprod1.thy
+qed_goal "antisym_less_cprod" Cprod1.thy
"[|less_cprod(p1,p2);less_cprod(p2,p1)|] ==> p1=p2"
(fn prems =>
[
@@ -91,7 +91,7 @@
]);
-val trans_less_cprod = prove_goal Cprod1.thy
+qed_goal "trans_less_cprod" Cprod1.thy
"[|less_cprod(p1,p2);less_cprod(p2,p3)|] ==> less_cprod(p1,p3)"
(fn prems =>
[
--- a/src/HOLCF/Cprod2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cprod2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -8,7 +8,7 @@
open Cprod2;
-val less_cprod3a = prove_goal Cprod2.thy
+qed_goal "less_cprod3a" Cprod2.thy
"p1=<UU,UU> ==> p1 << p2"
(fn prems =>
[
@@ -22,7 +22,7 @@
(rtac minimal 1)
]);
-val less_cprod3b = prove_goal Cprod2.thy
+qed_goal "less_cprod3b" Cprod2.thy
"(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
(fn prems =>
[
@@ -30,7 +30,7 @@
(rtac less_cprod1b 1)
]);
-val less_cprod4a = prove_goal Cprod2.thy
+qed_goal "less_cprod4a" Cprod2.thy
"<x1,x2> << <UU,UU> ==> x1=UU & x2=UU"
(fn prems =>
[
@@ -39,7 +39,7 @@
(etac (inst_cprod_po RS subst) 1)
]);
-val less_cprod4b = prove_goal Cprod2.thy
+qed_goal "less_cprod4b" Cprod2.thy
"p << <UU,UU> ==> p = <UU,UU>"
(fn prems =>
[
@@ -48,7 +48,7 @@
(etac (inst_cprod_po RS subst) 1)
]);
-val less_cprod4c = prove_goal Cprod2.thy
+qed_goal "less_cprod4c" Cprod2.thy
" <xa,ya> << <x,y> ==> xa<<x & ya << y"
(fn prems =>
[
@@ -62,7 +62,7 @@
(* type cprod is pointed *)
(* ------------------------------------------------------------------------ *)
-val minimal_cprod = prove_goal Cprod2.thy "<UU,UU><<p"
+qed_goal "minimal_cprod" Cprod2.thy "<UU,UU><<p"
(fn prems =>
[
(rtac less_cprod3a 1),
@@ -73,7 +73,7 @@
(* Pair <_,_> is monotone in both arguments *)
(* ------------------------------------------------------------------------ *)
-val monofun_pair1 = prove_goalw Cprod2.thy [monofun] "monofun(Pair)"
+qed_goalw "monofun_pair1" Cprod2.thy [monofun] "monofun(Pair)"
(fn prems =>
[
(strip_tac 1),
@@ -84,7 +84,7 @@
(asm_simp_tac Cfun_ss 1)
]);
-val monofun_pair2 = prove_goalw Cprod2.thy [monofun] "monofun(Pair(x))"
+qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
(fn prems =>
[
(strip_tac 1),
@@ -93,7 +93,7 @@
(asm_simp_tac Cfun_ss 1)
]);
-val monofun_pair = prove_goal Cprod2.thy
+qed_goal "monofun_pair" Cprod2.thy
"[|x1<<x2; y1<<y2|] ==> <x1,y1> << <x2,y2>"
(fn prems =>
[
@@ -110,7 +110,7 @@
(* fst and snd are monotone *)
(* ------------------------------------------------------------------------ *)
-val monofun_fst = prove_goalw Cprod2.thy [monofun] "monofun(fst)"
+qed_goalw "monofun_fst" Cprod2.thy [monofun] "monofun(fst)"
(fn prems =>
[
(strip_tac 1),
@@ -122,7 +122,7 @@
(etac (less_cprod4c RS conjunct1) 1)
]);
-val monofun_snd = prove_goalw Cprod2.thy [monofun] "monofun(snd)"
+qed_goalw "monofun_snd" Cprod2.thy [monofun] "monofun(snd)"
(fn prems =>
[
(strip_tac 1),
@@ -138,7 +138,7 @@
(* the type 'a * 'b is a cpo *)
(* ------------------------------------------------------------------------ *)
-val lub_cprod = prove_goal Cprod2.thy
+qed_goal "lub_cprod" Cprod2.thy
" is_chain(S) ==> range(S) <<| \
\ < lub(range(%i.fst(S(i)))),lub(range(%i.snd(S(i))))> "
(fn prems =>
@@ -170,7 +170,7 @@
(* <lub(range(%i. fst(?S1(i)))), lub(range(%i. snd(?S1(i))))>" *)
-val cpo_cprod = prove_goal Cprod2.thy
+qed_goal "cpo_cprod" Cprod2.thy
"is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
(fn prems =>
[
--- a/src/HOLCF/Cprod3.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cprod3.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* continuity of <_,_> , fst, snd *)
(* ------------------------------------------------------------------------ *)
-val Cprod3_lemma1 = prove_goal Cprod3.thy
+qed_goal "Cprod3_lemma1" Cprod3.thy
"is_chain(Y::(nat=>'a)) ==>\
\ <lub(range(Y)),(x::'b)> =\
\ <lub(range(%i. fst(<Y(i),x>))),lub(range(%i. snd(<Y(i),x>)))>"
@@ -33,7 +33,7 @@
(rtac (lub_const RS thelubI) 1)
]);
-val contlub_pair1 = prove_goal Cprod3.thy "contlub(Pair)"
+qed_goal "contlub_pair1" Cprod3.thy "contlub(Pair)"
(fn prems =>
[
(rtac contlubI 1),
@@ -49,7 +49,7 @@
(etac Cprod3_lemma1 1)
]);
-val Cprod3_lemma2 = prove_goal Cprod3.thy
+qed_goal "Cprod3_lemma2" Cprod3.thy
"is_chain(Y::(nat=>'a)) ==>\
\ <(x::'b),lub(range(Y))> =\
\ <lub(range(%i. fst(<x,Y(i)>))),lub(range(%i. snd(<x,Y(i)>)))>"
@@ -69,7 +69,7 @@
(simp_tac pair_ss 1)
]);
-val contlub_pair2 = prove_goal Cprod3.thy "contlub(Pair(x))"
+qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))"
(fn prems =>
[
(rtac contlubI 1),
@@ -80,7 +80,7 @@
(etac Cprod3_lemma2 1)
]);
-val contX_pair1 = prove_goal Cprod3.thy "contX(Pair)"
+qed_goal "contX_pair1" Cprod3.thy "contX(Pair)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -88,7 +88,7 @@
(rtac contlub_pair1 1)
]);
-val contX_pair2 = prove_goal Cprod3.thy "contX(Pair(x))"
+qed_goal "contX_pair2" Cprod3.thy "contX(Pair(x))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -96,7 +96,7 @@
(rtac contlub_pair2 1)
]);
-val contlub_fst = prove_goal Cprod3.thy "contlub(fst)"
+qed_goal "contlub_fst" Cprod3.thy "contlub(fst)"
(fn prems =>
[
(rtac contlubI 1),
@@ -106,7 +106,7 @@
(simp_tac pair_ss 1)
]);
-val contlub_snd = prove_goal Cprod3.thy "contlub(snd)"
+qed_goal "contlub_snd" Cprod3.thy "contlub(snd)"
(fn prems =>
[
(rtac contlubI 1),
@@ -116,7 +116,7 @@
(simp_tac pair_ss 1)
]);
-val contX_fst = prove_goal Cprod3.thy "contX(fst)"
+qed_goal "contX_fst" Cprod3.thy "contX(fst)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -124,7 +124,7 @@
(rtac contlub_fst 1)
]);
-val contX_snd = prove_goal Cprod3.thy "contX(snd)"
+qed_goal "contX_snd" Cprod3.thy "contX(snd)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -143,7 +143,7 @@
(* convert all lemmas to the continuous versions *)
(* ------------------------------------------------------------------------ *)
-val beta_cfun_cprod = prove_goalw Cprod3.thy [cpair_def]
+qed_goalw "beta_cfun_cprod" Cprod3.thy [cpair_def]
"(LAM x y.<x,y>)[a][b] = <a,b>"
(fn prems =>
[
@@ -157,7 +157,7 @@
(rtac refl 1)
]);
-val inject_cpair = prove_goalw Cprod3.thy [cpair_def]
+qed_goalw "inject_cpair" Cprod3.thy [cpair_def]
" (a#b)=(aa#ba) ==> a=aa & b=ba"
(fn prems =>
[
@@ -168,7 +168,7 @@
(fast_tac HOL_cs 1)
]);
-val inst_cprod_pcpo2 = prove_goalw Cprod3.thy [cpair_def] "UU = (UU#UU)"
+qed_goalw "inst_cprod_pcpo2" Cprod3.thy [cpair_def] "UU = (UU#UU)"
(fn prems =>
[
(rtac sym 1),
@@ -178,7 +178,7 @@
(rtac inst_cprod_pcpo 1)
]);
-val defined_cpair_rev = prove_goal Cprod3.thy
+qed_goal "defined_cpair_rev" Cprod3.thy
"(a#b) = UU ==> a = UU & b = UU"
(fn prems =>
[
@@ -187,7 +187,7 @@
(etac inject_cpair 1)
]);
-val Exh_Cprod2 = prove_goalw Cprod3.thy [cpair_def]
+qed_goalw "Exh_Cprod2" Cprod3.thy [cpair_def]
"? a b. z=(a#b) "
(fn prems =>
[
@@ -197,7 +197,7 @@
(etac (beta_cfun_cprod RS ssubst) 1)
]);
-val cprodE = prove_goalw Cprod3.thy [cpair_def]
+qed_goalw "cprodE" Cprod3.thy [cpair_def]
"[|!!x y. [|p=(x#y) |] ==> Q|] ==> Q"
(fn prems =>
[
@@ -206,7 +206,7 @@
(etac (beta_cfun_cprod RS ssubst) 1)
]);
-val cfst2 = prove_goalw Cprod3.thy [cfst_def,cpair_def]
+qed_goalw "cfst2" Cprod3.thy [cfst_def,cpair_def]
"cfst[x#y]=x"
(fn prems =>
[
@@ -217,7 +217,7 @@
(simp_tac pair_ss 1)
]);
-val csnd2 = prove_goalw Cprod3.thy [csnd_def,cpair_def]
+qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def]
"csnd[x#y]=y"
(fn prems =>
[
@@ -228,7 +228,7 @@
(simp_tac pair_ss 1)
]);
-val surjective_pairing_Cprod2 = prove_goalw Cprod3.thy
+qed_goalw "surjective_pairing_Cprod2" Cprod3.thy
[cfst_def,csnd_def,cpair_def] "(cfst[p] # csnd[p]) = p"
(fn prems =>
[
@@ -241,7 +241,7 @@
]);
-val less_cprod5b = prove_goalw Cprod3.thy [cfst_def,csnd_def,cpair_def]
+qed_goalw "less_cprod5b" Cprod3.thy [cfst_def,csnd_def,cpair_def]
" (p1 << p2) = (cfst[p1]<<cfst[p2] & csnd[p1]<<csnd[p2])"
(fn prems =>
[
@@ -256,7 +256,7 @@
(rtac less_cprod3b 1)
]);
-val less_cprod5c = prove_goalw Cprod3.thy [cfst_def,csnd_def,cpair_def]
+qed_goalw "less_cprod5c" Cprod3.thy [cfst_def,csnd_def,cpair_def]
"xa#ya << x#y ==>xa<<x & ya << y"
(fn prems =>
[
@@ -268,7 +268,7 @@
]);
-val lub_cprod2 = prove_goalw Cprod3.thy [cfst_def,csnd_def,cpair_def]
+qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
"[|is_chain(S)|] ==> range(S) <<| \
\ (lub(range(%i.cfst[S(i)])) # lub(range(%i.csnd[S(i)])))"
(fn prems =>
@@ -287,7 +287,7 @@
(* "is_chain(?S1) ==> lub(range(?S1)) = *)
(* lub(range(%i. cfst[?S1(i)]))#lub(range(%i. csnd[?S1(i)]))" *)
-val csplit2 = prove_goalw Cprod3.thy [csplit_def]
+qed_goalw "csplit2" Cprod3.thy [csplit_def]
"csplit[f][x#y]=f[x][y]"
(fn prems =>
[
@@ -297,7 +297,7 @@
(simp_tac (Cfun_ss addsimps [cfst2,csnd2]) 1)
]);
-val csplit3 = prove_goalw Cprod3.thy [csplit_def]
+qed_goalw "csplit3" Cprod3.thy [csplit_def]
"csplit[cpair][z]=z"
(fn prems =>
[
--- a/src/HOLCF/Dlist.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Dlist.ML Tue Feb 07 11:59:32 1995 +0100
@@ -63,7 +63,7 @@
(* Exhaustion and elimination for dlists *)
(* ------------------------------------------------------------------------*)
-val Exh_dlist = prove_goalw Dlist.thy [dcons_def,dnil_def]
+qed_goalw "Exh_dlist" Dlist.thy [dcons_def,dnil_def]
"l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons[x][xl])"
(fn prems =>
[
@@ -88,7 +88,7 @@
]);
-val dlistE = prove_goal Dlist.thy
+qed_goal "dlistE" Dlist.thy
"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons[x][xl];x~=UU;xl~=UU|]==>Q|]==>Q"
(fn prems =>
[
@@ -340,7 +340,7 @@
(* enhance the simplifier *)
(* ------------------------------------------------------------------------*)
-val dhd2 = prove_goal Dlist.thy "xl~=UU ==> dhd[dcons[x][xl]]=x"
+qed_goal "dhd2" Dlist.thy "xl~=UU ==> dhd[dcons[x][xl]]=x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -349,7 +349,7 @@
(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
]);
-val dtl2 = prove_goal Dlist.thy "x~=UU ==> dtl[dcons[x][xl]]=xl"
+qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl[dcons[x][xl]]=xl"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -446,7 +446,7 @@
(* Co -induction for dlists *)
(* ------------------------------------------------------------------------*)
-val dlist_coind_lemma = prove_goalw Dlist.thy [dlist_bisim_def]
+qed_goalw "dlist_coind_lemma" Dlist.thy [dlist_bisim_def]
"dlist_bisim(R) ==> ! p q.R(p,q) --> dlist_take(n)[p]=dlist_take(n)[q]"
(fn prems =>
[
@@ -468,7 +468,7 @@
(fast_tac HOL_cs 1)
]);
-val dlist_coind = prove_goal Dlist.thy "[|dlist_bisim(R);R(p,q)|] ==> p = q"
+qed_goal "dlist_coind" Dlist.thy "[|dlist_bisim(R);R(p,q)|] ==> p = q"
(fn prems =>
[
(rtac dlist_take_lemma 1),
@@ -481,7 +481,7 @@
(* structural induction *)
(* ------------------------------------------------------------------------*)
-val dlist_finite_ind = prove_goal Dlist.thy
+qed_goal "dlist_finite_ind" Dlist.thy
"[|P(UU);P(dnil);\
\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])\
\ |] ==> !l.P(dlist_take(n)[l])"
@@ -506,7 +506,7 @@
(etac spec 1)
]);
-val dlist_all_finite_lemma1 = prove_goal Dlist.thy
+qed_goal "dlist_all_finite_lemma1" Dlist.thy
"!l.dlist_take(n)[l]=UU |dlist_take(n)[l]=l"
(fn prems =>
[
@@ -523,7 +523,7 @@
(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
]);
-val dlist_all_finite_lemma2 = prove_goal Dlist.thy "? n.dlist_take(n)[l]=l"
+qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take(n)[l]=l"
(fn prems =>
[
(res_inst_tac [("Q","l=UU")] classical2 1),
@@ -540,13 +540,13 @@
(rtac dlist_all_finite_lemma1 1)
]);
-val dlist_all_finite= prove_goalw Dlist.thy [dlist_finite_def] "dlist_finite(l)"
+qed_goalw "dlist_all_finite" Dlist.thy [dlist_finite_def] "dlist_finite(l)"
(fn prems =>
[
(rtac dlist_all_finite_lemma2 1)
]);
-val dlist_ind = prove_goal Dlist.thy
+qed_goal "dlist_ind" Dlist.thy
"[|P(UU);P(dnil);\
\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons[x][l1])|] ==> P(l)"
(fn prems =>
--- a/src/HOLCF/Dnat.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Dnat.ML Tue Feb 07 11:59:32 1995 +0100
@@ -44,7 +44,7 @@
(* Exhaustion and elimination for dnat *)
(* ------------------------------------------------------------------------*)
-val Exh_dnat = prove_goalw Dnat.thy [dsucc_def,dzero_def]
+qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def]
"n = UU | n = dzero | (? x . x~=UU & n = dsucc[x])"
(fn prems =>
[
@@ -63,7 +63,7 @@
(fast_tac HOL_cs 1)
]);
-val dnatE = prove_goal Dnat.thy
+qed_goal "dnatE" Dnat.thy
"[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc[x];x~=UU|]==>Q|]==>Q"
(fn prems =>
[
@@ -359,7 +359,7 @@
(* Co -induction for dnats *)
(* ------------------------------------------------------------------------*)
-val dnat_coind_lemma = prove_goalw Dnat.thy [dnat_bisim_def]
+qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def]
"dnat_bisim(R) ==> ! p q.R(p,q) --> dnat_take(n)[p]=dnat_take(n)[q]"
(fn prems =>
[
@@ -380,7 +380,7 @@
(fast_tac HOL_cs 1)
]);
-val dnat_coind = prove_goal Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q"
+qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q"
(fn prems =>
[
(rtac dnat_take_lemma 1),
@@ -395,7 +395,7 @@
(* ------------------------------------------------------------------------*)
(* not needed any longer
-val dnat_ind = prove_goal Dnat.thy
+qed_goal "dnat_ind" Dnat.thy
"[| adm(P);\
\ P(UU);\
\ P(dzero);\
@@ -426,7 +426,7 @@
]);
*)
-val dnat_finite_ind = prove_goal Dnat.thy
+qed_goal "dnat_finite_ind" Dnat.thy
"[|P(UU);P(dzero);\
\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
\ |] ==> !s.P(dnat_take(n)[s])"
@@ -450,7 +450,7 @@
(etac spec 1)
]);
-val dnat_all_finite_lemma1 = prove_goal Dnat.thy
+qed_goal "dnat_all_finite_lemma1" Dnat.thy
"!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
(fn prems =>
[
@@ -467,7 +467,7 @@
(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
]);
-val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
+qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take(n)[s]=s"
(fn prems =>
[
(res_inst_tac [("Q","s=UU")] classical2 1),
@@ -485,7 +485,7 @@
]);
-val dnat_ind = prove_goal Dnat.thy
+qed_goal "dnat_ind" Dnat.thy
"[|P(UU);P(dzero);\
\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
\ |] ==> P(s)"
@@ -499,7 +499,7 @@
]);
-val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
+qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
(fn prems =>
[
(rtac allI 1),
--- a/src/HOLCF/Dnat2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Dnat2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -20,21 +20,21 @@
(* recursive properties *)
(* ------------------------------------------------------------------------- *)
-val iterator1 = prove_goal Dnat2.thy "iterator[UU][f][x] = UU"
+qed_goal "iterator1" Dnat2.thy "iterator[UU][f][x] = UU"
(fn prems =>
[
(rtac (iterator_def2 RS ssubst) 1),
(simp_tac (HOLCF_ss addsimps dnat_when) 1)
]);
-val iterator2 = prove_goal Dnat2.thy "iterator[dzero][f][x] = x"
+qed_goal "iterator2" Dnat2.thy "iterator[dzero][f][x] = x"
(fn prems =>
[
(rtac (iterator_def2 RS ssubst) 1),
(simp_tac (HOLCF_ss addsimps dnat_when) 1)
]);
-val iterator3 = prove_goal Dnat2.thy
+qed_goal "iterator3" Dnat2.thy
"n~=UU ==> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]"
(fn prems =>
[
--- a/src/HOLCF/Fix.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Fix.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,13 +12,13 @@
(* derive inductive properties of iterate from primitive recursion *)
(* ------------------------------------------------------------------------ *)
-val iterate_0 = prove_goal Fix.thy "iterate(0,F,x) = x"
+qed_goal "iterate_0" Fix.thy "iterate(0,F,x) = x"
(fn prems =>
[
(resolve_tac (nat_recs iterate_def) 1)
]);
-val iterate_Suc = prove_goal Fix.thy "iterate(Suc(n),F,x) = F[iterate(n,F,x)]"
+qed_goal "iterate_Suc" Fix.thy "iterate(Suc(n),F,x) = F[iterate(n,F,x)]"
(fn prems =>
[
(resolve_tac (nat_recs iterate_def) 1)
@@ -26,7 +26,7 @@
val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc];
-val iterate_Suc2 = prove_goal Fix.thy "iterate(Suc(n),F,x) = iterate(n,F,F[x])"
+qed_goal "iterate_Suc2" Fix.thy "iterate(Suc(n),F,x) = iterate(n,F,F[x])"
(fn prems =>
[
(nat_ind_tac "n" 1),
@@ -39,7 +39,7 @@
(* This property is essential since monotonicity of iterate makes no sense *)
(* ------------------------------------------------------------------------ *)
-val is_chain_iterate2 = prove_goalw Fix.thy [is_chain]
+qed_goalw "is_chain_iterate2" Fix.thy [is_chain]
" x << F[x] ==> is_chain(%i.iterate(i,F,x))"
(fn prems =>
[
@@ -53,7 +53,7 @@
]);
-val is_chain_iterate = prove_goal Fix.thy
+qed_goal "is_chain_iterate" Fix.thy
"is_chain(%i.iterate(i,F,UU))"
(fn prems =>
[
@@ -68,7 +68,7 @@
(* ------------------------------------------------------------------------ *)
-val Ifix_eq = prove_goalw Fix.thy [Ifix_def] "Ifix(F)=F[Ifix(F)]"
+qed_goalw "Ifix_eq" Fix.thy [Ifix_def] "Ifix(F)=F[Ifix(F)]"
(fn prems =>
[
(rtac (contlub_cfun_arg RS ssubst) 1),
@@ -92,7 +92,7 @@
]);
-val Ifix_least = prove_goalw Fix.thy [Ifix_def] "F[x]=x ==> Ifix(F) << x"
+qed_goalw "Ifix_least" Fix.thy [Ifix_def] "F[x]=x ==> Ifix(F) << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -113,7 +113,7 @@
(* monotonicity and continuity of iterate *)
(* ------------------------------------------------------------------------ *)
-val monofun_iterate = prove_goalw Fix.thy [monofun] "monofun(iterate(i))"
+qed_goalw "monofun_iterate" Fix.thy [monofun] "monofun(iterate(i))"
(fn prems =>
[
(strip_tac 1),
@@ -134,7 +134,7 @@
(* In this special case it is the application function fapp *)
(* ------------------------------------------------------------------------ *)
-val contlub_iterate = prove_goalw Fix.thy [contlub] "contlub(iterate(i))"
+qed_goalw "contlub_iterate" Fix.thy [contlub] "contlub(iterate(i))"
(fn prems =>
[
(strip_tac 1),
@@ -165,7 +165,7 @@
]);
-val contX_iterate = prove_goal Fix.thy "contX(iterate(i))"
+qed_goal "contX_iterate" Fix.thy "contX(iterate(i))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -177,7 +177,7 @@
(* a lemma about continuity of iterate in its third argument *)
(* ------------------------------------------------------------------------ *)
-val monofun_iterate2 = prove_goal Fix.thy "monofun(iterate(n,F))"
+qed_goal "monofun_iterate2" Fix.thy "monofun(iterate(n,F))"
(fn prems =>
[
(rtac monofunI 1),
@@ -188,7 +188,7 @@
(etac monofun_cfun_arg 1)
]);
-val contlub_iterate2 = prove_goal Fix.thy "contlub(iterate(n,F))"
+qed_goal "contlub_iterate2" Fix.thy "contlub(iterate(n,F))"
(fn prems =>
[
(rtac contlubI 1),
@@ -203,7 +203,7 @@
(etac (monofun_iterate2 RS ch2ch_monofun) 1)
]);
-val contX_iterate2 = prove_goal Fix.thy "contX(iterate(n,F))"
+qed_goal "contX_iterate2" Fix.thy "contX(iterate(n,F))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -215,7 +215,7 @@
(* monotonicity and continuity of Ifix *)
(* ------------------------------------------------------------------------ *)
-val monofun_Ifix = prove_goalw Fix.thy [monofun,Ifix_def] "monofun(Ifix)"
+qed_goalw "monofun_Ifix" Fix.thy [monofun,Ifix_def] "monofun(Ifix)"
(fn prems =>
[
(strip_tac 1),
@@ -233,7 +233,7 @@
(* be derived for lubs in this argument *)
(* ------------------------------------------------------------------------ *)
-val is_chain_iterate_lub = prove_goal Fix.thy
+qed_goal "is_chain_iterate_lub" Fix.thy
"is_chain(Y) ==> is_chain(%i. lub(range(%ia. iterate(ia,Y(i),UU))))"
(fn prems =>
[
@@ -254,7 +254,7 @@
(* chains is the essential argument which is usually derived from monot. *)
(* ------------------------------------------------------------------------ *)
-val contlub_Ifix_lemma1 = prove_goal Fix.thy
+qed_goal "contlub_Ifix_lemma1" Fix.thy
"is_chain(Y) ==> iterate(n,lub(range(Y)),y) = lub(range(%i. iterate(n,Y(i),y)))"
(fn prems =>
[
@@ -269,7 +269,7 @@
]);
-val ex_lub_iterate = prove_goal Fix.thy "is_chain(Y) ==>\
+qed_goal "ex_lub_iterate" Fix.thy "is_chain(Y) ==>\
\ lub(range(%i. lub(range(%ia. iterate(i,Y(ia),UU))))) =\
\ lub(range(%i. lub(range(%ia. iterate(ia,Y(i),UU)))))"
(fn prems =>
@@ -303,7 +303,7 @@
]);
-val contlub_Ifix = prove_goalw Fix.thy [contlub,Ifix_def] "contlub(Ifix)"
+qed_goalw "contlub_Ifix" Fix.thy [contlub,Ifix_def] "contlub(Ifix)"
(fn prems =>
[
(strip_tac 1),
@@ -313,7 +313,7 @@
]);
-val contX_Ifix = prove_goal Fix.thy "contX(Ifix)"
+qed_goal "contX_Ifix" Fix.thy "contX(Ifix)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -325,14 +325,14 @@
(* propagate properties of Ifix to its continuous counterpart *)
(* ------------------------------------------------------------------------ *)
-val fix_eq = prove_goalw Fix.thy [fix_def] "fix[F]=F[fix[F]]"
+qed_goalw "fix_eq" Fix.thy [fix_def] "fix[F]=F[fix[F]]"
(fn prems =>
[
(asm_simp_tac (Cfun_ss addsimps [contX_Ifix]) 1),
(rtac Ifix_eq 1)
]);
-val fix_least = prove_goalw Fix.thy [fix_def] "F[x]=x ==> fix[F] << x"
+qed_goalw "fix_least" Fix.thy [fix_def] "F[x]=x ==> fix[F] << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -341,14 +341,14 @@
]);
-val fix_eq2 = prove_goal Fix.thy "f == fix[F] ==> f = F[f]"
+qed_goal "fix_eq2" Fix.thy "f == fix[F] ==> f = F[f]"
(fn prems =>
[
(rewrite_goals_tac prems),
(rtac fix_eq 1)
]);
-val fix_eq3 = prove_goal Fix.thy "f == fix[F] ==> f[x] = F[f][x]"
+qed_goal "fix_eq3" Fix.thy "f == fix[F] ==> f[x] = F[f][x]"
(fn prems =>
[
(rtac trans 1),
@@ -358,7 +358,7 @@
fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i));
-val fix_eq4 = prove_goal Fix.thy "f = fix[F] ==> f = F[f]"
+qed_goal "fix_eq4" Fix.thy "f = fix[F] ==> f = F[f]"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -366,7 +366,7 @@
(rtac fix_eq 1)
]);
-val fix_eq5 = prove_goal Fix.thy "f = fix[F] ==> f[x] = F[f][x]"
+qed_goal "fix_eq5" Fix.thy "f = fix[F] ==> f[x] = F[f][x]"
(fn prems =>
[
(rtac trans 1),
@@ -406,7 +406,7 @@
(* ------------------------------------------------------------------------ *)
-val Ifix_def2 = prove_goal Fix.thy "Ifix=(%x. lub(range(%i. iterate(i,x,UU))))"
+qed_goal "Ifix_def2" Fix.thy "Ifix=(%x. lub(range(%i. iterate(i,x,UU))))"
(fn prems =>
[
(rtac ext 1),
@@ -418,7 +418,7 @@
(* direct connection between fix and iteration without Ifix *)
(* ------------------------------------------------------------------------ *)
-val fix_def2 = prove_goalw Fix.thy [fix_def]
+qed_goalw "fix_def2" Fix.thy [fix_def]
"fix[F] = lub(range(%i. iterate(i,F,UU)))"
(fn prems =>
[
@@ -435,14 +435,14 @@
(* access to definitions *)
(* ------------------------------------------------------------------------ *)
-val adm_def2 = prove_goalw Fix.thy [adm_def]
+qed_goalw "adm_def2" Fix.thy [adm_def]
"adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))"
(fn prems =>
[
(rtac refl 1)
]);
-val admw_def2 = prove_goalw Fix.thy [admw_def]
+qed_goalw "admw_def2" Fix.thy [admw_def]
"admw(P) = (!F.((!n.P(iterate(n,F,UU)))-->\
\ P(lub(range(%i.iterate(i,F,UU))))))"
(fn prems =>
@@ -454,7 +454,7 @@
(* an admissible formula is also weak admissible *)
(* ------------------------------------------------------------------------ *)
-val adm_impl_admw = prove_goalw Fix.thy [admw_def] "adm(P)==>admw(P)"
+qed_goalw "adm_impl_admw" Fix.thy [admw_def] "adm(P)==>admw(P)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -469,7 +469,7 @@
(* fixed point induction *)
(* ------------------------------------------------------------------------ *)
-val fix_ind = prove_goal Fix.thy
+qed_goal "fix_ind" Fix.thy
"[| adm(P);P(UU);!!x. P(x) ==> P(F[x])|] ==> P(fix[F])"
(fn prems =>
[
@@ -491,7 +491,7 @@
(* computational induction for weak admissible formulae *)
(* ------------------------------------------------------------------------ *)
-val wfix_ind = prove_goal Fix.thy
+qed_goal "wfix_ind" Fix.thy
"[| admw(P); !n. P(iterate(n,F,UU))|] ==> P(fix[F])"
(fn prems =>
[
@@ -507,7 +507,7 @@
(* for chain-finite (easy) types every formula is admissible *)
(* ------------------------------------------------------------------------ *)
-val adm_max_in_chain = prove_goalw Fix.thy [adm_def]
+qed_goalw "adm_max_in_chain" Fix.thy [adm_def]
"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y)) ==> adm(P::'a=>bool)"
(fn prems =>
[
@@ -524,7 +524,7 @@
]);
-val adm_chain_finite = prove_goalw Fix.thy [chain_finite_def]
+qed_goalw "adm_chain_finite" Fix.thy [chain_finite_def]
"chain_finite(x::'a) ==> adm(P::'a=>bool)"
(fn prems =>
[
@@ -536,7 +536,7 @@
(* flat types are chain_finite *)
(* ------------------------------------------------------------------------ *)
-val flat_imp_chain_finite = prove_goalw Fix.thy [flat_def,chain_finite_def]
+qed_goalw "flat_imp_chain_finite" Fix.thy [flat_def,chain_finite_def]
"flat(x::'a)==>chain_finite(x::'a)"
(fn prems =>
[
@@ -576,7 +576,7 @@
val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
-val flat_void = prove_goalw Fix.thy [flat_def] "flat(UU::void)"
+qed_goalw "flat_void" Fix.thy [flat_def] "flat(UU::void)"
(fn prems =>
[
(strip_tac 1),
@@ -589,7 +589,7 @@
(* a prove for embedding projection pairs is similar *)
(* ------------------------------------------------------------------------ *)
-val iso_strict = prove_goal Fix.thy
+qed_goal "iso_strict" Fix.thy
"!!f g.[|!y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
\ ==> f[UU]=UU & g[UU]=UU"
(fn prems =>
@@ -606,7 +606,7 @@
]);
-val isorep_defined = prove_goal Fix.thy
+qed_goal "isorep_defined" Fix.thy
"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> rep[z]~=UU"
(fn prems =>
[
@@ -620,7 +620,7 @@
(atac 1)
]);
-val isoabs_defined = prove_goal Fix.thy
+qed_goal "isoabs_defined" Fix.thy
"[|!x.rep[abs[x]]=x;!y.abs[rep[y]]=y;z~=UU|] ==> abs[z]~=UU"
(fn prems =>
[
@@ -638,7 +638,7 @@
(* propagation of flatness and chainfiniteness by continuous isomorphisms *)
(* ------------------------------------------------------------------------ *)
-val chfin2chfin = prove_goalw Fix.thy [chain_finite_def]
+qed_goalw "chfin2chfin" Fix.thy [chain_finite_def]
"!!f g.[|chain_finite(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
\ ==> chain_finite(y::'b)"
(fn prems =>
@@ -661,7 +661,7 @@
(atac 1)
]);
-val flat2flat = prove_goalw Fix.thy [flat_def]
+qed_goalw "flat2flat" Fix.thy [flat_def]
"!!f g.[|flat(x::'a); !y.f[g[y]]=(y::'b) ; !x.g[f[x]]=(x::'a) |] \
\ ==> flat(y::'b)"
(fn prems =>
@@ -692,7 +692,7 @@
(* a result about functions with flat codomain *)
(* ------------------------------------------------------------------------- *)
-val flat_codom = prove_goalw Fix.thy [flat_def]
+qed_goalw "flat_codom" Fix.thy [flat_def]
"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
(fn prems =>
[
@@ -729,7 +729,7 @@
(* admissibility of special formulae and propagation *)
(* ------------------------------------------------------------------------ *)
-val adm_less = prove_goalw Fix.thy [adm_def]
+qed_goalw "adm_less" Fix.thy [adm_def]
"[|contX(u);contX(v)|]==> adm(%x.u(x)<<v(x))"
(fn prems =>
[
@@ -749,7 +749,7 @@
(atac 1)
]);
-val adm_conj = prove_goal Fix.thy
+qed_goal "adm_conj" Fix.thy
"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
(fn prems =>
[
@@ -767,7 +767,7 @@
(fast_tac HOL_cs 1)
]);
-val adm_cong = prove_goal Fix.thy
+qed_goal "adm_cong" Fix.thy
"(!x. P(x) = Q(x)) ==> adm(P)=adm(Q)"
(fn prems =>
[
@@ -778,13 +778,13 @@
(etac spec 1)
]);
-val adm_not_free = prove_goalw Fix.thy [adm_def] "adm(%x.t)"
+qed_goalw "adm_not_free" Fix.thy [adm_def] "adm(%x.t)"
(fn prems =>
[
(fast_tac HOL_cs 1)
]);
-val adm_not_less = prove_goalw Fix.thy [adm_def]
+qed_goalw "adm_not_less" Fix.thy [adm_def]
"contX(t) ==> adm(%x.~ t(x) << u)"
(fn prems =>
[
@@ -799,7 +799,7 @@
(atac 1)
]);
-val adm_all = prove_goal Fix.thy
+qed_goal "adm_all" Fix.thy
" !y.adm(P(y)) ==> adm(%x.!y.P(y,x))"
(fn prems =>
[
@@ -816,7 +816,7 @@
val adm_all2 = (allI RS adm_all);
-val adm_subst = prove_goal Fix.thy
+qed_goal "adm_subst" Fix.thy
"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
(fn prems =>
[
@@ -834,7 +834,7 @@
(atac 1)
]);
-val adm_UU_not_less = prove_goal Fix.thy "adm(%x.~ UU << t(x))"
+qed_goal "adm_UU_not_less" Fix.thy "adm(%x.~ UU << t(x))"
(fn prems =>
[
(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
@@ -842,7 +842,7 @@
(rtac adm_not_free 1)
]);
-val adm_not_UU = prove_goalw Fix.thy [adm_def]
+qed_goalw "adm_not_UU" Fix.thy [adm_def]
"contX(t)==> adm(%x.~ t(x) = UU)"
(fn prems =>
[
@@ -860,7 +860,7 @@
(atac 1)
]);
-val adm_eq = prove_goal Fix.thy
+qed_goal "adm_eq" Fix.thy
"[|contX(u);contX(v)|]==> adm(%x.u(x)= v(x))"
(fn prems =>
[
@@ -886,7 +886,7 @@
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas *)
(* ------------------------------------------------------------------------ *)
-val adm_disj_lemma1 = prove_goal Pcpo.thy
+qed_goal "adm_disj_lemma1" Pcpo.thy
"[| is_chain(Y); !n.P(Y(n))|Q(Y(n))|]\
\ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
(fn prems =>
@@ -895,7 +895,7 @@
(fast_tac HOL_cs 1)
]);
-val adm_disj_lemma2 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma2" Fix.thy
"[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
(fn prems =>
@@ -912,7 +912,7 @@
(atac 1)
]);
-val adm_disj_lemma3 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma3" Fix.thy
"[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
\ is_chain(%m. if(m < Suc(i),Y(Suc(i)),Y(m)))"
(fn prems =>
@@ -944,7 +944,7 @@
(rtac refl_less 1)
]);
-val adm_disj_lemma4 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma4" Fix.thy
"[| ! j. i < j --> Q(Y(j)) |] ==>\
\ ! n. Q(if(n < Suc(i),Y(Suc(i)),Y(n)))"
(fn prems =>
@@ -982,7 +982,7 @@
(etac Suc_lessD 1)
]);
-val adm_disj_lemma5 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma5" Fix.thy
"[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. if(m < Suc(i),Y(Suc(i)),Y(m))))"
(fn prems =>
@@ -1006,7 +1006,7 @@
(rtac refl 1)
]);
-val adm_disj_lemma6 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma6" Fix.thy
"[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
\ ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
(fn prems =>
@@ -1027,7 +1027,7 @@
]);
-val adm_disj_lemma7 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma7" Fix.thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ is_chain(%m. Y(theleast(%j. m<j & P(Y(j)))))"
(fn prems =>
@@ -1050,7 +1050,7 @@
(atac 1)
]);
-val adm_disj_lemma8 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma8" Fix.thy
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(theleast(%j. m<j & P(Y(j)))))"
(fn prems =>
[
@@ -1061,7 +1061,7 @@
(etac (theleast1 RS conjunct2) 1)
]);
-val adm_disj_lemma9 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma9" Fix.thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. Y(theleast(%j. m<j & P(Y(j))))))"
(fn prems =>
@@ -1092,7 +1092,7 @@
(rtac lessI 1)
]);
-val adm_disj_lemma10 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma10" Fix.thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
(fn prems =>
@@ -1112,7 +1112,7 @@
]);
-val adm_disj_lemma11 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma11" Fix.thy
"[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
(fn prems =>
[
@@ -1122,7 +1122,7 @@
(atac 1)
]);
-val adm_disj_lemma12 = prove_goal Fix.thy
+qed_goal "adm_disj_lemma12" Fix.thy
"[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
(fn prems =>
[
@@ -1132,7 +1132,7 @@
(atac 1)
]);
-val adm_disj = prove_goal Fix.thy
+qed_goal "adm_disj" Fix.thy
"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
(fn prems =>
[
@@ -1153,7 +1153,7 @@
]);
-val adm_impl = prove_goal Fix.thy
+qed_goal "adm_impl" Fix.thy
"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
(fn prems =>
[
--- a/src/HOLCF/Fun1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Fun1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,13 +12,13 @@
(* less_fun is a partial order on 'a => 'b *)
(* ------------------------------------------------------------------------ *)
-val refl_less_fun = prove_goalw Fun1.thy [less_fun_def] "less_fun(f,f)"
+qed_goalw "refl_less_fun" Fun1.thy [less_fun_def] "less_fun(f,f)"
(fn prems =>
[
(fast_tac (HOL_cs addSIs [refl_less]) 1)
]);
-val antisym_less_fun = prove_goalw Fun1.thy [less_fun_def]
+qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def]
"[|less_fun(f1,f2); less_fun(f2,f1)|] ==> f1 = f2"
(fn prems =>
[
@@ -27,7 +27,7 @@
(fast_tac (HOL_cs addSIs [antisym_less]) 1)
]);
-val trans_less_fun = prove_goalw Fun1.thy [less_fun_def]
+qed_goalw "trans_less_fun" Fun1.thy [less_fun_def]
"[|less_fun(f1,f2); less_fun(f2,f3)|] ==> less_fun(f1,f3)"
(fn prems =>
[
--- a/src/HOLCF/Fun2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Fun2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* Type 'a::term => 'b::pcpo is pointed *)
(* ------------------------------------------------------------------------ *)
-val minimal_fun = prove_goalw Fun2.thy [UU_fun_def] "UU_fun << f"
+qed_goalw "minimal_fun" Fun2.thy [UU_fun_def] "UU_fun << f"
(fn prems =>
[
(rtac (inst_fun_po RS ssubst) 1),
@@ -24,7 +24,7 @@
(* make the symbol << accessible for type fun *)
(* ------------------------------------------------------------------------ *)
-val less_fun = prove_goal Fun2.thy "(f1 << f2) = (! x. f1(x) << f2(x))"
+qed_goal "less_fun" Fun2.thy "(f1 << f2) = (! x. f1(x) << f2(x))"
(fn prems =>
[
(rtac (inst_fun_po RS ssubst) 1),
@@ -36,7 +36,7 @@
(* chains of functions yield chains in the po range *)
(* ------------------------------------------------------------------------ *)
-val ch2ch_fun = prove_goal Fun2.thy
+qed_goal "ch2ch_fun" Fun2.thy
"is_chain(S::nat=>('a::term => 'b::po)) ==> is_chain(% i.S(i)(x))"
(fn prems =>
[
@@ -53,7 +53,7 @@
(* upper bounds of function chains yield upper bound in the po range *)
(* ------------------------------------------------------------------------ *)
-val ub2ub_fun = prove_goal Fun2.thy
+qed_goal "ub2ub_fun" Fun2.thy
" range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S(i,x)) <| u(x)"
(fn prems =>
[
@@ -70,7 +70,7 @@
(* Type 'a::term => 'b::pcpo is chain complete *)
(* ------------------------------------------------------------------------ *)
-val lub_fun = prove_goal Fun2.thy
+qed_goal "lub_fun" Fun2.thy
"is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \
\ range(S) <<| (% x.lub(range(% i.S(i)(x))))"
(fn prems =>
@@ -95,7 +95,7 @@
val thelub_fun = (lub_fun RS thelubI);
(* is_chain(?S1) ==> lub(range(?S1)) = (%x. lub(range(%i. ?S1(i,x)))) *)
-val cpo_fun = prove_goal Fun2.thy
+qed_goal "cpo_fun" Fun2.thy
"is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x"
(fn prems =>
[
--- a/src/HOLCF/Holcfb.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Holcfb.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* <::nat=>nat=>bool is a well-ordering *)
(* ------------------------------------------------------------------------ *)
-val well_ordering_nat = prove_goal Nat.thy
+qed_goal "well_ordering_nat" Nat.thy
"!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
(fn prems =>
[
@@ -40,7 +40,7 @@
(* Lemmas for selecting the least element in a nonempty set *)
(* ------------------------------------------------------------------------ *)
-val theleast = prove_goalw Holcfb.thy [theleast_def]
+qed_goalw "theleast" Holcfb.thy [theleast_def]
"P(x) ==> P(theleast(P)) & (!x.P(x)--> theleast(P) <= x)"
(fn prems =>
[
@@ -54,7 +54,7 @@
val theleast1= theleast RS conjunct1;
(* ?P1(?x1) ==> ?P1(theleast(?P1)) *)
-val theleast2 = prove_goal Holcfb.thy "P(x) ==> theleast(P) <= x"
+qed_goal "theleast2" Holcfb.thy "P(x) ==> theleast(P) <= x"
(fn prems =>
[
(rtac (theleast RS conjunct2 RS spec RS mp) 1),
@@ -68,7 +68,7 @@
(* ------------------------------------------------------------------------ *)
-val de_morgan1 = prove_goal HOL.thy "(~a & ~b)=(~(a | b))"
+qed_goal "de_morgan1" HOL.thy "(~a & ~b)=(~(a | b))"
(fn prems =>
[
(rtac iffI 1),
@@ -76,7 +76,7 @@
(fast_tac HOL_cs 1)
]);
-val de_morgan2 = prove_goal HOL.thy "(~a | ~b)=(~(a & b))"
+qed_goal "de_morgan2" HOL.thy "(~a | ~b)=(~(a & b))"
(fn prems =>
[
(rtac iffI 1),
@@ -85,7 +85,7 @@
]);
-val notall2ex = prove_goal HOL.thy "(~ (!x.P(x))) = (? x.~P(x))"
+qed_goal "notall2ex" HOL.thy "(~ (!x.P(x))) = (? x.~P(x))"
(fn prems =>
[
(rtac iffI 1),
@@ -93,7 +93,7 @@
(fast_tac HOL_cs 1)
]);
-val notex2all = prove_goal HOL.thy "(~ (? x.P(x))) = (!x.~P(x))"
+qed_goal "notex2all" HOL.thy "(~ (? x.P(x))) = (!x.~P(x))"
(fn prems =>
[
(rtac iffI 1),
@@ -102,7 +102,7 @@
]);
-val selectI2 = prove_goal HOL.thy "(? x. P(x)) ==> P(@ x.P(x))"
+qed_goal "selectI3" HOL.thy "(? x. P(x)) ==> P(@ x.P(x))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -110,25 +110,25 @@
(etac selectI 1)
]);
-val selectE = prove_goal HOL.thy "P(@ x.P(x)) ==> (? x. P(x))"
+qed_goal "selectE" HOL.thy "P(@ x.P(x)) ==> (? x. P(x))"
(fn prems =>
[
(cut_facts_tac prems 1),
(etac exI 1)
]);
-val select_eq_Ex = prove_goal HOL.thy "(P(@ x.P(x))) = (? x. P(x))"
+qed_goal "select_eq_Ex" HOL.thy "(P(@ x.P(x))) = (? x. P(x))"
(fn prems =>
[
(rtac (iff RS mp RS mp) 1),
(strip_tac 1),
(etac selectE 1),
(strip_tac 1),
- (etac selectI2 1)
+ (etac selectI3 1)
]);
-val notnotI = prove_goal HOL.thy "P ==> ~~P"
+qed_goal "notnotI" HOL.thy "P ==> ~~P"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -136,7 +136,7 @@
]);
-val classical2 = prove_goal HOL.thy "[|Q ==> R; ~Q ==> R|]==>R"
+qed_goal "classical2" HOL.thy "[|Q ==> R; ~Q ==> R|]==>R"
(fn prems =>
[
(rtac disjE 1),
@@ -151,7 +151,7 @@
(* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
-val nat_less_cases = prove_goal Nat.thy
+qed_goal "nat_less_cases" Nat.thy
"[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
( fn prems =>
[
--- a/src/HOLCF/Lift1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Lift1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -6,7 +6,7 @@
open Lift1;
-val Exh_Lift = prove_goalw Lift1.thy [UU_lift_def,Iup_def ]
+qed_goalw "Exh_Lift" Lift1.thy [UU_lift_def,Iup_def ]
"z = UU_lift | (? x. z = Iup(x))"
(fn prems =>
[
@@ -22,21 +22,21 @@
(atac 1)
]);
-val inj_Abs_Lift = prove_goal Lift1.thy "inj(Abs_Lift)"
+qed_goal "inj_Abs_Lift" Lift1.thy "inj(Abs_Lift)"
(fn prems =>
[
(rtac inj_inverseI 1),
(rtac Abs_Lift_inverse 1)
]);
-val inj_Rep_Lift = prove_goal Lift1.thy "inj(Rep_Lift)"
+qed_goal "inj_Rep_Lift" Lift1.thy "inj(Rep_Lift)"
(fn prems =>
[
(rtac inj_inverseI 1),
(rtac Rep_Lift_inverse 1)
]);
-val inject_Iup = prove_goalw Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
+qed_goalw "inject_Iup" Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -45,7 +45,7 @@
(atac 1)
]);
-val defined_Iup=prove_goalw Lift1.thy [Iup_def,UU_lift_def] "~ Iup(x)=UU_lift"
+qed_goalw "defined_Iup" Lift1.thy [Iup_def,UU_lift_def] "~ Iup(x)=UU_lift"
(fn prems =>
[
(rtac notI 1),
@@ -56,7 +56,7 @@
]);
-val liftE = prove_goal Lift1.thy
+qed_goal "liftE" Lift1.thy
"[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
(fn prems =>
[
@@ -66,7 +66,7 @@
(eresolve_tac prems 1)
]);
-val Ilift1 = prove_goalw Lift1.thy [Ilift_def,UU_lift_def]
+qed_goalw "Ilift1" Lift1.thy [Ilift_def,UU_lift_def]
"Ilift(f)(UU_lift)=UU"
(fn prems =>
[
@@ -75,7 +75,7 @@
(rtac refl 1)
]);
-val Ilift2 = prove_goalw Lift1.thy [Ilift_def,Iup_def]
+qed_goalw "Ilift2" Lift1.thy [Ilift_def,Iup_def]
"Ilift(f)(Iup(x))=f[x]"
(fn prems =>
[
@@ -86,7 +86,7 @@
val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2];
-val less_lift1a = prove_goalw Lift1.thy [less_lift_def,UU_lift_def]
+qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def]
"less_lift(UU_lift)(z)"
(fn prems =>
[
@@ -95,7 +95,7 @@
(rtac TrueI 1)
]);
-val less_lift1b = prove_goalw Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
+qed_goalw "less_lift1b" Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
"~less_lift(Iup(x),UU_lift)"
(fn prems =>
[
@@ -109,7 +109,7 @@
(rtac refl 1)
]);
-val less_lift1c = prove_goalw Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
+qed_goalw "less_lift1c" Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
"less_lift(Iup(x),Iup(y))=(x<<y)"
(fn prems =>
[
@@ -121,7 +121,7 @@
]);
-val refl_less_lift = prove_goal Lift1.thy "less_lift(p,p)"
+qed_goal "refl_less_lift" Lift1.thy "less_lift(p,p)"
(fn prems =>
[
(res_inst_tac [("p","p")] liftE 1),
@@ -132,7 +132,7 @@
(rtac refl_less 1)
]);
-val antisym_less_lift = prove_goal Lift1.thy
+qed_goal "antisym_less_lift" Lift1.thy
"[|less_lift(p1,p2);less_lift(p2,p1)|] ==> p1=p2"
(fn prems =>
[
@@ -159,7 +159,7 @@
(etac (less_lift1c RS iffD1) 1)
]);
-val trans_less_lift = prove_goal Lift1.thy
+qed_goal "trans_less_lift" Lift1.thy
"[|less_lift(p1,p2);less_lift(p2,p3)|] ==> less_lift(p1,p3)"
(fn prems =>
[
--- a/src/HOLCF/Lift2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Lift2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* type ('a)u is pointed *)
(* ------------------------------------------------------------------------ *)
-val minimal_lift = prove_goal Lift2.thy "UU_lift << z"
+qed_goal "minimal_lift" Lift2.thy "UU_lift << z"
(fn prems =>
[
(rtac (inst_lift_po RS ssubst) 1),
@@ -23,14 +23,14 @@
(* access to less_lift in class po *)
(* ------------------------------------------------------------------------ *)
-val less_lift2b = prove_goal Lift2.thy "~ Iup(x) << UU_lift"
+qed_goal "less_lift2b" Lift2.thy "~ Iup(x) << UU_lift"
(fn prems =>
[
(rtac (inst_lift_po RS ssubst) 1),
(rtac less_lift1b 1)
]);
-val less_lift2c = prove_goal Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
+qed_goal "less_lift2c" Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
(rtac (inst_lift_po RS ssubst) 1),
@@ -41,14 +41,14 @@
(* Iup and Ilift are monotone *)
(* ------------------------------------------------------------------------ *)
-val monofun_Iup = prove_goalw Lift2.thy [monofun] "monofun(Iup)"
+qed_goalw "monofun_Iup" Lift2.thy [monofun] "monofun(Iup)"
(fn prems =>
[
(strip_tac 1),
(etac (less_lift2c RS iffD2) 1)
]);
-val monofun_Ilift1 = prove_goalw Lift2.thy [monofun] "monofun(Ilift)"
+qed_goalw "monofun_Ilift1" Lift2.thy [monofun] "monofun(Ilift)"
(fn prems =>
[
(strip_tac 1),
@@ -60,7 +60,7 @@
(etac monofun_cfun_fun 1)
]);
-val monofun_Ilift2 = prove_goalw Lift2.thy [monofun] "monofun(Ilift(f))"
+qed_goalw "monofun_Ilift2" Lift2.thy [monofun] "monofun(Ilift(f))"
(fn prems =>
[
(strip_tac 1),
@@ -85,7 +85,7 @@
(* ------------------------------------------------------------------------ *)
-val lift_lemma1 = prove_goal Lift2.thy "z=Iup(x) ==> Iup(Ilift(LAM x.x)(z)) = z"
+qed_goal "lift_lemma1" Lift2.thy "z=Iup(x) ==> Iup(Ilift(LAM x.x)(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -96,7 +96,7 @@
(* ('a)u is a cpo *)
(* ------------------------------------------------------------------------ *)
-val lub_lift1a = prove_goal Lift2.thy
+qed_goal "lub_lift1a" Lift2.thy
"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
\ range(Y) <<| Iup(lub(range(%i.(Ilift (LAM x.x) (Y(i))))))"
(fn prems =>
@@ -133,7 +133,7 @@
(etac (monofun_Ilift2 RS ub2ub_monofun) 1)
]);
-val lub_lift1b = prove_goal Lift2.thy
+qed_goal "lub_lift1b" Lift2.thy
"[|is_chain(Y);!i x.~Y(i)=Iup(x)|] ==>\
\ range(Y) <<| UU_lift"
(fn prems =>
@@ -165,7 +165,7 @@
(* lub(range(?Y1)) = UU_lift *)
-val cpo_lift = prove_goal Lift2.thy
+qed_goal "cpo_lift" Lift2.thy
"is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
(fn prems =>
[
--- a/src/HOLCF/Lift3.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Lift3.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,14 +12,14 @@
(* some lemmas restated for class pcpo *)
(* ------------------------------------------------------------------------ *)
-val less_lift3b = prove_goal Lift3.thy "~ Iup(x) << UU"
+qed_goal "less_lift3b" Lift3.thy "~ Iup(x) << UU"
(fn prems =>
[
(rtac (inst_lift_pcpo RS ssubst) 1),
(rtac less_lift2b 1)
]);
-val defined_Iup2 = prove_goal Lift3.thy "~ Iup(x) = UU"
+qed_goal "defined_Iup2" Lift3.thy "~ Iup(x) = UU"
(fn prems =>
[
(rtac (inst_lift_pcpo RS ssubst) 1),
@@ -30,7 +30,7 @@
(* continuity for Iup *)
(* ------------------------------------------------------------------------ *)
-val contlub_Iup = prove_goal Lift3.thy "contlub(Iup)"
+qed_goal "contlub_Iup" Lift3.thy "contlub(Iup)"
(fn prems =>
[
(rtac contlubI 1),
@@ -47,7 +47,7 @@
(asm_simp_tac Lift_ss 1)
]);
-val contX_Iup = prove_goal Lift3.thy "contX(Iup)"
+qed_goal "contX_Iup" Lift3.thy "contX(Iup)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -60,7 +60,7 @@
(* continuity for Ilift *)
(* ------------------------------------------------------------------------ *)
-val contlub_Ilift1 = prove_goal Lift3.thy "contlub(Ilift)"
+qed_goal "contlub_Ilift1" Lift3.thy "contlub(Ilift)"
(fn prems =>
[
(rtac contlubI 1),
@@ -77,7 +77,7 @@
]);
-val contlub_Ilift2 = prove_goal Lift3.thy "contlub(Ilift(f))"
+qed_goal "contlub_Ilift2" Lift3.thy "contlub(Ilift(f))"
(fn prems =>
[
(rtac contlubI 1),
@@ -124,7 +124,7 @@
(atac 1)
]);
-val contX_Ilift1 = prove_goal Lift3.thy "contX(Ilift)"
+qed_goal "contX_Ilift1" Lift3.thy "contX(Ilift)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -132,7 +132,7 @@
(rtac contlub_Ilift1 1)
]);
-val contX_Ilift2 = prove_goal Lift3.thy "contX(Ilift(f))"
+qed_goal "contX_Ilift2" Lift3.thy "contX(Ilift(f))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -145,7 +145,7 @@
(* continuous versions of lemmas for ('a)u *)
(* ------------------------------------------------------------------------ *)
-val Exh_Lift1 = prove_goalw Lift3.thy [up_def] "z = UU | (? x. z = up[x])"
+qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up[x])"
(fn prems =>
[
(simp_tac (Lift_ss addsimps [contX_Iup]) 1),
@@ -153,7 +153,7 @@
(rtac Exh_Lift 1)
]);
-val inject_up = prove_goalw Lift3.thy [up_def] "up[x]=up[y] ==> x=y"
+qed_goalw "inject_up" Lift3.thy [up_def] "up[x]=up[y] ==> x=y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -163,14 +163,14 @@
(simp_tac (Lift_ss addsimps [contX_Iup]) 1)
]);
-val defined_up = prove_goalw Lift3.thy [up_def] "~ up[x]=UU"
+qed_goalw "defined_up" Lift3.thy [up_def] "~ up[x]=UU"
(fn prems =>
[
(simp_tac (Lift_ss addsimps [contX_Iup]) 1),
(rtac defined_Iup2 1)
]);
-val liftE1 = prove_goalw Lift3.thy [up_def]
+qed_goalw "liftE1" Lift3.thy [up_def]
"[| p=UU ==> Q; !!x. p=up[x]==>Q|] ==>Q"
(fn prems =>
[
@@ -182,7 +182,7 @@
]);
-val lift1 = prove_goalw Lift3.thy [up_def,lift_def] "lift[f][UU]=UU"
+qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift[f][UU]=UU"
(fn prems =>
[
(rtac (inst_lift_pcpo RS ssubst) 1),
@@ -195,7 +195,7 @@
(simp_tac (Lift_ss addsimps [contX_Iup,contX_Ilift1,contX_Ilift2]) 1)
]);
-val lift2 = prove_goalw Lift3.thy [up_def,lift_def] "lift[f][up[x]]=f[x]"
+qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift[f][up[x]]=f[x]"
(fn prems =>
[
(rtac (beta_cfun RS ssubst) 1),
@@ -208,14 +208,14 @@
(simp_tac (Lift_ss addsimps [contX_Iup,contX_Ilift1,contX_Ilift2]) 1)
]);
-val less_lift4b = prove_goalw Lift3.thy [up_def,lift_def] "~ up[x] << UU"
+qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up[x] << UU"
(fn prems =>
[
(simp_tac (Lift_ss addsimps [contX_Iup]) 1),
(rtac less_lift3b 1)
]);
-val less_lift4c = prove_goalw Lift3.thy [up_def,lift_def]
+qed_goalw "less_lift4c" Lift3.thy [up_def,lift_def]
"(up[x]<<up[y]) = (x<<y)"
(fn prems =>
[
@@ -223,7 +223,7 @@
(rtac less_lift2c 1)
]);
-val thelub_lift2a = prove_goalw Lift3.thy [up_def,lift_def]
+qed_goalw "thelub_lift2a" Lift3.thy [up_def,lift_def]
"[| is_chain(Y); ? i x. Y(i) = up[x] |] ==>\
\ lub(range(Y)) = up[lub(range(%i. lift[LAM x. x][Y(i)]))]"
(fn prems =>
@@ -252,7 +252,7 @@
-val thelub_lift2b = prove_goalw Lift3.thy [up_def,lift_def]
+qed_goalw "thelub_lift2b" Lift3.thy [up_def,lift_def]
"[| is_chain(Y); ! i x. ~ Y(i) = up[x] |] ==> lub(range(Y)) = UU"
(fn prems =>
[
@@ -272,7 +272,7 @@
]);
-val lift_lemma2 = prove_goal Lift3.thy " (? x.z = up[x]) = (~z=UU)"
+qed_goal "lift_lemma2" Lift3.thy " (? x.z = up[x]) = (~z=UU)"
(fn prems =>
[
(rtac iffI 1),
@@ -286,7 +286,7 @@
]);
-val thelub_lift2a_rev = prove_goal Lift3.thy
+qed_goal "thelub_lift2a_rev" Lift3.thy
"[| is_chain(Y); lub(range(Y)) = up[x] |] ==> ? i x. Y(i) = up[x]"
(fn prems =>
[
@@ -300,7 +300,7 @@
(atac 1)
]);
-val thelub_lift2b_rev = prove_goal Lift3.thy
+qed_goal "thelub_lift2b_rev" Lift3.thy
"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x. ~ Y(i) = up[x]"
(fn prems =>
[
@@ -316,7 +316,7 @@
]);
-val thelub_lift3 = prove_goal Lift3.thy
+qed_goal "thelub_lift3" Lift3.thy
"is_chain(Y) ==> lub(range(Y)) = UU |\
\ lub(range(Y)) = up[lub(range(%i. lift[LAM x. x][Y(i)]))]"
(fn prems =>
@@ -334,7 +334,7 @@
(fast_tac HOL_cs 1)
]);
-val lift3 = prove_goal Lift3.thy "lift[up][x]=x"
+qed_goal "lift3" Lift3.thy "lift[up][x]=x"
(fn prems =>
[
(res_inst_tac [("p","x")] liftE1 1),
--- a/src/HOLCF/One.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/One.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* Exhaustion and Elimination for type one *)
(* ------------------------------------------------------------------------ *)
-val Exh_one = prove_goalw One.thy [one_def] "z=UU | z = one"
+qed_goalw "Exh_one" One.thy [one_def] "z=UU | z = one"
(fn prems =>
[
(res_inst_tac [("p","rep_one[z]")] liftE1 1),
@@ -28,7 +28,7 @@
(atac 1)
]);
-val oneE = prove_goal One.thy
+qed_goal "oneE" One.thy
"[| p=UU ==> Q; p = one ==>Q|] ==>Q"
(fn prems =>
[
@@ -68,7 +68,7 @@
(* one is flat *)
(* ------------------------------------------------------------------------ *)
-val flat_one = prove_goalw One.thy [flat_def] "flat(one)"
+qed_goalw "flat_one" One.thy [flat_def] "flat(one)"
(fn prems =>
[
(rtac allI 1),
--- a/src/HOLCF/Pcpo.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Pcpo.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* in pcpo's everthing equal to THE lub has lub properties for every chain *)
(* ------------------------------------------------------------------------ *)
-val thelubE = prove_goal Pcpo.thy
+qed_goal "thelubE" Pcpo.thy
"[| is_chain(S);lub(range(S)) = (l::'a::pcpo)|] ==> range(S) <<| l "
(fn prems =>
[
@@ -38,7 +38,7 @@
(* the << relation between two chains is preserved by their lubs *)
(* ------------------------------------------------------------------------ *)
-val lub_mono = prove_goal Pcpo.thy
+qed_goal "lub_mono" Pcpo.thy
"[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
\ ==> lub(range(C1)) << lub(range(C2))"
(fn prems =>
@@ -56,7 +56,7 @@
(* the = relation between two chains is preserved by their lubs *)
(* ------------------------------------------------------------------------ *)
-val lub_equal = prove_goal Pcpo.thy
+qed_goal "lub_equal" Pcpo.thy
"[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\
\ ==> lub(range(C1))=lub(range(C2))"
(fn prems =>
@@ -81,7 +81,7 @@
(* more results about mono and = of lubs of chains *)
(* ------------------------------------------------------------------------ *)
-val lub_mono2 = prove_goal Pcpo.thy
+qed_goal "lub_mono2" Pcpo.thy
"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
\ ==> lub(range(X))<<lub(range(Y))"
(fn prems =>
@@ -110,7 +110,7 @@
(resolve_tac prems 1)
]);
-val lub_equal2 = prove_goal Pcpo.thy
+qed_goal "lub_equal2" Pcpo.thy
"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
\ ==> lub(range(X))=lub(range(Y))"
(fn prems =>
@@ -127,7 +127,7 @@
(fast_tac HOL_cs 1)
]);
-val lub_mono3 = prove_goal Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\
+qed_goal "lub_mono3" Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\
\! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
(fn prems =>
[
@@ -148,7 +148,7 @@
(* usefull lemmas about UU *)
(* ------------------------------------------------------------------------ *)
-val eq_UU_iff = prove_goal Pcpo.thy "(x=UU)=(x<<UU)"
+qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)"
(fn prems =>
[
(rtac iffI 1),
@@ -159,14 +159,14 @@
(rtac minimal 1)
]);
-val UU_I = prove_goal Pcpo.thy "x << UU ==> x = UU"
+qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU"
(fn prems =>
[
(rtac (eq_UU_iff RS ssubst) 1),
(resolve_tac prems 1)
]);
-val not_less2not_eq = prove_goal Pcpo.thy "~x<<y ==> ~x=y"
+qed_goal "not_less2not_eq" Pcpo.thy "~x<<y ==> ~x=y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -177,7 +177,7 @@
]);
-val chain_UU_I = prove_goal Pcpo.thy
+qed_goal "chain_UU_I" Pcpo.thy
"[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU"
(fn prems =>
[
@@ -191,7 +191,7 @@
]);
-val chain_UU_I_inverse = prove_goal Pcpo.thy
+qed_goal "chain_UU_I_inverse" Pcpo.thy
"!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
(fn prems =>
[
@@ -210,7 +210,7 @@
(etac spec 1)
]);
-val chain_UU_I_inverse2 = prove_goal Pcpo.thy
+qed_goal "chain_UU_I_inverse2" Pcpo.thy
"~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU"
(fn prems =>
[
@@ -223,7 +223,7 @@
]);
-val notUU_I = prove_goal Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU"
+qed_goal "notUU_I" Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -234,7 +234,7 @@
]);
-val chain_mono2 = prove_goal Pcpo.thy
+qed_goal "chain_mono2" Pcpo.thy
"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
\ ==> ? j.!i.j<i-->~Y(i)=UU"
(fn prems =>
@@ -256,7 +256,7 @@
(* uniqueness in void *)
(* ------------------------------------------------------------------------ *)
-val unique_void2 = prove_goal Pcpo.thy "(x::void)=UU"
+qed_goal "unique_void2" Pcpo.thy "(x::void)=UU"
(fn prems =>
[
(rtac (inst_void_pcpo RS ssubst) 1),
--- a/src/HOLCF/Porder.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Porder.ML Tue Feb 07 11:59:32 1995 +0100
@@ -14,7 +14,7 @@
(* the reverse law of anti--symmetrie of << *)
(* ------------------------------------------------------------------------ *)
-val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
+qed_goal "antisym_less_inverse" Porder.thy "x=y ==> x << y & y << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -24,7 +24,7 @@
]);
-val box_less = prove_goal Porder.thy
+qed_goal "box_less" Porder.thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>
[
@@ -38,7 +38,7 @@
(* lubs are unique *)
(* ------------------------------------------------------------------------ *)
-val unique_lub = prove_goalw Porder.thy [is_lub, is_ub]
+qed_goalw "unique_lub " Porder.thy [is_lub, is_ub]
"[| S <<| x ; S <<| y |] ==> x=y"
( fn prems =>
[
@@ -54,7 +54,7 @@
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
-val chain_mono = prove_goalw Porder.thy [is_chain]
+qed_goalw "chain_mono" Porder.thy [is_chain]
" is_chain(F) ==> x<y --> F(x)<<F(y)"
( fn prems =>
[
@@ -74,7 +74,7 @@
(atac 1)
]);
-val chain_mono3 = prove_goal Porder.thy
+qed_goal "chain_mono3" Porder.thy
"[| is_chain(F); x <= y |] ==> F(x) << F(y)"
(fn prems =>
[
@@ -92,7 +92,7 @@
(* The range of a chain is a totaly ordered << *)
(* ------------------------------------------------------------------------ *)
-val chain_is_tord = prove_goalw Porder.thy [is_tord]
+qed_goalw "chain_is_tord" Porder.thy [is_tord]
"is_chain(F) ==> is_tord(range(F))"
( fn prems =>
[
@@ -127,22 +127,22 @@
(* technical lemmas about lub and is_lub *)
(* ------------------------------------------------------------------------ *)
-val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
+qed_goal "lubI" Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac (lub RS ssubst) 1),
- (etac selectI2 1)
+ (etac selectI3 1)
]);
-val lubE = prove_goal Porder.thy " M <<| lub(M) ==> ? x. M <<| x"
+qed_goal "lubE" Porder.thy " M <<| lub(M) ==> ? x. M <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
(etac exI 1)
]);
-val lub_eq = prove_goal Porder.thy
+qed_goal "lub_eq" Porder.thy
"(? x. M <<| x) = M <<| lub(M)"
(fn prems =>
[
@@ -152,7 +152,7 @@
]);
-val thelubI = prove_goal Porder.thy " M <<| l ==> lub(M) = l"
+qed_goal "thelubI" Porder.thy " M <<| l ==> lub(M) = l"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -167,7 +167,7 @@
(* access to some definition as inference rule *)
(* ------------------------------------------------------------------------ *)
-val is_lubE = prove_goalw Porder.thy [is_lub]
+qed_goalw "is_lubE" Porder.thy [is_lub]
"S <<| x ==> S <| x & (! u. S <| u --> x << u)"
(fn prems =>
[
@@ -175,7 +175,7 @@
(atac 1)
]);
-val is_lubI = prove_goalw Porder.thy [is_lub]
+qed_goalw "is_lubI" Porder.thy [is_lub]
"S <| x & (! u. S <| u --> x << u) ==> S <<| x"
(fn prems =>
[
@@ -183,14 +183,14 @@
(atac 1)
]);
-val is_chainE = prove_goalw Porder.thy [is_chain]
+qed_goalw "is_chainE" Porder.thy [is_chain]
"is_chain(F) ==> ! i. F(i) << F(Suc(i))"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)]);
-val is_chainI = prove_goalw Porder.thy [is_chain]
+qed_goalw "is_chainI" Porder.thy [is_chain]
"! i. F(i) << F(Suc(i)) ==> is_chain(F) "
(fn prems =>
[
@@ -201,7 +201,7 @@
(* technical lemmas about (least) upper bounds of chains *)
(* ------------------------------------------------------------------------ *)
-val ub_rangeE = prove_goalw Porder.thy [is_ub]
+qed_goalw "ub_rangeE" Porder.thy [is_ub]
"range(S) <| x ==> ! i. S(i) << x"
(fn prems =>
[
@@ -212,7 +212,7 @@
(rtac rangeI 1)
]);
-val ub_rangeI = prove_goalw Porder.thy [is_ub]
+qed_goalw "ub_rangeI" Porder.thy [is_ub]
"! i. S(i) << x ==> range(S) <| x"
(fn prems =>
[
@@ -237,7 +237,7 @@
(* a technical argument about << on void *)
(* ------------------------------------------------------------------------ *)
-val less_void = prove_goal Porder.thy "((u1::void) << u2) = (u1 = u2)"
+qed_goal "less_void" Porder.thy "((u1::void) << u2) = (u1 = u2)"
(fn prems =>
[
(rtac (inst_void_po RS ssubst) 1),
@@ -254,7 +254,7 @@
(* void is pointed. The least element is UU_void *)
(* ------------------------------------------------------------------------ *)
-val minimal_void = prove_goal Porder.thy "UU_void << x"
+qed_goal "minimal_void" Porder.thy "UU_void << x"
(fn prems =>
[
(rtac (inst_void_po RS ssubst) 1),
@@ -266,7 +266,7 @@
(* UU_void is the trivial lub of all chains in void *)
(* ------------------------------------------------------------------------ *)
-val lub_void = prove_goalw Porder.thy [is_lub] "M <<| UU_void"
+qed_goalw "lub_void" Porder.thy [is_lub] "M <<| UU_void"
(fn prems =>
[
(rtac conjI 1),
@@ -289,7 +289,7 @@
(* void is a cpo wrt. countable chains *)
(* ------------------------------------------------------------------------ *)
-val cpo_void = prove_goal Porder.thy
+qed_goal "cpo_void" Porder.thy
"is_chain((S::nat=>void)) ==> ? x. range(S) <<| x "
(fn prems =>
[
@@ -307,7 +307,7 @@
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
-val lub_finch1 = prove_goalw Porder.thy [max_in_chain_def]
+qed_goalw "lub_finch1" Porder.thy [max_in_chain_def]
"[| is_chain(C) ; max_in_chain(i,C)|] ==> range(C) <<| C(i)"
(fn prems =>
[
@@ -329,19 +329,19 @@
(etac (ub_rangeE RS spec) 1)
]);
-val lub_finch2 = prove_goalw Porder.thy [finite_chain_def]
+qed_goalw "lub_finch2" Porder.thy [finite_chain_def]
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain(i,C))"
(fn prems=>
[
(cut_facts_tac prems 1),
(rtac lub_finch1 1),
(etac conjunct1 1),
- (rtac selectI2 1),
+ (rtac selectI3 1),
(etac conjunct2 1)
]);
-val bin_chain = prove_goal Porder.thy "x<<y ==> is_chain(%i. if(i=0,x,y))"
+qed_goal "bin_chain" Porder.thy "x<<y ==> is_chain(%i. if(i=0,x,y))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -353,7 +353,7 @@
(rtac refl_less 1)
]);
-val bin_chainmax = prove_goalw Porder.thy [max_in_chain_def,le_def]
+qed_goalw "bin_chainmax" Porder.thy [max_in_chain_def,le_def]
"x<<y ==> max_in_chain(Suc(0),%i. if(i=0,x,y))"
(fn prems =>
[
@@ -364,7 +364,7 @@
(asm_simp_tac nat_ss 1)
]);
-val lub_bin_chain = prove_goal Porder.thy
+qed_goal "lub_bin_chain" Porder.thy
"x << y ==> range(%i. if(i = 0,x,y)) <<| y"
(fn prems=>
[ (cut_facts_tac prems 1),
@@ -379,7 +379,7 @@
(* the maximal element in a chain is its lub *)
(* ------------------------------------------------------------------------ *)
-val lub_chain_maxelem = prove_goal Porder.thy
+qed_goal "lub_chain_maxelem" Porder.thy
"[|is_chain(Y);? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c"
(fn prems =>
[
@@ -399,7 +399,7 @@
(* the lub of a constant chain is the constant *)
(* ------------------------------------------------------------------------ *)
-val lub_const = prove_goal Porder.thy "range(%x.c) <<| c"
+qed_goal "lub_const" Porder.thy "range(%x.c) <<| c"
(fn prems =>
[
(rtac is_lubI 1),
--- a/src/HOLCF/Sprod0.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Sprod0.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* A non-emptyness result for Sprod *)
(* ------------------------------------------------------------------------ *)
-val SprodI = prove_goalw Sprod0.thy [Sprod_def]
+qed_goalw "SprodI" Sprod0.thy [Sprod_def]
"Spair_Rep(a,b):Sprod"
(fn prems =>
[
@@ -20,7 +20,7 @@
]);
-val inj_onto_Abs_Sprod = prove_goal Sprod0.thy
+qed_goal "inj_onto_Abs_Sprod" Sprod0.thy
"inj_onto(Abs_Sprod,Sprod)"
(fn prems =>
[
@@ -34,7 +34,7 @@
(* ------------------------------------------------------------------------ *)
-val strict_Spair_Rep = prove_goalw Sprod0.thy [Spair_Rep_def]
+qed_goalw "strict_Spair_Rep" Sprod0.thy [Spair_Rep_def]
"(a=UU | b=UU) ==> (Spair_Rep(a,b) = Spair_Rep(UU,UU))"
(fn prems =>
[
@@ -46,7 +46,7 @@
(fast_tac HOL_cs 1)
]);
-val defined_Spair_Rep_rev = prove_goalw Sprod0.thy [Spair_Rep_def]
+qed_goalw "defined_Spair_Rep_rev" Sprod0.thy [Spair_Rep_def]
"(Spair_Rep(a,b) = Spair_Rep(UU,UU)) ==> (a=UU | b=UU)"
(fn prems =>
[
@@ -64,7 +64,7 @@
(* injectivity of Spair_Rep and Ispair *)
(* ------------------------------------------------------------------------ *)
-val inject_Spair_Rep = prove_goalw Sprod0.thy [Spair_Rep_def]
+qed_goalw "inject_Spair_Rep" Sprod0.thy [Spair_Rep_def]
"[|~aa=UU ; ~ba=UU ; Spair_Rep(a,b)=Spair_Rep(aa,ba) |] ==> a=aa & b=ba"
(fn prems =>
[
@@ -76,7 +76,7 @@
]);
-val inject_Ispair = prove_goalw Sprod0.thy [Ispair_def]
+qed_goalw "inject_Ispair" Sprod0.thy [Ispair_def]
"[|~aa=UU ; ~ba=UU ; Ispair(a,b)=Ispair(aa,ba) |] ==> a=aa & b=ba"
(fn prems =>
[
@@ -93,7 +93,7 @@
(* strictness and definedness of Ispair *)
(* ------------------------------------------------------------------------ *)
-val strict_Ispair = prove_goalw Sprod0.thy [Ispair_def]
+qed_goalw "strict_Ispair" Sprod0.thy [Ispair_def]
"(a=UU | b=UU) ==> Ispair(a,b)=Ispair(UU,UU)"
(fn prems =>
[
@@ -101,7 +101,7 @@
(etac (strict_Spair_Rep RS arg_cong) 1)
]);
-val strict_Ispair1 = prove_goalw Sprod0.thy [Ispair_def]
+qed_goalw "strict_Ispair1" Sprod0.thy [Ispair_def]
"Ispair(UU,b) = Ispair(UU,UU)"
(fn prems =>
[
@@ -110,7 +110,7 @@
(rtac refl 1)
]);
-val strict_Ispair2 = prove_goalw Sprod0.thy [Ispair_def]
+qed_goalw "strict_Ispair2" Sprod0.thy [Ispair_def]
"Ispair(a,UU) = Ispair(UU,UU)"
(fn prems =>
[
@@ -119,7 +119,7 @@
(rtac refl 1)
]);
-val strict_Ispair_rev = prove_goal Sprod0.thy
+qed_goal "strict_Ispair_rev" Sprod0.thy
"~Ispair(x,y)=Ispair(UU,UU) ==> ~x=UU & ~y=UU"
(fn prems =>
[
@@ -129,7 +129,7 @@
(etac strict_Ispair 1)
]);
-val defined_Ispair_rev = prove_goalw Sprod0.thy [Ispair_def]
+qed_goalw "defined_Ispair_rev" Sprod0.thy [Ispair_def]
"Ispair(a,b) = Ispair(UU,UU) ==> (a = UU | b = UU)"
(fn prems =>
[
@@ -141,7 +141,7 @@
(rtac SprodI 1)
]);
-val defined_Ispair = prove_goal Sprod0.thy
+qed_goal "defined_Ispair" Sprod0.thy
"[|~a=UU; ~b=UU|] ==> ~(Ispair(a,b) = Ispair(UU,UU))"
(fn prems =>
[
@@ -158,7 +158,7 @@
(* Exhaustion of the strict product ** *)
(* ------------------------------------------------------------------------ *)
-val Exh_Sprod = prove_goalw Sprod0.thy [Ispair_def]
+qed_goalw "Exh_Sprod" Sprod0.thy [Ispair_def]
"z=Ispair(UU,UU) | (? a b. z=Ispair(a,b) & ~a=UU & ~b=UU)"
(fn prems =>
[
@@ -185,7 +185,7 @@
(* general elimination rule for strict product *)
(* ------------------------------------------------------------------------ *)
-val IsprodE = prove_goal Sprod0.thy
+qed_goal "IsprodE" Sprod0.thy
"[|p=Ispair(UU,UU) ==> Q ;!!x y. [|p=Ispair(x,y); ~x=UU ; ~y=UU|] ==> Q|] ==> Q"
(fn prems =>
[
@@ -205,7 +205,7 @@
(* some results about the selectors Isfst, Issnd *)
(* ------------------------------------------------------------------------ *)
-val strict_Isfst = prove_goalw Sprod0.thy [Isfst_def]
+qed_goalw "strict_Isfst" Sprod0.thy [Isfst_def]
"p=Ispair(UU,UU)==>Isfst(p)=UU"
(fn prems =>
[
@@ -221,7 +221,7 @@
]);
-val strict_Isfst1 = prove_goal Sprod0.thy
+qed_goal "strict_Isfst1" Sprod0.thy
"Isfst(Ispair(UU,y)) = UU"
(fn prems =>
[
@@ -230,7 +230,7 @@
(rtac refl 1)
]);
-val strict_Isfst2 = prove_goal Sprod0.thy
+qed_goal "strict_Isfst2" Sprod0.thy
"Isfst(Ispair(x,UU)) = UU"
(fn prems =>
[
@@ -240,7 +240,7 @@
]);
-val strict_Issnd = prove_goalw Sprod0.thy [Issnd_def]
+qed_goalw "strict_Issnd" Sprod0.thy [Issnd_def]
"p=Ispair(UU,UU)==>Issnd(p)=UU"
(fn prems =>
[
@@ -255,7 +255,7 @@
(REPEAT (fast_tac HOL_cs 1))
]);
-val strict_Issnd1 = prove_goal Sprod0.thy
+qed_goal "strict_Issnd1" Sprod0.thy
"Issnd(Ispair(UU,y)) = UU"
(fn prems =>
[
@@ -264,7 +264,7 @@
(rtac refl 1)
]);
-val strict_Issnd2 = prove_goal Sprod0.thy
+qed_goal "strict_Issnd2" Sprod0.thy
"Issnd(Ispair(x,UU)) = UU"
(fn prems =>
[
@@ -273,7 +273,7 @@
(rtac refl 1)
]);
-val Isfst = prove_goalw Sprod0.thy [Isfst_def]
+qed_goalw "Isfst" Sprod0.thy [Isfst_def]
"[|~x=UU ;~y=UU |] ==> Isfst(Ispair(x,y)) = x"
(fn prems =>
[
@@ -293,7 +293,7 @@
(fast_tac HOL_cs 1)
]);
-val Issnd = prove_goalw Sprod0.thy [Issnd_def]
+qed_goalw "Issnd" Sprod0.thy [Issnd_def]
"[|~x=UU ;~y=UU |] ==> Issnd(Ispair(x,y)) = y"
(fn prems =>
[
@@ -313,7 +313,7 @@
(fast_tac HOL_cs 1)
]);
-val Isfst2 = prove_goal Sprod0.thy "~y=UU ==>Isfst(Ispair(x,y))=x"
+qed_goal "Isfst2" Sprod0.thy "~y=UU ==>Isfst(Ispair(x,y))=x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -324,7 +324,7 @@
(rtac strict_Isfst1 1)
]);
-val Issnd2 = prove_goal Sprod0.thy "~x=UU ==>Issnd(Ispair(x,y))=y"
+qed_goal "Issnd2" Sprod0.thy "~x=UU ==>Issnd(Ispair(x,y))=y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -346,7 +346,7 @@
Isfst2,Issnd2];
-val defined_IsfstIssnd = prove_goal Sprod0.thy
+qed_goal "defined_IsfstIssnd" Sprod0.thy
"~p=Ispair(UU,UU) ==> ~Isfst(p)=UU & ~Issnd(p)=UU"
(fn prems =>
[
@@ -364,7 +364,7 @@
(* Surjective pairing: equivalent to Exh_Sprod *)
(* ------------------------------------------------------------------------ *)
-val surjective_pairing_Sprod = prove_goal Sprod0.thy
+qed_goal "surjective_pairing_Sprod" Sprod0.thy
"z = Ispair(Isfst(z))(Issnd(z))"
(fn prems =>
[
--- a/src/HOLCF/Sprod1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Sprod1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -13,7 +13,7 @@
(* ------------------------------------------------------------------------ *)
-val less_sprod1a = prove_goalw Sprod1.thy [less_sprod_def]
+qed_goalw "less_sprod1a" Sprod1.thy [less_sprod_def]
"p1=Ispair(UU,UU) ==> less_sprod(p1,p2)"
(fn prems =>
[
@@ -29,7 +29,7 @@
(atac 1)
]);
-val less_sprod1b = prove_goalw Sprod1.thy [less_sprod_def]
+qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def]
"~p1=Ispair(UU,UU) ==> \
\ less_sprod(p1,p2) = ( Isfst(p1) << Isfst(p2) & Issnd(p1) << Issnd(p2))"
(fn prems =>
@@ -45,7 +45,7 @@
(atac 1)
]);
-val less_sprod2a = prove_goal Sprod1.thy
+qed_goal "less_sprod2a" Sprod1.thy
"less_sprod(Ispair(x,y),Ispair(UU,UU)) ==> x = UU | y = UU"
(fn prems =>
[
@@ -65,7 +65,7 @@
(REPEAT (fast_tac HOL_cs 1))
]);
-val less_sprod2b = prove_goal Sprod1.thy
+qed_goal "less_sprod2b" Sprod1.thy
"less_sprod(p,Ispair(UU,UU)) ==> p = Ispair(UU,UU)"
(fn prems =>
[
@@ -77,7 +77,7 @@
(etac less_sprod2a 1)
]);
-val less_sprod2c = prove_goal Sprod1.thy
+qed_goal "less_sprod2c" Sprod1.thy
"[|less_sprod(Ispair(xa,ya),Ispair(x,y));\
\~ xa = UU ; ~ ya = UU;~ x = UU ; ~ y = UU |] ==> xa << x & ya << y"
(fn prems =>
@@ -105,7 +105,7 @@
(* less_sprod is a partial order on Sprod *)
(* ------------------------------------------------------------------------ *)
-val refl_less_sprod = prove_goal Sprod1.thy "less_sprod(p,p)"
+qed_goal "refl_less_sprod" Sprod1.thy "less_sprod(p,p)"
(fn prems =>
[
(res_inst_tac [("p","p")] IsprodE 1),
@@ -117,7 +117,7 @@
]);
-val antisym_less_sprod = prove_goal Sprod1.thy
+qed_goal "antisym_less_sprod" Sprod1.thy
"[|less_sprod(p1,p2);less_sprod(p2,p1)|] ==> p1=p2"
(fn prems =>
[
@@ -145,7 +145,7 @@
(asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1)
]);
-val trans_less_sprod = prove_goal Sprod1.thy
+qed_goal "trans_less_sprod" Sprod1.thy
"[|less_sprod(p1,p2);less_sprod(p2,p3)|] ==> less_sprod(p1,p3)"
(fn prems =>
[
--- a/src/HOLCF/Sprod2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Sprod2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -13,7 +13,7 @@
(* access to less_sprod in class po *)
(* ------------------------------------------------------------------------ *)
-val less_sprod3a = prove_goal Sprod2.thy
+qed_goal "less_sprod3a" Sprod2.thy
"p1=Ispair(UU,UU) ==> p1 << p2"
(fn prems =>
[
@@ -23,7 +23,7 @@
]);
-val less_sprod3b = prove_goal Sprod2.thy
+qed_goal "less_sprod3b" Sprod2.thy
"~p1=Ispair(UU,UU) ==>\
\ (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))"
(fn prems =>
@@ -33,7 +33,7 @@
(etac less_sprod1b 1)
]);
-val less_sprod4b = prove_goal Sprod2.thy
+qed_goal "less_sprod4b" Sprod2.thy
"p << Ispair(UU,UU) ==> p = Ispair(UU,UU)"
(fn prems =>
[
@@ -45,7 +45,7 @@
val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
(* Ispair(?a,?b) << Ispair(UU,UU) ==> ?a = UU | ?b = UU *)
-val less_sprod4c = prove_goal Sprod2.thy
+qed_goal "less_sprod4c" Sprod2.thy
"[|Ispair(xa,ya)<<Ispair(x,y);~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>\
\ xa<<x & ya << y"
(fn prems =>
@@ -60,7 +60,7 @@
(* type sprod is pointed *)
(* ------------------------------------------------------------------------ *)
-val minimal_sprod = prove_goal Sprod2.thy "Ispair(UU,UU)<<p"
+qed_goal "minimal_sprod" Sprod2.thy "Ispair(UU,UU)<<p"
(fn prems =>
[
(rtac less_sprod3a 1),
@@ -71,7 +71,7 @@
(* Ispair is monotone in both arguments *)
(* ------------------------------------------------------------------------ *)
-val monofun_Ispair1 = prove_goalw Sprod2.thy [monofun] "monofun(Ispair)"
+qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
(fn prems =>
[
(strip_tac 1),
@@ -111,7 +111,7 @@
]);
-val monofun_Ispair2 = prove_goalw Sprod2.thy [monofun] "monofun(Ispair(x))"
+qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
(fn prems =>
[
(strip_tac 1),
@@ -148,7 +148,7 @@
(etac (strict_Ispair_rev RS conjunct2) 1)
]);
-val monofun_Ispair = prove_goal Sprod2.thy
+qed_goal " monofun_Ispair" Sprod2.thy
"[|x1<<x2; y1<<y2|] ==> Ispair(x1,y1)<<Ispair(x2,y2)"
(fn prems =>
[
@@ -166,7 +166,7 @@
(* Isfst and Issnd are monotone *)
(* ------------------------------------------------------------------------ *)
-val monofun_Isfst = prove_goalw Sprod2.thy [monofun] "monofun(Isfst)"
+qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
(fn prems =>
[
(strip_tac 1),
@@ -193,7 +193,7 @@
(REPEAT (atac 1))
]);
-val monofun_Issnd = prove_goalw Sprod2.thy [monofun] "monofun(Issnd)"
+qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
(fn prems =>
[
(strip_tac 1),
@@ -225,7 +225,7 @@
(* the type 'a ** 'b is a cpo *)
(* ------------------------------------------------------------------------ *)
-val lub_sprod = prove_goal Sprod2.thy
+qed_goal "lub_sprod" Sprod2.thy
"[|is_chain(S)|] ==> range(S) <<| \
\ Ispair(lub(range(%i.Isfst(S(i)))),lub(range(%i.Issnd(S(i)))))"
(fn prems =>
@@ -256,7 +256,7 @@
(* is_chain(?S1) ==> lub(range(?S1)) = *)
(* Ispair(lub(range(%i. Isfst(?S1(i)))),lub(range(%i. Issnd(?S1(i))))) *)
-val cpo_sprod = prove_goal Sprod2.thy
+qed_goal "cpo_sprod" Sprod2.thy
"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
(fn prems =>
[
--- a/src/HOLCF/Sprod3.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Sprod3.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* continuity of Ispair, Isfst, Issnd *)
(* ------------------------------------------------------------------------ *)
-val sprod3_lemma1 = prove_goal Sprod3.thy
+qed_goal "sprod3_lemma1" Sprod3.thy
"[| is_chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\
\ Ispair(lub(range(Y)),x) =\
\ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
@@ -54,7 +54,7 @@
]);
-val sprod3_lemma2 = prove_goal Sprod3.thy
+qed_goal "sprod3_lemma2" Sprod3.thy
"[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
\ Ispair(lub(range(Y)),x) =\
\ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
@@ -76,7 +76,7 @@
]);
-val sprod3_lemma3 = prove_goal Sprod3.thy
+qed_goal "sprod3_lemma3" Sprod3.thy
"[| is_chain(Y); x = UU |] ==>\
\ Ispair(lub(range(Y)),x) =\
\ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
@@ -96,7 +96,7 @@
]);
-val contlub_Ispair1 = prove_goal Sprod3.thy "contlub(Ispair)"
+qed_goal "contlub_Ispair1" Sprod3.thy "contlub(Ispair)"
(fn prems =>
[
(rtac contlubI 1),
@@ -122,7 +122,7 @@
(atac 1)
]);
-val sprod3_lemma4 = prove_goal Sprod3.thy
+qed_goal "sprod3_lemma4" Sprod3.thy
"[| is_chain(Y); ~ x = UU; ~ lub(range(Y)) = UU |] ==>\
\ Ispair(x,lub(range(Y))) =\
\ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
@@ -161,7 +161,7 @@
(asm_simp_tac Sprod_ss 1)
]);
-val sprod3_lemma5 = prove_goal Sprod3.thy
+qed_goal "sprod3_lemma5" Sprod3.thy
"[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
\ Ispair(x,lub(range(Y))) =\
\ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
@@ -182,7 +182,7 @@
(atac 1)
]);
-val sprod3_lemma6 = prove_goal Sprod3.thy
+qed_goal "sprod3_lemma6" Sprod3.thy
"[| is_chain(Y); x = UU |] ==>\
\ Ispair(x,lub(range(Y))) =\
\ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
@@ -201,7 +201,7 @@
(simp_tac Sprod_ss 1)
]);
-val contlub_Ispair2 = prove_goal Sprod3.thy "contlub(Ispair(x))"
+qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
(fn prems =>
[
(rtac contlubI 1),
@@ -223,7 +223,7 @@
]);
-val contX_Ispair1 = prove_goal Sprod3.thy "contX(Ispair)"
+qed_goal "contX_Ispair1" Sprod3.thy "contX(Ispair)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -232,7 +232,7 @@
]);
-val contX_Ispair2 = prove_goal Sprod3.thy "contX(Ispair(x))"
+qed_goal "contX_Ispair2" Sprod3.thy "contX(Ispair(x))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -240,7 +240,7 @@
(rtac contlub_Ispair2 1)
]);
-val contlub_Isfst = prove_goal Sprod3.thy "contlub(Isfst)"
+qed_goal "contlub_Isfst" Sprod3.thy "contlub(Isfst)"
(fn prems =>
[
(rtac contlubI 1),
@@ -269,7 +269,7 @@
]);
-val contlub_Issnd = prove_goal Sprod3.thy "contlub(Issnd)"
+qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
(fn prems =>
[
(rtac contlubI 1),
@@ -297,7 +297,7 @@
]);
-val contX_Isfst = prove_goal Sprod3.thy "contX(Isfst)"
+qed_goal "contX_Isfst" Sprod3.thy "contX(Isfst)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -305,7 +305,7 @@
(rtac contlub_Isfst 1)
]);
-val contX_Issnd = prove_goal Sprod3.thy "contX(Issnd)"
+qed_goal "contX_Issnd" Sprod3.thy "contX(Issnd)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -320,7 +320,7 @@
--------------------------------------------------------------------------
*)
-val spair_eq = prove_goal Sprod3.thy "[|x1=x2;y1=y2|] ==> x1##y1 = x2##y2"
+qed_goal "spair_eq" Sprod3.thy "[|x1=x2;y1=y2|] ==> x1##y1 = x2##y2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -331,7 +331,7 @@
(* convert all lemmas to the continuous versions *)
(* ------------------------------------------------------------------------ *)
-val beta_cfun_sprod = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def]
"(LAM x y.Ispair(x,y))[a][b] = Ispair(a,b)"
(fn prems =>
[
@@ -345,7 +345,7 @@
(rtac refl 1)
]);
-val inject_spair = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "inject_spair" Sprod3.thy [spair_def]
"[|~aa=UU ; ~ba=UU ; (a##b)=(aa##ba) |] ==> a=aa & b=ba"
(fn prems =>
[
@@ -357,7 +357,7 @@
(rtac beta_cfun_sprod 1)
]);
-val inst_sprod_pcpo2 = prove_goalw Sprod3.thy [spair_def] "UU = (UU##UU)"
+qed_goalw "inst_sprod_pcpo2" Sprod3.thy [spair_def] "UU = (UU##UU)"
(fn prems =>
[
(rtac sym 1),
@@ -367,7 +367,7 @@
(rtac inst_sprod_pcpo 1)
]);
-val strict_spair = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "strict_spair" Sprod3.thy [spair_def]
"(a=UU | b=UU) ==> (a##b)=UU"
(fn prems =>
[
@@ -379,7 +379,7 @@
(etac strict_Ispair 1)
]);
-val strict_spair1 = prove_goalw Sprod3.thy [spair_def] "(UU##b) = UU"
+qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(UU##b) = UU"
(fn prems =>
[
(rtac (beta_cfun_sprod RS ssubst) 1),
@@ -388,7 +388,7 @@
(rtac strict_Ispair1 1)
]);
-val strict_spair2 = prove_goalw Sprod3.thy [spair_def] "(a##UU) = UU"
+qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(a##UU) = UU"
(fn prems =>
[
(rtac (beta_cfun_sprod RS ssubst) 1),
@@ -397,7 +397,7 @@
(rtac strict_Ispair2 1)
]);
-val strict_spair_rev = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "strict_spair_rev" Sprod3.thy [spair_def]
"~(x##y)=UU ==> ~x=UU & ~y=UU"
(fn prems =>
[
@@ -408,7 +408,7 @@
(atac 1)
]);
-val defined_spair_rev = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "defined_spair_rev" Sprod3.thy [spair_def]
"(a##b) = UU ==> (a = UU | b = UU)"
(fn prems =>
[
@@ -419,7 +419,7 @@
(atac 1)
]);
-val defined_spair = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "defined_spair" Sprod3.thy [spair_def]
"[|~a=UU; ~b=UU|] ==> ~(a##b) = UU"
(fn prems =>
[
@@ -430,7 +430,7 @@
(atac 1)
]);
-val Exh_Sprod2 = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "Exh_Sprod2" Sprod3.thy [spair_def]
"z=UU | (? a b. z=(a##b) & ~a=UU & ~b=UU)"
(fn prems =>
[
@@ -450,7 +450,7 @@
]);
-val sprodE = prove_goalw Sprod3.thy [spair_def]
+qed_goalw "sprodE" Sprod3.thy [spair_def]
"[|p=UU ==> Q;!!x y. [|p=(x##y);~x=UU ; ~y=UU|] ==> Q|] ==> Q"
(fn prems =>
[
@@ -466,7 +466,7 @@
]);
-val strict_sfst = prove_goalw Sprod3.thy [sfst_def]
+qed_goalw "strict_sfst" Sprod3.thy [sfst_def]
"p=UU==>sfst[p]=UU"
(fn prems =>
[
@@ -478,7 +478,7 @@
(atac 1)
]);
-val strict_sfst1 = prove_goalw Sprod3.thy [sfst_def,spair_def]
+qed_goalw "strict_sfst1" Sprod3.thy [sfst_def,spair_def]
"sfst[UU##y] = UU"
(fn prems =>
[
@@ -488,7 +488,7 @@
(rtac strict_Isfst1 1)
]);
-val strict_sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def]
+qed_goalw "strict_sfst2" Sprod3.thy [sfst_def,spair_def]
"sfst[x##UU] = UU"
(fn prems =>
[
@@ -498,7 +498,7 @@
(rtac strict_Isfst2 1)
]);
-val strict_ssnd = prove_goalw Sprod3.thy [ssnd_def]
+qed_goalw "strict_ssnd" Sprod3.thy [ssnd_def]
"p=UU==>ssnd[p]=UU"
(fn prems =>
[
@@ -510,7 +510,7 @@
(atac 1)
]);
-val strict_ssnd1 = prove_goalw Sprod3.thy [ssnd_def,spair_def]
+qed_goalw "strict_ssnd1" Sprod3.thy [ssnd_def,spair_def]
"ssnd[UU##y] = UU"
(fn prems =>
[
@@ -520,7 +520,7 @@
(rtac strict_Issnd1 1)
]);
-val strict_ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def]
+qed_goalw "strict_ssnd2" Sprod3.thy [ssnd_def,spair_def]
"ssnd[x##UU] = UU"
(fn prems =>
[
@@ -530,7 +530,7 @@
(rtac strict_Issnd2 1)
]);
-val sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def]
+qed_goalw "sfst2" Sprod3.thy [sfst_def,spair_def]
"~y=UU ==>sfst[x##y]=x"
(fn prems =>
[
@@ -541,7 +541,7 @@
(etac Isfst2 1)
]);
-val ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def]
+qed_goalw "ssnd2" Sprod3.thy [ssnd_def,spair_def]
"~x=UU ==>ssnd[x##y]=y"
(fn prems =>
[
@@ -553,7 +553,7 @@
]);
-val defined_sfstssnd = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "defined_sfstssnd" Sprod3.thy [sfst_def,ssnd_def,spair_def]
"~p=UU ==> ~sfst[p]=UU & ~ssnd[p]=UU"
(fn prems =>
[
@@ -568,7 +568,7 @@
]);
-val surjective_pairing_Sprod2 = prove_goalw Sprod3.thy
+qed_goalw "surjective_pairing_Sprod2" Sprod3.thy
[sfst_def,ssnd_def,spair_def] "(sfst[p] ## ssnd[p]) = p"
(fn prems =>
[
@@ -581,7 +581,7 @@
]);
-val less_sprod5b = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "less_sprod5b" Sprod3.thy [sfst_def,ssnd_def,spair_def]
"~p1=UU ==> (p1<<p2) = (sfst[p1]<<sfst[p2] & ssnd[p1]<<ssnd[p2])"
(fn prems =>
[
@@ -600,7 +600,7 @@
]);
-val less_sprod5c = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "less_sprod5c" Sprod3.thy [sfst_def,ssnd_def,spair_def]
"[|xa##ya<<x##y;~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>xa<<x & ya << y"
(fn prems =>
[
@@ -612,7 +612,7 @@
(atac 1)
]);
-val lub_sprod2 = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "lub_sprod2" Sprod3.thy [sfst_def,ssnd_def,spair_def]
"[|is_chain(S)|] ==> range(S) <<| \
\ (lub(range(%i.sfst[S(i)])) ## lub(range(%i.ssnd[S(i)])))"
(fn prems =>
@@ -634,7 +634,7 @@
-val ssplit1 = prove_goalw Sprod3.thy [ssplit_def]
+qed_goalw "ssplit1" Sprod3.thy [ssplit_def]
"ssplit[f][UU]=UU"
(fn prems =>
[
@@ -644,7 +644,7 @@
(rtac refl 1)
]);
-val ssplit2 = prove_goalw Sprod3.thy [ssplit_def]
+qed_goalw "ssplit2" Sprod3.thy [ssplit_def]
"[|~x=UU;~y=UU|] ==> ssplit[f][x##y]=f[x][y]"
(fn prems =>
[
@@ -664,7 +664,7 @@
]);
-val ssplit3 = prove_goalw Sprod3.thy [ssplit_def]
+qed_goalw "ssplit3" Sprod3.thy [ssplit_def]
"ssplit[spair][z]=z"
(fn prems =>
[
--- a/src/HOLCF/Ssum0.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Ssum0.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* A non-emptyness result for Sssum *)
(* ------------------------------------------------------------------------ *)
-val SsumIl = prove_goalw Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
+qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
(fn prems =>
[
(rtac CollectI 1),
@@ -21,7 +21,7 @@
(rtac refl 1)
]);
-val SsumIr = prove_goalw Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
+qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
(fn prems =>
[
(rtac CollectI 1),
@@ -30,7 +30,7 @@
(rtac refl 1)
]);
-val inj_onto_Abs_Ssum = prove_goal Ssum0.thy "inj_onto(Abs_Ssum,Ssum)"
+qed_goal "inj_onto_Abs_Ssum" Ssum0.thy "inj_onto(Abs_Ssum,Ssum)"
(fn prems =>
[
(rtac inj_onto_inverseI 1),
@@ -41,7 +41,7 @@
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-val strict_SinlSinr_Rep = prove_goalw Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
+qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
"Sinl_Rep(UU) = Sinr_Rep(UU)"
(fn prems =>
[
@@ -51,7 +51,7 @@
(fast_tac HOL_cs 1)
]);
-val strict_IsinlIsinr = prove_goalw Ssum0.thy [Isinl_def,Isinr_def]
+qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
"Isinl(UU) = Isinr(UU)"
(fn prems =>
[
@@ -63,7 +63,7 @@
(* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-val noteq_SinlSinr_Rep = prove_goalw Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
+qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
"(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
(fn prems =>
[
@@ -83,7 +83,7 @@
]);
-val noteq_IsinlIsinr = prove_goalw Ssum0.thy [Isinl_def,Isinr_def]
+qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
"Isinl(a)=Isinr(b) ==> a=UU & b=UU"
(fn prems =>
[
@@ -100,7 +100,7 @@
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
(* ------------------------------------------------------------------------ *)
-val inject_Sinl_Rep1 = prove_goalw Ssum0.thy [Sinl_Rep_def]
+qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def]
"(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
(fn prems =>
[
@@ -112,7 +112,7 @@
(atac 1)
]);
-val inject_Sinr_Rep1 = prove_goalw Ssum0.thy [Sinr_Rep_def]
+qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def]
"(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
(fn prems =>
[
@@ -124,7 +124,7 @@
(atac 1)
]);
-val inject_Sinl_Rep2 = prove_goalw Ssum0.thy [Sinl_Rep_def]
+qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def]
"[|~a1=UU ; ~a2=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
(fn prems =>
[
@@ -134,7 +134,7 @@
(resolve_tac prems 1)
]);
-val inject_Sinr_Rep2 = prove_goalw Ssum0.thy [Sinr_Rep_def]
+qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def]
"[|~b1=UU ; ~b2=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
(fn prems =>
[
@@ -144,7 +144,7 @@
(resolve_tac prems 1)
]);
-val inject_Sinl_Rep = prove_goal Ssum0.thy
+qed_goal "inject_Sinl_Rep" Ssum0.thy
"Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
(fn prems =>
[
@@ -161,7 +161,7 @@
(atac 1)
]);
-val inject_Sinr_Rep = prove_goal Ssum0.thy
+qed_goal "inject_Sinr_Rep" Ssum0.thy
"Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
(fn prems =>
[
@@ -178,7 +178,7 @@
(atac 1)
]);
-val inject_Isinl = prove_goalw Ssum0.thy [Isinl_def]
+qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
"Isinl(a1)=Isinl(a2)==> a1=a2"
(fn prems =>
[
@@ -189,7 +189,7 @@
(rtac SsumIl 1)
]);
-val inject_Isinr = prove_goalw Ssum0.thy [Isinr_def]
+qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
"Isinr(b1)=Isinr(b2) ==> b1=b2"
(fn prems =>
[
@@ -200,7 +200,7 @@
(rtac SsumIr 1)
]);
-val inject_Isinl_rev = prove_goal Ssum0.thy
+qed_goal "inject_Isinl_rev" Ssum0.thy
"~a1=a2 ==> ~Isinl(a1) = Isinl(a2)"
(fn prems =>
[
@@ -210,7 +210,7 @@
(atac 1)
]);
-val inject_Isinr_rev = prove_goal Ssum0.thy
+qed_goal "inject_Isinr_rev" Ssum0.thy
"~b1=b2 ==> ~Isinr(b1) = Isinr(b2)"
(fn prems =>
[
@@ -225,7 +225,7 @@
(* choice of the bottom representation is arbitrary *)
(* ------------------------------------------------------------------------ *)
-val Exh_Ssum = prove_goalw Ssum0.thy [Isinl_def,Isinr_def]
+qed_goalw "Exh_Ssum" Ssum0.thy [Isinl_def,Isinr_def]
"z=Isinl(UU) | (? a. z=Isinl(a) & ~a=UU) | (? b. z=Isinr(b) & ~b=UU)"
(fn prems =>
[
@@ -270,7 +270,7 @@
(* elimination rules for the strict sum ++ *)
(* ------------------------------------------------------------------------ *)
-val IssumE = prove_goal Ssum0.thy
+qed_goal "IssumE" Ssum0.thy
"[|p=Isinl(UU) ==> Q ;\
\ !!x.[|p=Isinl(x); ~x=UU |] ==> Q;\
\ !!y.[|p=Isinr(y); ~y=UU |] ==> Q|] ==> Q"
@@ -289,7 +289,7 @@
(atac 1)
]);
-val IssumE2 = prove_goal Ssum0.thy
+qed_goal "IssumE2" Ssum0.thy
"[| !!x. [| p = Isinl(x) |] ==> Q; !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
(fn prems =>
[
@@ -306,7 +306,7 @@
(* rewrites for Iwhen *)
(* ------------------------------------------------------------------------ *)
-val Iwhen1 = prove_goalw Ssum0.thy [Iwhen_def]
+qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def]
"Iwhen(f)(g)(Isinl(UU)) = UU"
(fn prems =>
[
@@ -331,7 +331,7 @@
]);
-val Iwhen2 = prove_goalw Ssum0.thy [Iwhen_def]
+qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def]
"~x=UU ==> Iwhen(f)(g)(Isinl(x)) = f[x]"
(fn prems =>
[
@@ -357,7 +357,7 @@
(fast_tac HOL_cs 1)
]);
-val Iwhen3 = prove_goalw Ssum0.thy [Iwhen_def]
+qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def]
"~y=UU ==> Iwhen(f)(g)(Isinr(y)) = g[y]"
(fn prems =>
[
--- a/src/HOLCF/Ssum1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Ssum1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -212,7 +212,7 @@
(* optimize lemmas about less_ssum *)
(* ------------------------------------------------------------------------ *)
-val less_ssum2a = prove_goal Ssum1.thy
+qed_goal "less_ssum2a" Ssum1.thy
"less_ssum(Isinl(x),Isinl(y)) = (x << y)"
(fn prems =>
[
@@ -221,7 +221,7 @@
(rtac refl 1)
]);
-val less_ssum2b = prove_goal Ssum1.thy
+qed_goal "less_ssum2b" Ssum1.thy
"less_ssum(Isinr(x),Isinr(y)) = (x << y)"
(fn prems =>
[
@@ -230,7 +230,7 @@
(rtac refl 1)
]);
-val less_ssum2c = prove_goal Ssum1.thy
+qed_goal "less_ssum2c" Ssum1.thy
"less_ssum(Isinl(x),Isinr(y)) = (x = UU)"
(fn prems =>
[
@@ -239,7 +239,7 @@
(rtac refl 1)
]);
-val less_ssum2d = prove_goal Ssum1.thy
+qed_goal "less_ssum2d" Ssum1.thy
"less_ssum(Isinr(x),Isinl(y)) = (x = UU)"
(fn prems =>
[
@@ -253,7 +253,7 @@
(* less_ssum is a partial order on ++ *)
(* ------------------------------------------------------------------------ *)
-val refl_less_ssum = prove_goal Ssum1.thy "less_ssum(p,p)"
+qed_goal "refl_less_ssum" Ssum1.thy "less_ssum(p,p)"
(fn prems =>
[
(res_inst_tac [("p","p")] IssumE2 1),
@@ -265,7 +265,7 @@
(rtac refl_less 1)
]);
-val antisym_less_ssum = prove_goal Ssum1.thy
+qed_goal "antisym_less_ssum" Ssum1.thy
"[|less_ssum(p1,p2);less_ssum(p2,p1)|] ==> p1=p2"
(fn prems =>
[
@@ -295,7 +295,7 @@
(etac (less_ssum2b RS iffD1) 1)
]);
-val trans_less_ssum = prove_goal Ssum1.thy
+qed_goal "trans_less_ssum" Ssum1.thy
"[|less_ssum(p1,p2);less_ssum(p2,p3)|] ==> less_ssum(p1,p3)"
(fn prems =>
[
--- a/src/HOLCF/Ssum2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Ssum2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* access to less_ssum in class po *)
(* ------------------------------------------------------------------------ *)
-val less_ssum3a = prove_goal Ssum2.thy
+qed_goal "less_ssum3a" Ssum2.thy
"(Isinl(x) << Isinl(y)) = (x << y)"
(fn prems =>
[
@@ -20,7 +20,7 @@
(rtac less_ssum2a 1)
]);
-val less_ssum3b = prove_goal Ssum2.thy
+qed_goal "less_ssum3b" Ssum2.thy
"(Isinr(x) << Isinr(y)) = (x << y)"
(fn prems =>
[
@@ -28,7 +28,7 @@
(rtac less_ssum2b 1)
]);
-val less_ssum3c = prove_goal Ssum2.thy
+qed_goal "less_ssum3c" Ssum2.thy
"(Isinl(x) << Isinr(y)) = (x = UU)"
(fn prems =>
[
@@ -36,7 +36,7 @@
(rtac less_ssum2c 1)
]);
-val less_ssum3d = prove_goal Ssum2.thy
+qed_goal "less_ssum3d" Ssum2.thy
"(Isinr(x) << Isinl(y)) = (x = UU)"
(fn prems =>
[
@@ -49,7 +49,7 @@
(* type ssum ++ is pointed *)
(* ------------------------------------------------------------------------ *)
-val minimal_ssum = prove_goal Ssum2.thy "Isinl(UU) << s"
+qed_goal "minimal_ssum" Ssum2.thy "Isinl(UU) << s"
(fn prems =>
[
(res_inst_tac [("p","s")] IssumE2 1),
@@ -67,14 +67,14 @@
(* Isinl, Isinr are monotone *)
(* ------------------------------------------------------------------------ *)
-val monofun_Isinl = prove_goalw Ssum2.thy [monofun] "monofun(Isinl)"
+qed_goalw "monofun_Isinl" Ssum2.thy [monofun] "monofun(Isinl)"
(fn prems =>
[
(strip_tac 1),
(etac (less_ssum3a RS iffD2) 1)
]);
-val monofun_Isinr = prove_goalw Ssum2.thy [monofun] "monofun(Isinr)"
+qed_goalw "monofun_Isinr" Ssum2.thy [monofun] "monofun(Isinr)"
(fn prems =>
[
(strip_tac 1),
@@ -87,7 +87,7 @@
(* ------------------------------------------------------------------------ *)
-val monofun_Iwhen1 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen)"
+qed_goalw "monofun_Iwhen1" Ssum2.thy [monofun] "monofun(Iwhen)"
(fn prems =>
[
(strip_tac 1),
@@ -103,7 +103,7 @@
(asm_simp_tac Ssum_ss 1)
]);
-val monofun_Iwhen2 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f))"
+qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))"
(fn prems =>
[
(strip_tac 1),
@@ -117,7 +117,7 @@
(etac monofun_cfun_fun 1)
]);
-val monofun_Iwhen3 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f)(g))"
+qed_goalw "monofun_Iwhen3" Ssum2.thy [monofun] "monofun(Iwhen(f)(g))"
(fn prems =>
[
(strip_tac 1),
@@ -165,7 +165,7 @@
(* ------------------------------------------------------------------------ *)
-val ssum_lemma1 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma1" Ssum2.thy
"[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.~Y(i)=Isinl(x))"
(fn prems =>
[
@@ -173,7 +173,7 @@
(fast_tac HOL_cs 1)
]);
-val ssum_lemma2 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma2" Ssum2.thy
"[|(? i.!x.~(Y::nat => 'a++'b)(i::nat)=Isinl(x::'a))|] ==>\
\ (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & ~y=UU)"
(fn prems =>
@@ -189,7 +189,7 @@
]);
-val ssum_lemma3 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma3" Ssum2.thy
"[|is_chain(Y);(? i x. Y(i)=Isinr(x) & ~x=UU)|] ==> (!i.? y.Y(i)=Isinr(y))"
(fn prems =>
[
@@ -227,7 +227,7 @@
(atac 1)
]);
-val ssum_lemma4 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma4" Ssum2.thy
"is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))"
(fn prems =>
[
@@ -245,7 +245,7 @@
(* restricted surjectivity of Isinl *)
(* ------------------------------------------------------------------------ *)
-val ssum_lemma5 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma5" Ssum2.thy
"z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z"
(fn prems =>
[
@@ -260,7 +260,7 @@
(* restricted surjectivity of Isinr *)
(* ------------------------------------------------------------------------ *)
-val ssum_lemma6 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma6" Ssum2.thy
"z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z"
(fn prems =>
[
@@ -275,7 +275,7 @@
(* technical lemmas *)
(* ------------------------------------------------------------------------ *)
-val ssum_lemma7 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma7" Ssum2.thy
"[|Isinl(x) << z; ~x=UU|] ==> ? y.z=Isinl(y) & ~y=UU"
(fn prems =>
[
@@ -293,7 +293,7 @@
(atac 1)
]);
-val ssum_lemma8 = prove_goal Ssum2.thy
+qed_goal "ssum_lemma8" Ssum2.thy
"[|Isinr(x) << z; ~x=UU|] ==> ? y.z=Isinr(y) & ~y=UU"
(fn prems =>
[
@@ -313,7 +313,7 @@
(* the type 'a ++ 'b is a cpo in three steps *)
(* ------------------------------------------------------------------------ *)
-val lub_ssum1a = prove_goal Ssum2.thy
+qed_goal "lub_ssum1a" Ssum2.thy
"[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\
\ range(Y) <<|\
\ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y(i)))))"
@@ -354,7 +354,7 @@
]);
-val lub_ssum1b = prove_goal Ssum2.thy
+qed_goal "lub_ssum1b" Ssum2.thy
"[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\
\ range(Y) <<|\
\ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y(i)))))"
@@ -403,7 +403,7 @@
(* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinr(x) |] ==> *)
(* lub(range(?Y1)) = Isinr(lub(range(%i. Iwhen(LAM y. UU,LAM x. x,?Y1(i)))))*)
-val cpo_ssum = prove_goal Ssum2.thy
+qed_goal "cpo_ssum" Ssum2.thy
"is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x"
(fn prems =>
[
--- a/src/HOLCF/Ssum3.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Ssum3.ML Tue Feb 07 11:59:32 1995 +0100
@@ -13,7 +13,7 @@
(* ------------------------------------------------------------------------ *)
-val contlub_Isinl = prove_goal Ssum3.thy "contlub(Isinl)"
+qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)"
(fn prems =>
[
(rtac contlubI 1),
@@ -45,7 +45,7 @@
(asm_simp_tac Ssum_ss 1)
]);
-val contlub_Isinr = prove_goal Ssum3.thy "contlub(Isinr)"
+qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
(fn prems =>
[
(rtac contlubI 1),
@@ -76,7 +76,7 @@
(asm_simp_tac Ssum_ss 1)
]);
-val contX_Isinl = prove_goal Ssum3.thy "contX(Isinl)"
+qed_goal "contX_Isinl" Ssum3.thy "contX(Isinl)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -84,7 +84,7 @@
(rtac contlub_Isinl 1)
]);
-val contX_Isinr = prove_goal Ssum3.thy "contX(Isinr)"
+qed_goal "contX_Isinr" Ssum3.thy "contX(Isinr)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -97,7 +97,7 @@
(* continuity for Iwhen in the firts two arguments *)
(* ------------------------------------------------------------------------ *)
-val contlub_Iwhen1 = prove_goal Ssum3.thy "contlub(Iwhen)"
+qed_goal "contlub_Iwhen1" Ssum3.thy "contlub(Iwhen)"
(fn prems =>
[
(rtac contlubI 1),
@@ -122,7 +122,7 @@
(rtac (lub_const RS thelubI RS sym) 1)
]);
-val contlub_Iwhen2 = prove_goal Ssum3.thy "contlub(Iwhen(f))"
+qed_goal "contlub_Iwhen2" Ssum3.thy "contlub(Iwhen(f))"
(fn prems =>
[
(rtac contlubI 1),
@@ -149,7 +149,7 @@
(* first 5 ugly lemmas *)
(* ------------------------------------------------------------------------ *)
-val ssum_lemma9 = prove_goal Ssum3.thy
+qed_goal "ssum_lemma9" Ssum3.thy
"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)"
(fn prems =>
[
@@ -167,7 +167,7 @@
]);
-val ssum_lemma10 = prove_goal Ssum3.thy
+qed_goal "ssum_lemma10" Ssum3.thy
"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)"
(fn prems =>
[
@@ -186,7 +186,7 @@
(etac is_ub_thelub 1)
]);
-val ssum_lemma11 = prove_goal Ssum3.thy
+qed_goal "ssum_lemma11" Ssum3.thy
"[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
\ Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))"
(fn prems =>
@@ -203,7 +203,7 @@
(asm_simp_tac Ssum_ss 1)
]);
-val ssum_lemma12 = prove_goal Ssum3.thy
+qed_goal "ssum_lemma12" Ssum3.thy
"[| is_chain(Y); lub(range(Y)) = Isinl(x); ~ x = UU |] ==>\
\ Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))"
(fn prems =>
@@ -262,7 +262,7 @@
]);
-val ssum_lemma13 = prove_goal Ssum3.thy
+qed_goal "ssum_lemma13" Ssum3.thy
"[| is_chain(Y); lub(range(Y)) = Isinr(x); ~ x = UU |] ==>\
\ Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))"
(fn prems =>
@@ -326,7 +326,7 @@
]);
-val contlub_Iwhen3 = prove_goal Ssum3.thy "contlub(Iwhen(f)(g))"
+qed_goal "contlub_Iwhen3" Ssum3.thy "contlub(Iwhen(f)(g))"
(fn prems =>
[
(rtac contlubI 1),
@@ -342,7 +342,7 @@
(atac 1)
]);
-val contX_Iwhen1 = prove_goal Ssum3.thy "contX(Iwhen)"
+qed_goal "contX_Iwhen1" Ssum3.thy "contX(Iwhen)"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -350,7 +350,7 @@
(rtac contlub_Iwhen1 1)
]);
-val contX_Iwhen2 = prove_goal Ssum3.thy "contX(Iwhen(f))"
+qed_goal "contX_Iwhen2" Ssum3.thy "contX(Iwhen(f))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -358,7 +358,7 @@
(rtac contlub_Iwhen2 1)
]);
-val contX_Iwhen3 = prove_goal Ssum3.thy "contX(Iwhen(f)(g))"
+qed_goal "contX_Iwhen3" Ssum3.thy "contX(Iwhen(f)(g))"
(fn prems =>
[
(rtac monocontlub2contX 1),
@@ -370,21 +370,21 @@
(* continuous versions of lemmas for 'a ++ 'b *)
(* ------------------------------------------------------------------------ *)
-val strict_sinl = prove_goalw Ssum3.thy [sinl_def] "sinl[UU]=UU"
+qed_goalw "strict_sinl" Ssum3.thy [sinl_def] "sinl[UU]=UU"
(fn prems =>
[
(simp_tac (Ssum_ss addsimps [contX_Isinl]) 1),
(rtac (inst_ssum_pcpo RS sym) 1)
]);
-val strict_sinr = prove_goalw Ssum3.thy [sinr_def] "sinr[UU]=UU"
+qed_goalw "strict_sinr" Ssum3.thy [sinr_def] "sinr[UU]=UU"
(fn prems =>
[
(simp_tac (Ssum_ss addsimps [contX_Isinr]) 1),
(rtac (inst_ssum_pcpo RS sym) 1)
]);
-val noteq_sinlsinr = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "noteq_sinlsinr" Ssum3.thy [sinl_def,sinr_def]
"sinl[a]=sinr[b] ==> a=UU & b=UU"
(fn prems =>
[
@@ -395,7 +395,7 @@
(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
]);
-val inject_sinl = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "inject_sinl" Ssum3.thy [sinl_def,sinr_def]
"sinl[a1]=sinl[a2]==> a1=a2"
(fn prems =>
[
@@ -406,7 +406,7 @@
(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
]);
-val inject_sinr = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "inject_sinr" Ssum3.thy [sinl_def,sinr_def]
"sinr[a1]=sinr[a2]==> a1=a2"
(fn prems =>
[
@@ -418,7 +418,7 @@
]);
-val defined_sinl = prove_goal Ssum3.thy
+qed_goal "defined_sinl" Ssum3.thy
"~x=UU ==> ~sinl[x]=UU"
(fn prems =>
[
@@ -429,7 +429,7 @@
(etac notnotD 1)
]);
-val defined_sinr = prove_goal Ssum3.thy
+qed_goal "defined_sinr" Ssum3.thy
"~x=UU ==> ~sinr[x]=UU"
(fn prems =>
[
@@ -440,7 +440,7 @@
(etac notnotD 1)
]);
-val Exh_Ssum1 = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "Exh_Ssum1" Ssum3.thy [sinl_def,sinr_def]
"z=UU | (? a. z=sinl[a] & ~a=UU) | (? b. z=sinr[b] & ~b=UU)"
(fn prems =>
[
@@ -450,7 +450,7 @@
]);
-val ssumE = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "ssumE" Ssum3.thy [sinl_def,sinr_def]
"[|p=UU ==> Q ;\
\ !!x.[|p=sinl[x]; ~x=UU |] ==> Q;\
\ !!y.[|p=sinr[y]; ~y=UU |] ==> Q|] ==> Q"
@@ -469,7 +469,7 @@
]);
-val ssumE2 = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "ssumE2" Ssum3.thy [sinl_def,sinr_def]
"[|!!x.[|p=sinl[x]|] ==> Q;\
\ !!y.[|p=sinr[y]|] ==> Q|] ==> Q"
(fn prems =>
@@ -485,7 +485,7 @@
(atac 1)
]);
-val when1 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def]
+qed_goalw "when1" Ssum3.thy [when_def,sinl_def,sinr_def]
"when[f][g][UU] = UU"
(fn prems =>
[
@@ -502,7 +502,7 @@
(simp_tac Ssum_ss 1)
]);
-val when2 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def]
+qed_goalw "when2" Ssum3.thy [when_def,sinl_def,sinr_def]
"~x=UU==>when[f][g][sinl[x]] = f[x]"
(fn prems =>
[
@@ -524,7 +524,7 @@
-val when3 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def]
+qed_goalw "when3" Ssum3.thy [when_def,sinl_def,sinr_def]
"~x=UU==>when[f][g][sinr[x]] = g[x]"
(fn prems =>
[
@@ -545,7 +545,7 @@
]);
-val less_ssum4a = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "less_ssum4a" Ssum3.thy [sinl_def,sinr_def]
"(sinl[x] << sinl[y]) = (x << y)"
(fn prems =>
[
@@ -558,7 +558,7 @@
(rtac less_ssum3a 1)
]);
-val less_ssum4b = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "less_ssum4b" Ssum3.thy [sinl_def,sinr_def]
"(sinr[x] << sinr[y]) = (x << y)"
(fn prems =>
[
@@ -571,7 +571,7 @@
(rtac less_ssum3b 1)
]);
-val less_ssum4c = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "less_ssum4c" Ssum3.thy [sinl_def,sinr_def]
"(sinl[x] << sinr[y]) = (x = UU)"
(fn prems =>
[
@@ -584,7 +584,7 @@
(rtac less_ssum3c 1)
]);
-val less_ssum4d = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "less_ssum4d" Ssum3.thy [sinl_def,sinr_def]
"(sinr[x] << sinl[y]) = (x = UU)"
(fn prems =>
[
@@ -597,7 +597,7 @@
(rtac less_ssum3d 1)
]);
-val ssum_chainE = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def]
"is_chain(Y) ==> (!i.? x.Y(i)=sinl[x])|(!i.? y.Y(i)=sinr[y])"
(fn prems =>
[
@@ -607,7 +607,7 @@
]);
-val thelub_ssum2a = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def]
+qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,when_def]
"[| is_chain(Y); !i.? x. Y(i) = sinl[x] |] ==>\
\ lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]"
(fn prems =>
@@ -632,7 +632,7 @@
(asm_simp_tac (Ssum_ss addsimps [contX_Isinl]) 1)
]);
-val thelub_ssum2b = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def]
+qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,when_def]
"[| is_chain(Y); !i.? x. Y(i) = sinr[x] |] ==>\
\ lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]"
(fn prems =>
@@ -663,7 +663,7 @@
contX_Iwhen3]) 1)
]);
-val thelub_ssum2a_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def]
"[| is_chain(Y); lub(range(Y)) = sinl[x]|] ==> !i.? x.Y(i)=sinl[x]"
(fn prems =>
[
@@ -677,7 +677,7 @@
contX_Iwhen3]) 1)
]);
-val thelub_ssum2b_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def]
+qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def]
"[| is_chain(Y); lub(range(Y)) = sinr[x]|] ==> !i.? x.Y(i)=sinr[x]"
(fn prems =>
[
@@ -691,7 +691,7 @@
contX_Iwhen3]) 1)
]);
-val thelub_ssum3 = prove_goal Ssum3.thy
+qed_goal "thelub_ssum3" Ssum3.thy
"is_chain(Y) ==>\
\ lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]\
\ | lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]"
@@ -709,7 +709,7 @@
]);
-val when4 = prove_goal Ssum3.thy
+qed_goal "when4" Ssum3.thy
"when[sinl][sinr][z]=z"
(fn prems =>
[
--- a/src/HOLCF/Stream.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Stream.ML Tue Feb 07 11:59:32 1995 +0100
@@ -43,7 +43,7 @@
(* Exhaustion and elimination for streams *)
(* ------------------------------------------------------------------------*)
-val Exh_stream = prove_goalw Stream.thy [scons_def]
+qed_goalw "Exh_stream" Stream.thy [scons_def]
"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
(fn prems =>
[
@@ -61,7 +61,7 @@
(asm_simp_tac HOLCF_ss 1)
]);
-val streamE = prove_goal Stream.thy
+qed_goal "streamE" Stream.thy
"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
(fn prems =>
[
@@ -269,7 +269,7 @@
(* enhance the simplifier *)
(* ------------------------------------------------------------------------*)
-val stream_copy2 = prove_goal Stream.thy
+qed_goal "stream_copy2" Stream.thy
"stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
(fn prems =>
[
@@ -278,7 +278,7 @@
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
]);
-val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
+qed_goal "shd2" Stream.thy "shd[scons[x][xs]]=x"
(fn prems =>
[
(res_inst_tac [("Q","x=UU")] classical2 1),
@@ -286,7 +286,7 @@
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
]);
-val stream_take2 = prove_goal Stream.thy
+qed_goal "stream_take2" Stream.thy
"stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
(fn prems =>
[
@@ -330,7 +330,7 @@
"(!!n.stream_take(n)[s1]=stream_take(n)[s2]) ==> s1=s2";
-val stream_reach2 = prove_goal Stream.thy "lub(range(%i.stream_take(i)[s]))=s"
+qed_goal "stream_reach2" Stream.thy "lub(range(%i.stream_take(i)[s]))=s"
(fn prems =>
[
(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
@@ -345,7 +345,7 @@
(* Co -induction for streams *)
(* ------------------------------------------------------------------------*)
-val stream_coind_lemma = prove_goalw Stream.thy [stream_bisim_def]
+qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def]
"stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_take(n)[q]"
(fn prems =>
[
@@ -365,7 +365,7 @@
(fast_tac HOL_cs 1)
]);
-val stream_coind = prove_goal Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
+qed_goal "stream_coind" Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
(fn prems =>
[
(rtac stream_take_lemma 1),
@@ -378,7 +378,7 @@
(* structural induction for admissible predicates *)
(* ------------------------------------------------------------------------*)
-val stream_finite_ind = prove_goal Stream.thy
+qed_goal "stream_finite_ind" Stream.thy
"[|P(UU);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
\ |] ==> !s.P(stream_take(n)[s])"
@@ -397,7 +397,7 @@
(etac spec 1)
]);
-val stream_finite_ind2 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_ind2" Stream.thy [stream_finite_def]
"(!!n.P(stream_take(n)[s])) ==> stream_finite(s) -->P(s)"
(fn prems =>
[
@@ -407,7 +407,7 @@
(resolve_tac prems 1)
]);
-val stream_finite_ind3 = prove_goal Stream.thy
+qed_goal "stream_finite_ind3" Stream.thy
"[|P(UU);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
\ |] ==> stream_finite(s) --> P(s)"
@@ -423,7 +423,7 @@
stream_reach rsp. stream_reach2
and finite induction stream_finite_ind *)
-val stream_ind = prove_goal Stream.thy
+qed_goal "stream_ind" Stream.thy
"[|adm(P);\
\ P(UU);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
@@ -443,7 +443,7 @@
]);
(* prove induction with usual LCF-Method using fixed point induction *)
-val stream_ind = prove_goal Stream.thy
+qed_goal "stream_ind" Stream.thy
"[|adm(P);\
\ P(UU);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
@@ -469,7 +469,7 @@
(* simplify use of Co-induction *)
(* ------------------------------------------------------------------------*)
-val surjectiv_scons = prove_goal Stream.thy "scons[shd[s]][stl[s]]=s"
+qed_goal "surjectiv_scons" Stream.thy "scons[shd[s]][stl[s]]=s"
(fn prems =>
[
(res_inst_tac [("s","s")] streamE 1),
@@ -478,7 +478,7 @@
]);
-val stream_coind_lemma2 = prove_goalw Stream.thy [stream_bisim_def]
+qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
"!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
(fn prems =>
[
@@ -523,7 +523,7 @@
(* 2 lemmas about stream_finite *)
(* ----------------------------------------------------------------------- *)
-val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
"stream_finite(UU)"
(fn prems =>
[
@@ -531,7 +531,7 @@
(simp_tac (HOLCF_ss addsimps stream_rews) 1)
]);
-val inf_stream_not_UU = prove_goal Stream.thy "~stream_finite(s) ==> s ~= UU"
+qed_goal "inf_stream_not_UU" Stream.thy "~stream_finite(s) ==> s ~= UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -545,7 +545,7 @@
(* a lemma about shd *)
(* ----------------------------------------------------------------------- *)
-val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
+qed_goal "stream_shd_lemma1" Stream.thy "shd[s]=UU --> s=UU"
(fn prems =>
[
(res_inst_tac [("s","s")] streamE 1),
@@ -559,7 +559,7 @@
(* lemmas about stream_take *)
(* ----------------------------------------------------------------------- *)
-val stream_take_lemma1 = prove_goal Stream.thy
+qed_goal "stream_take_lemma1" Stream.thy
"!x xs.x~=UU --> \
\ stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
(fn prems =>
@@ -576,7 +576,7 @@
]);
-val stream_take_lemma2 = prove_goal Stream.thy
+qed_goal "stream_take_lemma2" Stream.thy
"! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
(fn prems =>
[
@@ -599,7 +599,7 @@
(fast_tac HOL_cs 1)
]);
-val stream_take_lemma3 = prove_goal Stream.thy
+qed_goal "stream_take_lemma3" Stream.thy
"!x xs.x~=UU --> \
\ stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
(fn prems =>
@@ -618,7 +618,7 @@
(etac (stream_take2 RS subst) 1)
]);
-val stream_take_lemma4 = prove_goal Stream.thy
+qed_goal "stream_take_lemma4" Stream.thy
"!x xs.\
\stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
(fn prems =>
@@ -630,7 +630,7 @@
(* ---- *)
-val stream_take_lemma5 = prove_goal Stream.thy
+qed_goal "stream_take_lemma5" Stream.thy
"!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
(fn prems =>
[
@@ -651,7 +651,7 @@
(atac 1)
]);
-val stream_take_lemma6 = prove_goal Stream.thy
+qed_goal "stream_take_lemma6" Stream.thy
"!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
(fn prems =>
[
@@ -668,7 +668,7 @@
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
]);
-val stream_take_lemma7 = prove_goal Stream.thy
+qed_goal "stream_take_lemma7" Stream.thy
"(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
(fn prems =>
[
@@ -678,7 +678,7 @@
]);
-val stream_take_lemma8 = prove_goal Stream.thy
+qed_goal "stream_take_lemma8" Stream.thy
"[|adm(P); !n. ? m. n < m & P(stream_take(m)[s])|] ==> P(s)"
(fn prems =>
[
@@ -696,7 +696,7 @@
(* lemmas stream_finite *)
(* ----------------------------------------------------------------------- *)
-val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
"stream_finite(xs) ==> stream_finite(scons[x][xs])"
(fn prems =>
[
@@ -706,7 +706,7 @@
(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
]);
-val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
"[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
(fn prems =>
[
@@ -717,7 +717,7 @@
(atac 1)
]);
-val stream_finite_lemma3 = prove_goal Stream.thy
+qed_goal "stream_finite_lemma3" Stream.thy
"x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
(fn prems =>
[
@@ -729,7 +729,7 @@
]);
-val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
"(!n. s1 << s2 --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
\=(s1 << s2 --> stream_finite(s2) --> stream_finite(s1))"
(fn prems =>
@@ -739,7 +739,7 @@
(fast_tac HOL_cs 1)
]);
-val stream_finite_lemma6 = prove_goal Stream.thy
+qed_goal "stream_finite_lemma6" Stream.thy
"!s1 s2. s1 << s2 --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
(fn prems =>
[
@@ -781,7 +781,7 @@
(atac 1)
]);
-val stream_finite_lemma7 = prove_goal Stream.thy
+qed_goal "stream_finite_lemma7" Stream.thy
"s1 << s2 --> stream_finite(s2) --> stream_finite(s1)"
(fn prems =>
[
@@ -790,7 +790,7 @@
(rtac (stream_finite_lemma6 RS spec RS spec) 1)
]);
-val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
+qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
"stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
(fn prems =>
[
@@ -802,7 +802,7 @@
(* admissibility of ~stream_finite *)
(* ----------------------------------------------------------------------- *)
-val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
+qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
"adm(%s. ~ stream_finite(s))"
(fn prems =>
[
@@ -825,7 +825,7 @@
(* ----------------------------------------------------------------------- *)
-val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
+qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
(fn prems =>
[
(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
--- a/src/HOLCF/Stream2.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Stream2.ML Tue Feb 07 11:59:32 1995 +0100
@@ -21,14 +21,14 @@
(* ------------------------------------------------------------------------- *)
-val smap1 = prove_goal Stream2.thy "smap[f][UU] = UU"
+qed_goal "smap1" Stream2.thy "smap[f][UU] = UU"
(fn prems =>
[
(rtac (smap_def2 RS ssubst) 1),
(simp_tac (HOLCF_ss addsimps stream_when) 1)
]);
-val smap2 = prove_goal Stream2.thy
+qed_goal "smap2" Stream2.thy
"x~=UU ==> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]"
(fn prems =>
[
--- a/src/HOLCF/Tr1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Tr1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -77,7 +77,7 @@
(* Exhaustion and elimination for type tr *)
(* ------------------------------------------------------------------------ *)
-val Exh_tr = prove_goalw Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
+qed_goalw "Exh_tr" Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
(fn prems =>
[
(res_inst_tac [("p","rep_tr[t]")] ssumE 1),
@@ -107,7 +107,7 @@
]);
-val trE = prove_goal Tr1.thy
+qed_goal "trE" Tr1.thy
"[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
(fn prems =>
[
@@ -123,7 +123,7 @@
(* type tr is flat *)
(* ------------------------------------------------------------------------ *)
-val flat_tr = prove_goalw Tr1.thy [flat_def] "flat(TT)"
+qed_goalw "flat_tr" Tr1.thy [flat_def] "flat(TT)"
(fn prems =>
[
(rtac allI 1),
--- a/src/HOLCF/Void.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Void.ML Tue Feb 07 11:59:32 1995 +0100
@@ -15,7 +15,7 @@
(* A non-emptyness result for Void *)
(* ------------------------------------------------------------------------ *)
-val VoidI = prove_goalw Void.thy [UU_void_Rep_def,Void_def]
+qed_goalw "VoidI" Void.thy [UU_void_Rep_def,Void_def]
" UU_void_Rep : Void"
(fn prems =>
[
@@ -27,13 +27,13 @@
(* less_void is a partial ordering on void *)
(* ------------------------------------------------------------------------ *)
-val refl_less_void = prove_goalw Void.thy [ less_void_def ] "less_void(x,x)"
+qed_goalw "refl_less_void" Void.thy [ less_void_def ] "less_void(x,x)"
(fn prems =>
[
(fast_tac HOL_cs 1)
]);
-val antisym_less_void = prove_goalw Void.thy [ less_void_def ]
+qed_goalw "antisym_less_void" Void.thy [ less_void_def ]
"[|less_void(x,y); less_void(y,x)|] ==> x = y"
(fn prems =>
[
@@ -43,7 +43,7 @@
(rtac (Rep_Void_inverse RS sym) 1)
]);
-val trans_less_void = prove_goalw Void.thy [ less_void_def ]
+qed_goalw "trans_less_void" Void.thy [ less_void_def ]
"[|less_void(x,y); less_void(y,z)|] ==> less_void(x,z)"
(fn prems =>
[
@@ -56,7 +56,7 @@
(* every element in void is represented by UU_void_Rep *)
(* ------------------------------------------------------------------------ *)
-val unique_void = prove_goal Void.thy "Rep_Void(x) = UU_void_Rep"
+qed_goal "unique_void" Void.thy "Rep_Void(x) = UU_void_Rep"
(fn prems =>
[
(rtac (mem_Collect_eq RS subst) 1),
--- a/src/HOLCF/ccc1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/ccc1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -14,7 +14,7 @@
(* ------------------------------------------------------------------------ *)
-val ID1 = prove_goalw ccc1.thy [ID_def] "ID[x]=x"
+qed_goalw "ID1" ccc1.thy [ID_def] "ID[x]=x"
(fn prems =>
[
(rtac (beta_cfun RS ssubst) 1),
@@ -22,7 +22,7 @@
(rtac refl 1)
]);
-val cfcomp1 = prove_goalw ccc1.thy [oo_def] "(f oo g)=(LAM x.f[g[x]])"
+qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f[g[x]])"
(fn prems =>
[
(rtac (beta_cfun RS ssubst) 1),
@@ -32,7 +32,7 @@
(rtac refl 1)
]);
-val cfcomp2 = prove_goal ccc1.thy "(f oo g)[x]=f[g[x]]"
+qed_goal "cfcomp2" ccc1.thy "(f oo g)[x]=f[g[x]]"
(fn prems =>
[
(rtac (cfcomp1 RS ssubst) 1),
@@ -51,7 +51,7 @@
(* ------------------------------------------------------------------------ *)
-val ID2 = prove_goal ccc1.thy "f oo ID = f "
+qed_goal "ID2" ccc1.thy "f oo ID = f "
(fn prems =>
[
(rtac ext_cfun 1),
@@ -60,7 +60,7 @@
(rtac refl 1)
]);
-val ID3 = prove_goal ccc1.thy "ID oo f = f "
+qed_goal "ID3" ccc1.thy "ID oo f = f "
(fn prems =>
[
(rtac ext_cfun 1),
@@ -70,7 +70,7 @@
]);
-val assoc_oo = prove_goal ccc1.thy "f oo (g oo h) = (f oo g) oo h"
+qed_goal "assoc_oo" ccc1.thy "f oo (g oo h) = (f oo g) oo h"
(fn prems =>
[
(rtac ext_cfun 1),
--- a/src/HOLCF/ex/Coind.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/ex/Coind.ML Tue Feb 07 11:59:32 1995 +0100
@@ -24,7 +24,7 @@
(* ------------------------------------------------------------------------- *)
-val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
+qed_goal "from" Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
(fn prems =>
[
(rtac trans 1),
@@ -34,7 +34,7 @@
]);
-val from1 = prove_goal Coind.thy "from[UU] = UU"
+qed_goal "from1" Coind.thy "from[UU] = UU"
(fn prems =>
[
(rtac trans 1),
@@ -53,7 +53,7 @@
(* ------------------------------------------------------------------------- *)
-val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
+qed_goal "coind_lemma1" Coind.thy "iterator[n][smap[dsucc]][nats] =\
\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
(fn prems =>
[
@@ -74,7 +74,7 @@
]);
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+qed_goal "nats_eq_from" Coind.thy "nats = from[dzero]"
(fn prems =>
[
(res_inst_tac [("R",
@@ -105,7 +105,7 @@
(* another proof using stream_coind_lemma2 *)
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
+qed_goal "nats_eq_from" Coind.thy "nats = from[dzero]"
(fn prems =>
[
(res_inst_tac [("R","% p q.? n. p = \
--- a/src/HOLCF/ex/Dagstuhl.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/ex/Dagstuhl.ML Tue Feb 07 11:59:32 1995 +0100
@@ -20,14 +20,14 @@
by (rtac monofun_cfun_arg 1);
by (rtac monofun_cfun_arg 1);
by (atac 1);
-val lemma3 = result();
+qed "lemma3";
val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
by (rtac (YYS_def2 RS ssubst) 1);
back();
by (rtac monofun_cfun_arg 1);
by (rtac lemma3 1);
-val lemma4 = result();
+qed "lemma4";
(* val lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
@@ -35,7 +35,7 @@
by (rtac antisym_less 1);
by (rtac lemma4 1);
by (rtac lemma3 1);
-val lemma5 = result();
+qed "lemma5";
val prems = goal Dagstuhl.thy "YS = YYS";
by (rtac stream_take_lemma 1);
@@ -46,7 +46,7 @@
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
-val wir_moel = result();
+qed "wir_moel";
(* ------------------------------------------------------------------------ *)
(* Zweite L"osung: Bernhard M"oller *)
@@ -60,7 +60,7 @@
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
-val lemma6 = result();
+qed "lemma6";
val prems = goal Dagstuhl.thy "YS << YYS";
by (rtac (YS_def RS ssubst) 1);
@@ -72,7 +72,7 @@
by (contX_tacR 1);
by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
by (etac monofun_cfun_arg 1);
-val lemma7 = result();
+qed "lemma7";
val wir_moel = lemma6 RS (lemma7 RS antisym_less);
@@ -90,7 +90,7 @@
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (rtac refl 1);
-val lemma1 = result();
+qed "lemma1";
val prems = goal Stream2.thy
"(fix[ LAM z. scons[y][scons[y][z]]]) = \
@@ -101,7 +101,7 @@
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (rtac refl 1);
-val lemma2 = result();
+qed "lemma2";
val prems = goal Stream2.thy
"fix[LAM z. scons[y][scons[y][z]]] << \
@@ -114,7 +114,7 @@
by (rtac monofun_cfun_arg 1);
by (rtac monofun_cfun_arg 1);
by (atac 1);
-val lemma3 = result();
+qed "lemma3";
val prems = goal Stream2.thy
" scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
@@ -123,7 +123,7 @@
back();
by (rtac monofun_cfun_arg 1);
by (rtac lemma3 1);
-val lemma4 = result();
+qed "lemma4";
val prems = goal Stream2.thy
" scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
@@ -131,7 +131,7 @@
by (rtac antisym_less 1);
by (rtac lemma4 1);
by (rtac lemma3 1);
-val lemma5 = result();
+qed "lemma5";
val prems = goal Stream2.thy
"(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
@@ -143,7 +143,7 @@
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
-val wir_moel = result();
+qed "wir_moel";
--- a/src/HOLCF/ex/Hoare.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/ex/Hoare.ML Tue Feb 07 11:59:32 1995 +0100
@@ -8,7 +8,7 @@
(* --------- pure HOLCF logic, some little lemmas ------ *)
-val hoare_lemma2 = prove_goal HOLCF.thy "~b=TT ==> b=FF | b=UU"
+qed_goal "hoare_lemma2" HOLCF.thy "~b=TT ==> b=FF | b=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -19,14 +19,14 @@
(fast_tac HOL_cs 1)
]);
-val hoare_lemma3 = prove_goal HOLCF.thy
+qed_goal "hoare_lemma3" HOLCF.thy
" (!k.b1[iterate(k,g,x)]=TT) | (? k.~ b1[iterate(k,g,x)]=TT)"
(fn prems =>
[
(fast_tac HOL_cs 1)
]);
-val hoare_lemma4 = prove_goal HOLCF.thy
+qed_goal "hoare_lemma4" HOLCF.thy
"(? k.~ b1[iterate(k,g,x)]=TT) ==> \
\ ? k.b1[iterate(k,g,x)]=FF | b1[iterate(k,g,x)]=UU"
(fn prems =>
@@ -38,7 +38,7 @@
(atac 1)
]);
-val hoare_lemma5 = prove_goal HOLCF.thy
+qed_goal "hoare_lemma5" HOLCF.thy
"[|(? k.~ b1[iterate(k,g,x)]=TT);\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT)|] ==> \
\ b1[iterate(k,g,x)]=FF | b1[iterate(k,g,x)]=UU"
@@ -51,7 +51,7 @@
(etac theleast1 1)
]);
-val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> ~b=TT"
+qed_goal "hoare_lemma6" HOLCF.thy "b=UU ==> ~b=TT"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -59,7 +59,7 @@
(resolve_tac dist_eq_tr 1)
]);
-val hoare_lemma7 = prove_goal HOLCF.thy "b=FF ==> ~b=TT"
+qed_goal "hoare_lemma7" HOLCF.thy "b=FF ==> ~b=TT"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -67,7 +67,7 @@
(resolve_tac dist_eq_tr 1)
]);
-val hoare_lemma8 = prove_goal HOLCF.thy
+qed_goal "hoare_lemma8" HOLCF.thy
"[|(? k.~ b1[iterate(k,g,x)]=TT);\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT)|] ==> \
\ !m. m<k --> b1[iterate(m,g,x)]=TT"
@@ -89,7 +89,7 @@
(etac hoare_lemma7 1)
]);
-val hoare_lemma28 = prove_goal HOLCF.thy
+qed_goal "hoare_lemma28" HOLCF.thy
"b1[y::'a]=(UU::tr) ==> b1[UU] = UU"
(fn prems =>
[
@@ -102,14 +102,14 @@
(* ----- access to definitions ----- *)
-val p_def2 = prove_goalw Hoare.thy [p_def]
+qed_goalw "p_def2" Hoare.thy [p_def]
"p = fix[LAM f x. If b1[x] then f[g[x]] else x fi]"
(fn prems =>
[
(rtac refl 1)
]);
-val q_def2 = prove_goalw Hoare.thy [q_def]
+qed_goalw "q_def2" Hoare.thy [q_def]
"q = fix[LAM f x. If b1[x] orelse b2[x] then \
\ f[g[x]] else x fi]"
(fn prems =>
@@ -118,7 +118,7 @@
]);
-val p_def3 = prove_goal Hoare.thy
+qed_goal "p_def3" Hoare.thy
"p[x] = If b1[x] then p[g[x]] else x fi"
(fn prems =>
[
@@ -126,7 +126,7 @@
(simp_tac HOLCF_ss 1)
]);
-val q_def3 = prove_goal Hoare.thy
+qed_goal "q_def3" Hoare.thy
"q[x] = If b1[x] orelse b2[x] then q[g[x]] else x fi"
(fn prems =>
[
@@ -136,7 +136,7 @@
(** --------- proves about iterations of p and q ---------- **)
-val hoare_lemma9 = prove_goal Hoare.thy
+qed_goal "hoare_lemma9" Hoare.thy
"(! m. m<Suc(k) --> b1[iterate(m,g,x)]=TT) -->\
\ p[iterate(k,g,x)]=p[x]"
(fn prems =>
@@ -161,7 +161,7 @@
(simp_tac nat_ss 1)
]);
-val hoare_lemma24 = prove_goal Hoare.thy
+qed_goal "hoare_lemma24" Hoare.thy
"(! m. m<Suc(k) --> b1[iterate(m,g,x)]=TT) --> \
\ q[iterate(k,g,x)]=q[x]"
(fn prems =>
@@ -196,7 +196,7 @@
p[iterate(?k3,g,?x1)] = p[?x1]
*)
-val hoare_lemma11 = prove_goal Hoare.thy
+qed_goal "hoare_lemma11" Hoare.thy
"(? n.b1[iterate(n,g,x)]~=TT) ==>\
\ k=theleast(%n.b1[iterate(n,g,x)]~=TT) & b1[iterate(k,g,x)]=FF \
\ --> p[x] = iterate(k,g,x)"
@@ -235,7 +235,7 @@
(simp_tac HOLCF_ss 1)
]);
-val hoare_lemma12 = prove_goal Hoare.thy
+qed_goal "hoare_lemma12" Hoare.thy
"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
\ --> p[x] = UU"
@@ -273,7 +273,7 @@
(* -------- results about p for case (! k. b1[iterate(k,g,x)]=TT) ------- *)
-val fernpass_lemma = prove_goal Hoare.thy
+qed_goal "fernpass_lemma" Hoare.thy
"(! k. b1[iterate(k,g,x)]=TT) ==> !k.p[iterate(k,g,x)] = UU"
(fn prems =>
[
@@ -296,7 +296,7 @@
(etac spec 1)
]);
-val hoare_lemma16 = prove_goal Hoare.thy
+qed_goal "hoare_lemma16" Hoare.thy
"(! k. b1[iterate(k,g,x)]=TT) ==> p[x] = UU"
(fn prems =>
[
@@ -307,7 +307,7 @@
(* -------- results about q for case (! k. b1[iterate(k,g,x)]=TT) ------- *)
-val hoare_lemma17 = prove_goal Hoare.thy
+qed_goal "hoare_lemma17" Hoare.thy
"(! k. b1[iterate(k,g,x)]=TT) ==> !k.q[iterate(k,g,x)] = UU"
(fn prems =>
[
@@ -330,7 +330,7 @@
(etac spec 1)
]);
-val hoare_lemma18 = prove_goal Hoare.thy
+qed_goal "hoare_lemma18" Hoare.thy
"(! k. b1[iterate(k,g,x)]=TT) ==> q[x] = UU"
(fn prems =>
[
@@ -339,7 +339,7 @@
(etac (hoare_lemma17 RS spec) 1)
]);
-val hoare_lemma19 = prove_goal Hoare.thy
+qed_goal "hoare_lemma19" Hoare.thy
"(!k. (b1::'a->tr)[iterate(k,g,x)]=TT) ==> b1[UU::'a] = UU | (!y.b1[y::'a]=TT)"
(fn prems =>
[
@@ -349,7 +349,7 @@
(etac spec 1)
]);
-val hoare_lemma20 = prove_goal Hoare.thy
+qed_goal "hoare_lemma20" Hoare.thy
"(! y. b1[y::'a]=TT) ==> !k.q[iterate(k,g,x::'a)] = UU"
(fn prems =>
[
@@ -372,7 +372,7 @@
(etac spec 1)
]);
-val hoare_lemma21 = prove_goal Hoare.thy
+qed_goal "hoare_lemma21" Hoare.thy
"(! y. b1[y::'a]=TT) ==> q[x::'a] = UU"
(fn prems =>
[
@@ -381,7 +381,7 @@
(etac (hoare_lemma20 RS spec) 1)
]);
-val hoare_lemma22 = prove_goal Hoare.thy
+qed_goal "hoare_lemma22" Hoare.thy
"b1[UU::'a]=UU ==> q[UU::'a] = UU"
(fn prems =>
[
@@ -399,7 +399,7 @@
q[iterate(?k3,?g1,?x1)] = q[?x1]
*)
-val hoare_lemma26 = prove_goal Hoare.thy
+qed_goal "hoare_lemma26" Hoare.thy
"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=FF \
\ --> q[x] = q[iterate(k,g,x)]"
@@ -428,7 +428,7 @@
]);
-val hoare_lemma27 = prove_goal Hoare.thy
+qed_goal "hoare_lemma27" Hoare.thy
"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
\ --> q[x] = UU"
@@ -465,7 +465,7 @@
(* ------- (! k. b1[iterate(k,g,x)]=TT) ==> q o p = q ----- *)
-val hoare_lemma23 = prove_goal Hoare.thy
+qed_goal "hoare_lemma23" Hoare.thy
"(! k. b1[iterate(k,g,x)]=TT) ==> q[p[x]] = q[x]"
(fn prems =>
[
@@ -488,7 +488,7 @@
(* ------------ ? k. ~ b1[iterate(k,g,x)] = TT ==> q o p = q ----- *)
-val hoare_lemma29 = prove_goal Hoare.thy
+qed_goal "hoare_lemma29" Hoare.thy
"? k. ~ b1[iterate(k,g,x)] = TT ==> q[p[x]] = q[x]"
(fn prems =>
[
@@ -527,7 +527,7 @@
(* ------ the main prove q o p = q ------ *)
-val hoare_main = prove_goal Hoare.thy "q oo p = q"
+qed_goal "hoare_main" Hoare.thy "q oo p = q"
(fn prems =>
[
(rtac ext_cfun 1),
--- a/src/HOLCF/ex/Loop.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/ex/Loop.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,14 +12,14 @@
(* access to definitions *)
(* --------------------------------------------------------------------------- *)
-val step_def2 = prove_goalw Loop.thy [step_def]
+qed_goalw "step_def2" Loop.thy [step_def]
"step[b][g][x] = If b[x] then g[x] else x fi"
(fn prems =>
[
(simp_tac Cfun_ss 1)
]);
-val while_def2 = prove_goalw Loop.thy [while_def]
+qed_goalw "while_def2" Loop.thy [while_def]
"while[b][g] = fix[LAM f x. If b[x] then f[g[x]] else x fi]"
(fn prems =>
[
@@ -31,7 +31,7 @@
(* rekursive properties of while *)
(* ------------------------------------------------------------------------- *)
-val while_unfold = prove_goal Loop.thy
+qed_goal "while_unfold" Loop.thy
"while[b][g][x] = If b[x] then while[b][g][g[x]] else x fi"
(fn prems =>
[
@@ -39,7 +39,7 @@
(simp_tac Cfun_ss 1)
]);
-val while_unfold2 = prove_goal Loop.thy
+qed_goal "while_unfold2" Loop.thy
"!x.while[b][g][x] = while[b][g][iterate(k,step[b][g],x)]"
(fn prems =>
[
@@ -67,7 +67,7 @@
(asm_simp_tac HOLCF_ss 1)
]);
-val while_unfold3 = prove_goal Loop.thy
+qed_goal "while_unfold3" Loop.thy
"while[b][g][x] = while[b][g][step[b][g][x]]"
(fn prems =>
[
@@ -81,7 +81,7 @@
(* properties of while and iterations *)
(* --------------------------------------------------------------------------- *)
-val loop_lemma1 = prove_goal Loop.thy
+qed_goal "loop_lemma1" Loop.thy
"[|? y.b[y]=FF; iterate(k,step[b][g],x)=UU|]==>iterate(Suc(k),step[b][g],x)=UU"
(fn prems =>
[
@@ -96,7 +96,7 @@
(asm_simp_tac HOLCF_ss 1)
]);
-val loop_lemma2 = prove_goal Loop.thy
+qed_goal "loop_lemma2" Loop.thy
"[|? y.b[y]=FF;~iterate(Suc(k),step[b][g],x)=UU |]==>\
\~iterate(k,step[b][g],x)=UU"
(fn prems =>
@@ -108,7 +108,7 @@
(atac 1)
]);
-val loop_lemma3 = prove_goal Loop.thy
+qed_goal "loop_lemma3" Loop.thy
"[|!x. INV(x) & b[x]=TT & ~g[x]=UU --> INV(g[x]);\
\? y.b[y]=FF; INV(x)|] ==>\
\~iterate(k,step[b][g],x)=UU --> INV(iterate(k,step[b][g],x))"
@@ -134,7 +134,7 @@
]);
-val loop_lemma4 = prove_goal Loop.thy
+qed_goal "loop_lemma4" Loop.thy
"!x. b[iterate(k,step[b][g],x)]=FF --> while[b][g][x]=iterate(k,step[b][g],x)"
(fn prems =>
[
@@ -151,7 +151,7 @@
(asm_simp_tac HOLCF_ss 1)
]);
-val loop_lemma5 = prove_goal Loop.thy
+qed_goal "loop_lemma5" Loop.thy
"!k. ~b[iterate(k,step[b][g],x)]=FF ==>\
\ !m. while[b][g][iterate(m,step[b][g],x)]=UU"
(fn prems =>
@@ -179,7 +179,7 @@
]);
-val loop_lemma6 = prove_goal Loop.thy
+qed_goal "loop_lemma6" Loop.thy
"!k. ~b[iterate(k,step[b][g],x)]=FF ==> while[b][g][x]=UU"
(fn prems =>
[
@@ -188,7 +188,7 @@
(resolve_tac prems 1)
]);
-val loop_lemma7 = prove_goal Loop.thy
+qed_goal "loop_lemma7" Loop.thy
"~while[b][g][x]=UU ==> ? k. b[iterate(k,step[b][g],x)]=FF"
(fn prems =>
[
@@ -198,7 +198,7 @@
(fast_tac HOL_cs 1)
]);
-val loop_lemma8 = prove_goal Loop.thy
+qed_goal "loop_lemma8" Loop.thy
"~while[b][g][x]=UU ==> ? y. b[y]=FF"
(fn prems =>
[
@@ -212,7 +212,7 @@
(* an invariant rule for loops *)
(* --------------------------------------------------------------------------- *)
-val loop_inv2 = prove_goal Loop.thy
+qed_goal "loop_inv2" 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])"
@@ -239,7 +239,7 @@
(rtac refl 1)
]);
-val loop_inv3 = prove_goal Loop.thy
+qed_goal "loop_inv3" 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])"
@@ -261,7 +261,7 @@
(resolve_tac prems 1)
]);
-val loop_inv = prove_goal Loop.thy
+qed_goal "loop_inv" Loop.thy
"[| P(x);\
\ !!y.P(y) ==> INV(y);\
\ !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\