src/HOL/AxClasses/Lattice/Order.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 4831 dae4d63a1318
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
wenzelm@1440
     1
wenzelm@1440
     2
open Order;
wenzelm@1440
     3
wenzelm@1440
     4
wenzelm@1440
     5
(** basic properties of limits **)
wenzelm@1440
     6
wenzelm@1440
     7
(* uniqueness *)
wenzelm@1440
     8
wenzelm@1440
     9
val tac =
wenzelm@1440
    10
  rtac impI 1 THEN
wenzelm@1440
    11
  rtac (le_antisym RS mp) 1 THEN
berghofe@1899
    12
  Fast_tac 1;
wenzelm@1440
    13
wenzelm@1440
    14
wenzelm@1440
    15
goalw thy [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
wenzelm@1440
    16
  by tac;
wenzelm@1440
    17
qed "is_inf_uniq";
wenzelm@1440
    18
wenzelm@1440
    19
goalw thy [is_sup_def] "is_sup x y sup & is_sup x y sup' --> sup = sup'";
wenzelm@1440
    20
  by tac;
wenzelm@1440
    21
qed "is_sup_uniq";
wenzelm@1440
    22
wenzelm@1440
    23
wenzelm@1440
    24
goalw thy [is_Inf_def] "is_Inf A inf & is_Inf A inf' --> inf = inf'";
wenzelm@1440
    25
  by tac;
wenzelm@1440
    26
qed "is_Inf_uniq";
wenzelm@1440
    27
wenzelm@1440
    28
goalw thy [is_Sup_def] "is_Sup A sup & is_Sup A sup' --> sup = sup'";
wenzelm@1440
    29
  by tac;
wenzelm@1440
    30
qed "is_Sup_uniq";
wenzelm@1440
    31
wenzelm@1440
    32
wenzelm@1440
    33
wenzelm@1440
    34
(* commutativity *)
wenzelm@1440
    35
wenzelm@1440
    36
goalw thy [is_inf_def] "is_inf x y inf = is_inf y x inf";
berghofe@1899
    37
  by (Fast_tac 1);
wenzelm@1440
    38
qed "is_inf_commut";
wenzelm@1440
    39
wenzelm@1440
    40
goalw thy [is_sup_def] "is_sup x y sup = is_sup y x sup";
berghofe@1899
    41
  by (Fast_tac 1);
wenzelm@1440
    42
qed "is_sup_commut";
wenzelm@1440
    43
wenzelm@1440
    44
wenzelm@1440
    45
(* associativity *)
wenzelm@1440
    46
wenzelm@1440
    47
goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
paulson@4153
    48
  by Safe_tac;
wenzelm@1440
    49
  (*level 1*)
paulson@4153
    50
    by (rtac (le_trans RS mp) 1);
paulson@4153
    51
    by (etac conjI 1);
paulson@4153
    52
    by (assume_tac 1);
wenzelm@1440
    53
  (*level 4*)
berghofe@1899
    54
    by (Step_tac 1);
wenzelm@1440
    55
    back();
paulson@4153
    56
    by (etac mp 1);
paulson@4153
    57
    by (rtac conjI 1);
paulson@4153
    58
    by (rtac (le_trans RS mp) 1);
paulson@4153
    59
    by (etac conjI 1);
paulson@4153
    60
    by (assume_tac 1);
paulson@4153
    61
    by (assume_tac 1);
wenzelm@1440
    62
  (*level 11*)
berghofe@1899
    63
    by (Step_tac 1);
wenzelm@1440
    64
    back();
wenzelm@1440
    65
    back();
paulson@4153
    66
    by (etac mp 1);
paulson@4153
    67
    by (rtac conjI 1);
berghofe@1899
    68
    by (Step_tac 1);
paulson@4153
    69
    by (etac mp 1);
paulson@4153
    70
    by (etac conjI 1);
paulson@4153
    71
    by (rtac (le_trans RS mp) 1);
paulson@4153
    72
    by (etac conjI 1);
paulson@4153
    73
    by (assume_tac 1);
paulson@4153
    74
    by (rtac (le_trans RS mp) 1);
paulson@4153
    75
    by (etac conjI 1);
wenzelm@1440
    76
    back();     (* !! *)
paulson@4153
    77
    by (assume_tac 1);
wenzelm@1440
    78
qed "is_inf_assoc";
wenzelm@1440
    79
wenzelm@1440
    80
wenzelm@1440
    81
goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
paulson@4153
    82
  by Safe_tac;
wenzelm@1440
    83
  (*level 1*)
paulson@4153
    84
    by (rtac (le_trans RS mp) 1);
paulson@4153
    85
    by (etac conjI 1);
paulson@4153
    86
    by (assume_tac 1);
wenzelm@1440
    87
  (*level 4*)
berghofe@1899
    88
    by (Step_tac 1);
wenzelm@1440
    89
    back();
paulson@4153
    90
    by (etac mp 1);
paulson@4153
    91
    by (rtac conjI 1);
paulson@4153
    92
    by (rtac (le_trans RS mp) 1);
paulson@4153
    93
    by (etac conjI 1);
paulson@4153
    94
    by (assume_tac 1);
paulson@4153
    95
    by (assume_tac 1);
wenzelm@1440
    96
  (*level 11*)
berghofe@1899
    97
    by (Step_tac 1);
wenzelm@1440
    98
    back();
wenzelm@1440
    99
    back();
paulson@4153
   100
    by (etac mp 1);
paulson@4153
   101
    by (rtac conjI 1);
berghofe@1899
   102
    by (Step_tac 1);
paulson@4153
   103
    by (etac mp 1);
paulson@4153
   104
    by (etac conjI 1);
paulson@4153
   105
    by (rtac (le_trans RS mp) 1);
paulson@4153
   106
    by (etac conjI 1);
wenzelm@1440
   107
    back();     (* !! *)
paulson@4153
   108
    by (assume_tac 1);
paulson@4153
   109
    by (rtac (le_trans RS mp) 1);
paulson@4153
   110
    by (etac conjI 1);
paulson@4153
   111
    by (assume_tac 1);
wenzelm@1440
   112
qed "is_sup_assoc";
wenzelm@1440
   113
wenzelm@1440
   114
wenzelm@1440
   115
(** limits in linear orders **)
wenzelm@1440
   116
wenzelm@2606
   117
goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
wenzelm@1440
   118
  by (stac expand_if 1);
wenzelm@1440
   119
  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
wenzelm@1440
   120
  (*case "x [= y"*)
paulson@4153
   121
    by (rtac le_refl 1);
paulson@4153
   122
    by (assume_tac 1);
berghofe@1899
   123
    by (Fast_tac 1);
wenzelm@1440
   124
  (*case "~ x [= y"*)
paulson@4153
   125
    by (rtac (le_linear RS disjE) 1);
paulson@4153
   126
    by (assume_tac 1);
paulson@4153
   127
    by (etac notE 1);
paulson@4153
   128
    by (assume_tac 1);
paulson@4153
   129
    by (rtac le_refl 1);
berghofe@1899
   130
    by (Fast_tac 1);
wenzelm@1440
   131
qed "min_is_inf";
wenzelm@1440
   132
wenzelm@2606
   133
goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
wenzelm@1440
   134
  by (stac expand_if 1);
wenzelm@1440
   135
  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
wenzelm@1440
   136
  (*case "x [= y"*)
paulson@4153
   137
    by (assume_tac 1);
paulson@4153
   138
    by (rtac le_refl 1);
berghofe@1899
   139
    by (Fast_tac 1);
wenzelm@1440
   140
  (*case "~ x [= y"*)
paulson@4153
   141
    by (rtac le_refl 1);
paulson@4153
   142
    by (rtac (le_linear RS disjE) 1);
paulson@4153
   143
    by (assume_tac 1);
paulson@4153
   144
    by (etac notE 1);
paulson@4153
   145
    by (assume_tac 1);
berghofe@1899
   146
    by (Fast_tac 1);
wenzelm@1440
   147
qed "max_is_sup";
wenzelm@1440
   148
wenzelm@1440
   149
wenzelm@1440
   150
wenzelm@1440
   151
(** general vs. binary limits **)
wenzelm@1440
   152
wenzelm@1440
   153
goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
paulson@4153
   154
  by (rtac iffI 1);
wenzelm@1440
   155
  (*==>*)
berghofe@1899
   156
    by (Fast_tac 1);
wenzelm@1440
   157
  (*<==*)
paulson@4153
   158
    by Safe_tac;
berghofe@1899
   159
    by (Step_tac 1);
paulson@4153
   160
    by (etac mp 1);
berghofe@1899
   161
    by (Fast_tac 1);
wenzelm@1440
   162
qed "bin_is_Inf_eq";
wenzelm@1440
   163
wenzelm@1440
   164
goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
paulson@4153
   165
  by (rtac iffI 1);
wenzelm@1440
   166
  (*==>*)
berghofe@1899
   167
    by (Fast_tac 1);
wenzelm@1440
   168
  (*<==*)
paulson@4153
   169
    by Safe_tac;
berghofe@1899
   170
    by (Step_tac 1);
paulson@4153
   171
    by (etac mp 1);
berghofe@1899
   172
    by (Fast_tac 1);
wenzelm@1440
   173
qed "bin_is_Sup_eq";