equal
deleted
inserted
replaced
754 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x" |
754 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x" |
755 declare Inf'_def[symmetric, code_unfold] |
755 declare Inf'_def[symmetric, code_unfold] |
756 declare Inf_Set_fold[folded Inf'_def, code] |
756 declare Inf_Set_fold[folded Inf'_def, code] |
757 |
757 |
758 lemma INFI_Set_fold [code]: |
758 lemma INFI_Set_fold [code]: |
759 "INFI (Set t) f = fold_keys (inf \<circ> f) t top" |
759 fixes f :: "_ \<Rightarrow> 'a::complete_lattice" |
|
760 shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top" |
760 proof - |
761 proof - |
761 have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" |
762 have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" |
762 by default (auto simp add: fun_eq_iff ac_simps) |
763 by default (auto simp add: fun_eq_iff ac_simps) |
763 then show ?thesis |
764 then show ?thesis |
764 by (auto simp: INF_fold_inf finite_fold_fold_keys) |
765 by (auto simp: INF_fold_inf finite_fold_fold_keys) |
794 definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x" |
795 definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x" |
795 declare Sup'_def[symmetric, code_unfold] |
796 declare Sup'_def[symmetric, code_unfold] |
796 declare Sup_Set_fold[folded Sup'_def, code] |
797 declare Sup_Set_fold[folded Sup'_def, code] |
797 |
798 |
798 lemma SUPR_Set_fold [code]: |
799 lemma SUPR_Set_fold [code]: |
799 "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot" |
800 fixes f :: "_ \<Rightarrow> 'a::complete_lattice" |
|
801 shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot" |
800 proof - |
802 proof - |
801 have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" |
803 have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" |
802 by default (auto simp add: fun_eq_iff ac_simps) |
804 by default (auto simp add: fun_eq_iff ac_simps) |
803 then show ?thesis |
805 then show ?thesis |
804 by (auto simp: SUP_fold_sup finite_fold_fold_keys) |
806 by (auto simp: SUP_fold_sup finite_fold_fold_keys) |