--- a/src/HOLCF/Cfun2.ML Tue Jul 04 14:58:40 2000 +0200
+++ b/src/HOLCF/Cfun2.ML Tue Jul 04 15:58:11 2000 +0200
@@ -1,52 +1,42 @@
-(* Title: HOLCF/cfun2.thy
+(* Title: HOLCF/Cfun2
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for cfun2.thy
+Class Instance ->::(cpo,cpo)po
*)
-open Cfun2;
-
(* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"
- (fn prems =>
- [
- (fold_goals_tac [less_cfun_def]),
- (rtac refl 1)
- ]);
+val prems = goal thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
+by (fold_goals_tac [less_cfun_def]);
+by (rtac refl 1);
+qed "inst_cfun_po";
(* ------------------------------------------------------------------------ *)
(* access to less_cfun in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"
-(fn prems =>
- [
- (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
- ]);
+val prems = goal thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
+by (simp_tac (simpset() addsimps [inst_cfun_po]) 1);
+qed "less_cfun";
(* ------------------------------------------------------------------------ *)
(* Type 'a ->'b is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f"
-(fn prems =>
- [
- (stac less_cfun 1),
- (stac Abs_Cfun_inverse2 1),
- (rtac cont_const 1),
- (rtac minimal_fun 1)
- ]);
+val prems = goal thy "Abs_CFun(% x. UU) << f";
+by (stac less_cfun 1);
+by (stac Abs_Cfun_inverse2 1);
+by (rtac cont_const 1);
+by (rtac minimal_fun 1);
+qed "minimal_cfun";
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
-qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
-(fn prems =>
- [
- (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1),
- (rtac (minimal_cfun RS allI) 1)
- ]);
+val prems = goal thy "? x::'a->'b::pcpo.!y. x<<y";
+by (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1);
+by (rtac (minimal_cfun RS allI) 1);
+qed "least_cfun";
(* ------------------------------------------------------------------------ *)
(* Rep_CFun yields continuous functions in 'a => 'b *)
@@ -54,13 +44,11 @@
(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2 *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))"
-(fn prems =>
- [
- (res_inst_tac [("P","cont")] CollectD 1),
- (fold_goals_tac [CFun_def]),
- (rtac Rep_Cfun 1)
- ]);
+val prems = goal thy "cont(Rep_CFun(fo))";
+by (res_inst_tac [("P","cont")] CollectD 1);
+by (fold_goals_tac [CFun_def]);
+by (rtac Rep_Cfun 1);
+qed "cont_Rep_CFun2";
bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
(* monofun(Rep_CFun(?fo1)) *)
@@ -85,26 +73,22 @@
(* Rep_CFun is monotone in its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)"
-(fn prems =>
- [
- (strip_tac 1),
- (etac (less_cfun RS subst) 1)
- ]);
+val prems = goalw thy [monofun] "monofun(Rep_CFun)";
+by (strip_tac 1);
+by (etac (less_cfun RS subst) 1);
+qed "monofun_Rep_CFun1";
(* ------------------------------------------------------------------------ *)
(* monotonicity of application Rep_CFun in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_cfun_fun" thy "f1 << f2 ==> f1`x << f2`x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("x","x")] spec 1),
- (rtac (less_fun RS subst) 1),
- (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1)
- ]);
+val prems = goal thy "f1 << f2 ==> f1`x << f2`x";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("x","x")] spec 1);
+by (rtac (less_fun RS subst) 1);
+by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
+qed "monofun_cfun_fun";
bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
@@ -114,22 +98,20 @@
(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_cfun" thy
- "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac trans_less 1),
- (etac monofun_cfun_arg 1),
- (etac monofun_cfun_fun 1)
- ]);
+val prems = goal thy
+ "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
+by (cut_facts_tac prems 1);
+by (rtac trans_less 1);
+by (etac monofun_cfun_arg 1);
+by (etac monofun_cfun_fun 1);
+qed "monofun_cfun";
-qed_goal "strictI" thy "f`x = UU ==> f`UU = UU" (fn prems => [
- cut_facts_tac prems 1,
- rtac (eq_UU_iff RS iffD2) 1,
- etac subst 1,
- rtac (minimal RS monofun_cfun_arg) 1]);
+Goal "f`x = UU ==> f`UU = UU";
+by (rtac (eq_UU_iff RS iffD2) 1);
+by (etac subst 1);
+by (rtac (minimal RS monofun_cfun_arg) 1);
+qed "strictI";
(* ------------------------------------------------------------------------ *)
@@ -137,13 +119,11 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_Rep_CFunR" thy
- "chain(Y) ==> chain(%i. f`(Y i))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1)
- ]);
+val prems = goal thy
+ "chain(Y) ==> chain(%i. f`(Y i))";
+by (cut_facts_tac prems 1);
+by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
+qed "ch2ch_Rep_CFunR";
bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
@@ -155,142 +135,126 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_cfun_mono" thy
- "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac lub_MF2_mono 1),
- (rtac monofun_Rep_CFun1 1),
- (rtac (monofun_Rep_CFun2 RS allI) 1),
- (atac 1)
- ]);
+val prems = goal thy
+ "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
+by (cut_facts_tac prems 1);
+by (rtac lub_MF2_mono 1);
+by (rtac monofun_Rep_CFun1 1);
+by (rtac (monofun_Rep_CFun2 RS allI) 1);
+by (atac 1);
+qed "lub_cfun_mono";
(* ------------------------------------------------------------------------ *)
(* a lemma about the exchange of lubs for type 'a -> 'b *)
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ex_lubcfun" thy
+val prems = goal thy
"[| chain(F); chain(Y) |] ==>\
\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
-\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac ex_lubMF2 1),
- (rtac monofun_Rep_CFun1 1),
- (rtac (monofun_Rep_CFun2 RS allI) 1),
- (atac 1),
- (atac 1)
- ]);
+\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))";
+by (cut_facts_tac prems 1);
+by (rtac ex_lubMF2 1);
+by (rtac monofun_Rep_CFun1 1);
+by (rtac (monofun_Rep_CFun2 RS allI) 1);
+by (atac 1);
+by (atac 1);
+qed "ex_lubcfun";
(* ------------------------------------------------------------------------ *)
(* the lub of a chain of cont. functions is continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_lubcfun" thy
- "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac monocontlub2cont 1),
- (etac lub_cfun_mono 1),
- (rtac contlubI 1),
- (strip_tac 1),
- (stac (contlub_cfun_arg RS ext) 1),
- (atac 1),
- (etac ex_lubcfun 1),
- (atac 1)
- ]);
+val prems = goal thy
+ "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
+by (cut_facts_tac prems 1);
+by (rtac monocontlub2cont 1);
+by (etac lub_cfun_mono 1);
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (stac (contlub_cfun_arg RS ext) 1);
+by (atac 1);
+by (etac ex_lubcfun 1);
+by (atac 1);
+qed "cont_lubcfun";
(* ------------------------------------------------------------------------ *)
(* type 'a -> 'b is chain complete *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_cfun" thy
- "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (stac less_cfun 1),
- (stac Abs_Cfun_inverse2 1),
- (etac cont_lubcfun 1),
- (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
- (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
- (strip_tac 1),
- (stac less_cfun 1),
- (stac Abs_Cfun_inverse2 1),
- (etac cont_lubcfun 1),
- (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
- (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
- (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1)
- ]);
+val prems = goal thy
+ "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
+by (cut_facts_tac prems 1);
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 1);
+by (stac less_cfun 1);
+by (stac Abs_Cfun_inverse2 1);
+by (etac cont_lubcfun 1);
+by (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1);
+by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
+by (strip_tac 1);
+by (stac less_cfun 1);
+by (stac Abs_Cfun_inverse2 1);
+by (etac cont_lubcfun 1);
+by (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1);
+by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
+by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
+qed "lub_cfun";
bind_thm ("thelub_cfun", lub_cfun RS thelubI);
(*
chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
*)
-qed_goal "cpo_cfun" thy
- "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac exI 1),
- (etac lub_cfun 1)
- ]);
+val prems = goal thy
+ "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
+by (cut_facts_tac prems 1);
+by (rtac exI 1);
+by (etac lub_cfun 1);
+qed "cpo_cfun";
(* ------------------------------------------------------------------------ *)
(* Extensionality in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-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),
- (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
- (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
- (rtac ext 1),
- (resolve_tac prems 1)
- ]);
+val prems = goal Cfun1.thy "(!!x. f`x = g`x) ==> f = g";
+by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
+by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
+by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
+by (rtac ext 1);
+by (resolve_tac prems 1);
+qed "ext_cfun";
(* ------------------------------------------------------------------------ *)
(* Monotonicity of Abs_CFun *)
(* ------------------------------------------------------------------------ *)
-qed_goal "semi_monofun_Abs_CFun" thy
- "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
- (fn prems =>
- [
- (rtac (less_cfun RS iffD2) 1),
- (stac Abs_Cfun_inverse2 1),
- (resolve_tac prems 1),
- (stac Abs_Cfun_inverse2 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
+val prems = goal thy
+ "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)";
+by (rtac (less_cfun RS iffD2) 1);
+by (stac Abs_Cfun_inverse2 1);
+by (resolve_tac prems 1);
+by (stac Abs_Cfun_inverse2 1);
+by (resolve_tac prems 1);
+by (resolve_tac prems 1);
+qed "semi_monofun_Abs_CFun";
(* ------------------------------------------------------------------------ *)
(* Extenionality wrt. << in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_cfun2" thy "(!!x. f`x << g`x) ==> f << g"
- (fn prems =>
- [
- (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
- (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
- (rtac semi_monofun_Abs_CFun 1),
- (rtac cont_Rep_CFun2 1),
- (rtac cont_Rep_CFun2 1),
- (rtac (less_fun RS iffD2) 1),
- (rtac allI 1),
- (resolve_tac prems 1)
- ]);
+val prems = goal thy "(!!x. f`x << g`x) ==> f << g";
+by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
+by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
+by (rtac semi_monofun_Abs_CFun 1);
+by (rtac cont_Rep_CFun2 1);
+by (rtac cont_Rep_CFun2 1);
+by (rtac (less_fun RS iffD2) 1);
+by (rtac allI 1);
+by (resolve_tac prems 1);
+qed "less_cfun2";