src/HOLCF/Lift1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5068 fb28eaa07e01
child 9248 e1dee89de037
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Lift1.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1996 Technische Universitaet Muenchen
     5 
     6 Theorems for Lift1.thy
     7 *)
     8 
     9 
    10 open Lift1;
    11 
    12 (* ------------------------------------------------------------------------ *)
    13 (* less_lift is a partial order on type 'a -> 'b                            *)
    14 (* ------------------------------------------------------------------------ *)
    15 
    16 Goalw [less_lift_def] "(x::'a lift) << x";
    17 by (fast_tac HOL_cs 1);
    18 qed"refl_less_lift";
    19 
    20 val prems = goalw thy [less_lift_def] 
    21   "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
    22 by (cut_facts_tac prems 1);
    23 by (fast_tac HOL_cs 1);
    24 qed"antisym_less_lift";
    25 
    26 val prems = goalw Lift1.thy [less_lift_def] 
    27   "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
    28 by (cut_facts_tac prems 1);
    29 by (fast_tac HOL_cs 1);
    30 qed"trans_less_lift";