src/HOL/AxClasses/Lattice/CLattice.ML
author wenzelm
Tue, 30 May 2000 16:08:38 +0200
changeset 9000 c20d58286a51
parent 5711 5a1cd4b4b20e
child 9969 4753185f1dd2
permissions -rw-r--r--
cleaned up;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     1
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     2
(** basic properties of "Inf" and "Sup" **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     3
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     4
(* unique existence *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     5
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
     6
Goalw [Inf_def] "is_Inf A (Inf A)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
     7
  by (rtac (ex_Inf RS spec RS selectI1) 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     8
qed "Inf_is_Inf";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    10
Goal "is_Inf A inf --> Inf A = inf";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    11
  by (rtac impI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    12
  by (rtac (is_Inf_uniq RS mp) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    13
  by (rtac conjI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    14
  by (rtac Inf_is_Inf 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    15
  by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    16
qed "Inf_uniq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    17
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    18
Goalw [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    19
  by Safe_tac;
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    20
  by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    21
  by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    22
  by (rtac Inf_is_Inf 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    23
  by (rtac (Inf_uniq RS mp RS sym) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    24
  by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    25
qed "ex1_Inf";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    26
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    27
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    28
Goalw [Sup_def] "is_Sup A (Sup A)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    29
  by (rtac (ex_Sup RS spec RS selectI1) 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    30
qed "Sup_is_Sup";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    31
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    32
Goal "is_Sup A sup --> Sup A = sup";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    33
  by (rtac impI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    34
  by (rtac (is_Sup_uniq RS mp) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    35
  by (rtac conjI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    36
  by (rtac Sup_is_Sup 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    37
  by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    38
qed "Sup_uniq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    39
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    40
Goalw [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    41
  by Safe_tac;
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    42
  by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    43
  by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    44
  by (rtac Sup_is_Sup 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    45
  by (rtac (Sup_uniq RS mp RS sym) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    46
  by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    47
qed "ex1_Sup";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    48
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    49
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    50
(* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    51
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    52
val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    53
  by (cut_facts_tac prems 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    54
  by (rtac selectI2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    55
  by (rtac Inf_is_Inf 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
    56
  by (rewtac is_Inf_def);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    57
  by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    58
qed "Inf_lb";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    59
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    60
val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    61
  by (rtac selectI2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    62
  by (rtac Inf_is_Inf 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
    63
  by (rewtac is_Inf_def);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    64
  by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    65
  by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    66
  by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    67
  by (rtac ballI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    68
  by (etac prem 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    69
qed "Inf_ub_lbs";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    70
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    71
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    72
val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    73
  by (cut_facts_tac prems 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    74
  by (rtac selectI2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    75
  by (rtac Sup_is_Sup 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
    76
  by (rewtac is_Sup_def);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    77
  by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    78
qed "Sup_ub";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    79
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    80
val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    81
  by (rtac selectI2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    82
  by (rtac Sup_is_Sup 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
    83
  by (rewtac is_Sup_def);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    84
  by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    85
  by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    86
  by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    87
  by (rtac ballI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    88
  by (etac prem 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    89
qed "Sup_lb_ubs";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    90
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    91
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    92
(** minorized Infs / majorized Sups **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    93
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    94
Goal "(x [= Inf A) = (ALL y:A. x [= y)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    95
  by (rtac iffI 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    96
  (*==>*)
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    97
    by (rtac ballI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    98
    by (rtac (le_trans RS mp) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    99
    by (etac conjI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   100
    by (etac Inf_lb 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   101
  (*<==*)
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   102
    by (rtac Inf_ub_lbs 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
   103
    by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   104
qed "le_Inf_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   105
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   106
Goal "(Sup A [= x) = (ALL y:A. y [= x)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   107
  by (rtac iffI 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   108
  (*==>*)
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   109
    by (rtac ballI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   110
    by (rtac (le_trans RS mp) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   111
    by (rtac conjI 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   112
    by (etac Sup_ub 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   113
    by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   114
  (*<==*)
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   115
    by (rtac Sup_lb_ubs 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
   116
    by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   117
qed "ge_Sup_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   118
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   119
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   120
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   121
(** Subsets and limits **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   122
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   123
Goal "A <= B --> Inf B [= Inf A";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   124
  by (rtac impI 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   125
  by (stac le_Inf_eq 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
   126
  by (rewtac Ball_def);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   127
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   128
  by (dtac subsetD 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   129
  by (assume_tac 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   130
  by (etac Inf_lb 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   131
qed "Inf_subset_antimon";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   132
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   133
Goal "A <= B --> Sup A [= Sup B";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   134
  by (rtac impI 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   135
  by (stac ge_Sup_eq 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
   136
  by (rewtac Ball_def);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   137
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   138
  by (dtac subsetD 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   139
  by (assume_tac 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   140
  by (etac Sup_ub 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   141
qed "Sup_subset_mon";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   142
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   143
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   144
(** singleton / empty limits **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   145
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   146
Goal "Inf {x} = x";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   147
  by (rtac (Inf_uniq RS mp) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
   148
  by (rewtac is_Inf_def);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   149
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   150
  by (rtac le_refl 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
   151
  by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   152
qed "sing_Inf_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   153
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   154
Goal "Sup {x} = x";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   155
  by (rtac (Sup_uniq RS mp) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
   156
  by (rewtac is_Sup_def);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   157
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   158
  by (rtac le_refl 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
   159
  by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   160
qed "sing_Sup_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   161
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   162
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   163
Goal "Inf {} = Sup {x. True}";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   164
  by (rtac (Inf_uniq RS mp) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
   165
  by (rewtac is_Inf_def);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   166
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   167
  by (rtac (sing_Sup_eq RS subst) 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   168
  back();
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   169
  by (rtac (Sup_subset_mon RS mp) 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
   170
  by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   171
qed "empty_Inf_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   172
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   173
Goal "Sup {} = Inf {x. True}";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   174
  by (rtac (Sup_uniq RS mp) 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1440
diff changeset
   175
  by (rewtac is_Sup_def);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   176
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   177
  by (rtac (sing_Inf_eq RS subst) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
   178
  by (rtac (Inf_subset_antimon RS mp) 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
   179
  by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
   180
qed "empty_Sup_eq";