src/HOLCF/Lift.thy

     ID:         $Id$
     Author:     Olaf Mueller
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Lifting types of class term to flat pcpo's *}
+header {* Lifting types of class type to flat pcpo's *}
 
 theory Lift = Cprod3:
 
-defaultsort "term"
+defaultsort type
 
 
 typedef 'a lift = "UNIV :: 'a option set" ..
 
 constdefs
   Undef :: "'a lift"
   "Undef == Abs_lift None"
   Def :: "'a => 'a lift"
   "Def x == Abs_lift (Some x)"
 
-instance lift :: ("term") sq_ord ..
+instance lift :: (type) sq_ord ..
 
 defs (overloaded)
   less_lift_def: "x << y == (x=y | x=Undef)"
 
-instance lift :: ("term") po
+instance lift :: (type) po
 proof
   fix x y z :: "'a lift"
   show "x << x" by (unfold less_lift_def) blast
   { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast }
   { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast }

 theorem cpo_lift: "chain (Y::nat => 'a lift) ==> EX x. range Y <<| x"
   apply (cut_tac flat_imp_chfin_poo)
   apply (blast intro: lub_finch1)
   done
 
-instance lift :: ("term") pcpo
+instance lift :: (type) pcpo
   apply intro_classes
    apply (erule cpo_lift)
   apply (rule least_lift)
   done
 

 subsection {* Further operations *}
 
 consts
  flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
  flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
- liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
+ liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
 
 defs
  flift1_def:
   "flift1 f == (LAM x. (case x of
                    UU => UU

   by (simp add: less_lift)
 
 
 subsection {* Lift is flat *}
 
-instance lift :: ("term") flat
+instance lift :: (type) flat
 proof
   show "ALL x y::'a lift. x << y --> x = UU | x = y"
     by (simp add: less_lift)
 qed