src/HOLCF/Cfun1.ML
changeset 1168 74be52691d62
parent 892 d0dc8d057929
child 1461 6bcb44e4d6e5
     1.1 --- a/src/HOLCF/Cfun1.ML	Thu Jun 29 16:16:24 1995 +0200
     1.2 +++ b/src/HOLCF/Cfun1.ML	Thu Jun 29 16:28:40 1995 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4   (fn prems =>
     1.5  	[
     1.6  	(rtac (mem_Collect_eq RS ssubst) 1),
     1.7 -	(rtac contX_id 1)
     1.8 +	(rtac cont_id 1)
     1.9  	]);
    1.10  
    1.11  
    1.12 @@ -24,14 +24,14 @@
    1.13  (* less_cfun is a partial order on type 'a -> 'b                            *)
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  
    1.16 -qed_goalw "refl_less_cfun" 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  qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
    1.24 -	"[|less_cfun(f1,f2); less_cfun(f2,f1)|] ==> f1 = f2"
    1.25 +	"[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
    1.26  (fn prems =>
    1.27  	[
    1.28  	(cut_facts_tac prems 1),
    1.29 @@ -44,7 +44,7 @@
    1.30  	]);
    1.31  
    1.32  qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
    1.33 -	"[|less_cfun(f1,f2); less_cfun(f2,f3)|] ==> less_cfun(f1,f3)"
    1.34 +	"[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
    1.35  (fn prems =>
    1.36  	[
    1.37  	(cut_facts_tac prems 1),
    1.38 @@ -57,14 +57,14 @@
    1.39  (* ------------------------------------------------------------------------ *)
    1.40  
    1.41  qed_goal "cfun_cong" Cfun1.thy 
    1.42 -	 "[| f=g; x=y |] ==> f[x] = g[y]"
    1.43 +	 "[| f=g; x=y |] ==> f`x = g`y"
    1.44  (fn prems =>
    1.45  	[
    1.46  	(cut_facts_tac prems 1),
    1.47  	(fast_tac HOL_cs 1)
    1.48  	]);
    1.49  
    1.50 -qed_goal "cfun_fun_cong" 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 -qed_goal "cfun_arg_cong" 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 -qed_goal "Abs_Cfun_inverse2" Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
    1.69 +qed_goal "Abs_Cfun_inverse2" Cfun1.thy "cont(f) ==> fapp(fabs(f)) = f"
    1.70  (fn prems =>
    1.71  	[
    1.72  	(cut_facts_tac prems 1),
    1.73 @@ -100,7 +100,7 @@
    1.74  (* ------------------------------------------------------------------------ *)
    1.75  
    1.76  qed_goal "Cfunapp2" Cfun1.thy 
    1.77 -	"contX(f) ==> (fabs(f))[x] = f(x)"
    1.78 +	"cont(f) ==> (fabs f)`x = f x"
    1.79  (fn prems =>
    1.80  	[
    1.81  	(cut_facts_tac prems 1),
    1.82 @@ -112,7 +112,7 @@
    1.83  (* ------------------------------------------------------------------------ *)
    1.84  
    1.85  qed_goal "beta_cfun" Cfun1.thy 
    1.86 -	"contX(c1) ==> (LAM x .c1(x))[u] = c1(u)"
    1.87 +	"cont(c1) ==> (LAM x .c1 x)`u = c1 u"
    1.88  (fn prems =>
    1.89  	[
    1.90  	(cut_facts_tac prems 1),
    1.91 @@ -120,3 +120,6 @@
    1.92  	(atac 1)
    1.93  	]);
    1.94  
    1.95 +
    1.96 +
    1.97 +