equal
deleted
inserted
replaced
41 (*Lazy list functions; flip is not definitional!*) |
41 (*Lazy list functions; flip is not definitional!*) |
42 definition |
42 definition |
43 lconst :: "i => i" where |
43 lconst :: "i => i" where |
44 "lconst(a) == lfp(univ(a), %l. LCons(a,l))" |
44 "lconst(a) == lfp(univ(a), %l. LCons(a,l))" |
45 |
45 |
46 consts |
46 axiomatization flip :: "i => i" |
47 flip :: "i => i" |
47 where |
48 axioms |
48 flip_LNil: "flip(LNil) = LNil" and |
49 flip_LNil: "flip(LNil) = LNil" |
|
50 |
|
51 flip_LCons: "[| x \<in> bool; l \<in> llist(bool) |] |
49 flip_LCons: "[| x \<in> bool; l \<in> llist(bool) |] |
52 ==> flip(LCons(x,l)) = LCons(not(x), flip(l))" |
50 ==> flip(LCons(x,l)) = LCons(not(x), flip(l))" |
53 |
51 |
54 |
52 |
55 (*These commands cause classical reasoning to regard the subset relation |
53 (*These commands cause classical reasoning to regard the subset relation |