--- a/src/HOLCF/Lift2.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/Lift2.ML Thu Apr 13 14:25:45 1995 +0200
@@ -69,14 +69,12 @@
(asm_simp_tac Lift_ss 1),
(res_inst_tac [("p","y")] liftE 1),
(hyp_subst_tac 1),
- (hyp_subst_tac 1),
(rtac notE 1),
(rtac less_lift2b 1),
(atac 1),
(asm_simp_tac Lift_ss 1),
(rtac monofun_cfun_arg 1),
(hyp_subst_tac 1),
- (hyp_subst_tac 1),
(etac (less_lift2c RS iffD1) 1)
]);
--- a/src/HOLCF/Pcpo.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/Pcpo.ML Thu Apr 13 14:25:45 1995 +0200
@@ -176,33 +176,25 @@
(rtac refl_less 1)
]);
-
qed_goal "chain_UU_I" Pcpo.thy
"[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU"
-(fn prems =>
+ (fn prems =>
[
(cut_facts_tac prems 1),
(rtac allI 1),
(rtac antisym_less 1),
(rtac minimal 2),
- (res_inst_tac [("t","UU")] subst 1),
- (atac 1),
+ (etac subst 1),
(etac is_ub_thelub 1)
]);
qed_goal "chain_UU_I_inverse" Pcpo.thy
"!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
-(fn prems =>
+ (fn prems =>
[
(cut_facts_tac prems 1),
(rtac lub_chain_maxelem 1),
- (rtac is_chainI 1),
- (rtac allI 1),
- (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
- (rtac sym 1),
- (etac spec 1),
- (rtac minimal 1),
(rtac exI 1),
(etac spec 1),
(rtac allI 1),
--- a/src/HOLCF/Porder.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/Porder.ML Thu Apr 13 14:25:45 1995 +0200
@@ -92,37 +92,30 @@
(* The range of a chain is a totaly ordered << *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_is_tord" Porder.thy [is_tord]
- "is_chain(F) ==> is_tord(range(F))"
-( fn prems =>
+qed_goalw "chain_is_tord" Porder.thy [is_tord,range_def]
+"is_chain(F) ==> is_tord(range(F))"
+ (fn prems =>
[
(cut_facts_tac prems 1),
- (rewrite_goals_tac [range_def]),
- (rtac allI 1 ),
- (rtac allI 1 ),
+ (REPEAT (rtac allI 1 )),
(rtac (mem_Collect_eq RS ssubst) 1),
(rtac (mem_Collect_eq RS ssubst) 1),
(strip_tac 1),
(etac conjE 1),
- (etac exE 1),
- (etac exE 1),
- (hyp_subst_tac 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("m","xa"),("n","xb")] (nat_less_cases) 1),
+ (REPEAT (etac exE 1)),
+ (REPEAT (hyp_subst_tac 1)),
+ (rtac nat_less_cases 1),
(rtac disjI1 1),
- (rtac (chain_mono RS mp) 1),
- (atac 1),
+ (etac (chain_mono RS mp) 1),
(atac 1),
(rtac disjI1 1),
(hyp_subst_tac 1),
(rtac refl_less 1),
(rtac disjI2 1),
- (rtac (chain_mono RS mp) 1),
- (atac 1),
+ (etac (chain_mono RS mp) 1),
(atac 1)
]);
-
(* ------------------------------------------------------------------------ *)
(* technical lemmas about lub and is_lub *)
(* ------------------------------------------------------------------------ *)
@@ -380,8 +373,8 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_chain_maxelem" Porder.thy
-"[|is_chain(Y);? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c"
-(fn prems =>
+"[|? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c"
+ (fn prems =>
[
(cut_facts_tac prems 1),
(rtac thelubI 1),
@@ -389,8 +382,7 @@
(rtac conjI 1),
(etac ub_rangeI 1),
(strip_tac 1),
- (res_inst_tac [("P","%i.Y(i)=c")] exE 1),
- (atac 1),
+ (etac exE 1),
(hyp_subst_tac 1),
(etac (ub_rangeE RS spec) 1)
]);
--- a/src/HOLCF/Sprod3.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/Sprod3.ML Thu Apr 13 14:25:45 1995 +0200
@@ -31,10 +31,6 @@
(asm_simp_tac Sprod_ss 1),
(rtac sym 1),
(rtac lub_chain_maxelem 1),
- (rtac (monofun_Issnd RS ch2ch_monofun) 1),
- (rtac ch2ch_fun 1),
- (rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
- (atac 1),
(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
(rtac (notall2ex RS iffD1) 1),
(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
@@ -53,7 +49,6 @@
(rtac minimal 1)
]);
-
qed_goal "sprod3_lemma2" Sprod3.thy
"[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
\ Ispair(lub(range(Y)),x) =\
@@ -127,15 +122,12 @@
\ Ispair(x,lub(range(Y))) =\
\ Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
\ lub(range(%i. Issnd(Ispair(x,Y(i))))))"
-(fn prems =>
+ (fn prems =>
[
(cut_facts_tac prems 1),
(res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
(rtac sym 1),
(rtac lub_chain_maxelem 1),
- (rtac (monofun_Isfst RS ch2ch_monofun) 1),
- (rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
- (atac 1),
(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
(rtac (notall2ex RS iffD1) 1),
(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
--- a/src/HOLCF/ex/Coind.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/ex/Coind.ML Thu Apr 13 14:25:45 1995 +0200
@@ -24,7 +24,7 @@
(* ------------------------------------------------------------------------- *)
-qed_goal "from" Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
+val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
(fn prems =>
[
(rtac trans 1),
@@ -34,7 +34,7 @@
]);
-qed_goal "from1" Coind.thy "from[UU] = UU"
+val from1 = prove_goal Coind.thy "from[UU] = UU"
(fn prems =>
[
(rtac trans 1),
@@ -53,7 +53,7 @@
(* ------------------------------------------------------------------------- *)
-qed_goal "coind_lemma1" Coind.thy "iterator[n][smap[dsucc]][nats] =\
+val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
(fn prems =>
[
@@ -74,7 +74,7 @@
]);
-qed_goal "nats_eq_from" Coind.thy "nats = from[dzero]"
+val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
(fn prems =>
[
(res_inst_tac [("R",
@@ -90,7 +90,6 @@
(rtac disjI2 1),
(etac conjE 1),
(hyp_subst_tac 1),
- (hyp_subst_tac 1),
(res_inst_tac [("x","n")] exI 1),
(res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
(res_inst_tac [("x","from[dsucc[n]]")] exI 1),
@@ -105,7 +104,7 @@
(* another proof using stream_coind_lemma2 *)
-qed_goal "nats_eq_from" Coind.thy "nats = from[dzero]"
+val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
(fn prems =>
[
(res_inst_tac [("R","% p q.? n. p = \
@@ -119,7 +118,6 @@
(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
(etac conjE 1),
(hyp_subst_tac 1),
- (hyp_subst_tac 1),
(rtac conjI 1),
(rtac (coind_lemma1 RS ssubst) 1),
(rtac (from RS ssubst) 1),
--- a/src/HOLCF/ex/Hoare.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/ex/Hoare.ML Thu Apr 13 14:25:45 1995 +0200
@@ -8,7 +8,7 @@
(* --------- pure HOLCF logic, some little lemmas ------ *)
-qed_goal "hoare_lemma2" HOLCF.thy "~b=TT ==> b=FF | b=UU"
+val hoare_lemma2 = prove_goal HOLCF.thy "~b=TT ==> b=FF | b=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -19,14 +19,14 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "hoare_lemma3" HOLCF.thy
+val hoare_lemma3 = prove_goal HOLCF.thy
" (!k.b1[iterate(k,g,x)]=TT) | (? k.~ b1[iterate(k,g,x)]=TT)"
(fn prems =>
[
(fast_tac HOL_cs 1)
]);
-qed_goal "hoare_lemma4" HOLCF.thy
+val hoare_lemma4 = prove_goal 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)
]);
-qed_goal "hoare_lemma5" HOLCF.thy
+val hoare_lemma5 = prove_goal 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)
]);
-qed_goal "hoare_lemma6" HOLCF.thy "b=UU ==> ~b=TT"
+val hoare_lemma6 = prove_goal HOLCF.thy "b=UU ==> ~b=TT"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -59,7 +59,7 @@
(resolve_tac dist_eq_tr 1)
]);
-qed_goal "hoare_lemma7" HOLCF.thy "b=FF ==> ~b=TT"
+val hoare_lemma7 = prove_goal HOLCF.thy "b=FF ==> ~b=TT"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -67,7 +67,7 @@
(resolve_tac dist_eq_tr 1)
]);
-qed_goal "hoare_lemma8" HOLCF.thy
+val hoare_lemma8 = prove_goal 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)
]);
-qed_goal "hoare_lemma28" HOLCF.thy
+val hoare_lemma28 = prove_goal HOLCF.thy
"b1[y::'a]=(UU::tr) ==> b1[UU] = UU"
(fn prems =>
[
@@ -102,14 +102,14 @@
(* ----- access to definitions ----- *)
-qed_goalw "p_def2" Hoare.thy [p_def]
+val p_def2 = prove_goalw Hoare.thy [p_def]
"p = fix[LAM f x. If b1[x] then f[g[x]] else x fi]"
(fn prems =>
[
(rtac refl 1)
]);
-qed_goalw "q_def2" Hoare.thy [q_def]
+val q_def2 = prove_goalw 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 @@
]);
-qed_goal "p_def3" Hoare.thy
+val p_def3 = prove_goal 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)
]);
-qed_goal "q_def3" Hoare.thy
+val q_def3 = prove_goal 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 ---------- **)
-qed_goal "hoare_lemma9" Hoare.thy
+val hoare_lemma9 = prove_goal 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)
]);
-qed_goal "hoare_lemma24" Hoare.thy
+val hoare_lemma24 = prove_goal 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]
*)
-qed_goal "hoare_lemma11" Hoare.thy
+val hoare_lemma11 = prove_goal Hoare.thy
"(? n.b1[iterate(n,g,x)]~=TT) ==>\
\ k=theleast(%n.b1[iterate(n,g,x)]~=TT) & b1[iterate(k,g,x)]=FF \
\ --> p[x] = iterate(k,g,x)"
@@ -235,7 +235,7 @@
(simp_tac HOLCF_ss 1)
]);
-qed_goal "hoare_lemma12" Hoare.thy
+val hoare_lemma12 = prove_goal Hoare.thy
"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
\ --> p[x] = UU"
@@ -273,7 +273,7 @@
(* -------- results about p for case (! k. b1[iterate(k,g,x)]=TT) ------- *)
-qed_goal "fernpass_lemma" Hoare.thy
+val fernpass_lemma = prove_goal 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)
]);
-qed_goal "hoare_lemma16" Hoare.thy
+val hoare_lemma16 = prove_goal 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) ------- *)
-qed_goal "hoare_lemma17" Hoare.thy
+val hoare_lemma17 = prove_goal 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)
]);
-qed_goal "hoare_lemma18" Hoare.thy
+val hoare_lemma18 = prove_goal Hoare.thy
"(! k. b1[iterate(k,g,x)]=TT) ==> q[x] = UU"
(fn prems =>
[
@@ -339,7 +339,7 @@
(etac (hoare_lemma17 RS spec) 1)
]);
-qed_goal "hoare_lemma19" Hoare.thy
+val hoare_lemma19 = prove_goal 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)
]);
-qed_goal "hoare_lemma20" Hoare.thy
+val hoare_lemma20 = prove_goal Hoare.thy
"(! y. b1[y::'a]=TT) ==> !k.q[iterate(k,g,x::'a)] = UU"
(fn prems =>
[
@@ -372,7 +372,7 @@
(etac spec 1)
]);
-qed_goal "hoare_lemma21" Hoare.thy
+val hoare_lemma21 = prove_goal Hoare.thy
"(! y. b1[y::'a]=TT) ==> q[x::'a] = UU"
(fn prems =>
[
@@ -381,7 +381,7 @@
(etac (hoare_lemma20 RS spec) 1)
]);
-qed_goal "hoare_lemma22" Hoare.thy
+val hoare_lemma22 = prove_goal Hoare.thy
"b1[UU::'a]=UU ==> q[UU::'a] = UU"
(fn prems =>
[
@@ -399,7 +399,7 @@
q[iterate(?k3,?g1,?x1)] = q[?x1]
*)
-qed_goal "hoare_lemma26" Hoare.thy
+val hoare_lemma26 = prove_goal Hoare.thy
"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=FF \
\ --> q[x] = q[iterate(k,g,x)]"
@@ -428,7 +428,7 @@
]);
-qed_goal "hoare_lemma27" Hoare.thy
+val hoare_lemma27 = prove_goal Hoare.thy
"(? n.~ b1[iterate(n,g,x)]=TT) ==>\
\ k=theleast(%n.~ b1[iterate(n,g,x)]=TT) & b1[iterate(k,g,x)]=UU \
\ --> q[x] = UU"
@@ -465,7 +465,7 @@
(* ------- (! k. b1[iterate(k,g,x)]=TT) ==> q o p = q ----- *)
-qed_goal "hoare_lemma23" Hoare.thy
+val hoare_lemma23 = prove_goal 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 ----- *)
-qed_goal "hoare_lemma29" Hoare.thy
+val hoare_lemma29 = prove_goal 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 ------ *)
-qed_goal "hoare_main" Hoare.thy "q oo p = q"
+val hoare_main = prove_goal Hoare.thy "q oo p = q"
(fn prems =>
[
(rtac ext_cfun 1),
--- a/src/HOLCF/ex/Loop.ML Thu Apr 13 14:18:22 1995 +0200
+++ b/src/HOLCF/ex/Loop.ML Thu Apr 13 14:25:45 1995 +0200
@@ -12,14 +12,14 @@
(* access to definitions *)
(* --------------------------------------------------------------------------- *)
-qed_goalw "step_def2" Loop.thy [step_def]
+val step_def2 = prove_goalw Loop.thy [step_def]
"step[b][g][x] = If b[x] then g[x] else x fi"
(fn prems =>
[
(simp_tac Cfun_ss 1)
]);
-qed_goalw "while_def2" Loop.thy [while_def]
+val while_def2 = prove_goalw Loop.thy [while_def]
"while[b][g] = fix[LAM f x. If b[x] then f[g[x]] else x fi]"
(fn prems =>
[
@@ -31,7 +31,7 @@
(* rekursive properties of while *)
(* ------------------------------------------------------------------------- *)
-qed_goal "while_unfold" Loop.thy
+val while_unfold = prove_goal Loop.thy
"while[b][g][x] = If b[x] then while[b][g][g[x]] else x fi"
(fn prems =>
[
@@ -39,7 +39,7 @@
(simp_tac Cfun_ss 1)
]);
-qed_goal "while_unfold2" Loop.thy
+val while_unfold2 = prove_goal 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)
]);
-qed_goal "while_unfold3" Loop.thy
+val while_unfold3 = prove_goal Loop.thy
"while[b][g][x] = while[b][g][step[b][g][x]]"
(fn prems =>
[
@@ -81,7 +81,7 @@
(* properties of while and iterations *)
(* --------------------------------------------------------------------------- *)
-qed_goal "loop_lemma1" Loop.thy
+val loop_lemma1 = prove_goal 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)
]);
-qed_goal "loop_lemma2" Loop.thy
+val loop_lemma2 = prove_goal 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)
]);
-qed_goal "loop_lemma3" Loop.thy
+val loop_lemma3 = prove_goal 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 @@
]);
-qed_goal "loop_lemma4" Loop.thy
+val loop_lemma4 = prove_goal 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)
]);
-qed_goal "loop_lemma5" Loop.thy
+val loop_lemma5 = prove_goal 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 @@
]);
-qed_goal "loop_lemma6" Loop.thy
+val loop_lemma6 = prove_goal 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)
]);
-qed_goal "loop_lemma7" Loop.thy
+val loop_lemma7 = prove_goal 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)
]);
-qed_goal "loop_lemma8" Loop.thy
+val loop_lemma8 = prove_goal Loop.thy
"~while[b][g][x]=UU ==> ? y. b[y]=FF"
(fn prems =>
[
@@ -212,7 +212,7 @@
(* an invariant rule for loops *)
(* --------------------------------------------------------------------------- *)
-qed_goal "loop_inv2" Loop.thy
+val loop_inv2 = prove_goal Loop.thy
"[| (!y. INV(y) & b[y]=TT & ~g[y]=UU --> INV(g[y]));\
\ (!y. INV(y) & b[y]=FF --> Q(y));\
\ INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
@@ -239,7 +239,7 @@
(rtac refl 1)
]);
-qed_goal "loop_inv3" Loop.thy
+val loop_inv3 = prove_goal Loop.thy
"[| !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\
\ !!y.[| INV(y); b[y]=FF|]==> Q(y);\
\ INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])"
@@ -261,7 +261,7 @@
(resolve_tac prems 1)
]);
-qed_goal "loop_inv" Loop.thy
+val loop_inv = prove_goal Loop.thy
"[| P(x);\
\ !!y.P(y) ==> INV(y);\
\ !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\