src/HOLCF/Cfun1.ML
changeset 9245 428385c4bc50
parent 5291 5706f0ef1d43
child 9248 e1dee89de037
     1.1 --- a/src/HOLCF/Cfun1.ML	Tue Jul 04 14:58:40 2000 +0200
     1.2 +++ b/src/HOLCF/Cfun1.ML	Tue Jul 04 15:58:11 2000 +0200
     1.3 @@ -3,129 +3,103 @@
     1.4      Author:     Franz Regensburger
     1.5      Copyright   1993 Technische Universitaet Muenchen
     1.6  
     1.7 -Lemmas for Cfun1.thy 
     1.8 +The type ->  of continuous functions.
     1.9  *)
    1.10  
    1.11 -open Cfun1;
    1.12 -
    1.13  (* ------------------------------------------------------------------------ *)
    1.14  (* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
    1.15  (* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
    1.16  (* ------------------------------------------------------------------------ *)
    1.17 -qed_goal "Rep_Cfun" thy "Rep_CFun fo : CFun"
    1.18 -(fn prems =>
    1.19 -        [
    1.20 -        (rtac Rep_CFun 1)
    1.21 -        ]);
    1.22 +val prems = goal thy "Rep_CFun fo : CFun";
    1.23 +by (rtac Rep_CFun 1);
    1.24 +qed "Rep_Cfun";
    1.25  
    1.26 -qed_goal "Rep_Cfun_inverse" thy "Abs_CFun (Rep_CFun fo) = fo"
    1.27 -(fn prems =>
    1.28 -        [
    1.29 -        (rtac Rep_CFun_inverse 1)
    1.30 -        ]);
    1.31 +val prems = goal thy "Abs_CFun (Rep_CFun fo) = fo";
    1.32 +by (rtac Rep_CFun_inverse 1);
    1.33 +qed "Rep_Cfun_inverse";
    1.34  
    1.35 -qed_goal "Abs_Cfun_inverse" thy "f:CFun==>Rep_CFun(Abs_CFun f)=f"
    1.36 -(fn prems =>
    1.37 -        [
    1.38 -	(cut_facts_tac prems 1),
    1.39 -        (etac Abs_CFun_inverse 1)
    1.40 -        ]);
    1.41 +val prems = goal thy "f:CFun==>Rep_CFun(Abs_CFun f)=f";
    1.42 +by (cut_facts_tac prems 1);
    1.43 +by (etac Abs_CFun_inverse 1);
    1.44 +qed "Abs_Cfun_inverse";
    1.45  
    1.46  (* ------------------------------------------------------------------------ *)
    1.47  (* less_cfun is a partial order on type 'a -> 'b                            *)
    1.48  (* ------------------------------------------------------------------------ *)
    1.49  
    1.50 -qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
    1.51 -(fn prems =>
    1.52 -        [
    1.53 -        (rtac refl_less 1)
    1.54 -        ]);
    1.55 +val prems = goalw thy [less_cfun_def] "(f::'a->'b) << f";
    1.56 +by (rtac refl_less 1);
    1.57 +qed "refl_less_cfun";
    1.58  
    1.59 -qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
    1.60 -        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
    1.61 -(fn prems =>
    1.62 -        [
    1.63 -        (cut_facts_tac prems 1),
    1.64 -        (rtac injD 1),
    1.65 -        (rtac antisym_less 2),
    1.66 -        (atac 3),
    1.67 -        (atac 2),
    1.68 -        (rtac inj_inverseI 1),
    1.69 -        (rtac Rep_Cfun_inverse 1)
    1.70 -        ]);
    1.71 +val prems = goalw thy [less_cfun_def] 
    1.72 +        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2";
    1.73 +by (cut_facts_tac prems 1);
    1.74 +by (rtac injD 1);
    1.75 +by (rtac antisym_less 2);
    1.76 +by (atac 3);
    1.77 +by (atac 2);
    1.78 +by (rtac inj_inverseI 1);
    1.79 +by (rtac Rep_Cfun_inverse 1);
    1.80 +qed "antisym_less_cfun";
    1.81  
    1.82 -qed_goalw "trans_less_cfun" thy [less_cfun_def] 
    1.83 -        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
    1.84 -(fn prems =>
    1.85 -        [
    1.86 -        (cut_facts_tac prems 1),
    1.87 -        (etac trans_less 1),
    1.88 -        (atac 1)
    1.89 -        ]);
    1.90 +val prems = goalw thy [less_cfun_def] 
    1.91 +        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3";
    1.92 +by (cut_facts_tac prems 1);
    1.93 +by (etac trans_less 1);
    1.94 +by (atac 1);
    1.95 +qed "trans_less_cfun";
    1.96  
    1.97  (* ------------------------------------------------------------------------ *)
    1.98  (* lemmas about application of continuous functions                         *)
    1.99  (* ------------------------------------------------------------------------ *)
   1.100  
   1.101 -qed_goal "cfun_cong" thy 
   1.102 -         "[| f=g; x=y |] ==> f`x = g`y"
   1.103 -(fn prems =>
   1.104 -        [
   1.105 -        (cut_facts_tac prems 1),
   1.106 -        (fast_tac HOL_cs 1)
   1.107 -        ]);
   1.108 +val prems = goal thy 
   1.109 +         "[| f=g; x=y |] ==> f`x = g`y";
   1.110 +by (cut_facts_tac prems 1);
   1.111 +by (fast_tac HOL_cs 1);
   1.112 +qed "cfun_cong";
   1.113  
   1.114 -qed_goal "cfun_fun_cong" thy "f=g ==> f`x = g`x"
   1.115 -(fn prems =>
   1.116 -        [
   1.117 -        (cut_facts_tac prems 1),
   1.118 -        (etac cfun_cong 1),
   1.119 -        (rtac refl 1)
   1.120 -        ]);
   1.121 +val prems = goal thy "f=g ==> f`x = g`x";
   1.122 +by (cut_facts_tac prems 1);
   1.123 +by (etac cfun_cong 1);
   1.124 +by (rtac refl 1);
   1.125 +qed "cfun_fun_cong";
   1.126  
   1.127 -qed_goal "cfun_arg_cong" thy "x=y ==> f`x = f`y"
   1.128 -(fn prems =>
   1.129 -        [
   1.130 -        (cut_facts_tac prems 1),
   1.131 -        (rtac cfun_cong 1),
   1.132 -        (rtac refl 1),
   1.133 -        (atac 1)
   1.134 -        ]);
   1.135 +val prems = goal thy "x=y ==> f`x = f`y";
   1.136 +by (cut_facts_tac prems 1);
   1.137 +by (rtac cfun_cong 1);
   1.138 +by (rtac refl 1);
   1.139 +by (atac 1);
   1.140 +qed "cfun_arg_cong";
   1.141  
   1.142  
   1.143  (* ------------------------------------------------------------------------ *)
   1.144  (* additional lemma about the isomorphism between -> and Cfun               *)
   1.145  (* ------------------------------------------------------------------------ *)
   1.146  
   1.147 -qed_goal "Abs_Cfun_inverse2" thy "cont f ==> Rep_CFun (Abs_CFun f) = f"
   1.148 -(fn prems =>
   1.149 -        [
   1.150 -        (cut_facts_tac prems 1),
   1.151 -        (rtac Abs_Cfun_inverse 1),
   1.152 -        (rewtac CFun_def),
   1.153 -        (etac (mem_Collect_eq RS ssubst) 1)
   1.154 -        ]);
   1.155 +val prems = goal thy "cont f ==> Rep_CFun (Abs_CFun f) = f";
   1.156 +by (cut_facts_tac prems 1);
   1.157 +by (rtac Abs_Cfun_inverse 1);
   1.158 +by (rewtac CFun_def);
   1.159 +by (etac (mem_Collect_eq RS ssubst) 1);
   1.160 +qed "Abs_Cfun_inverse2";
   1.161  
   1.162  (* ------------------------------------------------------------------------ *)
   1.163  (* simplification of application                                            *)
   1.164  (* ------------------------------------------------------------------------ *)
   1.165  
   1.166 -qed_goal "Cfunapp2" thy "cont f ==> (Abs_CFun f)`x = f x"
   1.167 -(fn prems =>
   1.168 -        [
   1.169 -        (cut_facts_tac prems 1),
   1.170 -        (etac (Abs_Cfun_inverse2 RS fun_cong) 1)
   1.171 -        ]);
   1.172 +val prems = goal thy "cont f ==> (Abs_CFun f)`x = f x";
   1.173 +by (cut_facts_tac prems 1);
   1.174 +by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
   1.175 +qed "Cfunapp2";
   1.176  
   1.177  (* ------------------------------------------------------------------------ *)
   1.178  (* beta - equality for continuous functions                                 *)
   1.179  (* ------------------------------------------------------------------------ *)
   1.180  
   1.181 -qed_goal "beta_cfun" thy 
   1.182 -        "cont(c1) ==> (LAM x .c1 x)`u = c1 u"
   1.183 -(fn prems =>
   1.184 -        [
   1.185 -        (cut_facts_tac prems 1),
   1.186 -        (rtac Cfunapp2 1),
   1.187 -        (atac 1)
   1.188 -        ]);
   1.189 +val prems = goal thy 
   1.190 +        "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
   1.191 +by (cut_facts_tac prems 1);
   1.192 +by (rtac Cfunapp2 1);
   1.193 +by (atac 1);
   1.194 +qed "beta_cfun";