src/HOL/AxClasses/Lattice/OrdDefs.ML
author wenzelm
Mon Nov 03 12:24:13 1997 +0100 (1997-11-03)
changeset 4091 771b1f6422a8
parent 2606 27cdd600a3b1
child 4153 e534c4c32d54
permissions -rw-r--r--
isatool fixclasimp;
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)";
wenzelm@4091
    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@2606
    23
goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
wenzelm@4091
    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)";
wenzelm@4091
    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@2606
    47
goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
wenzelm@4091
    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@2606
    75
goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
wenzelm@4091
    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@2606
    86
goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
wenzelm@2606
    87
  br le_linear 1;
wenzelm@2606
    88
qed "le_dual_linear";