src/HOLCF/Lift1.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5068 fb28eaa07e01
child 9248 e1dee89de037
permissions -rw-r--r--
tidying
sandnerr@2357
     1
(*  Title:      HOLCF/Lift1.ML
sandnerr@2357
     2
    ID:         $Id$
mueller@3033
     3
    Author:     Olaf Mueller
sandnerr@2357
     4
    Copyright   1996 Technische Universitaet Muenchen
sandnerr@2357
     5
sandnerr@2357
     6
Theorems for Lift1.thy
sandnerr@2357
     7
*)
sandnerr@2357
     8
sandnerr@2356
     9
sandnerr@2356
    10
open Lift1;
sandnerr@2356
    11
sandnerr@2356
    12
(* ------------------------------------------------------------------------ *)
sandnerr@2356
    13
(* less_lift is a partial order on type 'a -> 'b                            *)
sandnerr@2356
    14
(* ------------------------------------------------------------------------ *)
sandnerr@2356
    15
wenzelm@5068
    16
Goalw [less_lift_def] "(x::'a lift) << x";
sandnerr@2356
    17
by (fast_tac HOL_cs 1);
sandnerr@2356
    18
qed"refl_less_lift";
sandnerr@2356
    19
slotosch@2640
    20
val prems = goalw thy [less_lift_def] 
slotosch@3323
    21
  "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
slotosch@2640
    22
by (cut_facts_tac prems 1);
sandnerr@2356
    23
by (fast_tac HOL_cs 1);
sandnerr@2356
    24
qed"antisym_less_lift";
sandnerr@2356
    25
slotosch@2640
    26
val prems = goalw Lift1.thy [less_lift_def] 
slotosch@3323
    27
  "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
slotosch@2640
    28
by (cut_facts_tac prems 1);
sandnerr@2356
    29
by (fast_tac HOL_cs 1);
sandnerr@2356
    30
qed"trans_less_lift";