src/HOLCF/Lift.thy
changeset 12338 de0f4a63baa5
parent 12026 0b1d80ada4ab
child 14096 f79d139c7e46
     1.1 --- a/src/HOLCF/Lift.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOLCF/Lift.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -4,11 +4,11 @@
     1.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.5  *)
     1.6  
     1.7 -header {* Lifting types of class term to flat pcpo's *}
     1.8 +header {* Lifting types of class type to flat pcpo's *}
     1.9  
    1.10  theory Lift = Cprod3:
    1.11  
    1.12 -defaultsort "term"
    1.13 +defaultsort type
    1.14  
    1.15  
    1.16  typedef 'a lift = "UNIV :: 'a option set" ..
    1.17 @@ -19,12 +19,12 @@
    1.18    Def :: "'a => 'a lift"
    1.19    "Def x == Abs_lift (Some x)"
    1.20  
    1.21 -instance lift :: ("term") sq_ord ..
    1.22 +instance lift :: (type) sq_ord ..
    1.23  
    1.24  defs (overloaded)
    1.25    less_lift_def: "x << y == (x=y | x=Undef)"
    1.26  
    1.27 -instance lift :: ("term") po
    1.28 +instance lift :: (type) po
    1.29  proof
    1.30    fix x y z :: "'a lift"
    1.31    show "x << x" by (unfold less_lift_def) blast
    1.32 @@ -111,7 +111,7 @@
    1.33    apply (blast intro: lub_finch1)
    1.34    done
    1.35  
    1.36 -instance lift :: ("term") pcpo
    1.37 +instance lift :: (type) pcpo
    1.38    apply intro_classes
    1.39     apply (erule cpo_lift)
    1.40    apply (rule least_lift)
    1.41 @@ -153,7 +153,7 @@
    1.42  consts
    1.43   flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
    1.44   flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
    1.45 - liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
    1.46 + liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
    1.47  
    1.48  defs
    1.49   flift1_def:
    1.50 @@ -219,7 +219,7 @@
    1.51  
    1.52  subsection {* Lift is flat *}
    1.53  
    1.54 -instance lift :: ("term") flat
    1.55 +instance lift :: (type) flat
    1.56  proof
    1.57    show "ALL x y::'a lift. x << y --> x = UU | x = y"
    1.58      by (simp add: less_lift)