equal
deleted
inserted
replaced
327 definition |
327 definition |
328 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
328 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
329 where |
329 where |
330 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
330 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
331 |
331 |
332 (* Babs p m = \<lambda>x. if x \<in> p then m x else undefined *) |
332 (* TODO: Consider defining it with an "if"; sth like: |
333 |
333 Babs p m = \<lambda>x. if x \<in> p then m x else undefined |
334 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where |
334 *) |
335 "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*) |
|
336 |
|
337 |
|
338 ML {* exists *} |
|
339 ML {* mem *} |
|
340 |
335 |
341 ML {* |
336 ML {* |
342 fun needs_lift (rty as Type (rty_s, _)) ty = |
337 fun needs_lift (rty as Type (rty_s, _)) ty = |
343 case ty of |
338 case ty of |
344 Type (s, tys) => |
339 Type (s, tys) => |