src/HOLCF/Porder0.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 9969 4753185f1dd2
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/Porder0.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 derive the characteristic axioms for the characteristic constants 
     7 *)
     8 
     9 AddIffs [refl_less];
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* minimal fixes least element                                              *)
    13 (* ------------------------------------------------------------------------ *)
    14 Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
    15 by (blast_tac (claset() addIs [someI2,antisym_less]) 1);
    16 bind_thm ("minimal2UU", allI RS result());
    17 
    18 (* ------------------------------------------------------------------------ *)
    19 (* the reverse law of anti--symmetrie of <<                                 *)
    20 (* ------------------------------------------------------------------------ *)
    21 
    22 Goal "(x::'a::po)=y ==> x << y & y << x";
    23 by (Blast_tac 1);
    24 qed "antisym_less_inverse";
    25 
    26 
    27 Goal "[| (a::'a::po) << b; c << a; b << d|] ==> c << d";
    28 by (etac trans_less 1);
    29 by (etac trans_less 1);
    30 by (atac 1);
    31 qed "box_less";
    32 
    33 Goal "((x::'a::po)=y) = (x << y & y << x)";
    34 by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
    35 qed "po_eq_conv";