src/HOL/Set_Interval.thy
changeset 62128 3201ddb00097
parent 61955 e96292f32c3c
child 62343 24106dc44def
     1.1 --- a/src/HOL/Set_Interval.thy	Mon Jan 11 15:20:17 2016 +0100
     1.2 +++ b/src/HOL/Set_Interval.thy	Mon Jan 11 16:38:39 2016 +0100
     1.3 @@ -1902,4 +1902,52 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +
     1.8 +subsection \<open>Efficient folding over intervals\<close>
     1.9 +
    1.10 +function fold_atLeastAtMost_nat where
    1.11 +  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
    1.12 +                 (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"
    1.13 +by pat_completeness auto
    1.14 +termination by (relation "measure (\<lambda>(_,a,b,_). Suc b - a)") auto
    1.15 +
    1.16 +lemma fold_atLeastAtMost_nat:
    1.17 +  assumes "comp_fun_commute f"
    1.18 +  shows   "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
    1.19 +using assms
    1.20 +proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
    1.21 +  case (1 f a b acc)
    1.22 +  interpret comp_fun_commute f by fact
    1.23 +  show ?case
    1.24 +  proof (cases "a > b")
    1.25 +    case True
    1.26 +    thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
    1.27 +  next
    1.28 +    case False
    1.29 +    with 1 show ?thesis
    1.30 +      by (subst fold_atLeastAtMost_nat.simps)
    1.31 +         (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
    1.32 +  qed
    1.33 +qed
    1.34 +
    1.35 +lemma setsum_atLeastAtMost_code:
    1.36 +  "setsum f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a + acc) a b 0"
    1.37 +proof -
    1.38 +  have "comp_fun_commute (\<lambda>a. op + (f a))"
    1.39 +    by unfold_locales (auto simp: o_def add_ac)
    1.40 +  thus ?thesis
    1.41 +    by (simp add: setsum.eq_fold fold_atLeastAtMost_nat o_def)
    1.42 +qed
    1.43 +
    1.44 +lemma setprod_atLeastAtMost_code:
    1.45 +  "setprod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
    1.46 +proof -
    1.47 +  have "comp_fun_commute (\<lambda>a. op * (f a))"
    1.48 +    by unfold_locales (auto simp: o_def mult_ac)
    1.49 +  thus ?thesis
    1.50 +    by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
    1.51 +qed
    1.52 +
    1.53 +(* TODO: Add support for more kinds of intervals here *)
    1.54 +
    1.55  end