--- 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),