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
     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   by (rtac conjI 1);
    11   by (rtac le_refl 1);
    12   by (rtac 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;
    17   by (etac (conjI RS (le_trans RS mp)) 1);
    18   by (assume_tac 1);
    19   by (etac (conjI RS (le_trans RS mp)) 1);
    20   by (assume_tac 1);
    21 qed "le_prod_trans";
    22 
    23 goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
    24   by Safe_tac;
    25   by (stac Pair_fst_snd_eq 1);
    26   by (rtac conjI 1);
    27   by (etac (conjI RS (le_antisym RS mp)) 1);
    28   by (assume_tac 1);
    29   by (etac (conjI RS (le_antisym RS mp)) 1);
    30   by (assume_tac 1);
    31 qed "le_prod_antisym";
    32 
    33 
    34 (* functions *)
    35 
    36 goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
    37   by (rtac allI 1);
    38   by (rtac 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;
    43   by (rtac (le_trans RS mp) 1);
    44   by (Fast_tac 1);
    45 qed "le_fun_trans";
    46 
    47 goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
    48   by Safe_tac;
    49   by (rtac ext 1);
    50   by (rtac (le_antisym RS mp) 1);
    51   by (Fast_tac 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   by (rtac Abs_dual_inverse 1);
    61   by (rewtac dual_def);
    62   by (Fast_tac 1);
    63 qed "Abs_dual_inverse'";
    64 
    65 
    66 goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
    67   by (rtac 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   by (rtac le_trans 1);
    73 qed "le_dual_trans";
    74 
    75 goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
    76   by Safe_tac;
    77   by (rtac (Rep_dual_inverse RS subst) 1);
    78   by (rtac sym 1);
    79   by (rtac (Rep_dual_inverse RS subst) 1);
    80   by (rtac arg_cong 1);
    81   back();
    82   by (etac (conjI RS (le_antisym RS mp)) 1);
    83   by (assume_tac 1);
    84 qed "le_dual_antisym";
    85 
    86 goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
    87   by (rtac le_linear 1);
    88 qed "le_dual_linear";