--- a/src/HOLCF/Up3.ML Wed Jun 28 10:52:02 2000 +0200
+++ b/src/HOLCF/Up3.ML Wed Jun 28 10:54:21 2000 +0200
@@ -3,85 +3,71 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for Up3.thy
+Class instance of ('a)u for class pcpo
*)
-open Up3;
-
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_up_pcpo" thy "UU = Abs_Up(Inl ())"
- (fn prems =>
- [
- (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1)
- ]);
+Goal "UU = Abs_Up(Inl ())";
+by (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1);
+qed "inst_up_pcpo";
(* -------------------------------------------------------------------------*)
(* some lemmas restated for class pcpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_up3b" thy "~ Iup(x) << UU"
- (fn prems =>
- [
- (stac inst_up_pcpo 1),
- (rtac less_up2b 1)
- ]);
+Goal "~ Iup(x) << UU";
+by (stac inst_up_pcpo 1);
+by (rtac less_up2b 1);
+qed "less_up3b";
-qed_goal "defined_Iup2" thy "Iup(x) ~= UU"
- (fn prems =>
- [
- (stac inst_up_pcpo 1),
- (rtac defined_Iup 1)
- ]);
+Goal "Iup(x) ~= UU";
+by (stac inst_up_pcpo 1);
+by (rtac defined_Iup 1);
+qed "defined_Iup2";
(* ------------------------------------------------------------------------ *)
(* continuity for Iup *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Iup" thy "contlub(Iup)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_up1a RS sym) 2),
- (fast_tac HOL_cs 3),
- (etac (monofun_Iup RS ch2ch_monofun) 2),
- (res_inst_tac [("f","Iup")] arg_cong 1),
- (rtac lub_equal 1),
- (atac 1),
- (rtac (monofun_Ifup2 RS ch2ch_monofun) 1),
- (etac (monofun_Iup RS ch2ch_monofun) 1),
- (asm_simp_tac Up0_ss 1)
- ]);
+Goal "contlub(Iup)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_up1a RS sym) 2);
+by (fast_tac HOL_cs 3);
+by (etac (monofun_Iup RS ch2ch_monofun) 2);
+by (res_inst_tac [("f","Iup")] arg_cong 1);
+by (rtac lub_equal 1);
+by (atac 1);
+by (rtac (monofun_Ifup2 RS ch2ch_monofun) 1);
+by (etac (monofun_Iup RS ch2ch_monofun) 1);
+by (asm_simp_tac Up0_ss 1);
+qed "contlub_Iup";
-qed_goal "cont_Iup" thy "cont(Iup)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Iup 1),
- (rtac contlub_Iup 1)
- ]);
+Goal "cont(Iup)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Iup 1);
+by (rtac contlub_Iup 1);
+qed "cont_Iup";
(* ------------------------------------------------------------------------ *)
(* continuity for Ifup *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Ifup1" thy "contlub(Ifup)"
- (fn prems =>
- [
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac trans 1),
- (rtac (thelub_fun RS sym) 2),
- (etac (monofun_Ifup1 RS ch2ch_monofun) 2),
- (rtac ext 1),
- (res_inst_tac [("p","x")] upE 1),
- (asm_simp_tac Up0_ss 1),
- (rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Up0_ss 1),
- (etac contlub_cfun_fun 1)
- ]);
+Goal "contlub(Ifup)";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac trans 1);
+by (rtac (thelub_fun RS sym) 2);
+by (etac (monofun_Ifup1 RS ch2ch_monofun) 2);
+by (rtac ext 1);
+by (res_inst_tac [("p","x")] upE 1);
+by (asm_simp_tac Up0_ss 1);
+by (rtac (lub_const RS thelubI RS sym) 1);
+by (asm_simp_tac Up0_ss 1);
+by (etac contlub_cfun_fun 1);
+qed "contlub_Ifup1";
Goal "contlub(Ifup(f))";
@@ -129,21 +115,17 @@
by (atac 1);
qed "contlub_Ifup2";
-qed_goal "cont_Ifup1" thy "cont(Ifup)"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Ifup1 1),
- (rtac contlub_Ifup1 1)
- ]);
+Goal "cont(Ifup)";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Ifup1 1);
+by (rtac contlub_Ifup1 1);
+qed "cont_Ifup1";
-qed_goal "cont_Ifup2" thy "cont(Ifup(f))"
- (fn prems =>
- [
- (rtac monocontlub2cont 1),
- (rtac monofun_Ifup2 1),
- (rtac contlub_Ifup2 1)
- ]);
+Goal "cont(Ifup(f))";
+by (rtac monocontlub2cont 1);
+by (rtac monofun_Ifup2 1);
+by (rtac contlub_Ifup2 1);
+qed "cont_Ifup2";
(* ------------------------------------------------------------------------ *)
@@ -272,72 +254,58 @@
]);
-qed_goal "up_lemma2" thy " (? x. z = up`x) = (z~=UU)"
- (fn prems =>
- [
- (rtac iffI 1),
- (etac exE 1),
- (hyp_subst_tac 1),
- (rtac defined_up 1),
- (res_inst_tac [("p","z")] upE1 1),
- (etac notE 1),
- (atac 1),
- (etac exI 1)
- ]);
+Goal "(? x. z = up`x) = (z~=UU)";
+by (rtac iffI 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (rtac defined_up 1);
+by (res_inst_tac [("p","z")] upE1 1);
+by (etac notE 1);
+by (atac 1);
+by (etac exI 1);
+qed "up_lemma2";
-qed_goal "thelub_up2a_rev" thy
-"[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac exE 1),
- (rtac chain_UU_I_inverse2 1),
- (rtac (up_lemma2 RS iffD1) 1),
- (etac exI 1),
- (rtac exI 1),
- (rtac (up_lemma2 RS iffD2) 1),
- (atac 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x";
+by (rtac exE 1);
+by (rtac chain_UU_I_inverse2 1);
+by (rtac (up_lemma2 RS iffD1) 1);
+by (etac exI 1);
+by (rtac exI 1);
+by (rtac (up_lemma2 RS iffD2) 1);
+by (atac 1);
+qed "thelub_up2a_rev";
-qed_goal "thelub_up2b_rev" thy
-"[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac allI 1),
- (rtac (not_ex RS iffD1) 1),
- (rtac contrapos 1),
- (etac (up_lemma2 RS iffD1) 2),
- (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1)
- ]);
+Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x";
+by (cut_facts_tac prems 1);
+by (rtac allI 1);
+by (rtac (not_ex RS iffD1) 1);
+by (rtac contrapos 1);
+by (etac (up_lemma2 RS iffD1) 2);
+by (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1);
+qed "thelub_up2b_rev";
-qed_goal "thelub_up3" thy
-"chain(Y) ==> lub(range(Y)) = UU |\
-\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac disjE 1),
- (rtac disjI1 2),
- (rtac thelub_up2b 2),
- (atac 2),
- (atac 2),
- (rtac disjI2 2),
- (rtac thelub_up2a 2),
- (atac 2),
- (atac 2),
- (fast_tac HOL_cs 1)
- ]);
+Goal "chain(Y) ==> lub(range(Y)) = UU | \
+\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
+by (cut_facts_tac prems 1);
+by (rtac disjE 1);
+by (rtac disjI1 2);
+by (rtac thelub_up2b 2);
+by (atac 2);
+by (atac 2);
+by (rtac disjI2 2);
+by (rtac thelub_up2a 2);
+by (atac 2);
+by (atac 2);
+by (fast_tac HOL_cs 1);
+qed "thelub_up3";
-qed_goal "fup3" thy "fup`up`x=x"
- (fn prems =>
- [
- (res_inst_tac [("p","x")] upE1 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1),
- (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1)
- ]);
+Goal "fup`up`x=x";
+by (res_inst_tac [("p","x")] upE1 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
+by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
+qed "fup3";
(* ------------------------------------------------------------------------ *)
(* install simplifier for ('a)u *)