src/HOL/AxClasses/Lattice/CLattice.ML
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -7,46 +7,46 @@
     1.4  (* unique existence *)
     1.5  
     1.6  goalw thy [Inf_def] "is_Inf A (Inf A)";
     1.7 -  br (ex_Inf RS spec RS selectI1) 1;
     1.8 +  by (rtac (ex_Inf RS spec RS selectI1) 1);
     1.9  qed "Inf_is_Inf";
    1.10  
    1.11  goal thy "is_Inf A inf --> Inf A = inf";
    1.12 -  br impI 1;
    1.13 -  br (is_Inf_uniq RS mp) 1;
    1.14 -  br conjI 1;
    1.15 -  br Inf_is_Inf 1;
    1.16 -  ba 1;
    1.17 +  by (rtac impI 1);
    1.18 +  by (rtac (is_Inf_uniq RS mp) 1);
    1.19 +  by (rtac conjI 1);
    1.20 +  by (rtac Inf_is_Inf 1);
    1.21 +  by (assume_tac 1);
    1.22  qed "Inf_uniq";
    1.23  
    1.24  goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
    1.25 -  by (safe_tac (claset()));
    1.26 +  by Safe_tac;
    1.27    by (Step_tac 1);
    1.28    by (Step_tac 1);
    1.29 -  br Inf_is_Inf 1;
    1.30 -  br (Inf_uniq RS mp RS sym) 1;
    1.31 -  ba 1;
    1.32 +  by (rtac Inf_is_Inf 1);
    1.33 +  by (rtac (Inf_uniq RS mp RS sym) 1);
    1.34 +  by (assume_tac 1);
    1.35  qed "ex1_Inf";
    1.36  
    1.37  
    1.38  goalw thy [Sup_def] "is_Sup A (Sup A)";
    1.39 -  br (ex_Sup RS spec RS selectI1) 1;
    1.40 +  by (rtac (ex_Sup RS spec RS selectI1) 1);
    1.41  qed "Sup_is_Sup";
    1.42  
    1.43  goal thy "is_Sup A sup --> Sup A = sup";
    1.44 -  br impI 1;
    1.45 -  br (is_Sup_uniq RS mp) 1;
    1.46 -  br conjI 1;
    1.47 -  br Sup_is_Sup 1;
    1.48 -  ba 1;
    1.49 +  by (rtac impI 1);
    1.50 +  by (rtac (is_Sup_uniq RS mp) 1);
    1.51 +  by (rtac conjI 1);
    1.52 +  by (rtac Sup_is_Sup 1);
    1.53 +  by (assume_tac 1);
    1.54  qed "Sup_uniq";
    1.55  
    1.56  goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
    1.57 -  by (safe_tac (claset()));
    1.58 +  by Safe_tac;
    1.59    by (Step_tac 1);
    1.60    by (Step_tac 1);
    1.61 -  br Sup_is_Sup 1;
    1.62 -  br (Sup_uniq RS mp RS sym) 1;
    1.63 -  ba 1;
    1.64 +  by (rtac Sup_is_Sup 1);
    1.65 +  by (rtac (Sup_uniq RS mp RS sym) 1);
    1.66 +  by (assume_tac 1);
    1.67  qed "ex1_Sup";
    1.68  
    1.69  
    1.70 @@ -54,68 +54,68 @@
    1.71  
    1.72  val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
    1.73    by (cut_facts_tac prems 1);
    1.74 -  br selectI2 1;
    1.75 -  br Inf_is_Inf 1;
    1.76 +  by (rtac selectI2 1);
    1.77 +  by (rtac Inf_is_Inf 1);
    1.78    by (rewtac is_Inf_def);
    1.79    by (Fast_tac 1);
    1.80  qed "Inf_lb";
    1.81  
    1.82  val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
    1.83 -  br selectI2 1;
    1.84 -  br Inf_is_Inf 1;
    1.85 +  by (rtac selectI2 1);
    1.86 +  by (rtac Inf_is_Inf 1);
    1.87    by (rewtac is_Inf_def);
    1.88    by (Step_tac 1);
    1.89    by (Step_tac 1);
    1.90 -  be mp 1;
    1.91 -  br ballI 1;
    1.92 -  be prem 1;
    1.93 +  by (etac mp 1);
    1.94 +  by (rtac ballI 1);
    1.95 +  by (etac prem 1);
    1.96  qed "Inf_ub_lbs";
    1.97  
    1.98  
    1.99  val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
   1.100    by (cut_facts_tac prems 1);
   1.101 -  br selectI2 1;
   1.102 -  br Sup_is_Sup 1;
   1.103 +  by (rtac selectI2 1);
   1.104 +  by (rtac Sup_is_Sup 1);
   1.105    by (rewtac is_Sup_def);
   1.106    by (Fast_tac 1);
   1.107  qed "Sup_ub";
   1.108  
   1.109  val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
   1.110 -  br selectI2 1;
   1.111 -  br Sup_is_Sup 1;
   1.112 +  by (rtac selectI2 1);
   1.113 +  by (rtac Sup_is_Sup 1);
   1.114    by (rewtac is_Sup_def);
   1.115    by (Step_tac 1);
   1.116    by (Step_tac 1);
   1.117 -  be mp 1;
   1.118 -  br ballI 1;
   1.119 -  be prem 1;
   1.120 +  by (etac mp 1);
   1.121 +  by (rtac ballI 1);
   1.122 +  by (etac prem 1);
   1.123  qed "Sup_lb_ubs";
   1.124  
   1.125  
   1.126  (** minorized Infs / majorized Sups **)
   1.127  
   1.128  goal thy "(x [= Inf A) = (ALL y:A. x [= y)";
   1.129 -  br iffI 1;
   1.130 +  by (rtac iffI 1);
   1.131    (*==>*)
   1.132 -    br ballI 1;
   1.133 -    br (le_trans RS mp) 1;
   1.134 -    be conjI 1;
   1.135 -    be Inf_lb 1;
   1.136 +    by (rtac ballI 1);
   1.137 +    by (rtac (le_trans RS mp) 1);
   1.138 +    by (etac conjI 1);
   1.139 +    by (etac Inf_lb 1);
   1.140    (*<==*)
   1.141 -    br Inf_ub_lbs 1;
   1.142 +    by (rtac Inf_ub_lbs 1);
   1.143      by (Fast_tac 1);
   1.144  qed "le_Inf_eq";
   1.145  
   1.146  goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
   1.147 -  br iffI 1;
   1.148 +  by (rtac iffI 1);
   1.149    (*==>*)
   1.150 -    br ballI 1;
   1.151 -    br (le_trans RS mp) 1;
   1.152 -    br conjI 1;
   1.153 -    be Sup_ub 1;
   1.154 -    ba 1;
   1.155 +    by (rtac ballI 1);
   1.156 +    by (rtac (le_trans RS mp) 1);
   1.157 +    by (rtac conjI 1);
   1.158 +    by (etac Sup_ub 1);
   1.159 +    by (assume_tac 1);
   1.160    (*<==*)
   1.161 -    br Sup_lb_ubs 1;
   1.162 +    by (rtac Sup_lb_ubs 1);
   1.163      by (Fast_tac 1);
   1.164  qed "ge_Sup_eq";
   1.165  
   1.166 @@ -124,60 +124,60 @@
   1.167  (** Subsets and limits **)
   1.168  
   1.169  goal thy "A <= B --> Inf B [= Inf A";
   1.170 -  br impI 1;
   1.171 +  by (rtac impI 1);
   1.172    by (stac le_Inf_eq 1);
   1.173    by (rewtac Ball_def);
   1.174 -  by (safe_tac (claset()));
   1.175 -  bd subsetD 1;
   1.176 -  ba 1;
   1.177 -  be Inf_lb 1;
   1.178 +  by Safe_tac;
   1.179 +  by (dtac subsetD 1);
   1.180 +  by (assume_tac 1);
   1.181 +  by (etac Inf_lb 1);
   1.182  qed "Inf_subset_antimon";
   1.183  
   1.184  goal thy "A <= B --> Sup A [= Sup B";
   1.185 -  br impI 1;
   1.186 +  by (rtac impI 1);
   1.187    by (stac ge_Sup_eq 1);
   1.188    by (rewtac Ball_def);
   1.189 -  by (safe_tac (claset()));
   1.190 -  bd subsetD 1;
   1.191 -  ba 1;
   1.192 -  be Sup_ub 1;
   1.193 +  by Safe_tac;
   1.194 +  by (dtac subsetD 1);
   1.195 +  by (assume_tac 1);
   1.196 +  by (etac Sup_ub 1);
   1.197  qed "Sup_subset_mon";
   1.198  
   1.199  
   1.200  (** singleton / empty limits **)
   1.201  
   1.202  goal thy "Inf {x} = x";
   1.203 -  br (Inf_uniq RS mp) 1;
   1.204 +  by (rtac (Inf_uniq RS mp) 1);
   1.205    by (rewtac is_Inf_def);
   1.206 -  by (safe_tac (claset()));
   1.207 -  br le_refl 1;
   1.208 +  by Safe_tac;
   1.209 +  by (rtac le_refl 1);
   1.210    by (Fast_tac 1);
   1.211  qed "sing_Inf_eq";
   1.212  
   1.213  goal thy "Sup {x} = x";
   1.214 -  br (Sup_uniq RS mp) 1;
   1.215 +  by (rtac (Sup_uniq RS mp) 1);
   1.216    by (rewtac is_Sup_def);
   1.217 -  by (safe_tac (claset()));
   1.218 -  br le_refl 1;
   1.219 +  by Safe_tac;
   1.220 +  by (rtac le_refl 1);
   1.221    by (Fast_tac 1);
   1.222  qed "sing_Sup_eq";
   1.223  
   1.224  
   1.225  goal thy "Inf {} = Sup {x. True}";
   1.226 -  br (Inf_uniq RS mp) 1;
   1.227 +  by (rtac (Inf_uniq RS mp) 1);
   1.228    by (rewtac is_Inf_def);
   1.229 -  by (safe_tac (claset()));
   1.230 -  br (sing_Sup_eq RS subst) 1;
   1.231 +  by Safe_tac;
   1.232 +  by (rtac (sing_Sup_eq RS subst) 1);
   1.233    back();
   1.234 -  br (Sup_subset_mon RS mp) 1;
   1.235 +  by (rtac (Sup_subset_mon RS mp) 1);
   1.236    by (Fast_tac 1);
   1.237  qed "empty_Inf_eq";
   1.238  
   1.239  goal thy "Sup {} = Inf {x. True}";
   1.240 -  br (Sup_uniq RS mp) 1;
   1.241 +  by (rtac (Sup_uniq RS mp) 1);
   1.242    by (rewtac is_Sup_def);
   1.243 -  by (safe_tac (claset()));
   1.244 -  br (sing_Inf_eq RS subst) 1;
   1.245 -  br (Inf_subset_antimon RS mp) 1;
   1.246 +  by Safe_tac;
   1.247 +  by (rtac (sing_Inf_eq RS subst) 1);
   1.248 +  by (rtac (Inf_subset_antimon RS mp) 1);
   1.249    by (Fast_tac 1);
   1.250  qed "empty_Sup_eq";