src/HOL/AxClasses/Lattice/Lattice.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 Lattice;
     3 
     4 
     5 (** basic properties of "&&" and "||" **)
     6 
     7 (* unique existence *)
     8 
     9 goalw thy [inf_def] "is_inf x y (x && y)";
    10   by (rtac (ex_inf RS spec RS spec RS selectI1) 1);
    11 qed "inf_is_inf";
    12 
    13 goal thy "is_inf x y inf --> x && y = inf";
    14   by (rtac impI 1);
    15   by (rtac (is_inf_uniq RS mp) 1);
    16   by (rtac conjI 1);
    17   by (rtac inf_is_inf 1);
    18   by (assume_tac 1);
    19 qed "inf_uniq";
    20 
    21 goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
    22   by Safe_tac;
    23   by (Step_tac 1);
    24   by (Step_tac 1);
    25   by (rtac inf_is_inf 1);
    26   by (rtac (inf_uniq RS mp RS sym) 1);
    27   by (assume_tac 1);
    28 qed "ex1_inf";
    29 
    30 
    31 goalw thy [sup_def] "is_sup x y (x || y)";
    32   by (rtac (ex_sup RS spec RS spec RS selectI1) 1);
    33 qed "sup_is_sup";
    34 
    35 goal thy "is_sup x y sup --> x || y = sup";
    36   by (rtac impI 1);
    37   by (rtac (is_sup_uniq RS mp) 1);
    38   by (rtac conjI 1);
    39   by (rtac sup_is_sup 1);
    40   by (assume_tac 1);
    41 qed "sup_uniq";
    42 
    43 goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
    44   by Safe_tac;
    45   by (Step_tac 1);
    46   by (Step_tac 1);
    47   by (rtac sup_is_sup 1);
    48   by (rtac (sup_uniq RS mp RS sym) 1);
    49   by (assume_tac 1);
    50 qed "ex1_sup";
    51 
    52 
    53 (* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *)
    54 
    55 val tac =
    56   cut_facts_tac [inf_is_inf] 1 THEN
    57   rewrite_goals_tac [inf_def, is_inf_def] THEN
    58   Fast_tac 1;
    59 
    60 goal thy "x && y [= x";
    61   by tac;
    62 qed "inf_lb1";
    63 
    64 goal thy "x && y [= y";
    65   by tac;
    66 qed "inf_lb2";
    67 
    68 val prems = goal thy "[| z [= x; z [= y |] ==> z [= x && y";
    69   by (cut_facts_tac prems 1);
    70   by tac;
    71 qed "inf_ub_lbs";
    72 
    73 
    74 val tac =
    75   cut_facts_tac [sup_is_sup] 1 THEN
    76   rewrite_goals_tac [sup_def, is_sup_def] THEN
    77   Fast_tac 1;
    78 
    79 goal thy "x [= x || y";
    80   by tac;
    81 qed "sup_ub1";
    82 
    83 goal thy "y [= x || y";
    84   by tac;
    85 qed "sup_ub2";
    86 
    87 val prems = goal thy "[| x [= z; y [= z |] ==> x || y [= z";
    88   by (cut_facts_tac prems 1);
    89   by tac;
    90 qed "sup_lb_ubs";
    91 
    92 
    93 
    94 (** some equations concerning "&&" and "||" vs. "[=" **)
    95 
    96 (* the Connection Theorems: "[=" expressed via "&&" or "||" *)
    97 
    98 goal thy "(x && y = x) = (x [= y)";
    99   by (rtac iffI 1);
   100   (*==>*)
   101     by (etac subst 1);
   102     by (rtac inf_lb2 1);
   103   (*<==*)
   104     by (rtac (inf_uniq RS mp) 1);
   105     by (rewtac is_inf_def);
   106     by (REPEAT_FIRST (rtac conjI));
   107     by (rtac le_refl 1);
   108     by (assume_tac 1);
   109     by (Fast_tac 1);
   110 qed "inf_connect";
   111 
   112 goal thy "(x || y = y) = (x [= y)";
   113   by (rtac iffI 1);
   114   (*==>*)
   115     by (etac subst 1);
   116     by (rtac sup_ub1 1);
   117   (*<==*)
   118     by (rtac (sup_uniq RS mp) 1);
   119     by (rewtac is_sup_def);
   120     by (REPEAT_FIRST (rtac conjI));
   121     by (assume_tac 1);
   122     by (rtac le_refl 1);
   123     by (Fast_tac 1);
   124 qed "sup_connect";
   125 
   126 
   127 (* minorized infs / majorized sups *)
   128 
   129 goal thy "(x [= y && z) = (x [= y & x [= z)";
   130   by (rtac iffI 1);
   131   (*==> (level 1)*)
   132     by (cut_facts_tac [inf_lb1, inf_lb2] 1);
   133     by (rtac conjI 1);
   134     by (rtac (le_trans RS mp) 1);
   135     by (etac conjI 1);
   136     by (assume_tac 1);
   137     by (rtac (le_trans RS mp) 1);
   138     by (etac conjI 1);
   139     by (assume_tac 1);
   140   (*<== (level 9)*)
   141     by (etac conjE 1);
   142     by (etac inf_ub_lbs 1);
   143     by (assume_tac 1);
   144 qed "le_inf_eq";
   145 
   146 goal thy "(x || y [= z) = (x [= z & y [= z)";
   147   by (rtac iffI 1);
   148   (*==> (level 1)*)
   149     by (cut_facts_tac [sup_ub1, sup_ub2] 1);
   150     by (rtac conjI 1);
   151     by (rtac (le_trans RS mp) 1);
   152     by (etac conjI 1);
   153     by (assume_tac 1);
   154     by (rtac (le_trans RS mp) 1);
   155     by (etac conjI 1);
   156     by (assume_tac 1);
   157   (*<== (level 9)*)
   158     by (etac conjE 1);
   159     by (etac sup_lb_ubs 1);
   160     by (assume_tac 1);
   161 qed "ge_sup_eq";
   162 
   163 
   164 (** algebraic properties of "&&" and "||": A, C, I, AB **)
   165 
   166 (* associativity *)
   167 
   168 goal thy "(x && y) && z = x && (y && z)";
   169   by (stac (inf_uniq RS mp RS sym) 1);
   170   back();
   171   back();
   172   back();
   173   back();
   174   back();
   175   back();
   176   back();
   177   back();
   178   by (rtac refl 2);
   179   by (rtac (is_inf_assoc RS mp) 1);
   180   by (REPEAT_FIRST (rtac conjI));
   181   by (REPEAT_FIRST (rtac inf_is_inf));
   182 qed "inf_assoc";
   183 
   184 goal thy "(x || y) || z = x || (y || z)";
   185   by (stac (sup_uniq RS mp RS sym) 1);
   186   back();
   187   back();
   188   back();
   189   back();
   190   back();
   191   back();
   192   back();
   193   back();
   194   by (rtac refl 2);
   195   by (rtac (is_sup_assoc RS mp) 1);
   196   by (REPEAT_FIRST (rtac conjI));
   197   by (REPEAT_FIRST (rtac sup_is_sup));
   198 qed "sup_assoc";
   199 
   200 
   201 (* commutativity *)
   202 
   203 goalw thy [inf_def] "x && y = y && x";
   204   by (stac (is_inf_commut RS ext) 1);
   205   by (rtac refl 1);
   206 qed "inf_commut";
   207 
   208 goalw thy [sup_def] "x || y = y || x";
   209   by (stac (is_sup_commut RS ext) 1);
   210   by (rtac refl 1);
   211 qed "sup_commut";
   212 
   213 
   214 (* idempotency *)
   215 
   216 goal thy "x && x = x";
   217   by (stac inf_connect 1);
   218   by (rtac le_refl 1);
   219 qed "inf_idemp";
   220 
   221 goal thy "x || x = x";
   222   by (stac sup_connect 1);
   223   by (rtac le_refl 1);
   224 qed "sup_idemp";
   225 
   226 
   227 (* absorption *)
   228 
   229 goal thy "x || (x && y) = x";
   230   by (stac sup_commut 1);
   231   by (stac sup_connect 1);
   232   by (rtac inf_lb1 1);
   233 qed "sup_inf_absorb";
   234 
   235 goal thy "x && (x || y) = x";
   236   by (stac inf_connect 1);
   237   by (rtac sup_ub1 1);
   238 qed "inf_sup_absorb";
   239 
   240 
   241 (* monotonicity *)
   242 
   243 val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
   244   by (cut_facts_tac prems 1);
   245   by (stac le_inf_eq 1);
   246   by (rtac conjI 1);
   247   by (rtac (le_trans RS mp) 1);
   248   by (rtac conjI 1);
   249   by (rtac inf_lb1 1);
   250   by (assume_tac 1);
   251   by (rtac (le_trans RS mp) 1);
   252   by (rtac conjI 1);
   253   by (rtac inf_lb2 1);
   254   by (assume_tac 1);
   255 qed "inf_mon";
   256 
   257 val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
   258   by (cut_facts_tac prems 1);
   259   by (stac ge_sup_eq 1);
   260   by (rtac conjI 1);
   261   by (rtac (le_trans RS mp) 1);
   262   by (rtac conjI 1);
   263   by (assume_tac 1);
   264   by (rtac sup_ub1 1);
   265   by (rtac (le_trans RS mp) 1);
   266   by (rtac conjI 1);
   267   by (assume_tac 1);
   268   by (rtac sup_ub2 1);
   269 qed "sup_mon";