equal
deleted
inserted
replaced
93 |
93 |
94 definition |
94 definition |
95 flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where |
95 flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where |
96 "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))" |
96 "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))" |
97 |
97 |
|
98 translations |
|
99 "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)" |
|
100 "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t" |
|
101 "\<Lambda>(CONST Def x). t" <= "FLIFT x. t" |
|
102 |
98 definition |
103 definition |
99 flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where |
104 flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where |
100 "flift2 f = (FLIFT x. Def (f x))" |
105 "flift2 f = (FLIFT x. Def (f x))" |
101 |
106 |
102 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" |
107 lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" |