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