equal
deleted
inserted
replaced
83 |
83 |
84 lemma [code, code del]: |
84 lemma [code, code del]: |
85 "Pow = Pow" .. |
85 "Pow = Pow" .. |
86 |
86 |
87 lemma [code, code del]: |
87 lemma [code, code del]: |
88 "setsum = setsum" .. |
88 "sum = sum" .. |
89 |
89 |
90 lemma [code, code del]: |
90 lemma [code, code del]: |
91 "setprod = setprod" .. |
91 "setprod = setprod" .. |
92 |
92 |
93 lemma [code, code del]: |
93 lemma [code, code del]: |
671 |
671 |
672 lemma card_Set [code]: |
672 lemma card_Set [code]: |
673 "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0" |
673 "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0" |
674 by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const) |
674 by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const) |
675 |
675 |
676 lemma setsum_Set [code]: |
676 lemma sum_Set [code]: |
677 "setsum f (Set xs) = fold_keys (plus o f) xs 0" |
677 "sum f (Set xs) = fold_keys (plus o f) xs 0" |
678 proof - |
678 proof - |
679 have "comp_fun_commute (\<lambda>x. op + (f x))" |
679 have "comp_fun_commute (\<lambda>x. op + (f x))" |
680 by standard (auto simp: ac_simps) |
680 by standard (auto simp: ac_simps) |
681 then show ?thesis |
681 then show ?thesis |
682 by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def) |
682 by (auto simp add: sum.eq_fold finite_fold_fold_keys o_def) |
683 qed |
683 qed |
684 |
684 |
685 lemma the_elem_set [code]: |
685 lemma the_elem_set [code]: |
686 fixes t :: "('a :: linorder, unit) rbt" |
686 fixes t :: "('a :: linorder, unit) rbt" |
687 shows "the_elem (Set t) = (case RBT.impl_of t of |
687 shows "the_elem (Set t) = (case RBT.impl_of t of |