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