src/HOL/AxClasses/Lattice/OrdDefs.ML
author berghofe
Fri Aug 02 12:25:26 1996 +0200 (1996-08-02)
changeset 1899 0075a8d26a80
parent 1465 5d7a7e439cec
child 2606 27cdd600a3b1
permissions -rw-r--r--
Classical tactics now use default claset.
wenzelm@1440
     1
wenzelm@1440
     2
open OrdDefs;
wenzelm@1440
     3
wenzelm@1440
     4
wenzelm@1440
     5
(** lifting of quasi / partial orders **)
wenzelm@1440
     6
wenzelm@1440
     7
(* pairs *)
wenzelm@1440
     8
wenzelm@1440
     9
goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
wenzelm@1440
    10
  br conjI 1;
wenzelm@1440
    11
  br le_refl 1;
wenzelm@1440
    12
  br le_refl 1;
wenzelm@1440
    13
qed "le_prod_refl";
wenzelm@1440
    14
wenzelm@1440
    15
goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
berghofe@1899
    16
  by (safe_tac (!claset));
wenzelm@1440
    17
  be (conjI RS (le_trans RS mp)) 1;
wenzelm@1440
    18
  ba 1;
wenzelm@1440
    19
  be (conjI RS (le_trans RS mp)) 1;
wenzelm@1440
    20
  ba 1;
wenzelm@1440
    21
qed "le_prod_trans";
wenzelm@1440
    22
wenzelm@1440
    23
goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
berghofe@1899
    24
  by (safe_tac (!claset));
wenzelm@1440
    25
  by (stac Pair_fst_snd_eq 1);
wenzelm@1440
    26
  br conjI 1;
wenzelm@1440
    27
  be (conjI RS (le_antisym RS mp)) 1;
wenzelm@1440
    28
  ba 1;
wenzelm@1440
    29
  be (conjI RS (le_antisym RS mp)) 1;
wenzelm@1440
    30
  ba 1;
wenzelm@1440
    31
qed "le_prod_antisym";
wenzelm@1440
    32
wenzelm@1440
    33
wenzelm@1440
    34
(* functions *)
wenzelm@1440
    35
wenzelm@1440
    36
goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
wenzelm@1440
    37
  br allI 1;
wenzelm@1440
    38
  br le_refl 1;
wenzelm@1440
    39
qed "le_fun_refl";
wenzelm@1440
    40
wenzelm@1440
    41
goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
berghofe@1899
    42
  by (safe_tac (!claset));
wenzelm@1440
    43
  br (le_trans RS mp) 1;
berghofe@1899
    44
  by (Fast_tac 1);
wenzelm@1440
    45
qed "le_fun_trans";
wenzelm@1440
    46
wenzelm@1440
    47
goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
berghofe@1899
    48
  by (safe_tac (!claset));
wenzelm@1440
    49
  br ext 1;
wenzelm@1440
    50
  br (le_antisym RS mp) 1;
berghofe@1899
    51
  by (Fast_tac 1);
wenzelm@1440
    52
qed "le_fun_antisym";
wenzelm@1440
    53
wenzelm@1440
    54
wenzelm@1440
    55
wenzelm@1440
    56
(** duals **)
wenzelm@1440
    57
wenzelm@1440
    58
(*"'a dual" is even an isotype*)
wenzelm@1440
    59
goal thy "Rep_dual (Abs_dual y) = y";
wenzelm@1440
    60
  br Abs_dual_inverse 1;
clasohm@1465
    61
  by (rewtac dual_def);
berghofe@1899
    62
  by (Fast_tac 1);
wenzelm@1440
    63
qed "Abs_dual_inverse'";
wenzelm@1440
    64
wenzelm@1440
    65
wenzelm@1440
    66
goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
wenzelm@1440
    67
  br le_refl 1;
wenzelm@1440
    68
qed "le_dual_refl";
wenzelm@1440
    69
wenzelm@1440
    70
goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
wenzelm@1440
    71
  by (stac conj_commut 1);
wenzelm@1440
    72
  br le_trans 1;
wenzelm@1440
    73
qed "le_dual_trans";
wenzelm@1440
    74
wenzelm@1440
    75
goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
berghofe@1899
    76
  by (safe_tac (!claset));
wenzelm@1440
    77
  br (Rep_dual_inverse RS subst) 1;
wenzelm@1440
    78
  br sym 1;
wenzelm@1440
    79
  br (Rep_dual_inverse RS subst) 1;
wenzelm@1440
    80
  br arg_cong 1;
wenzelm@1440
    81
  back();
wenzelm@1440
    82
  be (conjI RS (le_antisym RS mp)) 1;
wenzelm@1440
    83
  ba 1;
wenzelm@1440
    84
qed "le_dual_antisym";
wenzelm@1440
    85
wenzelm@1440
    86
goalw thy [le_dual_def] "x [= y | y [= (x::'a::lin_order dual)";
wenzelm@1440
    87
  br le_lin 1;
wenzelm@1440
    88
qed "le_dual_lin";