equal
deleted
inserted
replaced
23 "sorted le [] = True" |
23 "sorted le [] = True" |
24 "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)" |
24 "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)" |
25 |
25 |
26 |
26 |
27 definition |
27 definition |
28 total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" |
28 total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where |
29 "total r = (\<forall>x y. r x y | r y x)" |
29 "total r = (\<forall>x y. r x y | r y x)" |
30 |
30 |
31 transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" |
31 definition |
|
32 transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where |
32 "transf f = (\<forall>x y z. f x y & f y z --> f x z)" |
33 "transf f = (\<forall>x y z. f x y & f y z --> f x z)" |
33 |
34 |
34 |
35 |
35 |
36 |
36 (* Equivalence of two definitions of `sorted' *) |
37 (* Equivalence of two definitions of `sorted' *) |