src/HOLCF/Porder0.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5068 fb28eaa07e01
child 9169 85a47aa21f74
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Porder0.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6     derive the characteristic axioms for the characteristic constants *)
     7 
     8 open Porder0;
     9 
    10 AddIffs [refl_less];
    11 
    12 (* ------------------------------------------------------------------------ *)
    13 (* minimal fixes least element                                              *)
    14 (* ------------------------------------------------------------------------ *)
    15 bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po. uu<<x==>uu=(@u.!y. u<<y)"
    16 (fn prems =>
    17         [
    18         (cut_facts_tac prems 1),
    19         (rtac antisym_less 1),
    20         (etac spec 1),
    21         (res_inst_tac [("a","uu")] selectI2 1),
    22 	(atac 1),
    23 	(etac spec 1)
    24         ])));
    25 
    26 (* ------------------------------------------------------------------------ *)
    27 (* the reverse law of anti--symmetrie of <<                                 *)
    28 (* ------------------------------------------------------------------------ *)
    29 
    30 qed_goal "antisym_less_inverse" thy "(x::'a::po)=y ==> x << y & y << x"
    31 (fn prems =>
    32         [
    33         (cut_facts_tac prems 1),
    34         (rtac conjI 1),
    35         ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
    36         ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
    37         ]);
    38 
    39 
    40 qed_goal "box_less" thy
    41 "[| (a::'a::po) << b; c << a; b << d|] ==> c << d"
    42  (fn prems =>
    43         [
    44         (cut_facts_tac prems 1),
    45         (etac trans_less 1),
    46         (etac trans_less 1),
    47         (atac 1)
    48         ]);
    49 
    50 Goal "((x::'a::po)=y) = (x << y & y << x)";
    51 by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
    52 qed "po_eq_conv";