src/HOL/AxClasses/Lattice/Lattice.ML
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.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 x y (x && y)";
     1.7 -  br (ex_inf RS spec RS spec RS selectI1) 1;
     1.8 +  by (rtac (ex_inf RS spec RS spec RS selectI1) 1);
     1.9  qed "inf_is_inf";
    1.10  
    1.11  goal thy "is_inf x y inf --> x && y = 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 x y. EX! inf::'a::lattice. is_inf x y 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 x y (x || y)";
    1.39 -  br (ex_sup RS spec RS spec RS selectI1) 1;
    1.40 +  by (rtac (ex_sup RS spec RS spec RS selectI1) 1);
    1.41  qed "sup_is_sup";
    1.42  
    1.43  goal thy "is_sup x y sup --> x || y = 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 x y. EX! sup::'a::lattice. is_sup x y 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 @@ -96,30 +96,30 @@
    1.71  (* the Connection Theorems: "[=" expressed via "&&" or "||" *)
    1.72  
    1.73  goal thy "(x && y = x) = (x [= y)";
    1.74 -  br iffI 1;
    1.75 +  by (rtac iffI 1);
    1.76    (*==>*)
    1.77 -    be subst 1;
    1.78 -    br inf_lb2 1;
    1.79 +    by (etac subst 1);
    1.80 +    by (rtac inf_lb2 1);
    1.81    (*<==*)
    1.82 -    br (inf_uniq RS mp) 1;
    1.83 +    by (rtac (inf_uniq RS mp) 1);
    1.84      by (rewtac is_inf_def);
    1.85      by (REPEAT_FIRST (rtac conjI));
    1.86 -    br le_refl 1;
    1.87 -    ba 1;
    1.88 +    by (rtac le_refl 1);
    1.89 +    by (assume_tac 1);
    1.90      by (Fast_tac 1);
    1.91  qed "inf_connect";
    1.92  
    1.93  goal thy "(x || y = y) = (x [= y)";
    1.94 -  br iffI 1;
    1.95 +  by (rtac iffI 1);
    1.96    (*==>*)
    1.97 -    be subst 1;
    1.98 -    br sup_ub1 1;
    1.99 +    by (etac subst 1);
   1.100 +    by (rtac sup_ub1 1);
   1.101    (*<==*)
   1.102 -    br (sup_uniq RS mp) 1;
   1.103 +    by (rtac (sup_uniq RS mp) 1);
   1.104      by (rewtac is_sup_def);
   1.105      by (REPEAT_FIRST (rtac conjI));
   1.106 -    ba 1;
   1.107 -    br le_refl 1;
   1.108 +    by (assume_tac 1);
   1.109 +    by (rtac le_refl 1);
   1.110      by (Fast_tac 1);
   1.111  qed "sup_connect";
   1.112  
   1.113 @@ -127,37 +127,37 @@
   1.114  (* minorized infs / majorized sups *)
   1.115  
   1.116  goal thy "(x [= y && z) = (x [= y & x [= z)";
   1.117 -  br iffI 1;
   1.118 +  by (rtac iffI 1);
   1.119    (*==> (level 1)*)
   1.120      by (cut_facts_tac [inf_lb1, inf_lb2] 1);
   1.121 -    br conjI 1;
   1.122 -    br (le_trans RS mp) 1;
   1.123 -    be conjI 1;
   1.124 -    ba 1;
   1.125 -    br (le_trans RS mp) 1;
   1.126 -    be conjI 1;
   1.127 -    ba 1;
   1.128 +    by (rtac conjI 1);
   1.129 +    by (rtac (le_trans RS mp) 1);
   1.130 +    by (etac conjI 1);
   1.131 +    by (assume_tac 1);
   1.132 +    by (rtac (le_trans RS mp) 1);
   1.133 +    by (etac conjI 1);
   1.134 +    by (assume_tac 1);
   1.135    (*<== (level 9)*)
   1.136 -    be conjE 1;
   1.137 -    be inf_ub_lbs 1;
   1.138 -    ba 1;
   1.139 +    by (etac conjE 1);
   1.140 +    by (etac inf_ub_lbs 1);
   1.141 +    by (assume_tac 1);
   1.142  qed "le_inf_eq";
   1.143  
   1.144  goal thy "(x || y [= z) = (x [= z & y [= z)";
   1.145 -  br iffI 1;
   1.146 +  by (rtac iffI 1);
   1.147    (*==> (level 1)*)
   1.148      by (cut_facts_tac [sup_ub1, sup_ub2] 1);
   1.149 -    br conjI 1;
   1.150 -    br (le_trans RS mp) 1;
   1.151 -    be conjI 1;
   1.152 -    ba 1;
   1.153 -    br (le_trans RS mp) 1;
   1.154 -    be conjI 1;
   1.155 -    ba 1;
   1.156 +    by (rtac conjI 1);
   1.157 +    by (rtac (le_trans RS mp) 1);
   1.158 +    by (etac conjI 1);
   1.159 +    by (assume_tac 1);
   1.160 +    by (rtac (le_trans RS mp) 1);
   1.161 +    by (etac conjI 1);
   1.162 +    by (assume_tac 1);
   1.163    (*<== (level 9)*)
   1.164 -    be conjE 1;
   1.165 -    be sup_lb_ubs 1;
   1.166 -    ba 1;
   1.167 +    by (etac conjE 1);
   1.168 +    by (etac sup_lb_ubs 1);
   1.169 +    by (assume_tac 1);
   1.170  qed "ge_sup_eq";
   1.171  
   1.172  
   1.173 @@ -175,8 +175,8 @@
   1.174    back();
   1.175    back();
   1.176    back();
   1.177 -  br refl 2;
   1.178 -  br (is_inf_assoc RS mp) 1;
   1.179 +  by (rtac refl 2);
   1.180 +  by (rtac (is_inf_assoc RS mp) 1);
   1.181    by (REPEAT_FIRST (rtac conjI));
   1.182    by (REPEAT_FIRST (rtac inf_is_inf));
   1.183  qed "inf_assoc";
   1.184 @@ -191,8 +191,8 @@
   1.185    back();
   1.186    back();
   1.187    back();
   1.188 -  br refl 2;
   1.189 -  br (is_sup_assoc RS mp) 1;
   1.190 +  by (rtac refl 2);
   1.191 +  by (rtac (is_sup_assoc RS mp) 1);
   1.192    by (REPEAT_FIRST (rtac conjI));
   1.193    by (REPEAT_FIRST (rtac sup_is_sup));
   1.194  qed "sup_assoc";
   1.195 @@ -202,12 +202,12 @@
   1.196  
   1.197  goalw thy [inf_def] "x && y = y && x";
   1.198    by (stac (is_inf_commut RS ext) 1);
   1.199 -  br refl 1;
   1.200 +  by (rtac refl 1);
   1.201  qed "inf_commut";
   1.202  
   1.203  goalw thy [sup_def] "x || y = y || x";
   1.204    by (stac (is_sup_commut RS ext) 1);
   1.205 -  br refl 1;
   1.206 +  by (rtac refl 1);
   1.207  qed "sup_commut";
   1.208  
   1.209  
   1.210 @@ -215,12 +215,12 @@
   1.211  
   1.212  goal thy "x && x = x";
   1.213    by (stac inf_connect 1);
   1.214 -  br le_refl 1;
   1.215 +  by (rtac le_refl 1);
   1.216  qed "inf_idemp";
   1.217  
   1.218  goal thy "x || x = x";
   1.219    by (stac sup_connect 1);
   1.220 -  br le_refl 1;
   1.221 +  by (rtac le_refl 1);
   1.222  qed "sup_idemp";
   1.223  
   1.224  
   1.225 @@ -229,12 +229,12 @@
   1.226  goal thy "x || (x && y) = x";
   1.227    by (stac sup_commut 1);
   1.228    by (stac sup_connect 1);
   1.229 -  br inf_lb1 1;
   1.230 +  by (rtac inf_lb1 1);
   1.231  qed "sup_inf_absorb";
   1.232  
   1.233  goal thy "x && (x || y) = x";
   1.234    by (stac inf_connect 1);
   1.235 -  br sup_ub1 1;
   1.236 +  by (rtac sup_ub1 1);
   1.237  qed "inf_sup_absorb";
   1.238  
   1.239  
   1.240 @@ -243,27 +243,27 @@
   1.241  val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
   1.242    by (cut_facts_tac prems 1);
   1.243    by (stac le_inf_eq 1);
   1.244 -  br conjI 1;
   1.245 -  br (le_trans RS mp) 1;
   1.246 -  br conjI 1;
   1.247 -  br inf_lb1 1;
   1.248 -  ba 1;
   1.249 -  br (le_trans RS mp) 1;
   1.250 -  br conjI 1;
   1.251 -  br inf_lb2 1;
   1.252 -  ba 1;
   1.253 +  by (rtac conjI 1);
   1.254 +  by (rtac (le_trans RS mp) 1);
   1.255 +  by (rtac conjI 1);
   1.256 +  by (rtac inf_lb1 1);
   1.257 +  by (assume_tac 1);
   1.258 +  by (rtac (le_trans RS mp) 1);
   1.259 +  by (rtac conjI 1);
   1.260 +  by (rtac inf_lb2 1);
   1.261 +  by (assume_tac 1);
   1.262  qed "inf_mon";
   1.263  
   1.264  val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
   1.265    by (cut_facts_tac prems 1);
   1.266    by (stac ge_sup_eq 1);
   1.267 -  br conjI 1;
   1.268 -  br (le_trans RS mp) 1;
   1.269 -  br conjI 1;
   1.270 -  ba 1;
   1.271 -  br sup_ub1 1;
   1.272 -  br (le_trans RS mp) 1;
   1.273 -  br conjI 1;
   1.274 -  ba 1;
   1.275 -  br sup_ub2 1;
   1.276 +  by (rtac conjI 1);
   1.277 +  by (rtac (le_trans RS mp) 1);
   1.278 +  by (rtac conjI 1);
   1.279 +  by (assume_tac 1);
   1.280 +  by (rtac sup_ub1 1);
   1.281 +  by (rtac (le_trans RS mp) 1);
   1.282 +  by (rtac conjI 1);
   1.283 +  by (assume_tac 1);
   1.284 +  by (rtac sup_ub2 1);
   1.285  qed "sup_mon";