eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord
(* Title: HOLCF/Lift1.ML
ID: $Id$
Author: Olaf Mueller
Copyright 1996 Technische Universitaet Muenchen
Theorems for Lift1.thy
*)
open Lift1;
(* ------------------------------------------------------------------------ *)
(* less_lift is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
goalw thy [less_lift_def] "(x::'a lift) << x";
by (fast_tac HOL_cs 1);
qed"refl_less_lift";
val prems = goalw thy [less_lift_def]
"[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"antisym_less_lift";
val prems = goalw Lift1.thy [less_lift_def]
"[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"trans_less_lift";