src/HOL/AxClasses/Lattice/LatInsts.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 
     2 open LatInsts;
     3 
     4 
     5 goal thy "Inf {x, y} = x && y";
     6   by (rtac (Inf_uniq RS mp) 1);
     7   by (stac bin_is_Inf_eq 1);
     8   by (rtac inf_is_inf 1);
     9 qed "bin_Inf_eq";
    10 
    11 goal thy "Sup {x, y} = x || y";
    12   by (rtac (Sup_uniq RS mp) 1);
    13   by (stac bin_is_Sup_eq 1);
    14   by (rtac 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   by (rtac (Inf_uniq RS mp) 1);
    23   by (rewtac is_Inf_def);
    24   by Safe_tac;
    25 
    26   by (rtac (conjI RS (le_trans RS mp)) 1);
    27   by (rtac inf_lb1 1);
    28   by (etac Inf_lb 1);
    29 
    30   by (rtac (conjI RS (le_trans RS mp)) 1);
    31   by (rtac inf_lb2 1);
    32   by (etac Inf_lb 1);
    33 
    34   by (stac le_inf_eq 1);
    35   by (rtac conjI 1);
    36   by (rtac Inf_ub_lbs 1);
    37   by (Fast_tac 1);
    38   by (rtac Inf_ub_lbs 1);
    39   by (Fast_tac 1);
    40 qed "Inf_Un_eq";
    41 
    42 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    43   by (rtac (Inf_uniq RS mp) 1);
    44   by (rewtac is_Inf_def);
    45   by Safe_tac;
    46   (*level 3*)
    47   by (rtac (conjI RS (le_trans RS mp)) 1);
    48   by (etac Inf_lb 2);
    49   by (rtac (sing_Inf_eq RS subst) 1);
    50   by (rtac (Inf_subset_antimon RS mp) 1);
    51   by (Fast_tac 1);
    52   (*level 8*)
    53   by (stac le_Inf_eq 1);
    54   by Safe_tac;
    55   by (stac le_Inf_eq 1);
    56   by (Fast_tac 1);
    57 qed "Inf_UN_eq";
    58 
    59 
    60 
    61 goal thy "Sup (A Un B) = Sup A || Sup B";
    62   by (rtac (Sup_uniq RS mp) 1);
    63   by (rewtac is_Sup_def);
    64   by Safe_tac;
    65 
    66   by (rtac (conjI RS (le_trans RS mp)) 1);
    67   by (etac Sup_ub 1);
    68   by (rtac sup_ub1 1);
    69 
    70   by (rtac (conjI RS (le_trans RS mp)) 1);
    71   by (etac Sup_ub 1);
    72   by (rtac sup_ub2 1);
    73 
    74   by (stac ge_sup_eq 1);
    75   by (rtac conjI 1);
    76   by (rtac Sup_lb_ubs 1);
    77   by (Fast_tac 1);
    78   by (rtac Sup_lb_ubs 1);
    79   by (Fast_tac 1);
    80 qed "Sup_Un_eq";
    81 
    82 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
    83   by (rtac (Sup_uniq RS mp) 1);
    84   by (rewtac is_Sup_def);
    85   by Safe_tac;
    86   (*level 3*)
    87   by (rtac (conjI RS (le_trans RS mp)) 1);
    88   by (etac Sup_ub 1);
    89   by (rtac (sing_Sup_eq RS subst) 1);
    90   back();
    91   by (rtac (Sup_subset_mon RS mp) 1);
    92   by (Fast_tac 1);
    93   (*level 8*)
    94   by (stac ge_Sup_eq 1);
    95   by Safe_tac;
    96   by (stac ge_Sup_eq 1);
    97   by (Fast_tac 1);
    98 qed "Sup_UN_eq";