src/HOLCF/Cfun1.ML
changeset 892 d0dc8d057929
parent 752 b89462f9d5f1
child 1168 74be52691d62
     1.1 --- a/src/HOLCF/Cfun1.ML	Fri Feb 03 12:32:14 1995 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Tue Feb 07 11:59:32 1995 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  (* A non-emptyness result for Cfun                                          *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -val CfunI = prove_goalw Cfun1.thy [Cfun_def] "(% x.x):Cfun"
     1.8 +qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
     1.9   (fn prems =>
    1.10  	[
    1.11  	(rtac (mem_Collect_eq RS ssubst) 1),
    1.12 @@ -24,13 +24,13 @@
    1.13  (* less_cfun is a partial order on type 'a -> 'b                            *)
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  
    1.16 -val refl_less_cfun = prove_goalw Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
    1.17 +qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
    1.18  (fn prems =>
    1.19  	[
    1.20  	(rtac refl_less 1)
    1.21  	]);
    1.22  
    1.23 -val antisym_less_cfun = prove_goalw Cfun1.thy [less_cfun_def] 
    1.24 +qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
    1.25  	"[|less_cfun(f1,f2); less_cfun(f2,f1)|] ==> f1 = f2"
    1.26  (fn prems =>
    1.27  	[
    1.28 @@ -43,7 +43,7 @@
    1.29  	(rtac Rep_Cfun_inverse 1)
    1.30  	]);
    1.31  
    1.32 -val trans_less_cfun = prove_goalw Cfun1.thy [less_cfun_def] 
    1.33 +qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
    1.34  	"[|less_cfun(f1,f2); less_cfun(f2,f3)|] ==> less_cfun(f1,f3)"
    1.35  (fn prems =>
    1.36  	[
    1.37 @@ -56,7 +56,7 @@
    1.38  (* lemmas about application of continuous functions                         *)
    1.39  (* ------------------------------------------------------------------------ *)
    1.40  
    1.41 -val cfun_cong = prove_goal Cfun1.thy 
    1.42 +qed_goal "cfun_cong" Cfun1.thy 
    1.43  	 "[| f=g; x=y |] ==> f[x] = g[y]"
    1.44  (fn prems =>
    1.45  	[
    1.46 @@ -64,7 +64,7 @@
    1.47  	(fast_tac HOL_cs 1)
    1.48  	]);
    1.49  
    1.50 -val cfun_fun_cong = prove_goal Cfun1.thy "f=g ==> f[x] = g[x]"
    1.51 +qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f[x] = g[x]"
    1.52  (fn prems =>
    1.53  	[
    1.54  	(cut_facts_tac prems 1),
    1.55 @@ -72,7 +72,7 @@
    1.56  	(rtac refl 1)
    1.57  	]);
    1.58  
    1.59 -val cfun_arg_cong = prove_goal Cfun1.thy "x=y ==> f[x] = f[y]"
    1.60 +qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f[x] = f[y]"
    1.61  (fn prems =>
    1.62  	[
    1.63  	(cut_facts_tac prems 1),
    1.64 @@ -86,7 +86,7 @@
    1.65  (* additional lemma about the isomorphism between -> and Cfun               *)
    1.66  (* ------------------------------------------------------------------------ *)
    1.67  
    1.68 -val Abs_Cfun_inverse2 = prove_goal Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
    1.69 +qed_goal "Abs_Cfun_inverse2" Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
    1.70  (fn prems =>
    1.71  	[
    1.72  	(cut_facts_tac prems 1),
    1.73 @@ -99,7 +99,7 @@
    1.74  (* simplification of application                                            *)
    1.75  (* ------------------------------------------------------------------------ *)
    1.76  
    1.77 -val Cfunapp2 = prove_goal Cfun1.thy 
    1.78 +qed_goal "Cfunapp2" Cfun1.thy 
    1.79  	"contX(f) ==> (fabs(f))[x] = f(x)"
    1.80  (fn prems =>
    1.81  	[
    1.82 @@ -111,7 +111,7 @@
    1.83  (* beta - equality for continuous functions                                 *)
    1.84  (* ------------------------------------------------------------------------ *)
    1.85  
    1.86 -val beta_cfun = prove_goal Cfun1.thy 
    1.87 +qed_goal "beta_cfun" Cfun1.thy 
    1.88  	"contX(c1) ==> (LAM x .c1(x))[u] = c1(u)"
    1.89  (fn prems =>
    1.90  	[