src/HOLCF/Cfun1.ML
changeset 1461 6bcb44e4d6e5
parent 1168 74be52691d62
child 2033 639de962ded4
     1.1 --- a/src/HOLCF/Cfun1.ML	Mon Jan 29 14:16:13 1996 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Tue Jan 30 13:42:57 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOLCF/cfun1.ML
     1.5 +(*  Title:      HOLCF/cfun1.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Franz Regensburger
     1.8 +    Author:     Franz Regensburger
     1.9      Copyright   1993 Technische Universitaet Muenchen
    1.10  
    1.11  Lemmas for cfun1.thy 
    1.12 @@ -14,10 +14,10 @@
    1.13  
    1.14  qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
    1.15   (fn prems =>
    1.16 -	[
    1.17 -	(rtac (mem_Collect_eq RS ssubst) 1),
    1.18 -	(rtac cont_id 1)
    1.19 -	]);
    1.20 +        [
    1.21 +        (rtac (mem_Collect_eq RS ssubst) 1),
    1.22 +        (rtac cont_id 1)
    1.23 +        ]);
    1.24  
    1.25  
    1.26  (* ------------------------------------------------------------------------ *)
    1.27 @@ -26,60 +26,60 @@
    1.28  
    1.29  qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun f f"
    1.30  (fn prems =>
    1.31 -	[
    1.32 -	(rtac refl_less 1)
    1.33 -	]);
    1.34 +        [
    1.35 +        (rtac refl_less 1)
    1.36 +        ]);
    1.37  
    1.38  qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def] 
    1.39 -	"[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
    1.40 +        "[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
    1.41  (fn prems =>
    1.42 -	[
    1.43 -	(cut_facts_tac prems 1),
    1.44 -	(rtac injD 1),
    1.45 -	(rtac antisym_less 2),
    1.46 -	(atac 3),
    1.47 -	(atac 2),
    1.48 -	(rtac inj_inverseI 1),
    1.49 -	(rtac Rep_Cfun_inverse 1)
    1.50 -	]);
    1.51 +        [
    1.52 +        (cut_facts_tac prems 1),
    1.53 +        (rtac injD 1),
    1.54 +        (rtac antisym_less 2),
    1.55 +        (atac 3),
    1.56 +        (atac 2),
    1.57 +        (rtac inj_inverseI 1),
    1.58 +        (rtac Rep_Cfun_inverse 1)
    1.59 +        ]);
    1.60  
    1.61  qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def] 
    1.62 -	"[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
    1.63 +        "[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
    1.64  (fn prems =>
    1.65 -	[
    1.66 -	(cut_facts_tac prems 1),
    1.67 -	(etac trans_less 1),
    1.68 -	(atac 1)
    1.69 -	]);
    1.70 +        [
    1.71 +        (cut_facts_tac prems 1),
    1.72 +        (etac trans_less 1),
    1.73 +        (atac 1)
    1.74 +        ]);
    1.75  
    1.76  (* ------------------------------------------------------------------------ *)
    1.77  (* lemmas about application of continuous functions                         *)
    1.78  (* ------------------------------------------------------------------------ *)
    1.79  
    1.80  qed_goal "cfun_cong" Cfun1.thy 
    1.81 -	 "[| f=g; x=y |] ==> f`x = g`y"
    1.82 +         "[| f=g; x=y |] ==> f`x = g`y"
    1.83  (fn prems =>
    1.84 -	[
    1.85 -	(cut_facts_tac prems 1),
    1.86 -	(fast_tac HOL_cs 1)
    1.87 -	]);
    1.88 +        [
    1.89 +        (cut_facts_tac prems 1),
    1.90 +        (fast_tac HOL_cs 1)
    1.91 +        ]);
    1.92  
    1.93  qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f`x = g`x"
    1.94  (fn prems =>
    1.95 -	[
    1.96 -	(cut_facts_tac prems 1),
    1.97 -	(etac cfun_cong 1),
    1.98 -	(rtac refl 1)
    1.99 -	]);
   1.100 +        [
   1.101 +        (cut_facts_tac prems 1),
   1.102 +        (etac cfun_cong 1),
   1.103 +        (rtac refl 1)
   1.104 +        ]);
   1.105  
   1.106  qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f`x = f`y"
   1.107  (fn prems =>
   1.108 -	[
   1.109 -	(cut_facts_tac prems 1),
   1.110 -	(rtac cfun_cong 1),
   1.111 -	(rtac refl 1),
   1.112 -	(atac 1)
   1.113 -	]);
   1.114 +        [
   1.115 +        (cut_facts_tac prems 1),
   1.116 +        (rtac cfun_cong 1),
   1.117 +        (rtac refl 1),
   1.118 +        (atac 1)
   1.119 +        ]);
   1.120  
   1.121  
   1.122  (* ------------------------------------------------------------------------ *)
   1.123 @@ -88,37 +88,37 @@
   1.124  
   1.125  qed_goal "Abs_Cfun_inverse2" Cfun1.thy "cont(f) ==> fapp(fabs(f)) = f"
   1.126  (fn prems =>
   1.127 -	[
   1.128 -	(cut_facts_tac prems 1),
   1.129 -	(rtac Abs_Cfun_inverse 1),
   1.130 -	(rewrite_goals_tac [Cfun_def]),
   1.131 -	(etac (mem_Collect_eq RS ssubst) 1)
   1.132 -	]);
   1.133 +        [
   1.134 +        (cut_facts_tac prems 1),
   1.135 +        (rtac Abs_Cfun_inverse 1),
   1.136 +        (rewtac Cfun_def),
   1.137 +        (etac (mem_Collect_eq RS ssubst) 1)
   1.138 +        ]);
   1.139  
   1.140  (* ------------------------------------------------------------------------ *)
   1.141  (* simplification of application                                            *)
   1.142  (* ------------------------------------------------------------------------ *)
   1.143  
   1.144  qed_goal "Cfunapp2" Cfun1.thy 
   1.145 -	"cont(f) ==> (fabs f)`x = f x"
   1.146 +        "cont(f) ==> (fabs f)`x = f x"
   1.147  (fn prems =>
   1.148 -	[
   1.149 -	(cut_facts_tac prems 1),
   1.150 -	(etac (Abs_Cfun_inverse2 RS fun_cong) 1)
   1.151 -	]);
   1.152 +        [
   1.153 +        (cut_facts_tac prems 1),
   1.154 +        (etac (Abs_Cfun_inverse2 RS fun_cong) 1)
   1.155 +        ]);
   1.156  
   1.157  (* ------------------------------------------------------------------------ *)
   1.158  (* beta - equality for continuous functions                                 *)
   1.159  (* ------------------------------------------------------------------------ *)
   1.160  
   1.161  qed_goal "beta_cfun" Cfun1.thy 
   1.162 -	"cont(c1) ==> (LAM x .c1 x)`u = c1 u"
   1.163 +        "cont(c1) ==> (LAM x .c1 x)`u = c1 u"
   1.164  (fn prems =>
   1.165 -	[
   1.166 -	(cut_facts_tac prems 1),
   1.167 -	(rtac Cfunapp2 1),
   1.168 -	(atac 1)
   1.169 -	]);
   1.170 +        [
   1.171 +        (cut_facts_tac prems 1),
   1.172 +        (rtac Cfunapp2 1),
   1.173 +        (atac 1)
   1.174 +        ]);
   1.175  
   1.176  
   1.177