src/HOL/AxClasses/Lattice/LatInsts.ML
author wenzelm
Mon Jan 15 15:49:21 1996 +0100 (1996-01-15)
changeset 1440 de6f18da81bb
child 1465 5d7a7e439cec
permissions -rw-r--r--
added this stuff;
     1 
     2 open LatInsts;
     3 
     4 
     5 goal thy "Inf {x, y} = x && y";
     6   br (Inf_uniq RS mp) 1;
     7   by (stac bin_is_Inf_eq 1);
     8   br inf_is_inf 1;
     9 qed "bin_Inf_eq";
    10 
    11 goal thy "Sup {x, y} = x || y";
    12   br (Sup_uniq RS mp) 1;
    13   by (stac bin_is_Sup_eq 1);
    14   br sup_is_sup 1;
    15 qed "bin_Sup_eq";
    16 
    17 
    18 
    19 (* Unions and limits *)
    20 
    21 goal thy "Inf (A Un B) = Inf A && Inf B";
    22   br (Inf_uniq RS mp) 1;
    23   by (rewrite_goals_tac [is_Inf_def]);
    24   by (safe_tac set_cs);
    25 
    26   br (conjI RS (le_trans RS mp)) 1;
    27   br inf_lb1 1;
    28   be Inf_lb 1;
    29 
    30   br (conjI RS (le_trans RS mp)) 1;
    31   br inf_lb2 1;
    32   be Inf_lb 1;
    33 
    34   by (stac le_inf_eq 1);
    35   br conjI 1;
    36   br Inf_ub_lbs 1;
    37   by (fast_tac set_cs 1);
    38   br Inf_ub_lbs 1;
    39   by (fast_tac set_cs 1);
    40 qed "Inf_Un_eq";
    41 
    42 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    43   br (Inf_uniq RS mp) 1;
    44   by (rewrite_goals_tac [is_Inf_def]);
    45   by (safe_tac set_cs);
    46   (*level 3*)
    47   br (conjI RS (le_trans RS mp)) 1;
    48   be Inf_lb 2;
    49   br (sing_Inf_eq RS subst) 1;
    50   br (Inf_subset_antimon RS mp) 1;
    51   by (fast_tac set_cs 1);
    52   (*level 8*)
    53   by (stac le_Inf_eq 1);
    54   by (safe_tac set_cs);
    55   by (stac le_Inf_eq 1);
    56   by (fast_tac set_cs 1);
    57 qed "Inf_UN_eq";
    58 
    59 
    60 
    61 goal thy "Sup (A Un B) = Sup A || Sup B";
    62   br (Sup_uniq RS mp) 1;
    63   by (rewrite_goals_tac [is_Sup_def]);
    64   by (safe_tac set_cs);
    65 
    66   br (conjI RS (le_trans RS mp)) 1;
    67   be Sup_ub 1;
    68   br sup_ub1 1;
    69 
    70   br (conjI RS (le_trans RS mp)) 1;
    71   be Sup_ub 1;
    72   br sup_ub2 1;
    73 
    74   by (stac ge_sup_eq 1);
    75   br conjI 1;
    76   br Sup_lb_ubs 1;
    77   by (fast_tac set_cs 1);
    78   br Sup_lb_ubs 1;
    79   by (fast_tac set_cs 1);
    80 qed "Sup_Un_eq";
    81 
    82 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
    83   br (Sup_uniq RS mp) 1;
    84   by (rewrite_goals_tac [is_Sup_def]);
    85   by (safe_tac set_cs);
    86   (*level 3*)
    87   br (conjI RS (le_trans RS mp)) 1;
    88   be Sup_ub 1;
    89   br (sing_Sup_eq RS subst) 1;
    90   back();
    91   br (Sup_subset_mon RS mp) 1;
    92   by (fast_tac set_cs 1);
    93   (*level 8*)
    94   by (stac ge_Sup_eq 1);
    95   by (safe_tac set_cs);
    96   by (stac ge_Sup_eq 1);
    97   by (fast_tac set_cs 1);
    98 qed "Sup_UN_eq";