src/HOL/AxClasses/Lattice/LatInsts.ML
changeset 1440 de6f18da81bb
child 1465 5d7a7e439cec
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Mon Jan 15 15:49:21 1996 +0100
     1.3 @@ -0,0 +1,98 @@
     1.4 +
     1.5 +open LatInsts;
     1.6 +
     1.7 +
     1.8 +goal thy "Inf {x, y} = x && y";
     1.9 +  br (Inf_uniq RS mp) 1;
    1.10 +  by (stac bin_is_Inf_eq 1);
    1.11 +  br inf_is_inf 1;
    1.12 +qed "bin_Inf_eq";
    1.13 +
    1.14 +goal thy "Sup {x, y} = x || y";
    1.15 +  br (Sup_uniq RS mp) 1;
    1.16 +  by (stac bin_is_Sup_eq 1);
    1.17 +  br sup_is_sup 1;
    1.18 +qed "bin_Sup_eq";
    1.19 +
    1.20 +
    1.21 +
    1.22 +(* Unions and limits *)
    1.23 +
    1.24 +goal thy "Inf (A Un B) = Inf A && Inf B";
    1.25 +  br (Inf_uniq RS mp) 1;
    1.26 +  by (rewrite_goals_tac [is_Inf_def]);
    1.27 +  by (safe_tac set_cs);
    1.28 +
    1.29 +  br (conjI RS (le_trans RS mp)) 1;
    1.30 +  br inf_lb1 1;
    1.31 +  be Inf_lb 1;
    1.32 +
    1.33 +  br (conjI RS (le_trans RS mp)) 1;
    1.34 +  br inf_lb2 1;
    1.35 +  be Inf_lb 1;
    1.36 +
    1.37 +  by (stac le_inf_eq 1);
    1.38 +  br conjI 1;
    1.39 +  br Inf_ub_lbs 1;
    1.40 +  by (fast_tac set_cs 1);
    1.41 +  br Inf_ub_lbs 1;
    1.42 +  by (fast_tac set_cs 1);
    1.43 +qed "Inf_Un_eq";
    1.44 +
    1.45 +goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    1.46 +  br (Inf_uniq RS mp) 1;
    1.47 +  by (rewrite_goals_tac [is_Inf_def]);
    1.48 +  by (safe_tac set_cs);
    1.49 +  (*level 3*)
    1.50 +  br (conjI RS (le_trans RS mp)) 1;
    1.51 +  be Inf_lb 2;
    1.52 +  br (sing_Inf_eq RS subst) 1;
    1.53 +  br (Inf_subset_antimon RS mp) 1;
    1.54 +  by (fast_tac set_cs 1);
    1.55 +  (*level 8*)
    1.56 +  by (stac le_Inf_eq 1);
    1.57 +  by (safe_tac set_cs);
    1.58 +  by (stac le_Inf_eq 1);
    1.59 +  by (fast_tac set_cs 1);
    1.60 +qed "Inf_UN_eq";
    1.61 +
    1.62 +
    1.63 +
    1.64 +goal thy "Sup (A Un B) = Sup A || Sup B";
    1.65 +  br (Sup_uniq RS mp) 1;
    1.66 +  by (rewrite_goals_tac [is_Sup_def]);
    1.67 +  by (safe_tac set_cs);
    1.68 +
    1.69 +  br (conjI RS (le_trans RS mp)) 1;
    1.70 +  be Sup_ub 1;
    1.71 +  br sup_ub1 1;
    1.72 +
    1.73 +  br (conjI RS (le_trans RS mp)) 1;
    1.74 +  be Sup_ub 1;
    1.75 +  br sup_ub2 1;
    1.76 +
    1.77 +  by (stac ge_sup_eq 1);
    1.78 +  br conjI 1;
    1.79 +  br Sup_lb_ubs 1;
    1.80 +  by (fast_tac set_cs 1);
    1.81 +  br Sup_lb_ubs 1;
    1.82 +  by (fast_tac set_cs 1);
    1.83 +qed "Sup_Un_eq";
    1.84 +
    1.85 +goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
    1.86 +  br (Sup_uniq RS mp) 1;
    1.87 +  by (rewrite_goals_tac [is_Sup_def]);
    1.88 +  by (safe_tac set_cs);
    1.89 +  (*level 3*)
    1.90 +  br (conjI RS (le_trans RS mp)) 1;
    1.91 +  be Sup_ub 1;
    1.92 +  br (sing_Sup_eq RS subst) 1;
    1.93 +  back();
    1.94 +  br (Sup_subset_mon RS mp) 1;
    1.95 +  by (fast_tac set_cs 1);
    1.96 +  (*level 8*)
    1.97 +  by (stac ge_Sup_eq 1);
    1.98 +  by (safe_tac set_cs);
    1.99 +  by (stac ge_Sup_eq 1);
   1.100 +  by (fast_tac set_cs 1);
   1.101 +qed "Sup_UN_eq";