522 |
522 |
523 |
523 |
524 subsection {* A fold functional for finite sets *} |
524 subsection {* A fold functional for finite sets *} |
525 |
525 |
526 text {* The intended behaviour is |
526 text {* The intended behaviour is |
527 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"} |
527 @{text "fold f z {x1, ..., xn} = f x1 (\<dots> (f xn z)\<dots>)"} |
528 if @{text f} is ``left-commutative'': |
528 if @{text f} is ``left-commutative'': |
529 *} |
529 *} |
530 |
530 |
531 locale fun_left_comm = |
531 locale fun_left_comm = |
532 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
532 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
1877 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> |
1877 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> |
1878 (setprod f (A - {a}) :: 'a :: {field}) = |
1878 (setprod f (A - {a}) :: 'a :: {field}) = |
1879 (if a:A then setprod f A / f a else setprod f A)" |
1879 (if a:A then setprod f A / f a else setprod f A)" |
1880 by (erule finite_induct) (auto simp add: insert_Diff_if) |
1880 by (erule finite_induct) (auto simp add: insert_Diff_if) |
1881 |
1881 |
1882 lemma setprod_inversef: "finite A ==> |
1882 lemma setprod_inversef: |
1883 ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> |
1883 fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" |
1884 setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1884 shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1885 by (erule finite_induct) auto |
1885 by (erule finite_induct) auto |
1886 |
1886 |
1887 lemma setprod_dividef: |
1887 lemma setprod_dividef: |
1888 "[|finite A; |
1888 fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" |
1889 \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|] |
1889 shows "finite A |
1890 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
1890 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
1891 apply (subgoal_tac |
1891 apply (subgoal_tac |
1892 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
1892 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
1893 apply (erule ssubst) |
1893 apply (erule ssubst) |
1894 apply (subst divide_inverse) |
1894 apply (subst divide_inverse) |
2719 |
2719 |
2720 context lattice |
2720 context lattice |
2721 begin |
2721 begin |
2722 |
2722 |
2723 definition |
2723 definition |
2724 Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) |
2724 Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>fin_" [900] 900) |
2725 where |
2725 where |
2726 "Inf_fin = fold1 inf" |
2726 "Inf_fin = fold1 inf" |
2727 |
2727 |
2728 definition |
2728 definition |
2729 Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) |
2729 Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>fin_" [900] 900) |
2730 where |
2730 where |
2731 "Sup_fin = fold1 sup" |
2731 "Sup_fin = fold1 sup" |
2732 |
2732 |
2733 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A" |
2733 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>finA \<le> \<Squnion>finA" |
2734 apply(unfold Sup_fin_def Inf_fin_def) |
2734 apply(unfold Sup_fin_def Inf_fin_def) |
2735 apply(subgoal_tac "EX a. a:A") |
2735 apply(subgoal_tac "EX a. a:A") |
2736 prefer 2 apply blast |
2736 prefer 2 apply blast |
2737 apply(erule exE) |
2737 apply(erule exE) |
2738 apply(rule order_trans) |
2738 apply(rule order_trans) |
2739 apply(erule (1) fold1_belowI) |
2739 apply(erule (1) fold1_belowI) |
2740 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice]) |
2740 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice]) |
2741 done |
2741 done |
2742 |
2742 |
2743 lemma sup_Inf_absorb [simp]: |
2743 lemma sup_Inf_absorb [simp]: |
2744 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a" |
2744 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>finA) = a" |
2745 apply(subst sup_commute) |
2745 apply(subst sup_commute) |
2746 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI) |
2746 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI) |
2747 done |
2747 done |
2748 |
2748 |
2749 lemma inf_Sup_absorb [simp]: |
2749 lemma inf_Sup_absorb [simp]: |
2750 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a" |
2750 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>finA) = a" |
2751 by (simp add: Sup_fin_def inf_absorb1 |
2751 by (simp add: Sup_fin_def inf_absorb1 |
2752 lower_semilattice.fold1_belowI [OF dual_lattice]) |
2752 lower_semilattice.fold1_belowI [OF dual_lattice]) |
2753 |
2753 |
2754 end |
2754 end |
2755 |
2755 |
2769 (rule arg_cong [where f="fold1 inf"], blast) |
2769 (rule arg_cong [where f="fold1 inf"], blast) |
2770 qed |
2770 qed |
2771 |
2771 |
2772 lemma sup_Inf2_distrib: |
2772 lemma sup_Inf2_distrib: |
2773 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2773 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2774 shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}" |
2774 shows "sup (\<Sqinter>finA) (\<Sqinter>finB) = \<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B}" |
2775 using A proof (induct rule: finite_ne_induct) |
2775 using A proof (induct rule: finite_ne_induct) |
2776 case singleton thus ?case |
2776 case singleton thus ?case |
2777 by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def]) |
2777 by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def]) |
2778 next |
2778 next |
2779 interpret ab_semigroup_idem_mult inf |
2779 interpret ab_semigroup_idem_mult inf |
2786 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
2786 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
2787 by blast |
2787 by blast |
2788 thus ?thesis by(simp add: insert(1) B(1)) |
2788 thus ?thesis by(simp add: insert(1) B(1)) |
2789 qed |
2789 qed |
2790 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2790 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2791 have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)" |
2791 have "sup (\<Sqinter>fin(insert x A)) (\<Sqinter>finB) = sup (inf x (\<Sqinter>finA)) (\<Sqinter>finB)" |
2792 using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) |
2792 using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) |
2793 also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2) |
2793 also have "\<dots> = inf (sup x (\<Sqinter>finB)) (sup (\<Sqinter>finA) (\<Sqinter>finB))" by(rule sup_inf_distrib2) |
2794 also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})" |
2794 also have "\<dots> = inf (\<Sqinter>fin{sup x b|b. b \<in> B}) (\<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B})" |
2795 using insert by(simp add:sup_Inf1_distrib[OF B]) |
2795 using insert by(simp add:sup_Inf1_distrib[OF B]) |
2796 also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})" |
2796 also have "\<dots> = \<Sqinter>fin({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})" |
2797 (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M") |
2797 (is "_ = \<Sqinter>fin?M") |
2798 using B insert |
2798 using B insert |
2799 by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2799 by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2800 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2800 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2801 by blast |
2801 by blast |
2802 finally show ?case . |
2802 finally show ?case . |
2803 qed |
2803 qed |
2804 |
2804 |
2805 lemma inf_Sup1_distrib: |
2805 lemma inf_Sup1_distrib: |
2806 assumes "finite A" and "A \<noteq> {}" |
2806 assumes "finite A" and "A \<noteq> {}" |
2807 shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}" |
2807 shows "inf x (\<Squnion>finA) = \<Squnion>fin{inf x a|a. a \<in> A}" |
2808 proof - |
2808 proof - |
2809 interpret ab_semigroup_idem_mult sup |
2809 interpret ab_semigroup_idem_mult sup |
2810 by (rule ab_semigroup_idem_mult_sup) |
2810 by (rule ab_semigroup_idem_mult_sup) |
2811 from assms show ?thesis |
2811 from assms show ?thesis |
2812 by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1]) |
2812 by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1]) |
2813 (rule arg_cong [where f="fold1 sup"], blast) |
2813 (rule arg_cong [where f="fold1 sup"], blast) |
2814 qed |
2814 qed |
2815 |
2815 |
2816 lemma inf_Sup2_distrib: |
2816 lemma inf_Sup2_distrib: |
2817 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2817 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2818 shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}" |
2818 shows "inf (\<Squnion>finA) (\<Squnion>finB) = \<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B}" |
2819 using A proof (induct rule: finite_ne_induct) |
2819 using A proof (induct rule: finite_ne_induct) |
2820 case singleton thus ?case |
2820 case singleton thus ?case |
2821 by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def]) |
2821 by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def]) |
2822 next |
2822 next |
2823 case (insert x A) |
2823 case (insert x A) |
2830 thus ?thesis by(simp add: insert(1) B(1)) |
2830 thus ?thesis by(simp add: insert(1) B(1)) |
2831 qed |
2831 qed |
2832 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2832 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2833 interpret ab_semigroup_idem_mult sup |
2833 interpret ab_semigroup_idem_mult sup |
2834 by (rule ab_semigroup_idem_mult_sup) |
2834 by (rule ab_semigroup_idem_mult_sup) |
2835 have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)" |
2835 have "inf (\<Squnion>fin(insert x A)) (\<Squnion>finB) = inf (sup x (\<Squnion>finA)) (\<Squnion>finB)" |
2836 using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) |
2836 using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) |
2837 also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2) |
2837 also have "\<dots> = sup (inf x (\<Squnion>finB)) (inf (\<Squnion>finA) (\<Squnion>finB))" by(rule inf_sup_distrib2) |
2838 also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})" |
2838 also have "\<dots> = sup (\<Squnion>fin{inf x b|b. b \<in> B}) (\<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B})" |
2839 using insert by(simp add:inf_Sup1_distrib[OF B]) |
2839 using insert by(simp add:inf_Sup1_distrib[OF B]) |
2840 also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})" |
2840 also have "\<dots> = \<Squnion>fin({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})" |
2841 (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M") |
2841 (is "_ = \<Squnion>fin?M") |
2842 using B insert |
2842 using B insert |
2843 by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2843 by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2844 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2844 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2845 by blast |
2845 by blast |
2846 finally show ?case . |
2846 finally show ?case . |
2855 Coincidence on finite sets in complete lattices: |
2855 Coincidence on finite sets in complete lattices: |
2856 *} |
2856 *} |
2857 |
2857 |
2858 lemma Inf_fin_Inf: |
2858 lemma Inf_fin_Inf: |
2859 assumes "finite A" and "A \<noteq> {}" |
2859 assumes "finite A" and "A \<noteq> {}" |
2860 shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A" |
2860 shows "\<Sqinter>finA = Inf A" |
2861 proof - |
2861 proof - |
2862 interpret ab_semigroup_idem_mult inf |
2862 interpret ab_semigroup_idem_mult inf |
2863 by (rule ab_semigroup_idem_mult_inf) |
2863 by (rule ab_semigroup_idem_mult_inf) |
2864 from assms show ?thesis |
2864 from assms show ?thesis |
2865 unfolding Inf_fin_def by (induct A set: finite) |
2865 unfolding Inf_fin_def by (induct A set: finite) |
2866 (simp_all add: Inf_insert_simp) |
2866 (simp_all add: Inf_insert_simp) |
2867 qed |
2867 qed |
2868 |
2868 |
2869 lemma Sup_fin_Sup: |
2869 lemma Sup_fin_Sup: |
2870 assumes "finite A" and "A \<noteq> {}" |
2870 assumes "finite A" and "A \<noteq> {}" |
2871 shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A" |
2871 shows "\<Squnion>finA = Sup A" |
2872 proof - |
2872 proof - |
2873 interpret ab_semigroup_idem_mult sup |
2873 interpret ab_semigroup_idem_mult sup |
2874 by (rule ab_semigroup_idem_mult_sup) |
2874 by (rule ab_semigroup_idem_mult_sup) |
2875 from assms show ?thesis |
2875 from assms show ?thesis |
2876 unfolding Sup_fin_def by (induct A set: finite) |
2876 unfolding Sup_fin_def by (induct A set: finite) |