src/HOLCF/Cfun2.ML
changeset 892 d0dc8d057929
parent 297 5ef75ff3baeb
child 1168 74be52691d62
     1.1 --- a/src/HOLCF/Cfun2.ML	Fri Feb 03 12:32:14 1995 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Tue Feb 07 11:59:32 1995 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  (* access to less_cfun in class po                                          *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
     1.8 +qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
     1.9  (fn prems =>
    1.10  	[
    1.11  	(rtac (inst_cfun_po RS ssubst) 1),
    1.12 @@ -24,7 +24,7 @@
    1.13  (* Type 'a ->'b  is pointed                                                 *)
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  
    1.16 -val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
    1.17 +qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
    1.18  (fn prems =>
    1.19  	[
    1.20  	(rtac (less_cfun RS ssubst) 1),
    1.21 @@ -40,7 +40,7 @@
    1.22  (* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    1.23  (* ------------------------------------------------------------------------ *)
    1.24  
    1.25 -val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
    1.26 +qed_goal "contX_fapp2" Cfun2.thy "contX(fapp(fo))"
    1.27  (fn prems =>
    1.28  	[
    1.29  	(res_inst_tac [("P","contX")] CollectD 1),
    1.30 @@ -72,7 +72,7 @@
    1.31  (* fapp is monotone in its 'first' argument                                 *)
    1.32  (* ------------------------------------------------------------------------ *)
    1.33  
    1.34 -val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
    1.35 +qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
    1.36  (fn prems =>
    1.37  	[
    1.38  	(strip_tac 1),
    1.39 @@ -84,7 +84,7 @@
    1.40  (* monotonicity of application fapp in mixfix syntax [_]_                   *)
    1.41  (* ------------------------------------------------------------------------ *)
    1.42  
    1.43 -val monofun_cfun_fun = prove_goal Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
    1.44 +qed_goal "monofun_cfun_fun" Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
    1.45  (fn prems =>
    1.46  	[
    1.47  	(cut_facts_tac prems 1),
    1.48 @@ -101,7 +101,7 @@
    1.49  (* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
    1.50  (* ------------------------------------------------------------------------ *)
    1.51  
    1.52 -val monofun_cfun = prove_goal Cfun2.thy
    1.53 +qed_goal "monofun_cfun" Cfun2.thy
    1.54  	"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
    1.55  (fn prems =>
    1.56  	[
    1.57 @@ -117,7 +117,7 @@
    1.58  (* use MF2 lemmas from Cont.ML                                              *)
    1.59  (* ------------------------------------------------------------------------ *)
    1.60  
    1.61 -val ch2ch_fappR = prove_goal Cfun2.thy 
    1.62 +qed_goal "ch2ch_fappR" Cfun2.thy 
    1.63   "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
    1.64  (fn prems =>
    1.65  	[
    1.66 @@ -135,7 +135,7 @@
    1.67  (* use MF2 lemmas from Cont.ML                                              *)
    1.68  (* ------------------------------------------------------------------------ *)
    1.69  
    1.70 -val lub_cfun_mono = prove_goal Cfun2.thy 
    1.71 +qed_goal "lub_cfun_mono" Cfun2.thy 
    1.72  	"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
    1.73  (fn prems =>
    1.74  	[
    1.75 @@ -151,7 +151,7 @@
    1.76  (* use MF2 lemmas from Cont.ML                                              *)
    1.77  (* ------------------------------------------------------------------------ *)
    1.78  
    1.79 -val ex_lubcfun = prove_goal Cfun2.thy
    1.80 +qed_goal "ex_lubcfun" Cfun2.thy
    1.81  	"[| is_chain(F); is_chain(Y) |] ==>\
    1.82  \		lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
    1.83  \		lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
    1.84 @@ -169,7 +169,7 @@
    1.85  (* the lub of a chain of cont. functions is continuous                      *)
    1.86  (* ------------------------------------------------------------------------ *)
    1.87  
    1.88 -val contX_lubcfun = prove_goal Cfun2.thy 
    1.89 +qed_goal "contX_lubcfun" Cfun2.thy 
    1.90  	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
    1.91  (fn prems =>
    1.92  	[
    1.93 @@ -188,7 +188,7 @@
    1.94  (* type 'a -> 'b is chain complete                                          *)
    1.95  (* ------------------------------------------------------------------------ *)
    1.96  
    1.97 -val lub_cfun = prove_goal Cfun2.thy 
    1.98 +qed_goal "lub_cfun" Cfun2.thy 
    1.99    "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
   1.100  (fn prems =>
   1.101  	[
   1.102 @@ -216,7 +216,7 @@
   1.103  is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
   1.104  *)
   1.105  
   1.106 -val cpo_cfun = prove_goal Cfun2.thy 
   1.107 +qed_goal "cpo_cfun" Cfun2.thy 
   1.108    "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
   1.109  (fn prems =>
   1.110  	[
   1.111 @@ -230,7 +230,7 @@
   1.112  (* Extensionality in 'a -> 'b                                               *)
   1.113  (* ------------------------------------------------------------------------ *)
   1.114  
   1.115 -val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
   1.116 +qed_goal "ext_cfun" Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
   1.117   (fn prems =>
   1.118  	[
   1.119  	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.120 @@ -244,7 +244,7 @@
   1.121  (* Monotonicity of fabs                                                     *)
   1.122  (* ------------------------------------------------------------------------ *)
   1.123  
   1.124 -val semi_monofun_fabs = prove_goal Cfun2.thy 
   1.125 +qed_goal "semi_monofun_fabs" Cfun2.thy 
   1.126  	"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
   1.127   (fn prems =>
   1.128  	[
   1.129 @@ -260,7 +260,7 @@
   1.130  (* Extenionality wrt. << in 'a -> 'b                                        *)
   1.131  (* ------------------------------------------------------------------------ *)
   1.132  
   1.133 -val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
   1.134 +qed_goal "less_cfun2" Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
   1.135   (fn prems =>
   1.136  	[
   1.137  	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),