src/HOLCF/Cfun2.ML

 
 (* ------------------------------------------------------------------------ *)
 (* access to less_cfun in class po                                          *)
 (* ------------------------------------------------------------------------ *)
 
-val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
+qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
 (fn prems =>
 	[
 	(rtac (inst_cfun_po RS ssubst) 1),
 	(fold_goals_tac [less_cfun_def]),
 	(rtac refl 1)

 
 (* ------------------------------------------------------------------------ *)
 (* Type 'a ->'b  is pointed                                                 *)
 (* ------------------------------------------------------------------------ *)
 
-val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
+qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
 (fn prems =>
 	[
 	(rtac (less_cfun RS ssubst) 1),
 	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
 	(rtac contX_const 1),

 (* fapp yields continuous functions in 'a => 'b                             *)
 (* this is continuity of fapp in its 'second' argument                      *)
 (* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
 (* ------------------------------------------------------------------------ *)
 
-val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
+qed_goal "contX_fapp2" Cfun2.thy "contX(fapp(fo))"
 (fn prems =>
 	[
 	(res_inst_tac [("P","contX")] CollectD 1),
 	(fold_goals_tac [Cfun_def]),
 	(rtac Rep_Cfun 1)

 
 (* ------------------------------------------------------------------------ *)
 (* fapp is monotone in its 'first' argument                                 *)
 (* ------------------------------------------------------------------------ *)
 
-val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
+qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
 (fn prems =>
 	[
 	(strip_tac 1),
 	(etac (less_cfun RS subst) 1)
 	]);

 
 (* ------------------------------------------------------------------------ *)
 (* monotonicity of application fapp in mixfix syntax [_]_                   *)
 (* ------------------------------------------------------------------------ *)
 
-val monofun_cfun_fun = prove_goal Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
+qed_goal "monofun_cfun_fun" Cfun2.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),

 
 (* ------------------------------------------------------------------------ *)
 (* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
 (* ------------------------------------------------------------------------ *)
 
-val monofun_cfun = prove_goal Cfun2.thy
+qed_goal "monofun_cfun" Cfun2.thy
 	"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac trans_less 1),

 (* ------------------------------------------------------------------------ *)
 (* ch2ch - rules for the type 'a -> 'b                                      *)
 (* use MF2 lemmas from Cont.ML                                              *)
 (* ------------------------------------------------------------------------ *)
 
-val ch2ch_fappR = prove_goal Cfun2.thy 
+qed_goal "ch2ch_fappR" Cfun2.thy 
  "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(etac (monofun_fapp2 RS ch2ch_MF2R) 1)

 (* ------------------------------------------------------------------------ *)
 (*  the lub of a chain of continous functions is monotone                   *)
 (* use MF2 lemmas from Cont.ML                                              *)
 (* ------------------------------------------------------------------------ *)
 
-val lub_cfun_mono = prove_goal Cfun2.thy 
+qed_goal "lub_cfun_mono" Cfun2.thy 
 	"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac lub_MF2_mono 1),

 (* ------------------------------------------------------------------------ *)
 (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
 (* use MF2 lemmas from Cont.ML                                              *)
 (* ------------------------------------------------------------------------ *)
 
-val ex_lubcfun = prove_goal Cfun2.thy
+qed_goal "ex_lubcfun" Cfun2.thy
 	"[| is_chain(F); is_chain(Y) |] ==>\
 \		lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
 \		lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
 (fn prems =>
 	[

 
 (* ------------------------------------------------------------------------ *)
 (* the lub of a chain of cont. functions is continuous                      *)
 (* ------------------------------------------------------------------------ *)
 
-val contX_lubcfun = prove_goal Cfun2.thy 
+qed_goal "contX_lubcfun" Cfun2.thy 
 	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac monocontlub2contX 1),

 
 (* ------------------------------------------------------------------------ *)
 (* type 'a -> 'b is chain complete                                          *)
 (* ------------------------------------------------------------------------ *)
 
-val lub_cfun = prove_goal Cfun2.thy 
+qed_goal "lub_cfun" Cfun2.thy 
   "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac is_lubI 1),

 val thelub_cfun = (lub_cfun RS thelubI);
 (* 
 is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
 *)
 
-val cpo_cfun = prove_goal Cfun2.thy 
+qed_goal "cpo_cfun" Cfun2.thy 
   "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac exI 1),

 
 (* ------------------------------------------------------------------------ *)
 (* Extensionality in 'a -> 'b                                               *)
 (* ------------------------------------------------------------------------ *)
 
-val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
+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","fabs")] arg_cong 1),

 
 (* ------------------------------------------------------------------------ *)
 (* Monotonicity of fabs                                                     *)
 (* ------------------------------------------------------------------------ *)
 
-val semi_monofun_fabs = prove_goal Cfun2.thy 
+qed_goal "semi_monofun_fabs" Cfun2.thy 
 	"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
  (fn prems =>
 	[
 	(rtac (less_cfun RS iffD2) 1),
 	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),

 
 (* ------------------------------------------------------------------------ *)
 (* Extenionality wrt. << in 'a -> 'b                                        *)
 (* ------------------------------------------------------------------------ *)
 
-val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
+qed_goal "less_cfun2" 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_fabs 1),