equal
deleted
inserted
replaced
1826 by (blast intro: foldSet1_determ_aux [rule_format]) |
1826 by (blast intro: foldSet1_determ_aux [rule_format]) |
1827 |
1827 |
1828 lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y" |
1828 lemma (in ACf) foldSet1_equality: "(A, y) : foldSet1 f ==> fold1 f A = y" |
1829 by (unfold fold1_def) (blast intro: foldSet1_determ) |
1829 by (unfold fold1_def) (blast intro: foldSet1_determ) |
1830 |
1830 |
1831 lemma fold1_singleton: "fold1 f {a} = a" |
1831 lemma fold1_singleton[simp]: "fold1 f {a} = a" |
1832 by (unfold fold1_def) blast |
1832 by (unfold fold1_def) blast |
1833 |
1833 |
1834 lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> |
1834 lemma (in ACf) foldSet1_insert_aux: "x \<notin> A ==> A \<noteq> {} \<Longrightarrow> |
1835 ((insert x A, v) : foldSet1 f) = |
1835 ((insert x A, v) : foldSet1 f) = |
1836 (EX y. (A, y) : foldSet1 f & v = f x y)" |
1836 (EX y. (A, y) : foldSet1 f & v = f x y)" |