equal
deleted
inserted
replaced
27 text {* |
27 text {* |
28 Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"} |
28 Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"} |
29 (and similar for @{term A}). |
29 (and similar for @{term A}). |
30 *} |
30 *} |
31 |
31 |
32 constdefs |
32 definition |
33 bijP :: "('a => 'a => bool) => 'a set => bool" |
33 bijP :: "('a => 'a => bool) => 'a set => bool" |
34 "bijP P F == \<forall>a b. a \<in> F \<and> P a b --> b \<in> F" |
34 "bijP P F = (\<forall>a b. a \<in> F \<and> P a b --> b \<in> F)" |
35 |
35 |
36 uniqP :: "('a => 'a => bool) => bool" |
36 uniqP :: "('a => 'a => bool) => bool" |
37 "uniqP P == \<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d)" |
37 "uniqP P = (\<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d))" |
38 |
38 |
39 symP :: "('a => 'a => bool) => bool" |
39 symP :: "('a => 'a => bool) => bool" |
40 "symP P == \<forall>a b. P a b = P b a" |
40 "symP P = (\<forall>a b. P a b = P b a)" |
41 |
41 |
42 consts |
42 consts |
43 bijER :: "('a => 'a => bool) => 'a set set" |
43 bijER :: "('a => 'a => bool) => 'a set set" |
44 |
44 |
45 inductive "bijER P" |
45 inductive "bijER P" |