lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
authorhaftmann
Thu Sep 24 18:29:29 2009 +0200 (2009-09-24)
changeset 32681adeac3cbb659
parent 32680 faf6924430d9
child 32682 304a47739407
lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Sep 24 18:29:29 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 24 18:29:29 2009 +0200
     1.3 @@ -2167,6 +2167,71 @@
     1.4    "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
     1.5    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
     1.6  
     1.7 +lemma (in ab_semigroup_idem_mult) fold1_set:
     1.8 +  assumes "xs \<noteq> []"
     1.9 +  shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
    1.10 +proof -
    1.11 +  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
    1.12 +  from assms obtain y ys where xs: "xs = y # ys"
    1.13 +    by (cases xs) auto
    1.14 +  show ?thesis
    1.15 +  proof (cases "set ys = {}")
    1.16 +    case True with xs show ?thesis by simp
    1.17 +  next
    1.18 +    case False
    1.19 +    then have "fold1 times (insert y (set ys)) = fold times y (set ys)"
    1.20 +      by (simp only: finite_set fold1_eq_fold_idem)
    1.21 +    with xs show ?thesis by (simp add: fold_set mult_commute)
    1.22 +  qed
    1.23 +qed
    1.24 +
    1.25 +lemma (in lattice) Inf_fin_set_fold [code_unfold]:
    1.26 +  "Inf_fin (set (x # xs)) = foldl inf x xs"
    1.27 +proof -
    1.28 +  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.29 +    by (fact ab_semigroup_idem_mult_inf)
    1.30 +  show ?thesis
    1.31 +    by (simp add: Inf_fin_def fold1_set del: set.simps)
    1.32 +qed
    1.33 +
    1.34 +lemma (in lattice) Sup_fin_set_fold [code_unfold]:
    1.35 +  "Sup_fin (set (x # xs)) = foldl sup x xs"
    1.36 +proof -
    1.37 +  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.38 +    by (fact ab_semigroup_idem_mult_sup)
    1.39 +  show ?thesis
    1.40 +    by (simp add: Sup_fin_def fold1_set del: set.simps)
    1.41 +qed
    1.42 +
    1.43 +lemma (in linorder) Min_fin_set_fold [code_unfold]:
    1.44 +  "Min (set (x # xs)) = foldl min x xs"
    1.45 +proof -
    1.46 +  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.47 +    by (fact ab_semigroup_idem_mult_min)
    1.48 +  show ?thesis
    1.49 +    by (simp add: Min_def fold1_set del: set.simps)
    1.50 +qed
    1.51 +
    1.52 +lemma (in linorder) Max_fin_set_fold [code_unfold]:
    1.53 +  "Max (set (x # xs)) = foldl max x xs"
    1.54 +proof -
    1.55 +  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.56 +    by (fact ab_semigroup_idem_mult_max)
    1.57 +  show ?thesis
    1.58 +    by (simp add: Max_def fold1_set del: set.simps)
    1.59 +qed
    1.60 +
    1.61 +lemma (in complete_lattice) Inf_set_fold [code_unfold]:
    1.62 +  "Inf (set xs) = foldl inf top xs"
    1.63 +  by (cases xs)
    1.64 +    (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold
    1.65 +      inf_commute del: set.simps, simp add: top_def)
    1.66 +
    1.67 +lemma (in complete_lattice) Sup_set_fold [code_unfold]:
    1.68 +  "Sup (set xs) = foldl sup bot xs"
    1.69 +  by (cases xs)
    1.70 +    (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold
    1.71 +      sup_commute del: set.simps, simp add: bot_def)
    1.72  
    1.73  
    1.74  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    1.75 @@ -3763,6 +3828,11 @@
    1.76    "length (remdups xs) = length_unique xs"
    1.77    by (induct xs) simp_all
    1.78  
    1.79 +declare INFI_def [code_unfold]
    1.80 +declare SUPR_def [code_unfold]
    1.81 +
    1.82 +declare set_map [symmetric, code_unfold]
    1.83 +
    1.84  hide (open) const length_unique
    1.85  
    1.86