equal
deleted
inserted
replaced
5 theory More_List |
5 theory More_List |
6 imports List |
6 imports List |
7 begin |
7 begin |
8 |
8 |
9 hide_const (open) Finite_Set.fold |
9 hide_const (open) Finite_Set.fold |
10 |
|
11 text {* Repairing code generator setup *} |
|
12 |
|
13 declare (in lattice) Inf_fin_set_fold [code_unfold del] |
|
14 declare (in lattice) Sup_fin_set_fold [code_unfold del] |
|
15 declare (in linorder) Min_fin_set_fold [code_unfold del] |
|
16 declare (in linorder) Max_fin_set_fold [code_unfold del] |
|
17 declare (in complete_lattice) Inf_set_fold [code_unfold del] |
|
18 declare (in complete_lattice) Sup_set_fold [code_unfold del] |
|
19 |
|
20 |
10 |
21 text {* Fold combinator with canonical argument order *} |
11 text {* Fold combinator with canonical argument order *} |
22 |
12 |
23 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where |
13 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where |
24 "fold f [] = id" |
14 "fold f [] = id" |
236 lemma (in complete_lattice) Sup_set_fold: |
226 lemma (in complete_lattice) Sup_set_fold: |
237 "Sup (set xs) = fold sup xs bot" |
227 "Sup (set xs) = fold sup xs bot" |
238 proof - |
228 proof - |
239 interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
229 interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
240 by (fact comp_fun_idem_sup) |
230 by (fact comp_fun_idem_sup) |
241 show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute) |
231 show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute) |
242 qed |
232 qed |
243 |
233 |
244 lemma (in complete_lattice) Sup_set_foldr [code_unfold]: |
234 lemma (in complete_lattice) Sup_set_foldr [code_unfold]: |
245 "Sup (set xs) = foldr sup xs bot" |
235 "Sup (set xs) = foldr sup xs bot" |
246 by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) |
236 by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) |