526 |
526 |
527 |
527 |
528 subsection {* A fold functional for finite sets *} |
528 subsection {* A fold functional for finite sets *} |
529 |
529 |
530 text {* The intended behaviour is |
530 text {* The intended behaviour is |
531 @{text "fold f z {x1, ..., xn} = f x1 (\<dots> (f xn z)\<dots>)"} |
531 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"} |
532 if @{text f} is ``left-commutative'': |
532 if @{text f} is ``left-commutative'': |
533 *} |
533 *} |
534 |
534 |
535 locale fun_left_comm = |
535 locale fun_left_comm = |
536 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
536 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
1888 shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1888 shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1889 by (erule finite_induct) auto |
1889 by (erule finite_induct) auto |
1890 |
1890 |
1891 lemma setprod_dividef: |
1891 lemma setprod_dividef: |
1892 fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" |
1892 fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" |
1893 shows "finite A |
1893 shows "finite A |
1894 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
1894 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
1895 apply (subgoal_tac |
1895 apply (subgoal_tac |
1896 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
1896 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
1897 apply (erule ssubst) |
1897 apply (erule ssubst) |
1898 apply (subst divide_inverse) |
1898 apply (subst divide_inverse) |
2723 |
2723 |
2724 context lattice |
2724 context lattice |
2725 begin |
2725 begin |
2726 |
2726 |
2727 definition |
2727 definition |
2728 Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>fin_" [900] 900) |
2728 Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) |
2729 where |
2729 where |
2730 "Inf_fin = fold1 inf" |
2730 "Inf_fin = fold1 inf" |
2731 |
2731 |
2732 definition |
2732 definition |
2733 Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>fin_" [900] 900) |
2733 Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) |
2734 where |
2734 where |
2735 "Sup_fin = fold1 sup" |
2735 "Sup_fin = fold1 sup" |
2736 |
2736 |
2737 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>finA \<le> \<Squnion>finA" |
2737 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A" |
2738 apply(unfold Sup_fin_def Inf_fin_def) |
2738 apply(unfold Sup_fin_def Inf_fin_def) |
2739 apply(subgoal_tac "EX a. a:A") |
2739 apply(subgoal_tac "EX a. a:A") |
2740 prefer 2 apply blast |
2740 prefer 2 apply blast |
2741 apply(erule exE) |
2741 apply(erule exE) |
2742 apply(rule order_trans) |
2742 apply(rule order_trans) |
2743 apply(erule (1) fold1_belowI) |
2743 apply(erule (1) fold1_belowI) |
2744 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice]) |
2744 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice]) |
2745 done |
2745 done |
2746 |
2746 |
2747 lemma sup_Inf_absorb [simp]: |
2747 lemma sup_Inf_absorb [simp]: |
2748 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>finA) = a" |
2748 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a" |
2749 apply(subst sup_commute) |
2749 apply(subst sup_commute) |
2750 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI) |
2750 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI) |
2751 done |
2751 done |
2752 |
2752 |
2753 lemma inf_Sup_absorb [simp]: |
2753 lemma inf_Sup_absorb [simp]: |
2754 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>finA) = a" |
2754 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a" |
2755 by (simp add: Sup_fin_def inf_absorb1 |
2755 by (simp add: Sup_fin_def inf_absorb1 |
2756 lower_semilattice.fold1_belowI [OF dual_lattice]) |
2756 lower_semilattice.fold1_belowI [OF dual_lattice]) |
2757 |
2757 |
2758 end |
2758 end |
2759 |
2759 |
2773 (rule arg_cong [where f="fold1 inf"], blast) |
2773 (rule arg_cong [where f="fold1 inf"], blast) |
2774 qed |
2774 qed |
2775 |
2775 |
2776 lemma sup_Inf2_distrib: |
2776 lemma sup_Inf2_distrib: |
2777 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2777 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2778 shows "sup (\<Sqinter>finA) (\<Sqinter>finB) = \<Sqinter>fin{sup a b|a b. a \<in> A \<and> b \<in> B}" |
2778 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}" |
2779 using A proof (induct rule: finite_ne_induct) |
2779 using A proof (induct rule: finite_ne_induct) |
2780 case singleton thus ?case |
2780 case singleton thus ?case |
2781 by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def]) |
2781 by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def]) |
2782 next |
2782 next |
2783 interpret ab_semigroup_idem_mult inf |
2783 interpret ab_semigroup_idem_mult inf |
2790 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
2790 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
2791 by blast |
2791 by blast |
2792 thus ?thesis by(simp add: insert(1) B(1)) |
2792 thus ?thesis by(simp add: insert(1) B(1)) |
2793 qed |
2793 qed |
2794 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2794 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2795 have "sup (\<Sqinter>fin(insert x A)) (\<Sqinter>finB) = sup (inf x (\<Sqinter>finA)) (\<Sqinter>finB)" |
2795 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)" |
2796 using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) |
2796 using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) |
2797 also have "\<dots> = inf (sup x (\<Sqinter>finB)) (sup (\<Sqinter>finA) (\<Sqinter>finB))" by(rule sup_inf_distrib2) |
2797 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) |
2798 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})" |
2798 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})" |
2799 using insert by(simp add:sup_Inf1_distrib[OF B]) |
2799 using insert by(simp add:sup_Inf1_distrib[OF B]) |
2800 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})" |
2800 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})" |
2801 (is "_ = \<Sqinter>fin?M") |
2801 (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M") |
2802 using B insert |
2802 using B insert |
2803 by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2803 by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2804 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2804 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2805 by blast |
2805 by blast |
2806 finally show ?case . |
2806 finally show ?case . |
2807 qed |
2807 qed |
2808 |
2808 |
2809 lemma inf_Sup1_distrib: |
2809 lemma inf_Sup1_distrib: |
2810 assumes "finite A" and "A \<noteq> {}" |
2810 assumes "finite A" and "A \<noteq> {}" |
2811 shows "inf x (\<Squnion>finA) = \<Squnion>fin{inf x a|a. a \<in> A}" |
2811 shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}" |
2812 proof - |
2812 proof - |
2813 interpret ab_semigroup_idem_mult sup |
2813 interpret ab_semigroup_idem_mult sup |
2814 by (rule ab_semigroup_idem_mult_sup) |
2814 by (rule ab_semigroup_idem_mult_sup) |
2815 from assms show ?thesis |
2815 from assms show ?thesis |
2816 by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1]) |
2816 by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1]) |
2817 (rule arg_cong [where f="fold1 sup"], blast) |
2817 (rule arg_cong [where f="fold1 sup"], blast) |
2818 qed |
2818 qed |
2819 |
2819 |
2820 lemma inf_Sup2_distrib: |
2820 lemma inf_Sup2_distrib: |
2821 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2821 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
2822 shows "inf (\<Squnion>finA) (\<Squnion>finB) = \<Squnion>fin{inf a b|a b. a \<in> A \<and> b \<in> B}" |
2822 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}" |
2823 using A proof (induct rule: finite_ne_induct) |
2823 using A proof (induct rule: finite_ne_induct) |
2824 case singleton thus ?case |
2824 case singleton thus ?case |
2825 by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def]) |
2825 by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def]) |
2826 next |
2826 next |
2827 case (insert x A) |
2827 case (insert x A) |
2834 thus ?thesis by(simp add: insert(1) B(1)) |
2834 thus ?thesis by(simp add: insert(1) B(1)) |
2835 qed |
2835 qed |
2836 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2836 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
2837 interpret ab_semigroup_idem_mult sup |
2837 interpret ab_semigroup_idem_mult sup |
2838 by (rule ab_semigroup_idem_mult_sup) |
2838 by (rule ab_semigroup_idem_mult_sup) |
2839 have "inf (\<Squnion>fin(insert x A)) (\<Squnion>finB) = inf (sup x (\<Squnion>finA)) (\<Squnion>finB)" |
2839 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)" |
2840 using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) |
2840 using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) |
2841 also have "\<dots> = sup (inf x (\<Squnion>finB)) (inf (\<Squnion>finA) (\<Squnion>finB))" by(rule inf_sup_distrib2) |
2841 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) |
2842 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})" |
2842 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})" |
2843 using insert by(simp add:inf_Sup1_distrib[OF B]) |
2843 using insert by(simp add:inf_Sup1_distrib[OF B]) |
2844 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})" |
2844 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})" |
2845 (is "_ = \<Squnion>fin?M") |
2845 (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M") |
2846 using B insert |
2846 using B insert |
2847 by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2847 by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne]) |
2848 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2848 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
2849 by blast |
2849 by blast |
2850 finally show ?case . |
2850 finally show ?case . |
2859 Coincidence on finite sets in complete lattices: |
2859 Coincidence on finite sets in complete lattices: |
2860 *} |
2860 *} |
2861 |
2861 |
2862 lemma Inf_fin_Inf: |
2862 lemma Inf_fin_Inf: |
2863 assumes "finite A" and "A \<noteq> {}" |
2863 assumes "finite A" and "A \<noteq> {}" |
2864 shows "\<Sqinter>finA = Inf A" |
2864 shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A" |
2865 proof - |
2865 proof - |
2866 interpret ab_semigroup_idem_mult inf |
2866 interpret ab_semigroup_idem_mult inf |
2867 by (rule ab_semigroup_idem_mult_inf) |
2867 by (rule ab_semigroup_idem_mult_inf) |
2868 from assms show ?thesis |
2868 from assms show ?thesis |
2869 unfolding Inf_fin_def by (induct A set: finite) |
2869 unfolding Inf_fin_def by (induct A set: finite) |
2870 (simp_all add: Inf_insert_simp) |
2870 (simp_all add: Inf_insert_simp) |
2871 qed |
2871 qed |
2872 |
2872 |
2873 lemma Sup_fin_Sup: |
2873 lemma Sup_fin_Sup: |
2874 assumes "finite A" and "A \<noteq> {}" |
2874 assumes "finite A" and "A \<noteq> {}" |
2875 shows "\<Squnion>finA = Sup A" |
2875 shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A" |
2876 proof - |
2876 proof - |
2877 interpret ab_semigroup_idem_mult sup |
2877 interpret ab_semigroup_idem_mult sup |
2878 by (rule ab_semigroup_idem_mult_sup) |
2878 by (rule ab_semigroup_idem_mult_sup) |
2879 from assms show ?thesis |
2879 from assms show ?thesis |
2880 unfolding Sup_fin_def by (induct A set: finite) |
2880 unfolding Sup_fin_def by (induct A set: finite) |