src/HOLCF/Cfun2.ML
changeset 9248 e1dee89de037
parent 9245 428385c4bc50
child 10834 a7897aebbffc
     1.1 --- a/src/HOLCF/Cfun2.ML	Wed Jul 05 14:26:58 2000 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Wed Jul 05 16:37:52 2000 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  *)
     1.5  
     1.6  (* for compatibility with old HOLCF-Version *)
     1.7 -val prems = goal thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
     1.8 +Goal "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
     1.9  by (fold_goals_tac [less_cfun_def]);
    1.10  by (rtac refl 1);
    1.11  qed "inst_cfun_po";
    1.12 @@ -16,7 +16,7 @@
    1.13  (* access to less_cfun in class po                                          *)
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  
    1.16 -val prems = goal thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
    1.17 +Goal "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
    1.18  by (simp_tac (simpset() addsimps [inst_cfun_po]) 1);
    1.19  qed "less_cfun";
    1.20  
    1.21 @@ -24,7 +24,7 @@
    1.22  (* Type 'a ->'b  is pointed                                                 *)
    1.23  (* ------------------------------------------------------------------------ *)
    1.24  
    1.25 -val prems = goal thy "Abs_CFun(% x. UU) << f";
    1.26 +Goal "Abs_CFun(% x. UU) << f";
    1.27  by (stac less_cfun 1);
    1.28  by (stac Abs_Cfun_inverse2 1);
    1.29  by (rtac cont_const 1);
    1.30 @@ -33,7 +33,7 @@
    1.31  
    1.32  bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
    1.33  
    1.34 -val prems = goal thy "? x::'a->'b::pcpo.!y. x<<y";
    1.35 +Goal "? x::'a->'b::pcpo.!y. x<<y";
    1.36  by (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1);
    1.37  by (rtac (minimal_cfun RS allI) 1);
    1.38  qed "least_cfun";
    1.39 @@ -44,7 +44,7 @@
    1.40  (* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
    1.41  (* ------------------------------------------------------------------------ *)
    1.42  
    1.43 -val prems = goal thy "cont(Rep_CFun(fo))";
    1.44 +Goal "cont(Rep_CFun(fo))";
    1.45  by (res_inst_tac [("P","cont")] CollectD 1);
    1.46  by (fold_goals_tac [CFun_def]);
    1.47  by (rtac Rep_Cfun 1);
    1.48 @@ -73,7 +73,7 @@
    1.49  (* Rep_CFun is monotone in its 'first' argument                                 *)
    1.50  (* ------------------------------------------------------------------------ *)
    1.51  
    1.52 -val prems = goalw thy [monofun] "monofun(Rep_CFun)";
    1.53 +Goalw [monofun] "monofun(Rep_CFun)";
    1.54  by (strip_tac 1);
    1.55  by (etac (less_cfun RS subst) 1);
    1.56  qed "monofun_Rep_CFun1";
    1.57 @@ -83,8 +83,7 @@
    1.58  (* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
    1.59  (* ------------------------------------------------------------------------ *)
    1.60  
    1.61 -val prems = goal thy  "f1 << f2 ==> f1`x << f2`x";
    1.62 -by (cut_facts_tac prems 1);
    1.63 +Goal  "f1 << f2 ==> f1`x << f2`x";
    1.64  by (res_inst_tac [("x","x")] spec 1);
    1.65  by (rtac (less_fun RS subst) 1);
    1.66  by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
    1.67 @@ -98,9 +97,7 @@
    1.68  (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
    1.69  (* ------------------------------------------------------------------------ *)
    1.70  
    1.71 -val prems = goal thy
    1.72 -        "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
    1.73 -by (cut_facts_tac prems 1);
    1.74 +Goal "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
    1.75  by (rtac trans_less 1);
    1.76  by (etac monofun_cfun_arg 1);
    1.77  by (etac monofun_cfun_fun 1);
    1.78 @@ -119,9 +116,7 @@
    1.79  (* use MF2 lemmas from Cont.ML                                              *)
    1.80  (* ------------------------------------------------------------------------ *)
    1.81  
    1.82 -val prems = goal thy 
    1.83 - "chain(Y) ==> chain(%i. f`(Y i))";
    1.84 -by (cut_facts_tac prems 1);
    1.85 +Goal "chain(Y) ==> chain(%i. f`(Y i))";
    1.86  by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
    1.87  qed "ch2ch_Rep_CFunR";
    1.88  
    1.89 @@ -135,9 +130,7 @@
    1.90  (* use MF2 lemmas from Cont.ML                                              *)
    1.91  (* ------------------------------------------------------------------------ *)
    1.92  
    1.93 -val prems = goal thy 
    1.94 -        "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
    1.95 -by (cut_facts_tac prems 1);
    1.96 +Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
    1.97  by (rtac lub_MF2_mono 1);
    1.98  by (rtac monofun_Rep_CFun1 1);
    1.99  by (rtac (monofun_Rep_CFun2 RS allI) 1);
   1.100 @@ -149,11 +142,9 @@
   1.101  (* use MF2 lemmas from Cont.ML                                              *)
   1.102  (* ------------------------------------------------------------------------ *)
   1.103  
   1.104 -val prems = goal thy
   1.105 -        "[| chain(F); chain(Y) |] ==>\
   1.106 +Goal "[| chain(F); chain(Y) |] ==>\
   1.107  \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   1.108  \               lub(range(%i. lub(range(%j. F(j)`(Y i)))))";
   1.109 -by (cut_facts_tac prems 1);
   1.110  by (rtac ex_lubMF2 1);
   1.111  by (rtac monofun_Rep_CFun1 1);
   1.112  by (rtac (monofun_Rep_CFun2 RS allI) 1);
   1.113 @@ -165,9 +156,7 @@
   1.114  (* the lub of a chain of cont. functions is continuous                      *)
   1.115  (* ------------------------------------------------------------------------ *)
   1.116  
   1.117 -val prems = goal thy 
   1.118 -        "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
   1.119 -by (cut_facts_tac prems 1);
   1.120 +Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
   1.121  by (rtac monocontlub2cont 1);
   1.122  by (etac lub_cfun_mono 1);
   1.123  by (rtac contlubI 1);
   1.124 @@ -182,23 +171,18 @@
   1.125  (* type 'a -> 'b is chain complete                                          *)
   1.126  (* ------------------------------------------------------------------------ *)
   1.127  
   1.128 -val prems = goal thy 
   1.129 -  "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
   1.130 -by (cut_facts_tac prems 1);
   1.131 +Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
   1.132  by (rtac is_lubI 1);
   1.133 -by (rtac conjI 1);
   1.134  by (rtac ub_rangeI 1);
   1.135 -by (rtac allI 1);
   1.136  by (stac less_cfun 1);
   1.137  by (stac Abs_Cfun_inverse2 1);
   1.138  by (etac cont_lubcfun 1);
   1.139 -by (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1);
   1.140 +by (rtac (lub_fun RS is_lubD1 RS ub_rangeD) 1);
   1.141  by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   1.142 -by (strip_tac 1);
   1.143  by (stac less_cfun 1);
   1.144  by (stac Abs_Cfun_inverse2 1);
   1.145  by (etac cont_lubcfun 1);
   1.146 -by (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1);
   1.147 +by (rtac (lub_fun RS is_lub_lub) 1);
   1.148  by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   1.149  by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
   1.150  qed "lub_cfun";
   1.151 @@ -208,9 +192,7 @@
   1.152  chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
   1.153  *)
   1.154  
   1.155 -val prems = goal thy 
   1.156 -  "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
   1.157 -by (cut_facts_tac prems 1);
   1.158 +Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
   1.159  by (rtac exI 1);
   1.160  by (etac lub_cfun 1);
   1.161  qed "cpo_cfun";
   1.162 @@ -220,7 +202,7 @@
   1.163  (* Extensionality in 'a -> 'b                                               *)
   1.164  (* ------------------------------------------------------------------------ *)
   1.165  
   1.166 -val prems = goal Cfun1.thy "(!!x. f`x = g`x) ==> f = g";
   1.167 +val prems = Goal "(!!x. f`x = g`x) ==> f = g";
   1.168  by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   1.169  by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   1.170  by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
   1.171 @@ -232,21 +214,20 @@
   1.172  (* Monotonicity of Abs_CFun                                                     *)
   1.173  (* ------------------------------------------------------------------------ *)
   1.174  
   1.175 -val prems = goal thy 
   1.176 -        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)";
   1.177 +Goal "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)";
   1.178  by (rtac (less_cfun RS iffD2) 1);
   1.179  by (stac Abs_Cfun_inverse2 1);
   1.180 -by (resolve_tac prems 1);
   1.181 +by (assume_tac 1);
   1.182  by (stac Abs_Cfun_inverse2 1);
   1.183 -by (resolve_tac prems 1);
   1.184 -by (resolve_tac prems 1);
   1.185 +by (assume_tac 1);
   1.186 +by (assume_tac 1);
   1.187  qed "semi_monofun_Abs_CFun";
   1.188  
   1.189  (* ------------------------------------------------------------------------ *)
   1.190  (* Extenionality wrt. << in 'a -> 'b                                        *)
   1.191  (* ------------------------------------------------------------------------ *)
   1.192  
   1.193 -val prems = goal thy "(!!x. f`x << g`x) ==> f << g";
   1.194 +val prems = Goal "(!!x. f`x << g`x) ==> f << g";
   1.195  by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   1.196  by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   1.197  by (rtac semi_monofun_Abs_CFun 1);