src/HOL/AxClasses/Lattice/OrdDefs.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 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)";
paulson@4153
    10
  by (rtac conjI 1);
paulson@4153
    11
  by (rtac le_refl 1);
paulson@4153
    12
  by (rtac 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)";
paulson@4153
    16
  by Safe_tac;
paulson@4153
    17
  by (etac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    18
  by (assume_tac 1);
paulson@4153
    19
  by (etac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    20
  by (assume_tac 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)";
paulson@4153
    24
  by Safe_tac;
wenzelm@1440
    25
  by (stac Pair_fst_snd_eq 1);
paulson@4153
    26
  by (rtac conjI 1);
paulson@4153
    27
  by (etac (conjI RS (le_antisym RS mp)) 1);
paulson@4153
    28
  by (assume_tac 1);
paulson@4153
    29
  by (etac (conjI RS (le_antisym RS mp)) 1);
paulson@4153
    30
  by (assume_tac 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)";
paulson@4153
    37
  by (rtac allI 1);
paulson@4153
    38
  by (rtac 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)";
paulson@4153
    42
  by Safe_tac;
paulson@4153
    43
  by (rtac (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)";
paulson@4153
    48
  by Safe_tac;
paulson@4153
    49
  by (rtac ext 1);
paulson@4153
    50
  by (rtac (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";
paulson@4153
    60
  by (rtac 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)";
paulson@4153
    67
  by (rtac 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);
paulson@4153
    72
  by (rtac 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)";
paulson@4153
    76
  by Safe_tac;
paulson@4153
    77
  by (rtac (Rep_dual_inverse RS subst) 1);
paulson@4153
    78
  by (rtac sym 1);
paulson@4153
    79
  by (rtac (Rep_dual_inverse RS subst) 1);
paulson@4153
    80
  by (rtac arg_cong 1);
wenzelm@1440
    81
  back();
paulson@4153
    82
  by (etac (conjI RS (le_antisym RS mp)) 1);
paulson@4153
    83
  by (assume_tac 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)";
paulson@4153
    87
  by (rtac le_linear 1);
wenzelm@2606
    88
qed "le_dual_linear";