215 done |
215 done |
216 |
216 |
217 lemma finite_Union[simp, intro]: |
217 lemma finite_Union[simp, intro]: |
218 "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)" |
218 "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)" |
219 by (induct rule:finite_induct) simp_all |
219 by (induct rule:finite_induct) simp_all |
|
220 |
|
221 lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)" |
|
222 by (blast intro: Inter_lower finite_subset) |
|
223 |
|
224 lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)" |
|
225 by (blast intro: INT_lower finite_subset) |
220 |
226 |
221 lemma finite_empty_induct: |
227 lemma finite_empty_induct: |
222 assumes "finite A" |
228 assumes "finite A" |
223 and "P A" |
229 and "P A" |
224 and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})" |
230 and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})" |
782 "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" |
788 "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A" |
783 by(simp add:fold_fun_comm) |
789 by(simp add:fold_fun_comm) |
784 |
790 |
785 end |
791 end |
786 |
792 |
|
793 context ab_semigroup_idem_mult |
|
794 begin |
|
795 |
|
796 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)" |
|
797 apply unfold_locales |
|
798 apply (simp add: mult_ac) |
|
799 apply (simp add: mult_idem mult_assoc[symmetric]) |
|
800 done |
|
801 |
|
802 end |
|
803 |
|
804 context lower_semilattice |
|
805 begin |
|
806 |
|
807 lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf" |
|
808 proof qed (rule inf_assoc inf_commute inf_idem)+ |
|
809 |
|
810 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)" |
|
811 by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]]) |
|
812 |
|
813 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A" |
|
814 by (induct pred:finite) auto |
|
815 |
|
816 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b" |
|
817 proof(induct arbitrary: a pred:finite) |
|
818 case empty thus ?case by simp |
|
819 next |
|
820 case (insert x A) |
|
821 show ?case |
|
822 proof cases |
|
823 assume "A = {}" thus ?thesis using insert by simp |
|
824 next |
|
825 assume "A \<noteq> {}" thus ?thesis using insert by auto |
|
826 qed |
|
827 qed |
|
828 |
|
829 end |
|
830 |
|
831 context upper_semilattice |
|
832 begin |
|
833 |
|
834 lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup" |
|
835 by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice) |
|
836 |
|
837 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)" |
|
838 by(rule lower_semilattice.fold_inf_insert)(rule dual_semlattice) |
|
839 |
|
840 lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c" |
|
841 by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice) |
|
842 |
|
843 lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A" |
|
844 by(rule lower_semilattice.fold_inf_le_inf)(rule dual_semilattice) |
|
845 |
|
846 end |
|
847 |
|
848 |
787 subsubsection{* The derived combinator @{text fold_image} *} |
849 subsubsection{* The derived combinator @{text fold_image} *} |
788 |
850 |
789 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
851 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
790 where "fold_image f g = fold (%x y. f (g x) y)" |
852 where "fold_image f g = fold (%x y. f (g x) y)" |
791 |
853 |
799 assumes "finite A" and "a \<notin> A" |
861 assumes "finite A" and "a \<notin> A" |
800 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" |
862 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" |
801 proof - |
863 proof - |
802 interpret I: fun_left_comm "%x y. (g x) * y" |
864 interpret I: fun_left_comm "%x y. (g x) * y" |
803 by unfold_locales (simp add: mult_ac) |
865 by unfold_locales (simp add: mult_ac) |
804 show ?thesis using assms by(simp add:fold_image_def I.fold_insert) |
866 show ?thesis using assms by(simp add:fold_image_def) |
805 qed |
867 qed |
806 |
868 |
807 (* |
869 (* |
808 lemma fold_commute: |
870 lemma fold_commute: |
809 "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)" |
871 "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)" |
827 *) |
889 *) |
828 |
890 |
829 lemma fold_image_reindex: |
891 lemma fold_image_reindex: |
830 assumes fin: "finite A" |
892 assumes fin: "finite A" |
831 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A" |
893 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A" |
832 using fin apply induct |
894 using fin by induct auto |
833 apply simp |
|
834 apply simp |
|
835 done |
|
836 |
895 |
837 (* |
896 (* |
838 text{* |
897 text{* |
839 Fusion theorem, as described in Graham Hutton's paper, |
898 Fusion theorem, as described in Graham Hutton's paper, |
840 A Tutorial on the Universality and Expressiveness of Fold, |
899 A Tutorial on the Universality and Expressiveness of Fold, |
2349 |
2408 |
2350 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a" |
2409 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a" |
2351 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f" |
2410 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f" |
2352 by(fastsimp simp:surj_def dest!: endo_inj_surj) |
2411 by(fastsimp simp:surj_def dest!: endo_inj_surj) |
2353 |
2412 |
2354 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)" |
2413 corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)" |
2355 proof |
2414 proof |
2356 assume "finite(UNIV::nat set)" |
2415 assume "finite(UNIV::nat set)" |
2357 with finite_UNIV_inj_surj[of Suc] |
2416 with finite_UNIV_inj_surj[of Suc] |
2358 show False by simp (blast dest: Suc_neq_Zero surjD) |
2417 show False by simp (blast dest: Suc_neq_Zero surjD) |
2359 qed |
2418 qed |
2360 |
2419 |
2361 lemma infinite_UNIV_char_0: |
2420 (* Often leads to bogus ATP proofs because of reduced type information, hence noatp *) |
|
2421 lemma infinite_UNIV_char_0[noatp]: |
2362 "\<not> finite (UNIV::'a::semiring_char_0 set)" |
2422 "\<not> finite (UNIV::'a::semiring_char_0 set)" |
2363 proof |
2423 proof |
2364 assume "finite (UNIV::'a set)" |
2424 assume "finite (UNIV::'a set)" |
2365 with subset_UNIV have "finite (range of_nat::'a set)" |
2425 with subset_UNIV have "finite (range of_nat::'a set)" |
2366 by (rule finite_subset) |
2426 by (rule finite_subset) |
2496 |
2556 |
2497 end |
2557 end |
2498 |
2558 |
2499 context ab_semigroup_idem_mult |
2559 context ab_semigroup_idem_mult |
2500 begin |
2560 begin |
2501 |
|
2502 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)" |
|
2503 apply unfold_locales |
|
2504 apply (simp add: mult_ac) |
|
2505 apply (simp add: mult_idem mult_assoc[symmetric]) |
|
2506 done |
|
2507 |
|
2508 |
2561 |
2509 lemma fold1_insert_idem [simp]: |
2562 lemma fold1_insert_idem [simp]: |
2510 assumes nonempty: "A \<noteq> {}" and A: "finite A" |
2563 assumes nonempty: "A \<noteq> {}" and A: "finite A" |
2511 shows "fold1 times (insert x A) = x * fold1 times A" |
2564 shows "fold1 times (insert x A) = x * fold1 times A" |
2512 proof - |
2565 proof - |
2665 *} |
2718 *} |
2666 |
2719 |
2667 context lower_semilattice |
2720 context lower_semilattice |
2668 begin |
2721 begin |
2669 |
2722 |
2670 lemma ab_semigroup_idem_mult_inf: |
|
2671 "ab_semigroup_idem_mult inf" |
|
2672 proof qed (rule inf_assoc inf_commute inf_idem)+ |
|
2673 |
|
2674 lemma below_fold1_iff: |
2723 lemma below_fold1_iff: |
2675 assumes "finite A" "A \<noteq> {}" |
2724 assumes "finite A" "A \<noteq> {}" |
2676 shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" |
2725 shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" |
2677 proof - |
2726 proof - |
2678 interpret ab_semigroup_idem_mult inf |
2727 interpret ab_semigroup_idem_mult inf |