diff --git a/thys/Hidden_Markov_Models/Hidden_Markov_Model.thy b/thys/Hidden_Markov_Models/Hidden_Markov_Model.thy --- a/thys/Hidden_Markov_Models/Hidden_Markov_Model.thy +++ b/thys/Hidden_Markov_Models/Hidden_Markov_Model.thy @@ -1,626 +1,626 @@ section \Hidden Markov Models\ theory Hidden_Markov_Model imports Markov_Models.Discrete_Time_Markov_Chain Auxiliary "HOL-Library.IArray" begin subsection \Definitions\ text \Definition of Markov Kernels that are closed w.r.t. to a set of states.\ locale Closed_Kernel = fixes K :: "'s \ 't pmf" and S :: "'t set" assumes finite: "finite S" and wellformed: "S \ {}" and closed: "\ s. K s \ S" text \ An HMM is parameterized by a Markov kernel for the transition probabilites between internal states, a Markov kernel for the output probabilities of observations, and a fixed set of observations. \ locale HMM_defs = fixes \ :: "'s \ 's pmf" and \ :: "'s \ 't pmf" and \\<^sub>s :: "'t set" locale HMM = HMM_defs + O: Closed_Kernel \ \\<^sub>s begin lemma observations_finite: "finite \\<^sub>s" and observations_wellformed: "\\<^sub>s \ {}" and observations_closed: "\ s. \ s \ \\<^sub>s" using O.finite O.wellformed O.closed by - end text \Fixed set of internal states.\ locale HMM2_defs = HMM_defs \ \ for \ :: "'s \ 's pmf" and \ :: "'s \ 't pmf" + fixes \ :: "'s set" locale HMM2 = HMM2_defs + HMM + K: Closed_Kernel \ \ begin lemma states_finite: "finite \" and states_wellformed: "\ \ {}" and states_closed: "\ s. \ s \ \" using K.finite K.wellformed K.closed by - end text \ The set of internal states is now given as a list to iterate over. This is needed for the computations on HMMs. \ locale HMM3_defs = HMM2_defs \\<^sub>s \ for \\<^sub>s :: "'t set" and \ :: "'s \ 's pmf" + fixes state_list :: "'s list" locale HMM3 = HMM3_defs _ _ \\<^sub>s \ + HMM2 \\<^sub>s \ for \\<^sub>s :: "'t set" and \ :: "'s \ 's pmf" + assumes state_list_\: "set state_list = \" context HMM_defs begin no_notation (ASCII) comp (infixl "o" 55) text \The ``default'' observation.\ definition "obs \ SOME x. x \ \\<^sub>s" lemma (in HMM) obs: "obs \ \\<^sub>s" unfolding obs_def using observations_wellformed by (auto intro: someI_ex) text \ The HMM is encoded as a Markov chain over pairs of states and observations. This is the Markov chain's defining Markov kernel. \ definition "K \ \ (s\<^sub>1, o\<^sub>1 :: 't). bind_pmf (\ s\<^sub>1) (\ s\<^sub>2. map_pmf (\ o\<^sub>2. (s\<^sub>2, o\<^sub>2)) (\ s\<^sub>2))" sublocale MC_syntax K . text \ Uniform distribution of the pairs \(s, o)\ for a fixed state \s\. \ definition "I (s :: 's) = map_pmf (\ x. (s, x)) (pmf_of_set \\<^sub>s)" text \ The likelihood of an observation sequence given a starting state \s\ is defined in terms of the trace space of the Markov kernel given the uniform distribution of pairs for \s\. \ definition "likelihood s os = T' (I s) {\ \ space S. \ o\<^sub>0 xs \'. \ = (s, o\<^sub>0) ## xs @- \' \ map snd xs = os}" abbreviation (input) "L os \ \ \ xs \'. \ = xs @- \' \ map snd xs = os" lemma likelihood_alt_def: "likelihood s os = T' (I s) {(s, o) ## xs @- \' |o xs \'. map snd xs = os}" unfolding likelihood_def by (simp add: in_S) subsection \Iteration Rule For Likelihood\ lemma L_Nil: "L [] \ = True" by simp lemma emeasure_T_observation_Nil: "T (s, o\<^sub>0) {\ \ space S. L [] \} = 1" by simp lemma L_Cons: "L (o # os) \ \ snd (shd \) = o \ L os (stl \)" apply (cases \; cases "shd \"; safe; clarsimp) apply force subgoal for x xs \' by (force intro: exI[where x = "(x, o) # xs"]) done lemma L_measurable[measurable]: "Measurable.pred S (L os)" apply (induction os) apply (simp; fail) subgoal premises that for o os by(subst L_Cons) (intro Measurable.pred_intros_logic measurable_compose[OF measurable_shd] measurable_compose[OF measurable_stl that]; measurable) done lemma init_measurable[measurable]: "Measurable.pred S (\x. \o\<^sub>0 xs \'. x = (s, o\<^sub>0) ## xs @- \' \ map snd xs = os)" (is "Measurable.pred S ?f") proof - have *: "?f \ \ fst (shd \) = s \ L os (stl \)" for \ by (cases \) auto show ?thesis by (subst *) (intro Measurable.pred_intros_logic measurable_compose[OF measurable_shd]; measurable) qed lemma T_init_observation_eq: "T (s, o) {\ \ space S. L os \} = T (s, o') {\ \ space S. L os \}" apply (subst emeasure_Collect_T[unfolded space_T], (measurable; fail)) apply (subst (2) emeasure_Collect_T[unfolded space_T], (measurable; fail)) apply (simp add: K_def) done text \ Shows that it is equivalent to define likelihood in terms of the trace space starting at a single pair of an internal state \s\ and the default observation @{term obs}. \ lemma (in HMM) likelihood_init: "likelihood s os = T (s, obs) {\ \ space S. L os \}" proof - have *: "(\o\\\<^sub>s. emeasure (T (s, o)) {\ \ space S. L os \}) = of_nat (card \\<^sub>s) * emeasure (T (s, obs)) {\ \ space S. L os \}" by (subst sum_constant[symmetric]) (fastforce intro: sum.cong T_init_observation_eq[simplified]) show ?thesis unfolding likelihood_def apply (subst emeasure_T') subgoal by measurable using * apply (simp add: I_def in_S observations_finite observations_wellformed nn_integral_pmf_of_set) apply (subst mult.commute) apply (simp add: observations_finite observations_wellformed mult_divide_eq_ennreal) done qed lemma emeasure_T_observation_Cons: "T (s, o\<^sub>0) {\ \ space S. L (o\<^sub>1 # os) \} = (\\<^sup>+ t. ennreal (pmf (\ t) o\<^sub>1) * T (t, o\<^sub>1) {\ \ space S. L os \} \(\ s))" (is "?l = ?r") proof - have *: "\\<^sup>+ y. T (s', y) {x \ space S. \xs. (\\'. (s', y) ## x = xs @- \') \ map snd xs = o\<^sub>1 # os} \measure_pmf (\ s') = ennreal (pmf (\ s') o\<^sub>1) * T (s', o\<^sub>1) {\ \ space S. \xs. (\\'. \ = xs @- \') \ map snd xs = os}" (is "?L = ?R") for s' proof - have "?L = \\<^sup>+ x. ennreal (pmf (\ s') x) * T (s', x) {\ \ space S. \xs. (\\'. (s', x) ## \ = xs @- \') \ map snd xs = o\<^sub>1 # os} \count_space UNIV" by (rule nn_integral_measure_pmf) also have "\ = \\<^sup>+ o\<^sub>2. (if o\<^sub>2 = o\<^sub>1 then ennreal (pmf (\ s') o\<^sub>1) * T (s', o\<^sub>1) {\ \ space S. L os \} else 0) \count_space UNIV" apply (rule nn_integral_cong_AE [where v = "\ o\<^sub>2. if o\<^sub>2 = o\<^sub>1 then ennreal (pmf (\ s') o\<^sub>1) * T (s', o\<^sub>1) {\ \ space S. L os \} else 0"] ) apply (rule AE_I2) apply (split if_split, safe) subgoal by (auto intro!: arg_cong2[where f = times, OF HOL.refl] arg_cong2[where f = emeasure]; metis list.simps(9) shift.simps(2) snd_conv ) subgoal by (subst arg_cong2[where f = emeasure and d = "{}", OF HOL.refl]) auto done also have "\ = \\<^sup>+o\<^sub>2\{o\<^sub>1}. (ennreal (pmf (\ s') o\<^sub>1) * T (s', o\<^sub>1) {\ \ space S. L os \}) \count_space UNIV" by (rule nn_integral_cong_AE) auto also have "\ = ?R" by simp finally show ?thesis . qed have "?l = \\<^sup>+ t. T t {x \ space S. \xs \'. t ## x = xs @- \' \ map snd xs = o\<^sub>1 # os} \ (K (s, o\<^sub>0))" by (subst emeasure_Collect_T[unfolded space_T], measurable) also have "\ = ?r" using * by (simp add: K_def) finally show ?thesis . qed subsection \Computation of Likelihood\ fun backward where "backward s [] = 1" | "backward s (o # os) = (\\<^sup>+ t. ennreal (pmf (\ t) o) * backward t os \measure_pmf (\ s))" lemma emeasure_T_observation_backward: "emeasure (T (s, o)) {\ \ space S. L os \} = backward s os" using emeasure_T_observation_Cons by (induction os arbitrary: s o; simp) lemma (in HMM) likelihood_backward: "likelihood s os = backward s os" unfolding likelihood_init emeasure_T_observation_backward .. end (* HMM Defs *) context HMM2 begin fun (in HMM2_defs) forward where "forward s t_end [] = indicator {t_end} s" | "forward s t_end (o # os) = (\t \ \. ennreal (pmf (\ t) o) * ennreal (pmf (\ s) t) * forward t t_end os)" lemma forward_split: "forward s t (os1 @ os2) = (\t' \ \. forward s t' os1 * forward t' t os2)" if "s \ \" using that apply (induction os1 arbitrary: s) subgoal for s apply (simp add: sum_indicator_mult[OF states_finite]) apply (subst sum.cong[where B = "{s}"]) by auto subgoal for a os1 s apply simp apply (subst sum_distrib_right) apply (subst sum.swap) apply (simp add: sum_distrib_left algebra_simps) done done lemma (in -) "(\t \ S. f t) = f t" if "finite S" "t \ S" "\ s \ S - {t}. f s = 0" thm sum.empty sum.insert sum.mono_neutral_right[of S "{t}"] apply (subst sum.mono_neutral_right[of S "{t}"]) using that apply auto done (* oops by (metis add.right_neutral empty_iff finite.intros(1) insert_iff subsetI sum.empty sum.insert sum.mono_neutral_right that) using that apply auto *) lemma forward_backward: "(\t \ \. forward s t os) = backward s os" if "s \ \" using \s \ \\ apply (induction os arbitrary: s) subgoal for s by (subst sum.mono_neutral_right[of \ "{s}", OF states_finite]) (auto split: if_split_asm simp: indicator_def) subgoal for a os s apply (simp add: sum.swap sum_distrib_left[symmetric]) apply (subst nn_integral_measure_pmf_support[where A = \]) using states_finite states_closed by (auto simp: algebra_simps) done theorem likelihood_forward: "likelihood s os = (\t \ \. forward s t os)" if \s \ \\ unfolding likelihood_backward forward_backward[symmetric, OF \s \ \\] .. subsection \Definition of Maximum Probabilities\ abbreviation (input) "V os as \ \ (\ \'. \ = zip as os @- \')" definition "max_prob s os = Max {T' (I s) {\ \ space S. \o \'. \ = (s, o) ## zip as os @- \'} | as. length as = length os \ set as \ \}" fun viterbi_prob where "viterbi_prob s t_end [] = indicator {t_end} s" | "viterbi_prob s t_end (o # os) = (MAX t \ \. ennreal (pmf (\ t) o * pmf (\ s) t) * viterbi_prob t t_end os)" definition "is_decoding s os as \ T' (I s) {\ \ space S. \o \'. \ = (s, o) ## zip as os @- \'} = max_prob s os \ length as = length os \ set as \ \" subsection \Iteration Rule For Maximum Probabilities\ lemma emeasure_T_state_Nil: "T (s, o\<^sub>0) {\ \ space S. V [] as \} = 1" by simp lemma max_prob_T_state_Nil: "Max {T (s, o) {\ \ space S. V [] as \} | as. length as = length [] \ set as \ \} = 1" by (simp add: emeasure_T_state_Nil) lemma V_Cons: "V (o # os) (a # as) \ \ fst (shd \) = a \ snd (shd \) = o \ V os as (stl \)" by (cases \) auto lemma measurable_V[measurable]: "Measurable.pred S (\\. V os as \)" proof (induction os as rule: list_induct2') case (4 x xs y ys) then show ?case by (subst V_Cons) (intro Measurable.pred_intros_logic measurable_compose[OF measurable_shd] measurable_compose[OF measurable_stl]; measurable) qed simp+ lemma init_V_measurable[measurable]: "Measurable.pred S (\x. \o \'. x = (s, o) ## zip as os @- \')" (is "Measurable.pred S ?f") proof - have *: "?f \ \ fst (shd \) = s \ V os as (stl \)" for \ by (cases \) auto show ?thesis by (subst *) (intro Measurable.pred_intros_logic measurable_compose[OF measurable_shd]; measurable) qed lemma max_prob_Cons': "Max {T (s, o\<^sub>1) {\ \ space S. V (o # os) as \} | as. length as = length (o # os) \ set as \ \} = ( MAX t \ \. ennreal (pmf (\ t) o * pmf (\ s) t) * (MAX as \ {as. length as = length os \ set as \ \}. T (t, o) {\ \ space S. V os as \}) )" (is "?l = ?r") and T_V_Cons: "T (s, o\<^sub>1) {\ \ space S. V (o # os) (t # as) \} = ennreal (pmf (\ t) o * pmf (\ s) t) * T (t, o) {\ \ space S. V os as \}" (is "?l' = ?r'") if "length as = length os" proof - let ?S = "\ os. {as. length as = length os \ set as \ \}" have S_finite: "finite (?S os)" for os :: "'t list" using finite_lists_length_eq[OF states_finite] by (rule finite_subset[rotated]) auto have S_nonempty: "?S os \ {}" for os :: "'t list" proof - let ?a = "SOME a. a \ \" let ?as = "replicate (length os) ?a" from states_wellformed have "?a \ \" by (auto intro: someI_ex) then have "?as \ ?S os" by auto then show ?thesis by force qed let ?f = "\t as os. T t {\ \ space S. V os as (t ## \)}" let ?g = "\t as os. T t {\ \ space S. V os as \}" have *: "?f t as (o # os) = ?g t (tl as) os * indicator {(hd as, o)} t" if "length as = Suc n" for t as n unfolding indicator_def using that by (cases as) auto have **: "K (s, o\<^sub>1) {(t, o)} = pmf (\ t) o * pmf (\ s) t" for t unfolding K_def apply (simp add: vimage_def) apply (subst arg_cong2[where f = nn_integral and d = "\ x. \ x {xa. xa = o \ x = t} * indicator {t} x", OF HOL.refl]) subgoal by (auto simp: indicator_def) by (simp add: emeasure_pmf_single ennreal_mult') have "?l = (MAX as \ ?S (o # os). \\<^sup>+ t. ?f t as (o # os) \K (s, o\<^sub>1))" by (subst Max_to_image2; subst emeasure_Collect_T[unfolded space_T]; rule measurable_V HOL.refl) also have "\ = (MAX as \ ?S (o # os). \\<^sup>+ t. ?g t (tl as) os * indicator {(hd as,o)} t \K (s,o\<^sub>1))" by (simp cong: Max_image_cong_simp add: *) also have "\ = (MAX(t, as)\ \ \ ?S os. ennreal (pmf (\ t) o * pmf (\ s) t) * ?g (t, o) as os)" proof ((rule Max_eq_image_if; clarsimp?), goal_cases) case 1 from S_finite[of "o # os"] show ?case by simp next case 2 from states_finite show ?case by (blast intro: S_finite) next case (3 as) then show ?case by - (rule bexI[where x = "hd as"]; cases as; auto simp: algebra_simps **) next case (4 x as) then show ?case by - (rule exI[where x = "x # as"], simp add: algebra_simps **) qed also have "\ = ?r" by (subst Max_image_left_mult[symmetric], fact+) (rule sym, rule Max_image_pair, rule states_finite, fact+) finally show "?l = ?r" . have "?l' = \\<^sup>+ t'. ?f t' (t # as) (o # os) \K (s, o\<^sub>1)" by (rule emeasure_Collect_T[unfolded space_T]; rule measurable_V) also from that have "\ = \\<^sup>+ t'. ?g t' as os * indicator {(t,o)} t' \K (s,o\<^sub>1)" by (subst *[of _ "length as"]; simp) also have "\ = ?r'" by (simp add: **, simp only: algebra_simps) finally show "?l' = ?r'" . qed lemmas max_prob_Cons = max_prob_Cons'[OF length_replicate] subsection \Computation of Maximum Probabilities\ lemma T_init_V_eq: "T (s, o) {\ \ space S. V os as \} = T (s, o') {\ \ space S. V os as \}" apply (subst emeasure_Collect_T[unfolded space_T], (measurable; fail)) apply (subst (2) emeasure_Collect_T[unfolded space_T], (measurable; fail)) apply (simp add: K_def) done lemma T'_I_T: "T' (I s) {\ \ space S. \o \'. \ = (s, o) ## zip as os @- \'} = T (s,o) {\ \ space S. V os as \}" proof - have "(\o\\\<^sub>s. T (s, o) {\ \ space S. V os as \}) = of_nat (card \\<^sub>s) * T (s, o) {\ \ space S. V os as \}" for as by (subst sum_constant[symmetric]) (fastforce intro: sum.cong T_init_V_eq[simplified]) then show ?thesis unfolding max_prob_def apply (subst emeasure_T') subgoal by measurable apply (simp add: I_def in_S observations_finite observations_wellformed nn_integral_pmf_of_set) apply (subst mult.commute) apply (simp add: observations_finite observations_wellformed mult_divide_eq_ennreal) done qed lemma max_prob_init: "max_prob s os = Max {T (s,o) {\ \ space S. V os as \} | as. length as = length os \ set as \ \}" unfolding max_prob_def by (simp add: T'_I_T[symmetric]) lemma max_prob_Nil[simp]: "max_prob s [] = 1" unfolding max_prob_init[where o = obs] by auto lemma Max_start: "(MAX t\\. (indicator {t} s :: ennreal)) = 1" if "s \ \" using states_finite that by (auto simp: indicator_def intro: Max_eqI) lemma Max_V_viterbi: "(MAX t \ \. viterbi_prob s t os) = Max {T (s, o) {\ \ space S. V os as \} | as. length as = length os \ set as \ \}" if "s \ \" using that states_finite states_wellformed by (induction os arbitrary: s o; simp add: Max_start max_prob_Cons[simplified] Max_image_commute Max_image_left_mult Max_to_image2 cong: Max_image_cong ) lemma max_prob_viterbi: "(MAX t \ \. viterbi_prob s t os) = max_prob s os" if "s \ \" using max_prob_init[of s os] Max_V_viterbi[OF \s \ \\, symmetric] by simp end subsection \Decoding the Most Probable Hidden State Sequence\ context HMM3 begin fun viterbi where "viterbi s t_end [] = ([], indicator {t_end} s)" | "viterbi s t_end (o # os) = fst ( argmax snd (map (\t. let (xs, v) = viterbi t t_end os in (t # xs, ennreal (pmf (\ t) o * pmf (\ s) t) * v)) state_list))" lemma state_list_nonempty: "state_list \ []" using state_list_\ states_wellformed by auto lemma viterbi_viterbi_prob: "snd (viterbi s t_end os) = viterbi_prob s t_end os" proof (induction os arbitrary: s) case Nil then show ?case by simp next case (Cons o os) let ?f = "\t. let (xs, v) = viterbi t t_end os in (t # xs, ennreal (pmf (\ t) o * pmf (\ s) t) * v)" let ?xs = "map ?f state_list" from state_list_nonempty have "map ?f state_list \ []" by simp from argmax(2,3)[OF this, of snd] have *: "snd (fst (argmax snd ?xs)) = snd (argmax snd ?xs)" "snd (argmax snd ?xs) = (MAX x \ set ?xs. snd x)" . then show ?case apply (simp add: state_list_\) apply (rule Max_eq_image_if) apply (intro finite_imageI states_finite; fail) apply (intro finite_imageI states_finite; fail) subgoal apply clarsimp subgoal for x using Cons.IH[of x] by (auto split: prod.splits) done apply clarsimp subgoal for x using Cons.IH[of x] by (force split: prod.splits) done qed context begin private fun val_of where "val_of s [] [] = 1" | "val_of s (t # xs) (o # os) = ennreal (pmf (\ t) o * pmf (\ s) t) * val_of t xs os" lemma val_of_T: "val_of s as os = T (s, o\<^sub>1) {\ \ space S. V os as \}" if "length as = length os" using that by (induction arbitrary: o\<^sub>1 rule: val_of.induct; (subst T_V_Cons)?; simp) lemma viterbi_sequence: "snd (viterbi s t_end os) = val_of s (fst (viterbi s t_end os)) os" if "snd (viterbi s t_end os) > 0" using that proof (induction os arbitrary: s) case Nil then show ?case - by (simp add: indicator_def split: if_split_asm) + by (simp add: indicator_def split: if_split_asm split_of_bool_asm) next case (Cons o os s) let ?xs = "map (\t. let (xs, v) = viterbi t t_end os in (t # xs, ennreal (pmf (\ t) o * pmf (\ s) t) * v)) state_list" from state_list_nonempty have "?xs \ []" by simp from argmax(1)[OF this, of snd] obtain t where "t \ set state_list" "fst (argmax snd ?xs) = (t # fst (viterbi t t_end os), ennreal (pmf (\ t) o * pmf (\ s) t) * snd (viterbi t t_end os))" by (auto split: prod.splits) with Cons show ?case by (auto simp: ennreal_zero_less_mult_iff) qed lemma viterbi_valid_path: "length as = length os \ set as \ \" if "viterbi s t_end os = (as, v)" using that proof (induction os arbitrary: s as v) case Nil then show ?case by simp next case (Cons o os s as v) let ?xs = "map (\t. let (xs, v) = viterbi t t_end os in (t # xs, ennreal (pmf (\ t) o * pmf (\ s) t) * v)) state_list" from state_list_nonempty have "?xs \ []" by simp from argmax(1)[OF this, of snd] obtain t where "t \ \" "fst (argmax snd ?xs) = (t # fst (viterbi t t_end os), ennreal (pmf (\ t) o * pmf (\ s) t) * snd (viterbi t t_end os))" by (auto simp: state_list_\ split: prod.splits) with Cons.prems show ?case by (cases "viterbi t t_end os"; simp add: Cons.IH) qed definition "viterbi_final s os = fst (argmax snd (map (\ t. viterbi s t os) state_list))" lemma viterbi_finalE: obtains t where "t \ \" "viterbi_final s os = viterbi s t os" "snd (viterbi s t os) = Max ((\t. snd (viterbi s t os)) ` \)" proof - from state_list_nonempty have "map (\ t. viterbi s t os) state_list \ []" by simp from argmax[OF this, of snd] show ?thesis by (auto simp: state_list_\ image_comp comp_def viterbi_final_def intro: that) qed theorem viterbi_final_max_prob: assumes "viterbi_final s os = (as, v)" "s \ \" shows "v = max_prob s os" proof - obtain t where "t \ \" "viterbi_final s os = viterbi s t os" "snd (viterbi s t os) = Max ((\t. snd (viterbi s t os)) ` \)" by (rule viterbi_finalE) with assms show ?thesis by (simp add: viterbi_viterbi_prob max_prob_viterbi) qed theorem viterbi_final_is_decoding: assumes "viterbi_final s os = (as, v)" "v > 0" "s \ \" shows "is_decoding s os as" proof - from viterbi_valid_path[of s _ os as v] assms have as: "length as = length os" "set as \ \" by - (rule viterbi_finalE[of s os]; simp)+ obtain t where "t \ \" "viterbi_final s os = viterbi s t os" by (rule viterbi_finalE) with assms viterbi_sequence[of s t os] have "val_of s as os = v" by (cases "viterbi s t os") (auto simp: snd_def split!: prod.splits) with val_of_T as have "max_prob s os = T (s, obs) {\ \ space S. V os as \}" by (simp add: viterbi_final_max_prob[OF assms(1,3)]) with as show ?thesis unfolding is_decoding_def by (simp only: T'_I_T) qed end (* Anonymous context *) end (* HMM 3 *) end (* Theory *) \ No newline at end of file diff --git a/thys/Native_Word/Code_Target_Word_Base.thy b/thys/Native_Word/Code_Target_Word_Base.thy --- a/thys/Native_Word/Code_Target_Word_Base.thy +++ b/thys/Native_Word/Code_Target_Word_Base.thy @@ -1,425 +1,426 @@ (* Title: Code_Target_Word_Base.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Common base for target language implementations of word types\ theory Code_Target_Word_Base imports "HOL-Library.Word" "Word_Lib.Signed_Division_Word" Bits_Integer begin text \More lemmas\ lemma div_half_nat: fixes x y :: nat assumes "y \ 0" shows "(x div y, x mod y) = (let q = 2 * (x div 2 div y); r = x - q * y in if y \ r then (q + 1, r - y) else (q, r))" proof - let ?q = "2 * (x div 2 div y)" have q: "?q = x div y - x div y mod 2" by(metis div_mult2_eq mult.commute minus_mod_eq_mult_div [symmetric]) let ?r = "x - ?q * y" have r: "?r = x mod y + x div y mod 2 * y" by(simp add: q diff_mult_distrib minus_mod_eq_div_mult [symmetric])(metis diff_diff_cancel mod_less_eq_dividend mod_mult2_eq add.commute mult.commute) show ?thesis proof(cases "y \ x - ?q * y") case True with assms q have "x div y mod 2 \ 0" unfolding r by (metis Nat.add_0_right diff_0_eq_0 diff_Suc_1 le_div_geq mod2_gr_0 mod_div_trivial mult_0 neq0_conv numeral_1_eq_Suc_0 numerals(1)) hence "x div y = ?q + 1" unfolding q by simp moreover hence "x mod y = ?r - y" by simp(metis minus_div_mult_eq_mod [symmetric] diff_commute diff_diff_left mult_Suc) ultimately show ?thesis using True by(simp add: Let_def) next case False hence "x div y mod 2 = 0" unfolding r by(simp add: not_le)(metis Nat.add_0_right assms div_less div_mult_self2 mod_div_trivial mult.commute) hence "x div y = ?q" unfolding q by simp moreover hence "x mod y = ?r" by (metis minus_div_mult_eq_mod [symmetric]) ultimately show ?thesis using False by(simp add: Let_def) qed qed lemma div_half_word: fixes x y :: "'a :: len word" assumes "y \ 0" shows "(x div y, x mod y) = (let q = push_bit 1 (drop_bit 1 x div y); r = x - q * y in if y \ r then (q + 1, r - y) else (q, r))" proof - obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat x\]) simp_all moreover obtain m where m: "y = of_nat m" "m < 2 ^ LENGTH('a)" by (rule that [of \unat y\]) simp_all ultimately have [simp]: \unat (of_nat n :: 'a word) = n\ \unat (of_nat m :: 'a word) = m\ by (transfer, simp add: take_bit_of_nat take_bit_nat_eq_self_iff)+ let ?q = "push_bit 1 (drop_bit 1 x div y)" let ?q' = "2 * (n div 2 div m)" have "n div 2 div m < 2 ^ LENGTH('a)" using n by (metis of_nat_inverse unat_lt2p uno_simps(2)) hence q: "?q = of_nat ?q'" using n m by (auto simp add: drop_bit_eq_div word_arith_nat_div uno_simps take_bit_nat_eq_self unsigned_of_nat) from assms have "m \ 0" using m by -(rule notI, simp) from n have "2 * (n div 2 div m) < 2 ^ LENGTH('a)" by(metis mult.commute div_mult2_eq minus_mod_eq_mult_div [symmetric] less_imp_diff_less of_nat_inverse unat_lt2p uno_simps(2)) moreover have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric] by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq) moreover have "2 * (n div 2 div m) * m \ n" by (simp flip: div_mult2_eq ac_simps) ultimately have r: "x - ?q * y = of_nat (n - ?q' * m)" and "y \ x - ?q * y \ of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)" using n m unfolding q apply (simp_all add: of_nat_diff) apply (subst of_nat_diff) - apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths unsigned_of_nat) + apply (cases \LENGTH('a) \ 2\) + apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths unsigned_of_nat) done then show ?thesis using n m div_half_nat [OF \m \ 0\, of n] unfolding q by (simp add: word_le_nat_alt word_div_def word_mod_def Let_def take_bit_nat_eq_self unsigned_of_nat flip: zdiv_int zmod_int split del: if_split split: if_split_asm) qed lemma word_test_bit_set_bits: "bit (BITS n. f n :: 'a :: len word) n \ n < LENGTH('a) \ f n" by (fact bit_set_bits_word_iff) lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. bit i n)" by (rule word_eqI) (auto simp add: word_test_bit_set_bits bit_simps) context includes bit_operations_syntax begin lemma word_and_mask_or_conv_and_mask: "bit n index \ (n AND mask index) OR (push_bit index 1) = n AND mask (index + 1)" for n :: \'a::len word\ by(rule word_eqI)(auto simp add: bit_simps) lemma uint_and_mask_or_full: fixes n :: "'a :: len word" assumes "bit n (LENGTH('a) - 1)" and "mask1 = mask (LENGTH('a) - 1)" and "mask2 = push_bit (LENGTH('a) - 1) 1" shows "uint (n AND mask1) OR mask2 = uint n" proof - have "mask2 = uint (push_bit (LENGTH('a) - 1) 1 :: 'a word)" using assms by transfer (simp add: take_bit_push_bit) hence "uint (n AND mask1) OR mask2 = uint (n AND mask1 OR (push_bit (LENGTH('a) - 1) 1 :: 'a word))" by(simp add: uint_or) also have "\ = uint (n AND mask (LENGTH('a) - 1 + 1))" using assms by(simp only: word_and_mask_or_conv_and_mask) also have "\ = uint n" by simp finally show ?thesis . qed end text \Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.\ lemmas word_sdiv_def = sdiv_word_def lemmas word_smod_def = smod_word_def lemma [code]: "x sdiv y = (let x' = sint x; y' = sint y; negative = (x' < 0) \ (y' < 0); result = abs x' div abs y' in word_of_int (if negative then -result else result))" for x y :: \'a::len word\ by (simp add: sdiv_word_def signed_divide_int_def sgn_if Let_def not_less not_le) lemma [code]: "x smod y = (let x' = sint x; y' = sint y; negative = (x' < 0); result = abs x' mod abs y' in word_of_int (if negative then -result else result))" for x y :: \'a::len word\ proof - have *: \k mod l = k - k div l * l\ for k l :: int by (simp add: minus_div_mult_eq_mod) show ?thesis by (simp add: smod_word_def signed_modulo_int_def signed_divide_int_def * sgn_if Let_def) qed text \ This algorithm implements unsigned division in terms of signed division. Taken from Hacker's Delight. \ lemma divmod_via_sdivmod: fixes x y :: "'a :: len word" assumes "y \ 0" shows "(x div y, x mod y) = (if push_bit (LENGTH('a) - 1) 1 \ y then if x < y then (0, x) else (1, x - y) else let q = (push_bit 1 (drop_bit 1 x sdiv y)); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" proof(cases "push_bit (LENGTH('a) - 1) 1 \ y") case True note y = this show ?thesis proof(cases "x < y") case True then have "x mod y = x" by transfer simp thus ?thesis using True y by(simp add: word_div_lt_eq_0) next case False obtain n where n: "y = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat y\]) simp_all have "unat x < 2 ^ LENGTH('a)" by(rule unat_lt2p) also have "\ = 2 * 2 ^ (LENGTH('a) - 1)" by(metis Suc_pred len_gt_0 power_Suc One_nat_def) also have "\ \ 2 * n" using y n by transfer (simp add: push_bit_of_1 take_bit_eq_mod) finally have div: "x div of_nat n = 1" using False n by (simp add: word_div_eq_1_iff take_bit_nat_eq_self unsigned_of_nat) moreover have "x mod y = x - x div y * y" by (simp add: minus_div_mult_eq_mod) with div n have "x mod y = x - y" by simp ultimately show ?thesis using False y n by simp qed next case False note y = this obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat x\]) simp_all hence "int n div 2 + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)" by (cases \LENGTH('a)\) (auto dest: less_imp_of_nat_less [where ?'a = int]) with y n have "sint (drop_bit 1 x) = uint (drop_bit 1 x)" by (cases \LENGTH('a)\) (auto simp add: sint_uint drop_bit_eq_div take_bit_nat_eq_self uint_div_distrib signed_take_bit_int_eq_self_iff unsigned_of_nat) moreover have "uint y + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)" using y by (cases \LENGTH('a)\) (simp_all add: not_le push_bit_of_1 word_less_alt uint_power_lower) then have "sint y = uint y" apply (cases \LENGTH('a)\) apply (auto simp add: sint_uint signed_take_bit_int_eq_self_iff) using uint_ge_0 [of y] by linarith ultimately show ?thesis using y apply (subst div_half_word [OF assms]) apply (simp add: sdiv_word_def signed_divide_int_def flip: uint_div) done qed text \More implementations tailored towards target-language implementations\ context includes integer.lifting begin lift_definition word_of_integer :: "integer \ 'a :: len word" is word_of_int . lemma word_of_integer_code [code]: "word_of_integer n = word_of_int (int_of_integer n)" by(simp add: word_of_integer.rep_eq) end context includes bit_operations_syntax begin lemma word_of_int_code: "uint (word_of_int x :: 'a word) = x AND mask (LENGTH('a :: len))" by (simp add: unsigned_of_int take_bit_eq_mask) context fixes f :: "nat \ bool" begin definition set_bits_aux :: \nat \ 'a word \ 'a::len word\ where \set_bits_aux n w = push_bit n w OR take_bit n (set_bits f)\ lemma bit_set_bit_aux [bit_simps]: \bit (set_bits_aux n w) m \ m < LENGTH('a) \ (if m < n then f m else bit w (m - n))\ for w :: \'a::len word\ by (auto simp add: bit_simps set_bits_aux_def) corollary set_bits_conv_set_bits_aux: \set_bits f = (set_bits_aux LENGTH('a) 0 :: 'a :: len word)\ by (rule bit_word_eqI) (simp add: bit_simps) lemma set_bits_aux_0 [simp]: \set_bits_aux 0 w = w\ by (simp add: set_bits_aux_def) lemma set_bits_aux_Suc [simp]: \set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\ by (rule bit_word_eqI) (auto simp add: bit_simps le_less_Suc_eq mult.commute [of _ 2]) lemma set_bits_aux_simps [code]: \set_bits_aux 0 w = w\ \set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\ by simp_all lemma set_bits_aux_rec: \set_bits_aux n w = (if n = 0 then w else let n' = n - 1 in set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))\ by (cases n) simp_all end lemma word_of_int_via_signed: fixes mask assumes mask_def: "mask = Bit_Operations.mask (LENGTH('a))" and shift_def: "shift = push_bit LENGTH('a) 1" and index_def: "index = LENGTH('a) - 1" and overflow_def:"overflow = push_bit (LENGTH('a) - 1) 1" and least_def: "least = - overflow" shows "(word_of_int i :: 'a :: len word) = (let i' = i AND mask in if bit i' index then if i' - shift < least \ overflow \ i' - shift then arbitrary1 i' else word_of_int (i' - shift) else if i' < least \ overflow \ i' then arbitrary2 i' else word_of_int i')" proof - define i' where "i' = i AND mask" have "shift = mask + 1" unfolding assms by (simp add: mask_eq_exp_minus_1 push_bit_of_1) hence "i' < shift" by (simp add: mask_def i'_def) show ?thesis proof(cases "bit i' index") case True then have unf: "i' = overflow OR i'" apply (simp add: assms i'_def push_bit_of_1 flip: take_bit_eq_mask) apply (rule bit_eqI) apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff) done have \overflow \ overflow OR i'\ by (simp add: i'_def mask_def or_greater_eq) then have "overflow \ i'" by (subst unf) hence "i' - shift < least \ False" unfolding assms by(cases "LENGTH('a)")(simp_all add: not_less push_bit_of_1) moreover have "overflow \ i' - shift \ False" using \i' < shift\ unfolding assms by(cases "LENGTH('a)")(auto simp add: not_le push_bit_of_1 elim: less_le_trans) moreover have "word_of_int (i' - shift) = (word_of_int i :: 'a word)" using \i' < shift\ by (simp add: i'_def shift_def mask_def push_bit_of_1 word_of_int_eq_iff flip: take_bit_eq_mask) ultimately show ?thesis using True by(simp add: Let_def i'_def) next case False have "i' = i AND Bit_Operations.mask (LENGTH('a) - 1)" apply (rule bit_eqI) apply (use False in \auto simp add: bit_simps assms i'_def\) apply (auto simp add: less_le) done also have "\ \ Bit_Operations.mask (LENGTH('a) - 1)" using AND_upper2 mask_nonnegative_int by blast also have "\ < overflow" by (simp add: mask_int_def push_bit_of_1 overflow_def) also have "least \ 0" unfolding least_def overflow_def by simp have "0 \ i'" by (simp add: i'_def mask_def) hence "least \ i'" using \least \ 0\ by simp moreover have "word_of_int i' = (word_of_int i :: 'a word)" by (simp add: i'_def mask_def of_int_and_eq of_int_mask_eq) ultimately show ?thesis using False by(simp add: Let_def i'_def) qed qed end text \Quickcheck conversion functions\ context includes state_combinator_syntax begin definition qc_random_cnv :: "(natural \ 'a::term_of) \ natural \ Random.seed \ ('a \ (unit \ Code_Evaluation.term)) \ Random.seed" where "qc_random_cnv a_of_natural i = Random.range (i + 1) \\ (\k. Pair ( let n = a_of_natural k in (n, \_. Code_Evaluation.term_of n)))" end definition qc_exhaustive_cnv :: "(natural \ 'a) \ ('a \ (bool \ term list) option) \ natural \ (bool \ term list) option" where "qc_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.exhaustive (%x. f (a_of_natural x)) d" definition qc_full_exhaustive_cnv :: "(natural \ ('a::term_of)) \ ('a \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option" where "qc_full_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.full_exhaustive (%(x, xt). f (a_of_natural x, %_. Code_Evaluation.term_of (a_of_natural x))) d" declare [[quickcheck_narrowing_ghc_options = "-XTypeSynonymInstances"]] definition qc_narrowing_drawn_from :: "'a list \ integer \ _" where "qc_narrowing_drawn_from xs = foldr Quickcheck_Narrowing.sum (map Quickcheck_Narrowing.cons (butlast xs)) (Quickcheck_Narrowing.cons (last xs))" locale quickcheck_narrowing_samples = fixes a_of_integer :: "integer \ 'a \ 'a :: {partial_term_of, term_of}" and zero :: "'a" and tr :: "typerep" begin function narrowing_samples :: "integer \ 'a list" where "narrowing_samples i = (if i > 0 then let (a, a') = a_of_integer i in narrowing_samples (i - 1) @ [a, a'] else [zero])" by pat_completeness auto termination including integer.lifting proof(relation "measure nat_of_integer") fix i :: integer assume "0 < i" thus "(i - 1, i) \ measure nat_of_integer" by simp(transfer, simp) qed simp definition partial_term_of_sample :: "integer \ 'a" where "partial_term_of_sample i = (if i < 0 then undefined else if i = 0 then zero else if i mod 2 = 0 then snd (a_of_integer (i div 2)) else fst (a_of_integer (i div 2 + 1)))" lemma partial_term_of_code: "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_variable p t) \ Code_Evaluation.Free (STR ''_'') tr" "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_constructor i []) \ Code_Evaluation.term_of (partial_term_of_sample i)" by (rule partial_term_of_anything)+ end lemmas [code] = quickcheck_narrowing_samples.narrowing_samples.simps quickcheck_narrowing_samples.partial_term_of_sample_def text \ The separate code target \SML_word\ collects setups for the code generator that PolyML does not provide. \ setup \Code_Target.add_derived_target ("SML_word", [(Code_ML.target_SML, I)])\ code_identifier code_module Code_Target_Word_Base \ (SML) Word and (Haskell) Word and (OCaml) Word and (Scala) Word end diff --git a/thys/Stirling_Formula/Gamma_Asymptotics.thy b/thys/Stirling_Formula/Gamma_Asymptotics.thy --- a/thys/Stirling_Formula/Gamma_Asymptotics.thy +++ b/thys/Stirling_Formula/Gamma_Asymptotics.thy @@ -1,1893 +1,1893 @@ (* File: Gamma_Asymptotics.thy Author: Manuel Eberl The complete asymptotics of the real and complex logarithmic Gamma functions. Also of the real Polygamma functions (could be extended to the complex ones fairly easily if needed). *) section \Complete asymptotics of the logarithmic Gamma function\ theory Gamma_Asymptotics imports "HOL-Complex_Analysis.Complex_Analysis" "HOL-Real_Asymp.Real_Asymp" Bernoulli.Bernoulli_FPS Bernoulli.Periodic_Bernpoly Stirling_Formula begin subsection \Auxiliary Facts\ (* TODO: could be automated with Laurent series expansions in the future *) lemma stirling_limit_aux1: "((\y. Ln (1 + z * of_real y) / of_real y) \ z) (at_right 0)" for z :: complex proof (cases "z = 0") case True then show ?thesis by simp next case False have "((\y. ln (1 + z * of_real y)) has_vector_derivative 1 * z) (at 0)" by (rule has_vector_derivative_real_field) (auto intro!: derivative_eq_intros) then have "(\y. (Ln (1 + z * of_real y) - of_real y * z) / of_real \y\) \0\ 0" by (auto simp add: has_vector_derivative_def has_derivative_def netlimit_at scaleR_conv_of_real field_simps) then have "((\y. (Ln (1 + z * of_real y) - of_real y * z) / of_real \y\) \ 0) (at_right 0)" by (rule filterlim_mono[OF _ _ at_le]) simp_all also have "?this \ ((\y. Ln (1 + z * of_real y) / (of_real y) - z) \ 0) (at_right 0)" using eventually_at_right_less[of "0::real"] by (intro filterlim_cong refl) (auto elim!: eventually_mono simp: field_simps) finally show ?thesis by (simp only: LIM_zero_iff) qed lemma stirling_limit_aux2: "((\y. y * Ln (1 + z / of_real y)) \ z) at_top" for z :: complex using stirling_limit_aux1[of z] by (subst filterlim_at_top_to_right) (simp add: field_simps) lemma Union_atLeastAtMost: assumes "N > 0" shows "(\n\{0.. {0..real N}" thus "x \ (\n\{0.. 0" "x < real N" by simp_all hence "x \ real (nat \x\)" "x \ real (nat \x\ + 1)" by linarith+ moreover from x have "nat \x\ < N" by linarith ultimately have "\n\{0.. {real n..real (n + 1)}" by (intro bexI[of _ "nat \x\"]) simp_all thus ?thesis by blast qed qed auto subsection \Cones in the complex plane\ definition complex_cone :: "real \ real \ complex set" where "complex_cone a b = {z. \y\{a..b}. z = rcis (norm z) y}" abbreviation complex_cone' :: "real \ complex set" where "complex_cone' a \ complex_cone (-a) a" lemma zero_in_complex_cone [simp, intro]: "a \ b \ 0 \ complex_cone a b" by (auto simp: complex_cone_def) lemma complex_coneE: assumes "z \ complex_cone a b" obtains r \ where "r \ 0" "\ \ {a..b}" "z = rcis r \" proof - from assms obtain y where "y \ {a..b}" "z = rcis (norm z) y" unfolding complex_cone_def by auto thus ?thesis using that[of "norm z" y] by auto qed lemma arg_cis [simp]: assumes "x \ {-pi<..pi}" shows "Arg (cis x) = x" using assms by (intro cis_Arg_unique) auto lemma arg_mult_of_real_left [simp]: assumes "r > 0" shows "Arg (of_real r * z) = Arg z" proof (cases "z = 0") case False thus ?thesis using Arg_bounded[of z] assms by (intro cis_Arg_unique) (auto simp: sgn_mult sgn_of_real cis_Arg) qed auto lemma arg_mult_of_real_right [simp]: assumes "r > 0" shows "Arg (z * of_real r) = Arg z" by (subst mult.commute, subst arg_mult_of_real_left) (simp_all add: assms) lemma arg_rcis [simp]: assumes "x \ {-pi<..pi}" "r > 0" shows "Arg (rcis r x) = x" using assms by (simp add: rcis_def) lemma rcis_in_complex_cone [intro]: assumes "\ \ {a..b}" "r \ 0" shows "rcis r \ \ complex_cone a b" using assms by (auto simp: complex_cone_def) lemma arg_imp_in_complex_cone: assumes "Arg z \ {a..b}" shows "z \ complex_cone a b" proof - have "z = rcis (norm z) (Arg z)" by (simp add: rcis_cmod_Arg) also have "\ \ complex_cone a b" using assms by auto finally show ?thesis . qed lemma complex_cone_altdef: assumes "-pi < a" "a \ b" "b \ pi" shows "complex_cone a b = insert 0 {z. Arg z \ {a..b}}" proof (intro equalityI subsetI) fix z assume "z \ complex_cone a b" then obtain r \ where *: "r \ 0" "\ \ {a..b}" "z = rcis r \" by (auto elim: complex_coneE) have "Arg z \ {a..b}" if [simp]: "z \ 0" proof - have "r > 0" using that * by (subst (asm) *) auto hence "\ \ {a..b}" using *(1,2) assms by (auto simp: *(1)) moreover from assms *(2) have "\ \ {-pi<..pi}" by auto ultimately show ?thesis using *(3) \r > 0\ by (subst *) auto qed thus "z \ insert 0 {z. Arg z \ {a..b}}" by auto qed (use assms in \auto intro: arg_imp_in_complex_cone\) lemma nonneg_of_real_in_complex_cone [simp, intro]: assumes "x \ 0" "a \ 0" "0 \ b" shows "of_real x \ complex_cone a b" proof - from assms have "rcis x 0 \ complex_cone a b" by (intro rcis_in_complex_cone) auto thus ?thesis by simp qed lemma one_in_complex_cone [simp, intro]: "a \ 0 \ 0 \ b \ 1 \ complex_cone a b" using nonneg_of_real_in_complex_cone[of 1] by (simp del: nonneg_of_real_in_complex_cone) lemma of_nat_in_complex_cone [simp, intro]: "a \ 0 \ 0 \ b \ of_nat n \ complex_cone a b" using nonneg_of_real_in_complex_cone[of "real n"] by (simp del: nonneg_of_real_in_complex_cone) subsection \Another integral representation of the Beta function\ lemma complex_cone_inter_nonpos_Reals: assumes "-pi < a" "a \ b" "b < pi" shows "complex_cone a b \ \\<^sub>\\<^sub>0 = {0}" proof (safe elim!: nonpos_Reals_cases) fix x :: real assume "complex_of_real x \ complex_cone a b" "x \ 0" hence "\(x < 0)" using assms by (intro notI) (auto simp: complex_cone_altdef) with \x \ 0\ show "complex_of_real x = 0" by auto qed (use assms in auto) theorem assumes a: "a > 0" and b: "b > (0 :: real)" shows has_integral_Beta_real': "((\u. u powr (b - 1) / (1 + u) powr (a + b)) has_integral Beta a b) {0<..}" and Beta_conv_nn_integral: "Beta a b = (\\<^sup>+u. ennreal (indicator {0<..} u * u powr (b - 1) / (1 + u) powr (a + b)) \lborel)" proof - define I where "I = (\\<^sup>+u. ennreal (indicator {0<..} u * u powr (b - 1) / (1 + u) powr (a + b)) \lborel)" have "Gamma (a + b) > 0" "Beta a b > 0" using assms by (simp_all add: add_pos_pos Beta_def) from a b have "ennreal (Gamma a * Gamma b) = (\\<^sup>+ t. ennreal (indicator {0..} t * t powr (a - 1) / exp t) \lborel) * (\\<^sup>+ t. ennreal (indicator {0..} t * t powr (b - 1) / exp t) \lborel)" by (subst ennreal_mult') (simp_all add: Gamma_conv_nn_integral_real) also have "\ = (\\<^sup>+t. \\<^sup>+u. ennreal (indicator {0..} t * t powr (a - 1) / exp t) * ennreal (indicator {0..} u * u powr (b - 1) / exp u) \lborel \lborel)" by (simp add: nn_integral_cmult nn_integral_multc) also have "\ = (\\<^sup>+t. indicator {0<..} t * (\\<^sup>+u. indicator {0..} u * t powr (a - 1) * u powr (b - 1) / exp (t + u) \lborel) \lborel)" by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def divide_ennreal ennreal_mult' [symmetric] exp_add mult_ac) also have "\ = (\\<^sup>+t. indicator {0<..} t * (\\<^sup>+u. indicator {0..} u * t powr (a - 1) * u powr (b - 1) / exp (t + u) \(density (distr lborel borel ((*) t)) (\x. ennreal \t\))) \lborel)" by (intro nn_integral_cong mult_indicator_cong, subst lborel_distr_mult' [symmetric]) auto also have "\ = (\\<^sup>+(t::real). indicator {0<..} t * (\\<^sup>+u. indicator {0..} (u * t) * t powr a * (u * t) powr (b - 1) / exp (t + t * u) \lborel) \lborel)" by (intro nn_integral_cong mult_indicator_cong) (auto simp: nn_integral_density nn_integral_distr algebra_simps powr_diff simp flip: ennreal_mult) also have "\ = (\\<^sup>+(t::real). \\<^sup>+u. indicator ({0<..}\{0..}) (t, u) * t powr a * (u * t) powr (b - 1) / exp (t * (u + 1)) \lborel \lborel)" by (subst nn_integral_cmult [symmetric], simp, intro nn_integral_cong) (auto simp: indicator_def zero_le_mult_iff algebra_simps) also have "\ = (\\<^sup>+(t::real). \\<^sup>+u. indicator ({0<..}\{0..}) (t, u) * t powr (a + b - 1) * u powr (b - 1) / exp (t * (u + 1)) \lborel \lborel)" by (intro nn_integral_cong) (auto simp: powr_add powr_diff indicator_def powr_mult field_simps) also have "\ = (\\<^sup>+(u::real). \\<^sup>+t. indicator ({0<..}\{0..}) (t, u) * t powr (a + b - 1) * u powr (b - 1) / exp (t * (u + 1)) \lborel \lborel)" by (rule lborel_pair.Fubini') auto also have "\ = (\\<^sup>+(u::real). indicator {0..} u * (\\<^sup>+t. indicator {0<..} t * t powr (a + b - 1) * u powr (b - 1) / exp (t * (u + 1)) \lborel) \lborel)" by (intro nn_integral_cong mult_indicator_cong) (auto simp: indicator_def) also have "\ = (\\<^sup>+(u::real). indicator {0<..} u * (\\<^sup>+t. indicator {0<..} t * t powr (a + b - 1) * u powr (b - 1) / exp (t * (u + 1)) \lborel) \lborel)" by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) (auto simp: indicator_def) also have "\ = (\\<^sup>+(u::real). indicator {0<..} u * (\\<^sup>+t. indicator {0<..} t * t powr (a + b - 1) * u powr (b - 1) / exp (t * (u + 1)) \(density (distr lborel borel ((*) (1/(1+u)))) (\x. ennreal \1/(1+u)\))) \lborel)" by (intro nn_integral_cong mult_indicator_cong, subst lborel_distr_mult' [symmetric]) auto also have "\ = (\\<^sup>+(u::real). indicator {0<..} u * (\\<^sup>+t. ennreal (1 / (u + 1)) * ennreal (indicator {0<..} (t / (u + 1)) * (t / (1+u)) powr (a + b - 1) * u powr (b - 1) / exp t) \lborel) \lborel)" by (intro nn_integral_cong mult_indicator_cong) (auto simp: nn_integral_distr nn_integral_density add_ac) also have "\ = (\\<^sup>+u. \\<^sup>+t. indicator ({0<..}\{0<..}) (u, t) * 1/(u+1) * (t / (u+1)) powr (a + b - 1) * u powr (b - 1) / exp t \lborel \lborel)" by (subst nn_integral_cmult [symmetric], simp, intro nn_integral_cong) (auto simp: indicator_def field_simps divide_ennreal simp flip: ennreal_mult ennreal_mult') also have "\ = (\\<^sup>+u. \\<^sup>+t. ennreal (indicator {0<..} u * u powr (b - 1) / (1 + u) powr (a + b)) * ennreal (indicator {0<..} t * t powr (a + b - 1) / exp t) \lborel \lborel)" by (intro nn_integral_cong) (auto simp: indicator_def powr_add powr_diff powr_divide powr_minus divide_simps add_ac simp flip: ennreal_mult) also have "\ = I * (\\<^sup>+t. indicator {0<..} t * t powr (a + b - 1) / exp t \lborel)" by (simp add: nn_integral_cmult nn_integral_multc I_def) also have "(\\<^sup>+t. indicator {0<..} t * t powr (a + b - 1) / exp t \lborel) = ennreal (Gamma (a + b))" using assms by (subst Gamma_conv_nn_integral_real) (auto intro!: nn_integral_cong_AE[OF AE_I[of _ _ "{0}"]] - simp: indicator_def split: if_splits) + simp: indicator_def split: if_splits split_of_bool_asm) finally have "ennreal (Gamma a * Gamma b) = I * ennreal (Gamma (a + b))" . hence "ennreal (Gamma a * Gamma b) / ennreal (Gamma (a + b)) = I * ennreal (Gamma (a + b)) / ennreal (Gamma (a + b))" by simp also have "\ = I" using \Gamma (a + b) > 0\ by (intro ennreal_mult_divide_eq) (auto simp: ) also have "ennreal (Gamma a * Gamma b) / ennreal (Gamma (a + b)) = ennreal (Gamma a * Gamma b / Gamma (a + b))" using assms by (intro divide_ennreal) auto also have "\ = ennreal (Beta a b)" by (simp add: Beta_def) finally show *: "ennreal (Beta a b) = I" . define f where "f = (\u. u powr (b - 1) / (1 + u) powr (a + b))" have "((\u. indicator {0<..} u * f u) has_integral Beta a b) UNIV" using * \Beta a b > 0\ by (subst has_integral_iff_nn_integral_lebesgue) (auto simp: f_def measurable_completion nn_integral_completion I_def mult_ac) also have "(\u. indicator {0<..} u * f u) = (\u. if u \ {0<..} then f u else 0)" by (auto simp: fun_eq_iff) also have "(\ has_integral Beta a b) UNIV \ (f has_integral Beta a b) {0<..}" by (rule has_integral_restrict_UNIV) finally show \ by (simp add: f_def) qed lemma has_integral_Beta2: fixes a :: real assumes "a < -1/2" shows "((\x. (1 + x ^ 2) powr a) has_integral Beta (- a - 1 / 2) (1 / 2) / 2) {0<..}" proof - define f where "f = (\u. u powr (-1/2) / (1 + u) powr (-a))" define C where "C = Beta (-a-1/2) (1/2)" have I: "(f has_integral C) {0<..}" using has_integral_Beta_real'[of "-a-1/2" "1/2"] assms by (simp_all add: diff_divide_distrib f_def C_def) define g where "g = (\x. x ^ 2 :: real)" have bij: "bij_betw g {0<..} {0<..}" by (intro bij_betwI[of _ _ _ sqrt]) (auto simp: g_def) have "(f absolutely_integrable_on g ` {0<..} \ integral (g ` {0<..}) f = C)" using I bij by (simp add: bij_betw_def has_integral_iff absolutely_integrable_on_def f_def) also have "?this \ ((\x. \2 * x\ *\<^sub>R f (g x)) absolutely_integrable_on {0<..} \ integral {0<..} (\x. \2 * x\ *\<^sub>R f (g x)) = C)" using bij by (intro has_absolute_integral_change_of_variables_1' [symmetric]) (auto intro!: derivative_eq_intros simp: g_def bij_betw_def) finally have "((\x. \2 * x\ * f (g x)) has_integral C) {0<..}" by (simp add: absolutely_integrable_on_def f_def has_integral_iff) also have "?this \ ((\x::real. 2 * (1 + x\<^sup>2) powr a) has_integral C) {0<..}" by (intro has_integral_cong) (auto simp: f_def g_def powr_def exp_minus ln_realpow field_simps) finally have "((\x::real. 1/2 * (2 * (1 + x\<^sup>2) powr a)) has_integral 1/2 * C) {0<..}" by (intro has_integral_mult_right) thus ?thesis by (simp add: C_def) qed lemma has_integral_Beta3: fixes a b :: real assumes "a < -1/2" and "b > 0" shows "((\x. (b + x ^ 2) powr a) has_integral Beta (-a - 1/2) (1/2) / 2 * b powr (a + 1/2)) {0<..}" proof - define C where "C = Beta (- a - 1 / 2) (1 / 2) / 2" have int: "nn_integral lborel (\x. indicator {0<..} x * (1 + x ^ 2) powr a) = C" using nn_integral_has_integral_lebesgue[OF _ has_integral_Beta2[OF assms(1)]] by (auto simp: C_def) have "nn_integral lborel (\x. indicator {0<..} x * (b + x ^ 2) powr a) = (\\<^sup>+x. ennreal (indicat_real {0<..} (x * sqrt b) * (b + (x * sqrt b)\<^sup>2) powr a * sqrt b) \lborel)" using assms by (subst lborel_distr_mult'[of "sqrt b"]) (auto simp: nn_integral_density nn_integral_distr mult_ac simp flip: ennreal_mult) also have "\ = (\\<^sup>+x. ennreal (indicat_real {0<..} x * (b * (1 + x ^ 2)) powr a * sqrt b) \lborel)" using assms by (intro nn_integral_cong) (auto simp: indicator_def field_simps zero_less_mult_iff) also have "\ = (\\<^sup>+x. ennreal (indicat_real {0<..} x * b powr (a + 1/2) * (1 + x ^ 2) powr a) \lborel)" using assms by (intro nn_integral_cong) (auto simp: indicator_def powr_add powr_half_sqrt powr_mult) also have "\ = b powr (a + 1/2) * (\\<^sup>+x. ennreal (indicat_real {0<..} x * (1 + x ^ 2) powr a) \lborel)" using assms by (subst nn_integral_cmult [symmetric]) (simp_all add: mult_ac flip: ennreal_mult) also have "(\\<^sup>+x. ennreal (indicat_real {0<..} x * (1 + x ^ 2) powr a) \lborel) = C" using int by simp also have "ennreal (b powr (a + 1/2)) * ennreal C = ennreal (C * b powr (a + 1/2))" using assms by (subst ennreal_mult) (auto simp: C_def mult_ac Beta_def) finally have *: "(\\<^sup>+ x. ennreal (indicat_real {0<..} x * (b + x\<^sup>2) powr a) \lborel) = \" . hence "((\x. indicator {0<..} x * (b + x^2) powr a) has_integral C * b powr (a + 1/2)) UNIV" using assms by (subst has_integral_iff_nn_integral_lebesgue) (auto simp: C_def measurable_completion nn_integral_completion Beta_def) also have "(\x. indicator {0<..} x * (b + x^2) powr a) = (\x. if x \ {0<..} then (b + x^2) powr a else 0)" by (auto simp: fun_eq_iff) finally show ?thesis by (subst (asm) has_integral_restrict_UNIV) (auto simp: C_def) qed subsection \Asymptotics of the real $\log\Gamma$ function and its derivatives\ text \ This is the error term that occurs in the expansion of @{term ln_Gamma}. It can be shown to be of order $O(s^{-n})$. \ definition stirling_integral :: "nat \ 'a :: {real_normed_div_algebra, banach} \ 'a" where "stirling_integral n s = lim (\N. integral {0..N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n))" context fixes s :: complex assumes s: "s \ \\<^sub>\\<^sub>0" fixes approx :: "nat \ complex" defines "approx \ (\N. (\n = 1.. \\\ ln_Gamma s\\ (ln_Gamma (of_nat N) - ln (2 * pi / of_nat N) / 2 - of_nat N * ln (of_nat N) + of_nat N) - \ \\\ 0\\ s * (harm (N - 1) - ln (of_nat (N - 1)) - euler_mascheroni) + \ \\\ 0\\ s * (ln (of_nat N + s) - ln (of_nat (N - 1))) - \ \\\ 0\\ (1/2) * (ln (of_nat N + s) - ln (of_nat N)) + \ \\\ 0\\ of_nat N * (ln (of_nat N + s) - ln (of_nat N)) - \ \\\ s\\ (s - 1/2) * ln s - ln (2 * pi) / 2)" begin qualified lemma assumes N: "N > 0" shows integrable_pbernpoly_1: "(\x. of_real (-pbernpoly 1 x) / (of_real x + s)) integrable_on {0..real N}" and integral_pbernpoly_1_aux: "integral {0..real N} (\x. -of_real (pbernpoly 1 x) / (of_real x + s)) = approx N" and has_integral_pbernpoly_1: "((\x. pbernpoly 1 x /(x + s)) has_integral (\mx. -pbernpoly 1 x / (x + s)) has_integral (of_nat n + 1/2 + s) * (ln (of_nat (n + 1) + s) - ln (of_nat n + s)) - 1) {of_nat n..of_nat (n + 1)}" for n proof (rule has_integral_spike) have "((\x. (of_nat n + 1/2 + s) * (1 / (of_real x + s)) - 1) has_integral (of_nat n + 1/2 + s) * (ln (of_real (real (n + 1)) + s) - ln (of_real (real n) + s)) - 1) {of_nat n..of_nat (n + 1)}" using s has_integral_const_real[of 1 "of_nat n" "of_nat (n + 1)"] by (intro has_integral_diff has_integral_mult_right fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros has_vector_derivative_real_field simp: has_field_derivative_iff_has_vector_derivative [symmetric] field_simps complex_nonpos_Reals_iff) thus "((\x. (of_nat n + 1/2 + s) * (1 / (of_real x + s)) - 1) has_integral (of_nat n + 1/2 + s) * (ln (of_nat (n + 1) + s) - ln (of_nat n + s)) - 1) {of_nat n..of_nat (n + 1)}" by simp show "-pbernpoly 1 x / (x + s) = (of_nat n + 1/2 + s) * (1 / (x + s)) - 1" if "x \ {of_nat n..of_nat (n + 1)} - {of_nat (n + 1)}" for x proof - have x: "x \ real n" "x < real (n + 1)" using that by simp_all hence "floor x = int n" by linarith moreover from s x have "complex_of_real x \ -s" by (auto simp add: complex_eq_iff complex_nonpos_Reals_iff simp del: of_nat_Suc) ultimately show "-pbernpoly 1 x / (x + s) = (of_nat n + 1/2 + s) * (1 / (x + s)) - 1" by (auto simp: pbernpoly_def bernpoly_def frac_def divide_simps add_eq_0_iff2) qed qed simp_all hence *: "\I. I\?A \ ((\x. -pbernpoly 1 x / (x + s)) has_integral (Inf I + 1/2 + s) * (ln (Inf I + 1 + s) - ln (Inf I + s)) - 1) I" by (auto simp: add_ac) have "((\x. - pbernpoly 1 x / (x + s)) has_integral (\I\?A. (Inf I + 1 / 2 + s) * (ln (Inf I + 1 + s) - ln (Inf I + s)) - 1)) (\n\{0..x. - pbernpoly 1 x / (x + s)) has_integral ?i) {0..real N}" by (subst has_integral_spike_set_eq) (use Union_atLeastAtMost assms in \auto simp: intro!: empty_imp_negligible\) hence "(\x. - pbernpoly 1 x / (x + s)) integrable_on {0..real N}" and integral: "integral {0..real N} (\x. - pbernpoly 1 x / (x + s)) = ?i" by (simp_all add: has_integral_iff) show "(\x. - pbernpoly 1 x / (x + s)) integrable_on {0..real N}" by fact note has_integral_neg[OF has_integral] also have "-?i = (\xx. of_real (pbernpoly 1 x) / (of_real x + s)) has_integral \) {0..real N}" by simp note integral also have "?i = (\nnnn=1.. = (\n=1..n=1..n=1..n=1.. - (\n = 1..n=1.. 0" for x by (auto simp: complex_nonpos_Reals_iff complex_eq_iff) hence "(\n=1..n=1.. = ln (fact (N - 1)) + (\n=1..n=1..n=1..n=1..n = 1..n = 1..x. -of_real (pbernpoly 1 x) / (of_real x + s)) = \" by simp qed lemma integrable_ln_Gamma_aux: shows "(\x. of_real (pbernpoly n x) / (of_real x + s) ^ n) integrable_on {0..real N}" proof (cases "n = 1") case True with s show ?thesis using integrable_neg[OF integrable_pbernpoly_1[of N]] by (cases "N = 0") (simp_all add: integrable_negligible) next case False from s have "of_real x + s \ 0" if "x \ 0" for x using that by (auto simp: complex_eq_iff add_eq_0_iff2 complex_nonpos_Reals_iff) with False s show ?thesis by (auto intro!: integrable_continuous_real continuous_intros) qed text \ This following proof is based on ``Rudiments of the theory of the gamma function'' by Bruce Berndt~\cite{berndt}. \ lemma tendsto_of_real_0_I: "(f \ 0) G \ ((\x. (of_real (f x))) \ (0 ::'a::real_normed_div_algebra)) G" using tendsto_of_real_iff by force qualified lemma integral_pbernpoly_1: "(\N. integral {0..real N} (\x. pbernpoly 1 x / (x + s))) \ -ln_Gamma s - s + (s - 1 / 2) * ln s + ln (2 * pi) / 2" proof - have neq: "s + of_real x \ 0" if "x \ 0" for x :: real using that s by (auto simp: complex_eq_iff complex_nonpos_Reals_iff) have "(approx \ ln_Gamma s - 0 - 0 + 0 - 0 + s - (s - 1/2) * ln s - ln (2 * pi) / 2) at_top" unfolding approx_def proof (intro tendsto_add tendsto_diff) from s have s': "s \ \\<^sub>\\<^sub>0" by (auto simp: complex_nonpos_Reals_iff elim!: nonpos_Ints_cases) have "(\n. \i=1.. ln_Gamma s + euler_mascheroni * s + ln s" (is "?f \ _") using ln_Gamma_series'_aux[OF s'] unfolding sums_def by (subst filterlim_sequentially_Suc [symmetric], subst (asm) sum.atLeast1_atMost_eq [symmetric]) (simp add: atLeastLessThanSuc_atLeastAtMost) thus "((\n. ?f n - (euler_mascheroni * s + ln s)) \ ln_Gamma s) at_top" by (auto intro: tendsto_eq_intros) next show "(\x. complex_of_real (ln_Gamma (real x) - ln (2 * pi / real x) / 2 - real x * ln (real x) + real x)) \ 0" proof (intro tendsto_of_real_0_I filterlim_compose[OF tendsto_sandwich filterlim_real_sequentially]) show "eventually (\x::real. ln_Gamma x - ln (2 * pi / x) / 2 - x * ln x + x \ 0) at_top" using eventually_ge_at_top[of "1::real"] by eventually_elim (insert ln_Gamma_bounds(1), simp add: algebra_simps) show "eventually (\x::real. ln_Gamma x - ln (2 * pi / x) / 2 - x * ln x + x \ 1 / 12 * inverse x) at_top" using eventually_ge_at_top[of "1::real"] by eventually_elim (insert ln_Gamma_bounds(2), simp add: field_simps) show "((\x::real. 1 / 12 * inverse x) \ 0) at_top" by (intro tendsto_mult_right_zero tendsto_inverse_0_at_top filterlim_ident) qed simp_all next have "(\x. s * of_real (harm (x - 1) - ln (real (x - 1)) - euler_mascheroni)) \ s * of_real (euler_mascheroni - euler_mascheroni)" by (subst filterlim_sequentially_Suc [symmetric], intro tendsto_intros) (insert euler_mascheroni_LIMSEQ, simp_all) also have "?this \ (\x. s * (harm (x - 1) - ln (of_nat (x - 1)) - euler_mascheroni)) \ 0" by (intro filterlim_cong refl eventually_mono[OF eventually_gt_at_top[of "1::nat"]]) (auto simp: Ln_of_nat of_real_harm) finally show "(\x. s * (harm (x - 1) - ln (of_nat (x - 1)) - euler_mascheroni)) \ 0" . next have "((\x. ln (1 + (s + 1) / of_real x)) \ ln (1 + 0)) at_top" (is ?P) by (intro tendsto_intros tendsto_divide_0[OF tendsto_const]) (simp_all add: filterlim_ident filterlim_at_infinity_conv_norm_at_top filterlim_abs_real) also have "ln (of_real (x + 1) + s) - ln (complex_of_real x) = ln (1 + (s + 1) / of_real x)" if "x > 1" for x using that s using Ln_divide_of_real[of x "of_real (x + 1) + s", symmetric] neq[of "x+1"] by (simp add: field_simps Ln_of_real) hence "?P \ ((\x. ln (of_real (x + 1) + s) - ln (of_real x)) \ 0) at_top" by (intro filterlim_cong refl) (auto intro: eventually_mono[OF eventually_gt_at_top[of "1::real"]]) finally have "((\n. ln (of_real (real n + 1) + s) - ln (of_real (real n))) \ 0) at_top" by (rule filterlim_compose[OF _ filterlim_real_sequentially]) hence "((\n. ln (of_nat n + s) - ln (of_nat (n - 1))) \ 0) at_top" by (subst filterlim_sequentially_Suc [symmetric]) (simp add: add_ac) thus "(\x. s * (ln (of_nat x + s) - ln (of_nat (x - 1)))) \ 0" by (rule tendsto_mult_right_zero) next have "((\x. ln (1 + s / of_real x)) \ ln (1 + 0)) at_top" (is ?P) by (intro tendsto_intros tendsto_divide_0[OF tendsto_const]) (simp_all add: filterlim_ident filterlim_at_infinity_conv_norm_at_top filterlim_abs_real) also have "ln (of_real x + s) - ln (of_real x) = ln (1 + s / of_real x)" if "x > 0" for x using Ln_divide_of_real[of x "of_real x + s"] neq[of x] that by (auto simp: field_simps Ln_of_real) hence "?P \ ((\x. ln (of_real x + s) - ln (of_real x)) \ 0) at_top" using s by (intro filterlim_cong refl) (auto intro: eventually_mono [OF eventually_gt_at_top[of "1::real"]]) finally have "(\x. (1/2) * (ln (of_real (real x) + s) - ln (of_real (real x)))) \ 0" by (rule tendsto_mult_right_zero[OF filterlim_compose[OF _ filterlim_real_sequentially]]) thus "(\x. (1/2) * (ln (of_nat x + s) - ln (of_nat x))) \ 0" by simp next have "((\x. x * (ln (1 + s / of_real x))) \ s) at_top" (is ?P) by (rule stirling_limit_aux2) also have "ln (1 + s / of_real x) = ln (of_real x + s) - ln (of_real x)" if "x > 1" for x using that s Ln_divide_of_real [of x "of_real x + s", symmetric] neq[of x] by (auto simp: Ln_of_real field_simps) hence "?P \ ((\x. of_real x * (ln (of_real x + s) - ln (of_real x))) \ s) at_top" by (intro filterlim_cong refl) (auto intro: eventually_mono[OF eventually_gt_at_top[of "1::real"]]) finally have "(\n. of_real (real n) * (ln (of_real (real n) + s) - ln (of_real (real n)))) \ s" by (rule filterlim_compose[OF _ filterlim_real_sequentially]) thus "(\n. of_nat n * (ln (of_nat n + s) - ln (of_nat n))) \ s" by simp qed simp_all also have "?this \ ((\N. integral {0..real N} (\x. -pbernpoly 1 x / (x + s))) \ ln_Gamma s + s - (s - 1/2) * ln s - ln (2 * pi) / 2) at_top" using integral_pbernpoly_1_aux by (intro filterlim_cong refl) (auto intro: eventually_mono[OF eventually_gt_at_top[of "0::nat"]]) also have "(\N. integral {0..real N} (\x. -pbernpoly 1 x / (x + s))) = (\N. -integral {0..real N} (\x. pbernpoly 1 x / (x + s)))" by (simp add: fun_eq_iff) finally show ?thesis by (simp add: tendsto_minus_cancel_left [symmetric] algebra_simps) qed qualified lemma pbernpoly_integral_conv_pbernpoly_integral_Suc: assumes "n \ 1" shows "integral {0..real N} (\x. pbernpoly n x / (x + s) ^ n) = of_real (pbernpoly (Suc n) (real N)) / (of_nat (Suc n) * (s + of_nat N) ^ n) - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n) + of_nat n / of_nat (Suc n) * integral {0..real N} (\x. of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n)" proof - note [derivative_intros] = has_field_derivative_pbernpoly_Suc' define I where "I = -of_real (pbernpoly (Suc n) (of_nat N)) / (of_nat (Suc n) * (of_nat N + s) ^ n) + of_real (bernoulli (Suc n) / real (Suc n)) / s ^ n + integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)" have "((\x. (-of_nat n * inverse (of_real x + s) ^ Suc n) * (of_real (pbernpoly (Suc n) x) / (of_nat (Suc n)))) has_integral -I) {0..real N}" proof (rule integration_by_parts_interior_strong[OF bounded_bilinear_mult]) fix x :: real assume x: "x \ {0<.. \" proof assume "x \ \" then obtain n where "x = of_int n" by (auto elim!: Ints_cases) with x have x': "x = of_nat (nat n)" by simp from x show False by (auto simp: x') qed hence "((\x. of_real (pbernpoly (Suc n) x / of_nat (Suc n))) has_vector_derivative complex_of_real (pbernpoly n x)) (at x)" by (intro has_vector_derivative_of_real) (auto intro!: derivative_eq_intros) thus "((\x. of_real (pbernpoly (Suc n) x) / of_nat (Suc n)) has_vector_derivative complex_of_real (pbernpoly n x)) (at x)" by simp from x s have "complex_of_real x + s \ 0" by (auto simp: complex_eq_iff complex_nonpos_Reals_iff) thus "((\x. inverse (of_real x + s) ^ n) has_vector_derivative - of_nat n * inverse (of_real x + s) ^ Suc n) (at x)" using x s assms by (auto intro!: derivative_eq_intros has_vector_derivative_real_field simp: divide_simps power_add [symmetric] simp del: power_Suc) next have "complex_of_real x + s \ 0" if "x \ 0" for x using that s by (auto simp: complex_eq_iff complex_nonpos_Reals_iff) thus "continuous_on {0..real N} (\x. inverse (of_real x + s) ^ n)" "continuous_on {0..real N} (\x. complex_of_real (pbernpoly (Suc n) x) / of_nat (Suc n))" using assms s by (auto intro!: continuous_intros simp del: of_nat_Suc) next have "((\x. inverse (of_real x + s) ^ n * of_real (pbernpoly n x)) has_integral pbernpoly (Suc n) (of_nat N) / (of_nat (Suc n) * (of_nat N + s) ^ n) - of_real (bernoulli (Suc n) / real (Suc n)) / s ^ n - -I) {0..real N}" using integrable_ln_Gamma_aux[of n N] assms by (auto simp: I_def has_integral_integral divide_simps) thus "((\x. inverse (of_real x + s) ^ n * of_real (pbernpoly n x)) has_integral inverse (of_real (real N) + s) ^ n * (of_real (pbernpoly (Suc n) (real N)) / of_nat (Suc n)) - inverse (of_real 0 + s) ^ n * (of_real (pbernpoly (Suc n) 0) / of_nat (Suc n)) - - I) {0..real N}" by (simp_all add: field_simps) qed simp_all also have "(\x. - of_nat n * inverse (of_real x + s) ^ Suc n * (of_real (pbernpoly (Suc n) x) / of_nat (Suc n))) = (\x. - (of_nat n / of_nat (Suc n) * of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n))" by (simp add: divide_simps fun_eq_iff) finally have "((\x. - (of_nat n / of_nat (Suc n) * of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n)) has_integral - I) {0..real N}" . from has_integral_neg[OF this] show ?thesis by (auto simp add: I_def has_integral_iff algebra_simps integral_mult_right [symmetric] simp del: power_Suc of_nat_Suc ) qed lemma pbernpoly_over_power_tendsto_0: assumes "n > 0" shows "(\x. of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \ 0" proof - from s have neq: "s + of_nat n \ 0" for n by (auto simp: complex_eq_iff complex_nonpos_Reals_iff) obtain c where c: "\x. norm (pbernpoly (Suc n) x) \ c" using bounded_pbernpoly by auto have "eventually (\x. real x + Re s > 0) at_top" by real_asymp hence "eventually (\x. norm (of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \ (c / real (Suc n)) / (real x + Re s) ^ n) at_top" using eventually_gt_at_top[of "0::nat"] proof eventually_elim case (elim x) have "norm (of_real (pbernpoly (Suc n) (real x)) / (of_nat (Suc n) * (s + of_nat x) ^ n)) \ (c / real (Suc n)) / norm (s + of_nat x) ^ n" (is "_ \ ?rhs") using c[of x] by (auto simp: norm_divide norm_mult norm_power neq field_simps simp del: of_nat_Suc) also have "(real x + Re s) \ cmod (s + of_nat x)" using complex_Re_le_cmod[of "s + of_nat x"] s by (auto simp add: complex_nonpos_Reals_iff) hence "?rhs \ (c / real (Suc n)) / (real x + Re s) ^ n" using s elim c[of 0] neq[of x] by (intro divide_left_mono power_mono mult_pos_pos divide_nonneg_pos zero_less_power) auto finally show ?case . qed moreover have "(\x. (c / real (Suc n)) / (real x + Re s) ^ n) \ 0" using \n > 0\ by real_asymp ultimately show ?thesis by (rule Lim_null_comparison) qed lemma convergent_stirling_integral: assumes "n > 0" shows "convergent (\N. integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n))" (is "convergent (?f n)") proof - have "convergent (?f (Suc n))" for n proof (induction n) case 0 thus ?case using integral_pbernpoly_1 by (auto intro!: convergentI) next case (Suc n) have "convergent (\N. ?f (Suc n) N - of_real (pbernpoly (Suc (Suc n)) (real N)) / (of_nat (Suc (Suc n)) * (s + of_nat N) ^ Suc n) + of_real (bernoulli (Suc (Suc n)) / (real (Suc (Suc n)))) / s ^ Suc n)" (is "convergent ?g") by (intro convergent_add convergent_diff Suc convergent_const convergentI[OF pbernpoly_over_power_tendsto_0]) simp_all also have "?g = (\N. of_nat (Suc n) / of_nat (Suc (Suc n)) * ?f (Suc (Suc n)) N)" using s by (subst pbernpoly_integral_conv_pbernpoly_integral_Suc) (auto simp: fun_eq_iff field_simps simp del: of_nat_Suc power_Suc) also have "convergent \ \ convergent (?f (Suc (Suc n)))" by (intro convergent_mult_const_iff) (simp_all del: of_nat_Suc) finally show ?case . qed from this[of "n - 1"] assms show ?thesis by simp qed lemma stirling_integral_conv_stirling_integral_Suc: assumes "n > 0" shows "stirling_integral n s = of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" proof - have "(\N. of_real (pbernpoly (Suc n) (real N)) / (of_nat (Suc n) * (s + of_nat N) ^ n) - of_real (bernoulli (Suc n)) / (real (Suc n) * s ^ n) + integral {0..real N} (\x. of_nat n / of_nat (Suc n) * (of_real (pbernpoly (Suc n) x) / (of_real x + s) ^ Suc n))) \ 0 - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n) + of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s" (is "?f \ _") unfolding stirling_integral_def integral_mult_right using convergent_stirling_integral[of "Suc n"] assms s by (intro tendsto_intros pbernpoly_over_power_tendsto_0) (auto simp: convergent_LIMSEQ_iff simp del: of_nat_Suc) also have "?this \ (\N. integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" using eventually_gt_at_top[of "0::nat"] pbernpoly_integral_conv_pbernpoly_integral_Suc[of n] assms unfolding integral_mult_right by (intro filterlim_cong refl) (auto elim!: eventually_mono simp del: power_Suc) finally show ?thesis unfolding stirling_integral_def[of n] by (rule limI) qed lemma stirling_integral_1_unfold: assumes "m > 0" shows "stirling_integral 1 s = stirling_integral m s / of_nat m - (\k=1..k=1..k = 1.. 0" shows "ln_Gamma s = (s - 1 / 2) * ln s - s + ln (2 * pi) / 2 + (\k=1..k = 1.. 0 \ (\x. integral {0..real x} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ stirling_integral n s" unfolding stirling_integral_def using convergent_stirling_integral[of n] by (simp only: convergent_LIMSEQ_iff) end lemmas has_integral_of_real = has_integral_linear[OF _ bounded_linear_of_real, unfolded o_def] lemmas integral_of_real = integral_linear[OF _ bounded_linear_of_real, unfolded o_def] lemma integrable_ln_Gamma_aux_real: assumes "0 < s" shows "(\x. pbernpoly n x / (x + s) ^ n) integrable_on {0..real N}" proof - have "(\x. complex_of_real (pbernpoly n x / (x + s) ^ n)) integrable_on {0..real N}" using integrable_ln_Gamma_aux[of "of_real s" n N] assms by simp from integrable_linear[OF this bounded_linear_Re] show ?thesis by (simp only: o_def Re_complex_of_real) qed lemma assumes "x > 0" "n > 0" shows stirling_integral_complex_of_real: "stirling_integral n (complex_of_real x) = of_real (stirling_integral n x)" and LIMSEQ_stirling_integral_real: "(\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n)) \ stirling_integral n x" and stirling_integral_real_convergent: "convergent (\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n))" proof - have "(\N. integral {0..real N} (\t. of_real (pbernpoly n t / (t + x) ^ n))) \ stirling_integral n (complex_of_real x)" using LIMSEQ_stirling_integral[of "complex_of_real x" n] assms by simp hence "(\N. of_real (integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n))) \ stirling_integral n (complex_of_real x)" using integrable_ln_Gamma_aux_real[OF assms(1), of n] by (subst (asm) integral_of_real) simp from tendsto_Re[OF this] have "(\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n)) \ Re (stirling_integral n (complex_of_real x))" by simp thus "convergent (\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n))" by (rule convergentI) thus "(\N. integral {0..real N} (\t. pbernpoly n t / (t + x) ^ n)) \ stirling_integral n x" unfolding stirling_integral_def by (simp add: convergent_LIMSEQ_iff) from tendsto_of_real[OF this, where 'a = complex] integrable_ln_Gamma_aux_real[OF assms(1), of n] have "(\xa. integral {0..real xa} (\xa. complex_of_real (pbernpoly n xa) / (complex_of_real xa + x) ^ n)) \ complex_of_real (stirling_integral n x)" by (subst (asm) integral_of_real [symmetric]) simp_all from LIMSEQ_unique[OF this LIMSEQ_stirling_integral[of "complex_of_real x" n]] assms show "stirling_integral n (complex_of_real x) = of_real (stirling_integral n x)" by simp qed lemma ln_Gamma_stirling_real: assumes "x > (0 :: real)" "m > (0::nat)" shows "ln_Gamma x = (x - 1 / 2) * ln x - x + ln (2 * pi) / 2 + (\k = 1..k = 1.. (1::nat)" obtains c where "\s. Re s > 0 \ norm (stirling_integral n s) \ c / Re s ^ (n - 1)" proof - obtain c where c: "norm (pbernpoly n x) \ c" for x by (rule bounded_pbernpoly[of n]) blast have c': "pbernpoly n x \ c" for x using c[of x] by (simp add: abs_real_def split: if_splits) from c[of 0] have c_nonneg: "c \ 0" by simp have "norm (stirling_integral n s) \ c / (real n - 1) / Re s ^ (n - 1)" if s: "Re s > 0" for s proof (rule Lim_norm_ubound[OF _ LIMSEQ_stirling_integral]) have pos: "x + norm s > 0" if "x \ 0" for x using s that by (intro add_nonneg_pos) auto have nz: "of_real x + s \ 0" if "x \ 0" for x using s that by (auto simp: complex_eq_iff) let ?bound = "\N. c / (Re s ^ (n - 1) * (real n - 1)) - c / ((real N + Re s) ^ (n - 1) * (real n - 1))" show "eventually (\N. norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ c / (real n - 1) / Re s ^ (n - 1)) at_top" using eventually_gt_at_top[of "0::nat"] proof eventually_elim case (elim N) let ?F = "\x. -c / ((x + Re s) ^ (n - 1) * (real n - 1))" from n s have "((\x. c / (x + Re s) ^ n) has_integral (?F (real N) - ?F 0)) {0..real N}" by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros simp: divide_simps power_diff add_eq_0_iff2 has_field_derivative_iff_has_vector_derivative [symmetric]) also have "?F (real N) - ?F 0 = ?bound N" by simp finally have *: "((\x. c / (x + Re s) ^ n) has_integral ?bound N) {0..real N}" . have "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ integral {0..real N} (\x. c / (x + Re s) ^ n)" proof (intro integral_norm_bound_integral integrable_ln_Gamma_aux s ballI) fix x assume x: "x \ {0..real N}" have "norm (of_real (pbernpoly n x) / (of_real x + s) ^ n) \ c / norm (of_real x + s) ^ n" unfolding norm_divide norm_power using c by (intro divide_right_mono) simp_all also have "\ \ c / (x + Re s) ^ n" using x c c_nonneg s nz[of x] complex_Re_le_cmod[of "of_real x + s"] by (intro divide_left_mono power_mono mult_pos_pos zero_less_power add_nonneg_pos) auto finally show "norm (of_real (pbernpoly n x) / (of_real x + s) ^ n) \ \" . qed (insert n s * pos nz c, auto simp: complex_nonpos_Reals_iff) also have "\ = ?bound N" using * by (simp add: has_integral_iff) also have "\ \ c / (Re s ^ (n - 1) * (real n - 1))" using c_nonneg elim s n by simp also have "\ = c / (real n - 1) / (Re s ^ (n - 1))" by simp finally show "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ c / (real n - 1) / Re s ^ (n - 1)" . qed qed (insert s n, simp_all add: complex_nonpos_Reals_iff) thus ?thesis by (rule that) qed lemma stirling_integral_bound_aux_integral1: fixes a b c :: real and n :: nat assumes "a \ 0" "b > 0" "c \ 0" "n > 1" "l < a - b" "r > a + b" shows "((\x. c / max b \x - a\ ^ n) has_integral 2*c*(n / (n - 1))/b^(n-1) - c/(n-1) * (1/(a-l)^(n-1) + 1/(r-a)^(n-1))) {l..r}" proof - define x1 x2 where "x1 = a - b" and "x2 = a + b" define F1 where "F1 = (\x::real. c / (a - x) ^ (n - 1) / (n - 1))" define F3 where "F3 = (\x::real. -c / (x - a) ^ (n - 1) / (n - 1))" have deriv: "(F1 has_vector_derivative (c / (a - x) ^ n)) (at x within A)" "(F3 has_vector_derivative (c / (x - a) ^ n)) (at x within A)" if "x \ a" for x :: real and A unfolding F1_def F3_def using assms that by (auto intro!: derivative_eq_intros simp: divide_simps power_diff add_eq_0_iff2 simp flip: has_field_derivative_iff_has_vector_derivative) from assms have "((\x. c / (a - x) ^ n) has_integral (F1 x1 - F1 l)) {l..x1}" by (intro fundamental_theorem_of_calculus deriv) (auto simp: x1_def max_def split: if_splits) also have "?this \ ((\x. c / max b \x - a\ ^ n) has_integral (F1 x1 - F1 l)) {l..x1}" using assms by (intro has_integral_spike_finite_eq[of "{l}"]) (auto simp: x1_def max_def split: if_splits) finally have I1: "((\x. c / max b \x - a\ ^ n) has_integral (F1 x1 - F1 l)) {l..x1}" . have "((\x. c / b ^ n) has_integral (x2 - x1) * c / b ^ n) {x1..x2}" using has_integral_const_real[of "c / b ^ n" x1 x2] assms by (simp add: x1_def x2_def) also have "?this \ ((\x. c / max b \x - a\ ^ n) has_integral ((x2 - x1) * c / b ^ n)) {x1..x2}" by (intro has_integral_spike_finite_eq[of "{x1, x2}"]) (auto simp: x1_def x2_def split: if_splits) finally have I2: "((\x. c / max b \x - a\ ^ n) has_integral ((x2 - x1) * c / b ^ n)) {x1..x2}" . from assms have I3: "((\x. c / (x - a) ^ n) has_integral (F3 r - F3 x2)) {x2..r}" by (intro fundamental_theorem_of_calculus deriv) (auto simp: x2_def min_def split: if_splits) also have "?this \ ((\x. c / max b \x - a\ ^ n) has_integral (F3 r - F3 x2)) {x2..r}" using assms by (intro has_integral_spike_finite_eq[of "{r}"]) (auto simp: x2_def min_def split: if_splits) finally have I3: "((\x. c / max b \x - a\ ^ n) has_integral (F3 r - F3 x2)) {x2..r}" . have "((\x. c / max b \x - a\ ^ n) has_integral (F1 x1 - F1 l) + ((x2 - x1) * c / b ^ n) + (F3 r - F3 x2)) {l..r}" using assms by (intro has_integral_combine[OF _ _ has_integral_combine[OF _ _ I1 I2] I3]) (auto simp: x1_def x2_def) also have "(F1 x1 - F1 l) + ((x2 - x1) * c / b ^ n) + (F3 r - F3 x2) = F1 x1 - F1 l + F3 r - F3 x2 + (x2 - x1) * c / b ^ n" by (simp add: algebra_simps) also have "x2 - x1 = 2 * b" using assms by (simp add: x2_def x1_def min_def max_def) also have "2 * b * c / b ^ n = 2 * c / b ^ (n - 1)" using assms by (simp add: power_diff field_simps) also have "F1 x1 - F1 l + F3 r - F3 x2 = c/(n-1) * (2/b^(n-1) - 1/(a-l)^(n-1) - 1/(r-a)^(n-1))" using assms by (simp add: x1_def x2_def F1_def F3_def field_simps) also have "\ + 2 * c / b ^ (n - 1) = 2*c*(1 + 1/(n-1))/b^(n-1) - c/(n-1) * (1/(a-l)^(n-1) + 1/(r-a)^(n-1))" using assms by (simp add: field_simps) also have "1 + 1 / (n - 1) = n / (n - 1)" using assms by (simp add: field_simps) finally show ?thesis . qed lemma stirling_integral_bound_aux_integral2: fixes a b c :: real and n :: nat assumes "a \ 0" "b > 0" "c \ 0" "n > 1" obtains I where "((\x. c / max b \x - a\ ^ n) has_integral I) {l..r}" "I \ 2 * c * (n / (n - 1)) / b ^ (n-1)" proof - define l' where "l' = min l (a - b - 1)" define r' where "r' = max r (a + b + 1)" define A where "A = 2 * c * (n / (n - 1)) / b ^ (n - 1)" define B where "B = c / real (n - 1) * (1 / (a - l') ^ (n - 1) + 1 / (r' - a) ^ (n - 1))" have has_int: "((\x. c / max b \x - a\ ^ n) has_integral (A - B)) {l'..r'}" using assms unfolding A_def B_def by (intro stirling_integral_bound_aux_integral1) (auto simp: l'_def r'_def) have "(\x. c / max b \x - a\ ^ n) integrable_on {l..r}" by (rule integrable_on_subinterval[OF has_integral_integrable[OF has_int]]) (auto simp: l'_def r'_def) then obtain I where has_int': "((\x. c / max b \x - a\ ^ n) has_integral I) {l..r}" by (auto simp: integrable_on_def) from assms have "I \ A - B" by (intro has_integral_subset_le[OF _ has_int' has_int]) (auto simp: l'_def r'_def) also have "\ \ A" using assms by (simp add: B_def l'_def r'_def) finally show ?thesis using that[of I] has_int' unfolding A_def by blast qed lemma stirling_integral_bound_aux': assumes n: "n > (1::nat)" and \: "\ \ {0<..s::complex. s \ complex_cone' \ - {0} \ norm (stirling_integral n s) \ c / norm s ^ (n - 1)" proof - obtain c where c: "norm (pbernpoly n x) \ c" for x by (rule bounded_pbernpoly[of n]) blast have c': "pbernpoly n x \ c" for x using c[of x] by (simp add: abs_real_def split: if_splits) from c[of 0] have c_nonneg: "c \ 0" by simp define D where "D = c * Beta (- (real_of_int (- int n) / 2) - 1 / 2) (1 / 2) / 2" define C where "C = max D (2*c*(n/(n-1))/sin \^(n-1))" have *: "norm (stirling_integral n s) \ C / norm s ^ (n - 1)" if s: "s \ complex_cone' \ - {0}" for s :: complex proof (rule Lim_norm_ubound[OF _ LIMSEQ_stirling_integral]) from s \ have Arg: "\Arg s\ \ \" by (auto simp: complex_cone_altdef) have s': "s \ \\<^sub>\\<^sub>0" using complex_cone_inter_nonpos_Reals[of "-\" \] \ s by auto from s have [simp]: "s \ 0" by auto show "eventually (\N. norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ C / norm s ^ (n - 1)) at_top" using eventually_gt_at_top[of "0::nat"] proof eventually_elim case (elim N) show ?case proof (cases "Re s > 0") case True have int: "((\x. c * (x^2 + norm s^2) powr (-n / 2)) has_integral D * (norm s ^ 2) powr (-n / 2 + 1 / 2)) {0<..}" using has_integral_mult_left[OF has_integral_Beta3[of "-n/2" "norm s ^ 2"], of c] assms True unfolding D_def by (simp add: algebra_simps) hence int': "((\x. c * (x^2 + norm s^2) powr (-n / 2)) has_integral D * (norm s ^ 2) powr (-n / 2 + 1 / 2)) {0..}" by (subst has_integral_interior [symmetric]) simp_all hence integrable: "(\x. c * (x^2 + norm s^2) powr (-n / 2)) integrable_on {0..}" by (simp add: has_integral_iff) have "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ integral {0..real N} (\x. c * (x^2 + norm s^2) powr (-n / 2))" proof (intro integral_norm_bound_integral s ballI integrable_ln_Gamma_aux) have [simp]: "{0<..} - {0::real..} = {}" "{0..} - {0<..} = {0::real}" by auto have "(\x. c * (x\<^sup>2 + (cmod s)\<^sup>2) powr (real_of_int (- int n) / 2)) integrable_on {0<..}" using int by (simp add: has_integral_iff) also have "?this \ (\x. c * (x\<^sup>2 + (cmod s)\<^sup>2) powr (real_of_int (- int n) / 2)) integrable_on {0..}" by (intro integrable_spike_set_eq) auto finally show "(\x. c * (x\<^sup>2 + (cmod s)\<^sup>2) powr (real_of_int (- int n) / 2)) integrable_on {0..real N}" by (rule integrable_on_subinterval) auto next fix x assume x: "x \ {0..real N}" have nz: "complex_of_real x + s \ 0" using True x by (auto simp: complex_eq_iff) have "norm (of_real (pbernpoly n x) / (of_real x + s) ^ n) \ c / norm (of_real x + s) ^ n" unfolding norm_divide norm_power using c by (intro divide_right_mono) simp_all also have "\ \ c / sqrt (x ^ 2 + norm s ^ 2) ^ n" proof (intro divide_left_mono mult_pos_pos zero_less_power power_mono) show "sqrt (x\<^sup>2 + (cmod s)\<^sup>2) \ cmod (complex_of_real x + s)" using x True by (simp add: cmod_def algebra_simps power2_eq_square) qed (use x True c_nonneg assms nz in \auto simp: add_nonneg_pos\) also have "sqrt (x ^ 2 + norm s ^ 2) ^ n = (x ^ 2 + norm s ^ 2) powr (1/2 * n)" by (subst powr_powr [symmetric], subst powr_realpow) (auto simp: powr_half_sqrt add_nonneg_pos) also have "c / \ = c * (x^2 + norm s^2) powr (-n / 2)" by (simp add: powr_minus field_simps) finally show "norm (complex_of_real (pbernpoly n x) / (complex_of_real x + s) ^ n) \ \" . qed fact+ also have "\ \ integral {0..} (\x. c * (x^2 + norm s^2) powr (-n / 2))" using c_nonneg by (intro integral_subset_le integrable integrable_on_subinterval[OF integrable]) auto also have "\ = D * (norm s ^ 2) powr (-n / 2 + 1 / 2)" using int' by (simp add: has_integral_iff) also have "(norm s ^ 2) powr (-n / 2 + 1 / 2) = norm s powr (2 * (-n / 2 + 1 / 2))" by (subst powr_powr [symmetric]) auto also have "\ = norm s powr (-real (n - 1))" using assms by (simp add: of_nat_diff) also have "D * \ = D / norm s ^ (n - 1)" by (auto simp: powr_minus powr_realpow field_simps) also have "\ \ C / norm s ^ (n - 1)" by (intro divide_right_mono) (auto simp: C_def) finally show "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ \" . next case False have "cos \Arg s\ = cos (Arg s)" by (simp add: abs_if) also have "cos (Arg s) = Re (rcis (norm s) (Arg s)) / norm s" by (subst Re_rcis) auto also have "\ = Re s / norm s" by (subst rcis_cmod_Arg) auto also have "\ \ cos (pi / 2)" using False by (auto simp: field_simps) finally have "\Arg s\ \ pi / 2" using Arg \ by (subst (asm) cos_mono_le_eq) auto have "sin \ * norm s = sin (pi - \) * norm s" by simp also have "\ \ sin (pi - \Arg s\) * norm s" using \ Arg \\Arg s\ \ pi / 2\ by (intro mult_right_mono sin_monotone_2pi_le) auto also have "sin \Arg s\ \ 0" using Arg_bounded[of s] by (intro sin_ge_zero) auto hence "sin (pi - \Arg s\) = \sin \Arg s\\" by simp also have "\ = \sin (Arg s)\" by (simp add: abs_if) also have "\ * norm s = \Im (rcis (norm s) (Arg s))\" by (simp add: abs_mult) also have "\ = \Im s\" by (subst rcis_cmod_Arg) auto finally have abs_Im_ge: "\Im s\ \ sin \ * norm s" . have [simp]: "Im s \ 0" "s \ 0" using s \s \ \\<^sub>\\<^sub>0\ False by (auto simp: cmod_def zero_le_mult_iff complex_nonpos_Reals_iff) have "sin \ > 0" using assms by (intro sin_gt_zero) auto obtain I where I: "((\x. c / max \Im s\ \x + Re s\ ^ n) has_integral I) {0..real N}" "I \ 2*c*(n/(n-1)) / \Im s\ ^ (n - 1)" using s c_nonneg assms False stirling_integral_bound_aux_integral2[of "-Re s" "\Im s\" c n 0 "real N"] by auto have "norm (integral {0..real N} (\x. of_real (pbernpoly n x) / (of_real x + s) ^ n)) \ integral {0..real N} (\x. c / max \Im s\ \x + Re s\ ^ n)" proof (intro integral_norm_bound_integral integrable_ln_Gamma_aux s ballI) show "(\x. c / max \Im s\ \x + Re s\ ^ n) integrable_on {0..real N}" using I(1) by (simp add: has_integral_iff) next fix x assume x: "x \ {0..real N}" have nz: "complex_of_real x + s \ 0" by (auto simp: complex_eq_iff) have "norm (complex_of_real (pbernpoly n x) / (complex_of_real x + s) ^ n) \ c / norm (complex_of_real x + s) ^ n" unfolding norm_divide norm_power using c[of x] by (intro divide_right_mono) simp_all also have "\ \ c / max \Im s\ \x + Re s\ ^ n" using c_nonneg nz abs_Re_le_cmod[of "of_real x + s"] abs_Im_le_cmod[of "of_real x + s"] by (intro divide_left_mono power_mono mult_pos_pos zero_less_power) (auto simp: less_max_iff_disj) finally show "norm (complex_of_real (pbernpoly n x) / (complex_of_real x + s) ^ n) \ \" . qed (auto simp: complex_nonpos_Reals_iff) also have "\ \ 2*c*(n/(n-1)) / \Im s\ ^ (n - 1)" using I by (simp add: has_integral_iff) also have "\ \ 2*c*(n/(n-1)) / (sin \ * norm s) ^ (n - 1)" using \sin \ > 0\ s c_nonneg abs_Im_ge by (intro divide_left_mono mult_pos_pos zero_less_power power_mono mult_nonneg_nonneg) auto also have "\ = 2*c*(n/(n-1))/sin \^(n-1) / norm s ^ (n - 1)" by (simp add: field_simps) also have "\ \ C / norm s ^ (n - 1)" by (intro divide_right_mono) (auto simp: C_def) finally show ?thesis . qed qed qed (use that assms complex_cone_inter_nonpos_Reals[of "-\" \] \ in auto) thus ?thesis by (rule that) qed lemma stirling_integral_bound: assumes "n > 0" obtains c where "\s. Re s > 0 \ norm (stirling_integral n s) \ c / Re s ^ n" proof - let ?f = "\s. of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" from stirling_integral_bound_aux[of "Suc n"] assms obtain c where c: "\s. Re s > 0 \ norm (stirling_integral (Suc n) s) \ c / Re s ^ n" by auto define c1 where "c1 = real n / real (Suc n) * c" define c2 where "c2 = \bernoulli (Suc n)\ / real (Suc n)" have c2_nonneg: "c2 \ 0" by (simp add: c2_def) show ?thesis proof (rule that) fix s :: complex assume s: "Re s > 0" hence s': "s \ \\<^sub>\\<^sub>0" by (auto simp: complex_nonpos_Reals_iff) have "stirling_integral n s = ?f s" using s' assms by (rule stirling_integral_conv_stirling_integral_Suc) also have "norm \ \ norm (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + norm (of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))" by (rule norm_triangle_ineq4) also have "\ = real n / real (Suc n) * norm (stirling_integral (Suc n) s) + c2 / norm s ^ n" (is "_ = ?A + ?B") by (simp add: norm_divide norm_mult norm_power c2_def field_simps del: of_nat_Suc) also have "?A \ real n / real (Suc n) * (c / Re s ^ n)" by (intro mult_left_mono c s) simp_all also have "\ = c1 / Re s ^ n" by (simp add: c1_def) also have "c2 / norm s ^ n \ c2 / Re s ^ n" using s c2_nonneg by (intro divide_left_mono power_mono complex_Re_le_cmod mult_pos_pos zero_less_power) auto also have "c1 / Re s ^ n + c2 / Re s ^ n = (c1 + c2) / Re s ^ n" using s by (simp add: field_simps) finally show "norm (stirling_integral n s) \ (c1 + c2) / Re s ^ n" by - simp_all qed qed lemma stirling_integral_bound': assumes "n > 0" and "\ \ {0<..s::complex. s \ complex_cone' \ - {0} \ norm (stirling_integral n s) \ c / norm s ^ n" proof - let ?f = "\s. of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s - of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n)" from stirling_integral_bound_aux'[of "Suc n"] assms obtain c where c: "\s::complex. s \ complex_cone' \ - {0} \ norm (stirling_integral (Suc n) s) \ c / norm s ^ n" by auto define c1 where "c1 = real n / real (Suc n) * c" define c2 where "c2 = \bernoulli (Suc n)\ / real (Suc n)" have c2_nonneg: "c2 \ 0" by (simp add: c2_def) show ?thesis proof (rule that) fix s :: complex assume s: "s \ complex_cone' \ - {0}" have s': "s \ \\<^sub>\\<^sub>0" using complex_cone_inter_nonpos_Reals[of "-\" \] assms s by auto have "stirling_integral n s = ?f s" using s' assms by (intro stirling_integral_conv_stirling_integral_Suc) auto also have "norm \ \ norm (of_nat n / of_nat (Suc n) * stirling_integral (Suc n) s) + norm (of_real (bernoulli (Suc n)) / (of_nat (Suc n) * s ^ n))" by (rule norm_triangle_ineq4) also have "\ = real n / real (Suc n) * norm (stirling_integral (Suc n) s) + c2 / norm s ^ n" (is "_ = ?A + ?B") by (simp add: norm_divide norm_mult norm_power c2_def field_simps del: of_nat_Suc) also have "?A \ real n / real (Suc n) * (c / norm s ^ n)" by (intro mult_left_mono c s) simp_all also have "\ = c1 / norm s ^ n" by (simp add: c1_def) also have "c1 / norm s ^ n + c2 / norm s ^ n = (c1 + c2) / norm s ^ n" using s by (simp add: divide_simps) finally show "norm (stirling_integral n s) \ (c1 + c2) / norm s ^ n" by - simp_all qed qed lemma stirling_integral_holomorphic [holomorphic_intros]: assumes m: "m > 0" and "A \ \\<^sub>\\<^sub>0 = {}" shows "stirling_integral m holomorphic_on A" proof - from assms have [simp]: "z \ \\<^sub>\\<^sub>0" if "z \ A" for z using that by auto let ?f = "\s::complex. of_nat m * ((s - 1 / 2) * Ln s - s + of_real (ln (2 * pi) / 2) + (\k=1.. stirling_integral m holomorphic_on A" using assms by (intro holomorphic_cong refl) (simp_all add: field_simps ln_Gamma_stirling_complex) finally show "stirling_integral m holomorphic_on A" . qed lemma stirling_integral_continuous_on_complex [continuous_intros]: assumes m: "m > 0" and "A \ \\<^sub>\\<^sub>0 = {}" shows "continuous_on A (stirling_integral m :: _ \ complex)" by (intro holomorphic_on_imp_continuous_on stirling_integral_holomorphic assms) lemma has_field_derivative_stirling_integral_complex: fixes x :: complex assumes "x \ \\<^sub>\\<^sub>0" "n > 0" shows "(stirling_integral n has_field_derivative deriv (stirling_integral n) x) (at x)" using assms by (intro holomorphic_derivI[OF stirling_integral_holomorphic, of n "-\\<^sub>\\<^sub>0"]) auto lemma assumes n: "n > 0" and "x > 0" shows deriv_stirling_integral_complex_of_real: "(deriv ^^ j) (stirling_integral n) (complex_of_real x) = complex_of_real ((deriv ^^ j) (stirling_integral n) x)" (is "?lhs x = ?rhs x") and differentiable_stirling_integral_real: "(deriv ^^ j) (stirling_integral n) field_differentiable at x" (is ?thesis2) proof - let ?A = "{s. Re s > 0}" let ?f = "\j x. (deriv ^^ j) (stirling_integral n) (complex_of_real x)" let ?f' = "\j x. complex_of_real ((deriv ^^ j) (stirling_integral n) x)" have [simp]: "open ?A" by (simp add: open_halfspace_Re_gt) have "?lhs x = ?rhs x \ (deriv ^^ j) (stirling_integral n) field_differentiable at x" if "x > 0" for x using that proof (induction j arbitrary: x) case 0 have "((\x. Re (stirling_integral n (of_real x))) has_field_derivative Re (deriv (\x. stirling_integral n x) (of_real x))) (at x)" using 0 n by (auto intro!: derivative_intros has_vector_derivative_real_field field_differentiable_derivI holomorphic_on_imp_differentiable_at[of _ ?A] stirling_integral_holomorphic simp: complex_nonpos_Reals_iff) also have "?this \ (stirling_integral n has_field_derivative Re (deriv (\x. stirling_integral n x) (of_real x))) (at x)" using eventually_nhds_in_open[of "{0<..}" x] 0 n by (intro has_field_derivative_cong_ev refl) (auto elim!: eventually_mono simp: stirling_integral_complex_of_real) finally have "stirling_integral n field_differentiable at x" by (auto simp: field_differentiable_def) with 0 n show ?case by (auto simp: stirling_integral_complex_of_real) next case (Suc j x) note IH = conjunct1[OF Suc.IH] conjunct2[OF Suc.IH] have *: "(deriv ^^ Suc j) (stirling_integral n) (complex_of_real x) = of_real ((deriv ^^ Suc j) (stirling_integral n) x)" if x: "x > 0" for x proof - have "deriv ((deriv ^^ j) (stirling_integral n)) (complex_of_real x) = vector_derivative (\x. (deriv ^^ j) (stirling_integral n) (of_real x)) (at x)" using n x by (intro vector_derivative_of_real_right [symmetric] holomorphic_on_imp_differentiable_at[of _ ?A] holomorphic_higher_deriv stirling_integral_holomorphic) (auto simp: complex_nonpos_Reals_iff) also have "\ = vector_derivative (\x. of_real ((deriv ^^ j) (stirling_integral n) x)) (at x)" using eventually_nhds_in_open[of "{0<..}" x] x by (intro vector_derivative_cong_eq) (auto elim!: eventually_mono simp: IH(1)) also have "\ = of_real (deriv ((deriv ^^ j) (stirling_integral n)) x)" by (intro vector_derivative_of_real_left holomorphic_on_imp_differentiable_at[of _ ?A] field_differentiable_imp_differentiable IH(2) x) finally show ?thesis by simp qed have "((\x. Re ((deriv ^^ Suc j) (stirling_integral n) (of_real x))) has_field_derivative Re (deriv ((deriv ^^ Suc j) (stirling_integral n)) (of_real x))) (at x)" using Suc.prems n by (intro derivative_intros has_vector_derivative_real_field field_differentiable_derivI holomorphic_on_imp_differentiable_at[of _ ?A] stirling_integral_holomorphic holomorphic_higher_deriv) (auto simp: complex_nonpos_Reals_iff) also have "?this \ ((deriv ^^ Suc j) (stirling_integral n) has_field_derivative Re (deriv ((deriv ^^ Suc j) (stirling_integral n)) (of_real x))) (at x)" using eventually_nhds_in_open[of "{0<..}" x] Suc.prems * by (intro has_field_derivative_cong_ev refl) (auto elim!: eventually_mono) finally have "(deriv ^^ Suc j) (stirling_integral n) field_differentiable at x" by (auto simp: field_differentiable_def) with *[OF Suc.prems] show ?case by blast qed from this[OF assms(2)] show "?lhs x = ?rhs x" ?thesis2 by blast+ qed text \ Unfortunately, asymptotic power series cannot, in general, be differentiated. However, since @{term ln_Gamma} is holomorphic on the entire positive real half-space, we can differentiate its asymptotic expansion after all. To do this, we use an ad-hoc version of the more general approach outlined in Erdelyi's ``Asymptotic Expansions'' for holomorphic functions: We bound the value of the $j$-th derivative of the remainder term at some value $x$ by applying Cauchy's integral formula along a circle centred at $x$ with radius $\frac{1}{2} x$. \ lemma deriv_stirling_integral_real_bound: assumes m: "m > 0" shows "(deriv ^^ j) (stirling_integral m) \ O(\x::real. 1 / x ^ (m + j))" proof - obtain c where c: "\s. 0 < Re s \ cmod (stirling_integral m s) \ c / Re s ^ m" using stirling_integral_bound[OF m] by auto have "0 \ cmod (stirling_integral m 1)" by simp also have "\ \ c" using c[of 1] by simp finally have c_nonneg: "c \ 0" . define B where "B = c * 2 ^ (m + Suc j)" define B' where "B' = B * fact j / 2" have "eventually (\x::real. norm ((deriv ^^ j) (stirling_integral m) x) \ B' * norm (1 / x ^ (m+ j))) at_top" using eventually_gt_at_top[of "0::real"] proof eventually_elim case (elim x) have "s \ \\<^sub>\\<^sub>0" if "s \ cball (of_real x) (x/2)" for s :: complex proof - have "x - Re s \ norm (of_real x - s)" using complex_Re_le_cmod[of "of_real x - s"] by simp also from that have "\ \ x/2" by (simp add: dist_complex_def) finally show ?thesis using elim by (auto simp: complex_nonpos_Reals_iff) qed hence "((\u. stirling_integral m u / (u - of_real x) ^ Suc j) has_contour_integral complex_of_real (2 * pi) * \ / fact j * (deriv ^^ j) (stirling_integral m) (of_real x)) (circlepath (of_real x) (x/2))" using m elim by (intro Cauchy_has_contour_integral_higher_derivative_circlepath stirling_integral_continuous_on_complex stirling_integral_holomorphic) auto hence "norm (of_real (2 * pi) * \ / fact j * (deriv ^^ j) (stirling_integral m) (of_real x)) \ B / x ^ (m + Suc j) * (2 * pi * (x / 2))" proof (rule has_contour_integral_bound_circlepath) fix u :: complex assume dist: "norm (u - of_real x) = x / 2" have "Re (of_real x - u) \ norm (of_real x - u)" by (rule complex_Re_le_cmod) also have "\ = x / 2" using dist by (simp add: norm_minus_commute) finally have Re_u: "Re u \ x/2" using elim by simp have "norm (stirling_integral m u / (u - of_real x) ^ Suc j) \ c / Re u ^ m / (x / 2) ^ Suc j" using Re_u elim unfolding norm_divide norm_power dist by (intro divide_right_mono zero_le_power c) simp_all also have "\ \ c / (x/2) ^ m / (x / 2) ^ Suc j" using c_nonneg elim Re_u by (intro divide_right_mono divide_left_mono power_mono) simp_all also have "\ = B / x ^ (m + Suc j)" using elim by (simp add: B_def field_simps power_add) finally show "norm (stirling_integral m u / (u - of_real x) ^ Suc j) \ B / x ^ (m + Suc j)" . qed (insert elim c_nonneg, auto simp: B_def simp del: power_Suc) hence "cmod ((deriv ^^ j) (stirling_integral m) (of_real x)) \ B' / x ^ (j + m)" using elim by (simp add: field_simps norm_divide norm_mult norm_power B'_def) with elim m show ?case by (simp_all add: add_ac deriv_stirling_integral_complex_of_real) qed thus ?thesis by (rule bigoI) qed definition stirling_sum where "stirling_sum j m x = (-1) ^ j * (\k = 1..k\m. (of_real (bernoulli' k) * pochhammer (of_nat (Suc k)) (j - 1) * inverse x ^ (k + j)))" lemma stirling_sum_complex_of_real: "stirling_sum j m (complex_of_real x) = complex_of_real (stirling_sum j m x)" by (simp add: stirling_sum_def pochhammer_of_real [symmetric] del: of_nat_Suc) lemma stirling_sum'_complex_of_real: "stirling_sum' j m (complex_of_real x) = complex_of_real (stirling_sum' j m x)" by (simp add: stirling_sum'_def pochhammer_of_real [symmetric] del: of_nat_Suc) lemma has_field_derivative_stirling_sum_complex [derivative_intros]: "Re x > 0 \ (stirling_sum j m has_field_derivative stirling_sum (Suc j) m x) (at x)" unfolding stirling_sum_def [abs_def] sum_distrib_left by (rule DERIV_sum) (auto intro!: derivative_eq_intros simp del: of_nat_Suc simp: pochhammer_Suc power_diff) lemma has_field_derivative_stirling_sum_real [derivative_intros]: "x > (0::real) \ (stirling_sum j m has_field_derivative stirling_sum (Suc j) m x) (at x)" unfolding stirling_sum_def [abs_def] sum_distrib_left by (rule DERIV_sum) (auto intro!: derivative_eq_intros simp del: of_nat_Suc simp: pochhammer_Suc power_diff) lemma has_field_derivative_stirling_sum'_complex [derivative_intros]: assumes "j > 0" "Re x > 0" shows "(stirling_sum' j m has_field_derivative stirling_sum' (Suc j) m x) (at x)" proof (cases j) case (Suc j') from assms have [simp]: "x \ 0" by auto define c where "c = (\n. (-1) ^ Suc j * complex_of_real (bernoulli' n) * pochhammer (of_nat (Suc n)) j')" define T where "T = (\n x. c n * inverse x ^ (j + n))" define T' where "T' = (\n x. - (of_nat (j + n)) * c n * inverse x ^ (Suc (j + n)))" have "((\x. \k\m. T k x) has_field_derivative (\k\m. T' k x)) (at x)" using assms Suc by (intro DERIV_sum) (auto simp: T_def T'_def intro!: derivative_eq_intros simp: field_simps power_add [symmetric] simp del: of_nat_Suc power_Suc of_nat_add) also have "(\x. (\k\m. T k x)) = stirling_sum' j m" by (simp add: Suc T_def c_def stirling_sum'_def fun_eq_iff add_ac mult.assoc sum_distrib_left) also have "(\k\m. T' k x) = stirling_sum' (Suc j) m x" by (simp add: T'_def c_def Suc stirling_sum'_def sum_distrib_left sum_distrib_right algebra_simps pochhammer_Suc) finally show ?thesis . qed (insert assms, simp_all) lemma has_field_derivative_stirling_sum'_real [derivative_intros]: assumes "j > 0" "x > (0::real)" shows "(stirling_sum' j m has_field_derivative stirling_sum' (Suc j) m x) (at x)" proof (cases j) case (Suc j') from assms have [simp]: "x \ 0" by auto define c where "c = (\n. (-1) ^ Suc j * (bernoulli' n) * pochhammer (of_nat (Suc n)) j')" define T where "T = (\n x. c n * inverse x ^ (j + n))" define T' where "T' = (\n x. - (of_nat (j + n)) * c n * inverse x ^ (Suc (j + n)))" have "((\x. \k\m. T k x) has_field_derivative (\k\m. T' k x)) (at x)" using assms Suc by (intro DERIV_sum) (auto simp: T_def T'_def intro!: derivative_eq_intros simp: field_simps power_add [symmetric] simp del: of_nat_Suc power_Suc of_nat_add) also have "(\x. (\k\m. T k x)) = stirling_sum' j m" by (simp add: Suc T_def c_def stirling_sum'_def fun_eq_iff add_ac mult.assoc sum_distrib_left) also have "(\k\m. T' k x) = stirling_sum' (Suc j) m x" by (simp add: T'_def c_def Suc stirling_sum'_def sum_distrib_left sum_distrib_right algebra_simps pochhammer_Suc) finally show ?thesis . qed (insert assms, simp_all) lemma higher_deriv_stirling_sum_complex: "Re x > 0 \ (deriv ^^ i) (stirling_sum j m) x = stirling_sum (i + j) m x" proof (induction i arbitrary: x) case (Suc i) have "deriv ((deriv ^^ i) (stirling_sum j m)) x = deriv (stirling_sum (i + j) m) x" using eventually_nhds_in_open[of "{x. Re x > 0}" x] Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: open_halfspace_Re_gt Suc.IH) also from Suc.prems have "\ = stirling_sum (Suc (i + j)) m x" by (intro DERIV_imp_deriv has_field_derivative_stirling_sum_complex) finally show ?case by simp qed simp_all definition Polygamma_approx :: "nat \ nat \ 'a \ 'a :: {real_normed_field, ln}" where "Polygamma_approx j m = (deriv ^^ j) (\x. (x - 1 / 2) * ln x - x + of_real (ln (2 * pi)) / 2 + stirling_sum 0 m x)" lemma Polygamma_approx_Suc: "Polygamma_approx (Suc j) m = deriv (Polygamma_approx j m)" by (simp add: Polygamma_approx_def) lemma Polygamma_approx_0: "Polygamma_approx 0 m x = (x - 1/2) * ln x - x + of_real (ln (2*pi)) / 2 + stirling_sum 0 m x" by (simp add: Polygamma_approx_def) lemma Polygamma_approx_1_complex: "Re x > 0 \ Polygamma_approx (Suc 0) m x = ln x - 1 / (2*x) + stirling_sum (Suc 0) m x" unfolding Polygamma_approx_Suc Polygamma_approx_0 by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps) lemma Polygamma_approx_1_real: "x > (0 :: real) \ Polygamma_approx (Suc 0) m x = ln x - 1 / (2*x) + stirling_sum (Suc 0) m x" unfolding Polygamma_approx_Suc Polygamma_approx_0 by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps) lemma stirling_sum_2_conv_stirling_sum'_1: fixes x :: "'a :: {real_div_algebra, field_char_0}" assumes "m > 0" "x \ 0" shows "stirling_sum' 1 m x = 1 / x + 1 / (2 * x^2) + stirling_sum 2 m x" proof - have pochhammer_2: "pochhammer (of_nat k) 2 = of_nat k * of_nat (Suc k)" for k by (simp add: pochhammer_Suc eval_nat_numeral add_ac) have "stirling_sum 2 m x = (\k = Suc 0.. = (\k=0.. = (\k=0.. = (\k\m. of_real (bernoulli' k) * inverse x ^ Suc k)" by (intro sum.cong) auto also have "\ = stirling_sum' 1 m x" by (simp add: stirling_sum'_def) finally show ?thesis by (simp add: add_ac) qed lemma Polygamma_approx_2_real: assumes "x > (0::real)" "m > 0" shows "Polygamma_approx (Suc (Suc 0)) m x = stirling_sum' 1 m x" proof - have "Polygamma_approx (Suc (Suc 0)) m x = deriv (Polygamma_approx (Suc 0) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (\x. ln x - 1 / (2*x) + stirling_sum (Suc 0) m x) x" using eventually_nhds_in_open[of "{0<..}" x] assms by (intro deriv_cong_ev) (auto elim!: eventually_mono simp: Polygamma_approx_1_real) also have "\ = 1 / x + 1 / (2*x^2) + stirling_sum (Suc (Suc 0)) m x" using assms by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps power2_eq_square) also have "\ = stirling_sum' 1 m x" using stirling_sum_2_conv_stirling_sum'_1[of m x] assms by (simp add: eval_nat_numeral) finally show ?thesis . qed lemma Polygamma_approx_2_complex: assumes "Re x > 0" "m > 0" shows "Polygamma_approx (Suc (Suc 0)) m x = stirling_sum' 1 m x" proof - have "Polygamma_approx (Suc (Suc 0)) m x = deriv (Polygamma_approx (Suc 0) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (\x. ln x - 1 / (2*x) + stirling_sum (Suc 0) m x) x" using eventually_nhds_in_open[of "{s. Re s > 0}" x] assms by (intro deriv_cong_ev) (auto simp: open_halfspace_Re_gt elim!: eventually_mono simp: Polygamma_approx_1_complex) also have "\ = 1 / x + 1 / (2*x^2) + stirling_sum (Suc (Suc 0)) m x" using assms by (intro DERIV_imp_deriv) (auto intro!: derivative_eq_intros elim!: nonpos_Reals_cases simp: field_simps power2_eq_square) also have "\ = stirling_sum' 1 m x" using stirling_sum_2_conv_stirling_sum'_1[of m x] assms by (subst stirling_sum_2_conv_stirling_sum'_1) (auto simp: eval_nat_numeral) finally show ?thesis . qed lemma Polygamma_approx_ge_2_real: assumes "x > (0::real)" "m > 0" shows "Polygamma_approx (Suc (Suc j)) m x = stirling_sum' (Suc j) m x" using assms(1) proof (induction j arbitrary: x) case (0 x) with assms show ?case by (simp add: Polygamma_approx_2_real) next case (Suc j x) have "Polygamma_approx (Suc (Suc (Suc j))) m x = deriv (Polygamma_approx (Suc (Suc j)) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (stirling_sum' (Suc j) m) x" using eventually_nhds_in_open[of "{0<..}" x] Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH) also have "\ = stirling_sum' (Suc (Suc j)) m x" using Suc.prems by (intro DERIV_imp_deriv derivative_intros) simp_all finally show ?case . qed lemma Polygamma_approx_ge_2_complex: assumes "Re x > 0" "m > 0" shows "Polygamma_approx (Suc (Suc j)) m x = stirling_sum' (Suc j) m x" using assms(1) proof (induction j arbitrary: x) case (0 x) with assms show ?case by (simp add: Polygamma_approx_2_complex) next case (Suc j x) have "Polygamma_approx (Suc (Suc (Suc j))) m x = deriv (Polygamma_approx (Suc (Suc j)) m) x" by (simp add: Polygamma_approx_Suc) also have "\ = deriv (stirling_sum' (Suc j) m) x" using eventually_nhds_in_open[of "{x. Re x > 0}" x] Suc.prems by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH open_halfspace_Re_gt) also have "\ = stirling_sum' (Suc (Suc j)) m x" using Suc.prems by (intro DERIV_imp_deriv derivative_intros) simp_all finally show ?case . qed lemma Polygamma_approx_complex_of_real: assumes "x > 0" "m > 0" shows "Polygamma_approx j m (complex_of_real x) = of_real (Polygamma_approx j m x)" proof (cases j) case 0 with assms show ?thesis by (simp add: Polygamma_approx_0 Ln_of_real stirling_sum_complex_of_real) next case [simp]: (Suc j') thus ?thesis proof (cases j') case 0 with assms show ?thesis by (simp add: Polygamma_approx_1_complex Polygamma_approx_1_real stirling_sum_complex_of_real Ln_of_real) next case (Suc j'') with assms show ?thesis by (simp add: Polygamma_approx_ge_2_complex Polygamma_approx_ge_2_real stirling_sum'_complex_of_real) qed qed lemma higher_deriv_Polygamma_approx [simp]: "(deriv ^^ j) (Polygamma_approx i m) = Polygamma_approx (j + i) m" by (simp add: Polygamma_approx_def funpow_add) lemma stirling_sum_holomorphic [holomorphic_intros]: "0 \ A \ stirling_sum j m holomorphic_on A" unfolding stirling_sum_def by (intro holomorphic_intros) auto lemma Polygamma_approx_holomorphic [holomorphic_intros]: "Polygamma_approx j m holomorphic_on {s. Re s > 0}" unfolding Polygamma_approx_def by (intro holomorphic_intros) (auto simp: open_halfspace_Re_gt elim!: nonpos_Reals_cases) lemma higher_deriv_lnGamma_stirling: assumes m: "m > 0" shows "(\x::real. (deriv ^^ j) ln_Gamma x - Polygamma_approx j m x) \ O(\x. 1 / x ^ (m + j))" proof - have "eventually (\x. \(deriv ^^ j) ln_Gamma x - Polygamma_approx j m x\ = inverse (real m) * \(deriv ^^ j) (stirling_integral m) x\) at_top" using eventually_gt_at_top[of "0::real"] proof eventually_elim case (elim x) note x = this have "\\<^sub>F y in nhds (complex_of_real x). y \ - \\<^sub>\\<^sub>0" using elim by (intro eventually_nhds_in_open) auto hence "(deriv ^^ j) (\x. ln_Gamma x - Polygamma_approx 0 m x) (complex_of_real x) = (deriv ^^ j) (\x. (-inverse (of_nat m)) * stirling_integral m x) (complex_of_real x)" using x m by (intro higher_deriv_cong_ev refl) (auto elim!: eventually_mono simp: ln_Gamma_stirling_complex Polygamma_approx_def field_simps open_halfspace_Re_gt stirling_sum_def) also have "\ = - inverse (of_nat m) * (deriv ^^ j) (stirling_integral m) (of_real x)" using x m by (intro higher_deriv_cmult[of _ "-\\<^sub>\\<^sub>0"] stirling_integral_holomorphic) (auto simp: open_halfspace_Re_gt) also have "(deriv ^^ j) (\x. ln_Gamma x - Polygamma_approx 0 m x) (complex_of_real x) = (deriv ^^ j) ln_Gamma (of_real x) - (deriv ^^ j) (Polygamma_approx 0 m) (of_real x)" using x by (intro higher_deriv_diff[of _ "{s. Re s > 0}"]) (auto intro!: holomorphic_intros elim!: nonpos_Reals_cases simp: open_halfspace_Re_gt) also have "(deriv ^^ j) (Polygamma_approx 0 m) (complex_of_real x) = of_real (Polygamma_approx j m x)" using x m by (simp add: Polygamma_approx_complex_of_real) also have "norm (- inverse (of_nat m) * (deriv ^^ j) (stirling_integral m) (complex_of_real x)) = inverse (real m) * \(deriv ^^ j) (stirling_integral m) x\" using x m by (simp add: norm_mult norm_inverse deriv_stirling_integral_complex_of_real) also have "(deriv ^^ j) ln_Gamma (complex_of_real x) = of_real ((deriv ^^ j) ln_Gamma x)" using x by (simp add: higher_deriv_ln_Gamma_complex_of_real) also have "norm (\ - of_real (Polygamma_approx j m x)) = \(deriv ^^ j) ln_Gamma x - Polygamma_approx j m x\" by (simp only: of_real_diff [symmetric] norm_of_real) finally show ?case . qed from bigthetaI_cong[OF this] m have "(\x::real. (deriv ^^ j) ln_Gamma x - Polygamma_approx j m x) \ \(\x. (deriv ^^ j) (stirling_integral m) x)" by simp also have "(\x::real. (deriv ^^ j) (stirling_integral m) x) \ O(\x. 1 / x ^ (m + j))" using m by (rule deriv_stirling_integral_real_bound) finally show ?thesis . qed lemma Polygamma_approx_1_real': assumes x: "(x::real) > 0" and m: "m > 0" shows "Polygamma_approx 1 m x = ln x - (\k = Suc 0..m. bernoulli' k * inverse x ^ k / real k)" proof - have "Polygamma_approx 1 m x = ln x - (1 / (2 * x) + (\k=Suc 0..k=Suc 0.. = (\k=0.. = (\k = Suc 0..m. bernoulli' k * inverse x ^ k / real k)" using assms by (subst sum.shift_bounds_Suc_ivl [symmetric]) (simp add: atLeastLessThanSuc_atLeastAtMost) finally show ?thesis . qed theorem assumes m: "m > 0" shows ln_Gamma_real_asymptotics: "(\x. ln_Gamma x - ((x - 1 / 2) * ln x - x + ln (2 * pi) / 2 + (\k = 1.. O(\x. 1 / x ^ m)" (is ?th1) and Digamma_real_asymptotics: "(\x. Digamma x - (ln x - (\k=1..m. bernoulli' k / real k / x ^ k))) \ O(\x. 1 / (x ^ Suc m))" (is ?th2) and Polygamma_real_asymptotics: "j > 0 \ (\x. Polygamma j x - (- 1) ^ Suc j * (\k\m. bernoulli' k * pochhammer (real (Suc k)) (j - 1) / x ^ (k + j))) \ O(\x. 1 / x ^ (m+j+1))" (is "_ \ ?th3") proof - define G :: "nat \ real \ real" where "G = (\m. if m = 0 then ln_Gamma else Polygamma (m - 1))" have *: "(\x. G j x - h x) \ O(\x. 1 / x ^ (m + j))" if "\x::real. x > 0 \ Polygamma_approx j m x = h x" for j h proof - have "(\x. G j x - h x) \ \(\x. (deriv ^^ j) ln_Gamma x - Polygamma_approx j m x)" (is "_ \ \(?f)") using that by (intro bigthetaI_cong) (auto intro: eventually_mono[OF eventually_gt_at_top[of "0::real"]] simp del: funpow.simps simp: higher_deriv_ln_Gamma_real G_def) also have "?f \ O(\x::real. 1 / x ^ (m + j))" using m by (rule higher_deriv_lnGamma_stirling) finally show ?thesis . qed note [[simproc del: simplify_landau_sum]] from *[OF Polygamma_approx_0] assms show ?th1 by (simp add: G_def Polygamma_approx_0 stirling_sum_def field_simps) from *[OF Polygamma_approx_1_real'] assms show ?th2 by (simp add: G_def field_simps) assume j: "j > 0" from *[OF Polygamma_approx_ge_2_real, of "j - 1"] assms j show ?th3 by (simp add: G_def stirling_sum'_def power_add power_diff field_simps) qed subsection \Asymptotics of the complex Gamma function\ text \ The \m\-th order remainder of Stirling's formula for $\log\Gamma$ is $O(s^{-m})$ uniformly over any complex cone $\text{Arg}(z) \leq \alpha$, $z\neq 0$ for any angle $\alpha\in(0, \pi)$. This means that there is bounded by $c z^{-m}$ for some constant $c$ for all $z$ in this cone. \ context fixes F and \ assumes \: "\ \ {0<.. principal (complex_cone' \ - {0})" begin lemma stirling_integral_bigo: fixes m :: nat assumes m: "m > 0" shows "stirling_integral m \ O[F](\s. 1 / s ^ m)" proof - obtain c where c: "\s. s \ complex_cone' \ - {0} \ norm (stirling_integral m s) \ c / norm s ^ m" using stirling_integral_bound'[OF \m > 0\ \] by blast have "0 \ norm (stirling_integral m 1 :: complex)" by simp also have "\ \ c" using c[of 1] \ by simp finally have "c \ 0" . have "eventually (\s. s \ complex_cone' \ - {0}) F" unfolding F_def by (auto simp: eventually_principal) hence "eventually (\s. norm (stirling_integral m s) \ c * norm (1 / s ^ m)) F" by eventually_elim (use c in \simp add: norm_divide norm_power\) thus "stirling_integral m \ O[F](\s. 1 / s ^ m)" by (intro bigoI[of _ c]) auto qed end text \ The following is a more explicit statement of this: \ theorem ln_Gamma_complex_asymptotics_explicit: fixes m :: nat and \ :: real assumes "m > 0" and "\ \ {0<.. complex" where "\s::complex. s \ \\<^sub>\\<^sub>0 \ ln_Gamma s = (s - 1/2) * ln s - s + ln (2 * pi) / 2 + (\k=1..s. s \ 0 \ \Arg s\ \ \ \ norm (R s) \ C / norm s ^ m" proof - obtain c where c: "\s. s \ complex_cone' \ - {0} \ norm (stirling_integral m s) \ c / norm s ^ m" using stirling_integral_bound'[OF assms] by blast have "0 \ norm (stirling_integral m 1 :: complex)" by simp also have "\ \ c" using c[of 1] assms by simp finally have "c \ 0" . define R where "R = (\s::complex. stirling_integral m s / of_nat m)" show ?thesis proof (rule that) from ln_Gamma_stirling_complex[of _ m] assms show "\s::complex. s \ \\<^sub>\\<^sub>0 \ ln_Gamma s = (s - 1 / 2) * ln s - s + ln (2 * pi) / 2 + (\k=1..s. s \ 0 \ \Arg s\ \ \ \ cmod (R s) \ c / real m / cmod s ^ m" proof (safe, goal_cases) case (1 s) show ?case using 1 c[of s] assms by (auto simp: complex_cone_altdef abs_le_iff R_def norm_divide field_simps) qed qed qed text \ Lastly, we can also derive the asymptotics of $\Gamma$ itself: \[\Gamma(z) \sim \sqrt{2\pi / z} \left(\frac{z}{e}\right)^z\] uniformly for $|z|\to\infty$ within the cone $\text{Arg}(z) \leq \alpha$ for $\alpha\in(0,\pi)$: \ context fixes F and \ assumes \: "\ \ {0<.. inf at_infinity (principal (complex_cone' \))" begin lemma Gamma_complex_asymp_equiv: "Gamma \[F] (\s. sqrt (2 * pi) * (s / exp 1) powr s / s powr (1 / 2))" proof - define I :: "complex \ complex" where "I = stirling_integral 1" have "eventually (\s. s \ complex_cone' \) F" by (auto simp: eventually_inf_principal F_def) moreover have "eventually (\s. s \ 0) F" unfolding F_def eventually_inf_principal using eventually_not_equal_at_infinity by eventually_elim auto ultimately have "eventually (\s. Gamma s = sqrt (2 * pi) * (s / exp 1) powr s / s powr (1 / 2) / exp (I s)) F" proof eventually_elim case (elim s) from elim have s': "s \ \\<^sub>\\<^sub>0" using complex_cone_inter_nonpos_Reals[of "-\" \] \ by auto from elim have [simp]: "s \ 0" by auto from s' have "Gamma s = exp (ln_Gamma s)" unfolding Gamma_complex_altdef using nonpos_Ints_subset_nonpos_Reals by auto also from s' have "ln_Gamma s = (s-1/2) * Ln s - s + complex_of_real (ln (2 * pi) / 2) - I s" by (subst ln_Gamma_stirling_complex[of _ 1]) (simp_all add: exp_add exp_diff I_def) also have "exp \ = exp ((s - 1 / 2) * Ln s) / exp s * exp (complex_of_real (ln (2 * pi) / 2)) / exp (I s)" unfolding exp_diff exp_add by (simp add: exp_diff exp_add) also have "exp ((s - 1 / 2) * Ln s) = s powr (s - 1 / 2)" by (simp add: powr_def) also have "exp (complex_of_real (ln (2 * pi) / 2)) = sqrt (2 * pi)" by (subst exp_of_real) (auto simp: powr_def simp flip: powr_half_sqrt) also have "exp s = exp 1 powr s" by (simp add: powr_def) also have "s powr (s - 1 / 2) / exp 1 powr s = (s powr s / exp 1 powr s) / s powr (1/2)" by (subst powr_diff) auto also have *: "Ln (s / exp 1) = Ln s - 1" using Ln_divide_of_real[of "exp 1" s] by (simp flip: exp_of_real) hence "s powr s / exp 1 powr s = (s / exp 1) powr s" unfolding powr_def by (subst *) (auto simp: exp_diff field_simps) finally show "Gamma s = sqrt (2 * pi) * (s / exp 1) powr s / s powr (1 / 2) / exp (I s)" by (simp add: algebra_simps) qed hence "Gamma \[F] (\s. sqrt (2 * pi) * (s / exp 1) powr s / s powr (1 / 2) / exp (I s))" by (rule asymp_equiv_refl_ev) also have "\ \[F] (\s. sqrt (2 * pi) * (s / exp 1) powr s / s powr (1 / 2) / 1)" proof (intro asymp_equiv_intros) have "F \ principal (complex_cone' \ - {0})" unfolding le_principal F_def eventually_inf_principal using eventually_not_equal_at_infinity by eventually_elim auto moreover have "I \ O[principal (complex_cone' \ - {0})](\s. 1 / s)" using stirling_integral_bigo[of \ 1] \ unfolding F_def by (simp add: I_def) ultimately have "I \ O[F](\s. 1 / s)" by (rule landau_o.big.filter_mono) also have "(\s. 1 / s) \ o[F](\s. 1)" proof (rule landau_o.smallI) fix c :: real assume c: "c > 0" hence "eventually (\z::complex. norm z \ 1 / c) at_infinity" by (auto simp: eventually_at_infinity) moreover have "eventually (\z::complex. z \ 0) at_infinity" by (rule eventually_not_equal_at_infinity) ultimately show "eventually (\z::complex. norm (1 / z) \ c * norm (1 :: complex)) F" unfolding F_def eventually_inf_principal by eventually_elim (use \c > 0\ in \auto simp: norm_divide field_simps\) qed finally have "I \ o[F](\s. 1)" . from smalloD_tendsto[OF this] have [tendsto_intros]: "(I \ 0) F" by simp show "(\x. exp (I x)) \[F] (\x. 1)" by (rule asymp_equivI' tendsto_eq_intros refl | simp)+ qed finally show ?thesis by simp qed end end diff --git a/thys/Word_Lib/More_Word.thy b/thys/Word_Lib/More_Word.thy --- a/thys/Word_Lib/More_Word.thy +++ b/thys/Word_Lib/More_Word.thy @@ -1,2550 +1,2546 @@ (* * Copyright Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section \Lemmas on words\ theory More_Word imports "HOL-Library.Word" More_Arithmetic More_Divides begin context includes bit_operations_syntax begin \ \problem posed by TPHOLs referee: criterion for overflow of addition of signed integers\ lemma sofl_test: \sint x + sint y = sint (x + y) \ drop_bit (size x - 1) ((x + y XOR x) AND (x + y XOR y)) = 0\ for x y :: \'a::len word\ proof - obtain n where n: \LENGTH('a) = Suc n\ by (cases \LENGTH('a)\) simp_all have *: \sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \ sint x + sint y \ - (2 ^ n)\ \signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \ 2 ^ n > sint x + sint y\ using signed_take_bit_int_greater_eq [of \sint x + sint y\ n] signed_take_bit_int_less_eq [of n \sint x + sint y\] by (auto intro: ccontr) have \sint x + sint y = sint (x + y) \ (sint (x + y) < 0 \ sint x < 0) \ (sint (x + y) < 0 \ sint y < 0)\ using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y] signed_take_bit_int_eq_self [of \LENGTH('a) - 1\ \sint x + sint y\] apply (auto simp add: not_less) apply (unfold sint_word_ariths) apply (subst signed_take_bit_int_eq_self) prefer 4 apply (subst signed_take_bit_int_eq_self) prefer 7 apply (subst signed_take_bit_int_eq_self) prefer 10 apply (subst signed_take_bit_int_eq_self) apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *) - apply (smt (z3) take_bit_nonnegative) - apply (smt (z3) take_bit_int_less_exp) - apply (smt (z3) take_bit_nonnegative) - apply (smt (z3) take_bit_int_less_exp) done then show ?thesis apply (simp only: One_nat_def word_size drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff) apply (simp add: bit_last_iff) done qed lemma unat_power_lower [simp]: "unat ((2::'a::len word) ^ n) = 2 ^ n" if "n < LENGTH('a::len)" using that by transfer simp lemma unat_p2: "n < LENGTH('a :: len) \ unat (2 ^ n :: 'a word) = 2 ^ n" by (fact unat_power_lower) lemma word_div_lt_eq_0: "x < y \ x div y = 0" for x :: "'a :: len word" by transfer simp lemma word_div_eq_1_iff: "n div m = 1 \ n \ m \ unat n < 2 * unat (m :: 'a :: len word)" apply (simp only: word_arith_nat_defs word_le_nat_alt word_of_nat_eq_iff flip: nat_div_eq_Suc_0_iff) apply (simp flip: unat_div unsigned_take_bit_eq) done lemma AND_twice [simp]: "(w AND m) AND m = w AND m" by (fact and.right_idem) lemma word_combine_masks: "w AND m = z \ w AND m' = z' \ w AND (m OR m') = (z OR z')" for w m m' z z' :: \'a::len word\ by (simp add: bit.conj_disj_distrib) lemma p2_gt_0: "(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))" by (simp add : word_gt_0 not_le) lemma uint_2p_alt: \n < LENGTH('a::len) \ uint ((2::'a::len word) ^ n) = 2 ^ n\ using p2_gt_0 [of n, where ?'a = 'a] by (simp add: uint_2p) lemma p2_eq_0: \(2::'a::len word) ^ n = 0 \ LENGTH('a::len) \ n\ by (fact exp_eq_zero_iff) lemma p2len: \(2 :: 'a word) ^ LENGTH('a::len) = 0\ by simp lemma neg_mask_is_div: "w AND NOT (mask n) = (w div 2^n) * 2^n" for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps simp flip: push_bit_eq_mult drop_bit_eq_div) lemma neg_mask_is_div': "n < size w \ w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))" for w :: \'a::len word\ by (rule neg_mask_is_div) lemma and_mask_arith: "w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)" for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps word_size simp flip: push_bit_eq_mult drop_bit_eq_div) lemma and_mask_arith': "0 < n \ w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)" for w :: \'a::len word\ by (rule and_mask_arith) lemma mask_2pm1: "mask n = 2 ^ n - (1 :: 'a::len word)" by (fact mask_eq_decr_exp) lemma add_mask_fold: "x + 2 ^ n - 1 = x + mask n" for x :: \'a::len word\ by (simp add: mask_eq_decr_exp) lemma word_and_mask_le_2pm1: "w AND mask n \ 2 ^ n - 1" for w :: \'a::len word\ by (simp add: mask_2pm1[symmetric] word_and_le1) lemma is_aligned_AND_less_0: "u AND mask n = 0 \ v < 2^n \ u AND v = 0" for u v :: \'a::len word\ apply (drule less_mask_eq) apply (simp flip: take_bit_eq_mask) apply (simp add: bit_eq_iff) apply (auto simp add: bit_simps) done lemma and_mask_eq_iff_le_mask: \w AND mask n = w \ w \ mask n\ for w :: \'a::len word\ apply (simp flip: take_bit_eq_mask) apply (cases \n \ LENGTH('a)\; transfer) apply (simp_all add: not_le min_def) apply (simp_all add: mask_eq_exp_minus_1) apply auto apply (metis take_bit_int_less_exp) apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit) done lemma less_eq_mask_iff_take_bit_eq_self: \w \ mask n \ take_bit n w = w\ for w :: \'a::len word\ by (simp add: and_mask_eq_iff_le_mask take_bit_eq_mask) lemma NOT_eq: "NOT (x :: 'a :: len word) = - x - 1" apply (cut_tac x = "x" in word_add_not) apply (drule add.commute [THEN trans]) apply (drule eq_diff_eq [THEN iffD2]) by simp lemma NOT_mask: "NOT (mask n :: 'a::len word) = - (2 ^ n)" by (simp add : NOT_eq mask_2pm1) lemma le_m1_iff_lt: "(x > (0 :: 'a :: len word)) = ((y \ x - 1) = (y < x))" by uint_arith lemma gt0_iff_gem1: \0 < x \ x - 1 < x\ for x :: \'a::len word\ by (metis add.right_neutral diff_add_cancel less_irrefl measure_unat unat_arith_simps(2) word_neq_0_conv word_sub_less_iff) lemma power_2_ge_iff: \2 ^ n - (1 :: 'a::len word) < 2 ^ n \ n < LENGTH('a)\ using gt0_iff_gem1 p2_gt_0 by blast lemma le_mask_iff_lt_2n: "n < len_of TYPE ('a) = (((w :: 'a :: len word) \ mask n) = (w < 2 ^ n))" unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt]) lemma mask_lt_2pn: \n < LENGTH('a) \ mask n < (2 :: 'a::len word) ^ n\ by (simp add: mask_eq_exp_minus_1 power_2_ge_iff) lemma word_unat_power: "(2 :: 'a :: len word) ^ n = of_nat (2 ^ n)" by simp lemma of_nat_mono_maybe: assumes xlt: "x < 2 ^ len_of TYPE ('a)" shows "y < x \ of_nat y < (of_nat x :: 'a :: len word)" apply (subst word_less_nat_alt) apply (subst unat_of_nat)+ apply (subst mod_less) apply (erule order_less_trans [OF _ xlt]) apply (subst mod_less [OF xlt]) apply assumption done lemma word_and_max_word: fixes a::"'a::len word" shows "x = - 1 \ a AND x = a" by simp lemma word_and_full_mask_simp: \x AND mask LENGTH('a) = x\ for x :: \'a::len word\ by (simp add: bit_eq_iff bit_simps) lemma of_int_uint: "of_int (uint x) = x" by (fact word_of_int_uint) corollary word_plus_and_or_coroll: "x AND y = 0 \ x + y = x OR y" for x y :: \'a::len word\ using word_plus_and_or[where x=x and y=y] by simp corollary word_plus_and_or_coroll2: "(x AND w) + (x AND NOT w) = x" for x w :: \'a::len word\ apply (subst disjunctive_add) apply (simp add: bit_simps) apply (simp flip: bit.conj_disj_distrib) done lemma unat_mask_eq: \unat (mask n :: 'a::len word) = mask (min LENGTH('a) n)\ by transfer (simp add: nat_mask_eq) lemma word_plus_mono_left: fixes x :: "'a :: len word" shows "\y \ z; x \ x + z\ \ y + x \ z + x" by unat_arith lemma less_Suc_unat_less_bound: "n < Suc (unat (x :: 'a :: len word)) \ n < 2 ^ LENGTH('a)" by (auto elim!: order_less_le_trans intro: Suc_leI) lemma up_ucast_inj: "\ ucast x = (ucast y::'b::len word); LENGTH('a) \ len_of TYPE ('b) \ \ x = (y::'a::len word)" by transfer (simp add: min_def split: if_splits) lemmas ucast_up_inj = up_ucast_inj lemma up_ucast_inj_eq: "LENGTH('a) \ len_of TYPE ('b) \ (ucast x = (ucast y::'b::len word)) = (x = (y::'a::len word))" by (fastforce dest: up_ucast_inj) lemma no_plus_overflow_neg: "(x :: 'a :: len word) < -y \ x \ x + y" by (metis diff_minus_eq_add less_imp_le sub_wrap_lt) lemma ucast_ucast_eq: "\ ucast x = (ucast (ucast y::'a word)::'c::len word); LENGTH('a) \ LENGTH('b); LENGTH('b) \ LENGTH('c) \ \ x = ucast y" for x :: "'a::len word" and y :: "'b::len word" apply transfer apply (cases \LENGTH('c) = LENGTH('a)\) apply (auto simp add: min_def) done lemma ucast_0_I: "x = 0 \ ucast x = 0" by simp lemma word_add_offset_less: fixes x :: "'a :: len word" assumes yv: "y < 2 ^ n" and xv: "x < 2 ^ m" and mnv: "sz < LENGTH('a :: len)" and xv': "x < 2 ^ (LENGTH('a :: len) - n)" and mn: "sz = m + n" shows "x * 2 ^ n + y < 2 ^ sz" proof (subst mn) from mnv mn have nv: "n < LENGTH('a)" and mv: "m < LENGTH('a)" by auto have uy: "unat y < 2 ^ n" by (rule order_less_le_trans [OF unat_mono [OF yv] order_eq_refl], rule unat_power_lower[OF nv]) have ux: "unat x < 2 ^ m" by (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl], rule unat_power_lower[OF mv]) then show "x * 2 ^ n + y < 2 ^ (m + n)" using ux uy nv mnv xv' apply (subst word_less_nat_alt) apply (subst unat_word_ariths)+ apply (subst mod_less) apply simp apply (subst mult.commute) apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]]) apply (rule order_less_le_trans [OF unat_mono [OF xv']]) apply (cases "n = 0"; simp) apply (subst unat_power_lower[OF nv]) apply (subst mod_less) apply (erule order_less_le_trans [OF nat_add_offset_less], assumption) apply (rule mn) apply simp apply (simp add: mn mnv) apply (erule nat_add_offset_less; simp) done qed lemma word_less_power_trans: fixes n :: "'a :: len word" assumes nv: "n < 2 ^ (m - k)" and kv: "k \ m" and mv: "m < len_of TYPE ('a)" shows "2 ^ k * n < 2 ^ m" using nv kv mv apply - apply (subst word_less_nat_alt) apply (subst unat_word_ariths) apply (subst mod_less) apply simp apply (rule nat_less_power_trans) apply (erule order_less_trans [OF unat_mono]) apply simp apply simp apply simp apply (rule nat_less_power_trans) apply (subst unat_power_lower[where 'a = 'a, symmetric]) apply simp apply (erule unat_mono) apply simp done lemma word_less_power_trans2: fixes n :: "'a::len word" shows "\n < 2 ^ (m - k); k \ m; m < LENGTH('a)\ \ n * 2 ^ k < 2 ^ m" by (subst field_simps, rule word_less_power_trans) lemma Suc_unat_diff_1: fixes x :: "'a :: len word" assumes lt: "1 \ x" shows "Suc (unat (x - 1)) = unat x" proof - have "0 < unat x" by (rule order_less_le_trans [where y = 1], simp, subst unat_1 [symmetric], rule iffD1 [OF word_le_nat_alt lt]) then show ?thesis by ((subst unat_sub [OF lt])+, simp only: unat_1) qed lemma word_eq_unatI: \v = w\ if \unat v = unat w\ using that by transfer (simp add: nat_eq_iff) lemma word_div_sub: fixes x :: "'a :: len word" assumes yx: "y \ x" and y0: "0 < y" shows "(x - y) div y = x div y - 1" apply (rule word_eq_unatI) apply (subst unat_div) apply (subst unat_sub [OF yx]) apply (subst unat_sub) apply (subst word_le_nat_alt) apply (subst unat_div) apply (subst le_div_geq) apply (rule order_le_less_trans [OF _ unat_mono [OF y0]]) apply simp apply (subst word_le_nat_alt [symmetric], rule yx) apply simp apply (subst unat_div) apply (subst le_div_geq [OF _ iffD1 [OF word_le_nat_alt yx]]) apply (rule order_le_less_trans [OF _ unat_mono [OF y0]]) apply simp apply simp done lemma word_mult_less_mono1: fixes i :: "'a :: len word" assumes ij: "i < j" and knz: "0 < k" and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)" shows "i * k < j * k" proof - from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)" by (auto intro: order_less_subst2 simp: word_less_nat_alt elim: mult_less_mono1) then show ?thesis using ujk knz ij by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem]) qed lemma word_mult_less_dest: fixes i :: "'a :: len word" assumes ij: "i * k < j * k" and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)" shows "i < j" using uik ujk ij by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem] elim: mult_less_mono1) lemma word_mult_less_cancel: fixes k :: "'a :: len word" assumes knz: "0 < k" and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)" shows "(i * k < j * k) = (i < j)" by (rule iffI [OF word_mult_less_dest [OF _ uik ujk] word_mult_less_mono1 [OF _ knz ujk]]) lemma Suc_div_unat_helper: assumes szv: "sz < LENGTH('a :: len)" and usszv: "us \ sz" shows "2 ^ (sz - us) = Suc (unat (((2::'a :: len word) ^ sz - 1) div 2 ^ us))" proof - note usv = order_le_less_trans [OF usszv szv] from usszv obtain q where qv: "sz = us + q" by (auto simp: le_iff_add) have "Suc (unat (((2:: 'a word) ^ sz - 1) div 2 ^ us)) = (2 ^ us + unat ((2:: 'a word) ^ sz - 1)) div 2 ^ us" apply (subst unat_div unat_power_lower[OF usv])+ apply (subst div_add_self1, simp+) done also have "\ = ((2 ^ us - 1) + 2 ^ sz) div 2 ^ us" using szv by (simp add: unat_minus_one) also have "\ = 2 ^ q + ((2 ^ us - 1) div 2 ^ us)" apply (subst qv) apply (subst power_add) apply (subst div_mult_self2; simp) done also have "\ = 2 ^ (sz - us)" using qv by simp finally show ?thesis .. qed lemma enum_word_nth_eq: \(Enum.enum :: 'a::len word list) ! n = word_of_nat n\ if \n < 2 ^ LENGTH('a)\ for n using that by (simp add: enum_word_def) lemma length_enum_word_eq: \length (Enum.enum :: 'a::len word list) = 2 ^ LENGTH('a)\ by (simp add: enum_word_def) lemma unat_lt2p [iff]: \unat x < 2 ^ LENGTH('a)\ for x :: \'a::len word\ by transfer simp lemma of_nat_unat [simp]: "of_nat \ unat = id" by (rule ext, simp) lemma Suc_unat_minus_one [simp]: "x \ 0 \ Suc (unat (x - 1)) = unat x" by (metis Suc_diff_1 unat_gt_0 unat_minus_one) lemma word_add_le_dest: fixes i :: "'a :: len word" assumes le: "i + k \ j + k" and uik: "unat i + unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)" shows "i \ j" using uik ujk le by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem] elim: add_le_mono1) lemma word_add_le_mono1: fixes i :: "'a :: len word" assumes ij: "i \ j" and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)" shows "i + k \ j + k" proof - from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)" by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: add_le_mono1) then show ?thesis using ujk ij by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem]) qed lemma word_add_le_mono2: fixes i :: "'a :: len word" shows "\i \ j; unat j + unat k < 2 ^ LENGTH('a)\ \ k + i \ k + j" by (subst field_simps, subst field_simps, erule (1) word_add_le_mono1) lemma word_add_le_iff: fixes i :: "'a :: len word" assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)" shows "(i + k \ j + k) = (i \ j)" proof assume "i \ j" show "i + k \ j + k" by (rule word_add_le_mono1) fact+ next assume "i + k \ j + k" show "i \ j" by (rule word_add_le_dest) fact+ qed lemma word_add_less_mono1: fixes i :: "'a :: len word" assumes ij: "i < j" and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)" shows "i + k < j + k" proof - from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)" by (auto elim: order_le_less_subst2 simp: word_less_nat_alt elim: add_less_mono1) then show ?thesis using ujk ij by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem]) qed lemma word_add_less_dest: fixes i :: "'a :: len word" assumes le: "i + k < j + k" and uik: "unat i + unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)" shows "i < j" using uik ujk le by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem] elim: add_less_mono1) lemma word_add_less_iff: fixes i :: "'a :: len word" assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)" shows "(i + k < j + k) = (i < j)" proof assume "i < j" show "i + k < j + k" by (rule word_add_less_mono1) fact+ next assume "i + k < j + k" show "i < j" by (rule word_add_less_dest) fact+ qed lemma word_mult_less_iff: fixes i :: "'a :: len word" assumes knz: "0 < k" and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)" shows "(i * k < j * k) = (i < j)" using assms by (rule word_mult_less_cancel) lemma word_le_imp_diff_le: fixes n :: "'a::len word" shows "\k \ n; n \ m\ \ n - k \ m" by (auto simp: unat_sub word_le_nat_alt) lemma word_less_imp_diff_less: fixes n :: "'a::len word" shows "\k \ n; n < m\ \ n - k < m" by (clarsimp simp: unat_sub word_less_nat_alt intro!: less_imp_diff_less) lemma word_mult_le_mono1: fixes i :: "'a :: len word" assumes ij: "i \ j" and knz: "0 < k" and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)" shows "i * k \ j * k" proof - from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)" by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: mult_le_mono1) then show ?thesis using ujk knz ij by (auto simp: word_le_nat_alt iffD1 [OF unat_mult_lem]) qed lemma word_mult_le_iff: fixes i :: "'a :: len word" assumes knz: "0 < k" and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)" and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)" shows "(i * k \ j * k) = (i \ j)" proof assume "i \ j" show "i * k \ j * k" by (rule word_mult_le_mono1) fact+ next assume p: "i * k \ j * k" have "0 < unat k" using knz by (simp add: word_less_nat_alt) then show "i \ j" using p by (clarsimp simp: word_le_nat_alt iffD1 [OF unat_mult_lem uik] iffD1 [OF unat_mult_lem ujk]) qed lemma word_diff_less: fixes n :: "'a :: len word" shows "\0 < n; 0 < m; n \ m\ \ m - n < m" apply (subst word_less_nat_alt) apply (subst unat_sub) apply assumption apply (rule diff_less) apply (simp_all add: word_less_nat_alt) done lemma word_add_increasing: fixes x :: "'a :: len word" shows "\ p + w \ x; p \ p + w \ \ p \ x" by unat_arith lemma word_random: fixes x :: "'a :: len word" shows "\ p \ p + x'; x \ x' \ \ p \ p + x" by unat_arith lemma word_sub_mono: "\ a \ c; d \ b; a - b \ a; c - d \ c \ \ (a - b) \ (c - d :: 'a :: len word)" by unat_arith lemma power_not_zero: "n < LENGTH('a::len) \ (2 :: 'a word) ^ n \ 0" by (metis p2_gt_0 word_neq_0_conv) lemma word_gt_a_gt_0: "a < n \ (0 :: 'a::len word) < n" apply (case_tac "n = 0") apply clarsimp apply (clarsimp simp: word_neq_0_conv) done lemma word_power_less_1 [simp]: "sz < LENGTH('a::len) \ (2::'a word) ^ sz - 1 < 2 ^ sz" apply (simp add: word_less_nat_alt) apply (subst unat_minus_one) apply simp_all done lemma word_sub_1_le: "x \ 0 \ x - 1 \ (x :: ('a :: len) word)" apply (subst no_ulen_sub) apply simp apply (cases "uint x = 0") apply (simp add: uint_0_iff) apply (insert uint_ge_0[where x=x]) apply arith done lemma push_bit_word_eq_nonzero: \push_bit n w \ 0\ if \w < 2 ^ m\ \m + n < LENGTH('a)\ \w \ 0\ for w :: \'a::len word\ using that apply (simp only: word_neq_0_conv word_less_nat_alt mod_0 unat_word_ariths unat_power_lower word_le_nat_alt) apply (metis add_diff_cancel_right' gr0I gr_implies_not0 less_or_eq_imp_le min_def push_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_push_bit take_bit_take_bit unsigned_push_bit_eq) done lemma unat_less_power: fixes k :: "'a::len word" assumes szv: "sz < LENGTH('a)" and kv: "k < 2 ^ sz" shows "unat k < 2 ^ sz" using szv unat_mono [OF kv] by simp lemma unat_mult_power_lem: assumes kv: "k < 2 ^ (LENGTH('a::len) - sz)" shows "unat (2 ^ sz * of_nat k :: (('a::len) word)) = 2 ^ sz * k" proof (cases \sz < LENGTH('a)\) case True with assms show ?thesis by (simp add: unat_word_ariths take_bit_eq_mod mod_simps unsigned_of_nat) (simp add: take_bit_nat_eq_self_iff nat_less_power_trans flip: take_bit_eq_mod) next case False with assms show ?thesis by simp qed lemma word_plus_mcs_4: "\v + x \ w + x; x \ v + x\ \ v \ (w::'a::len word)" by uint_arith lemma word_plus_mcs_3: "\v \ w; x \ w + x\ \ v + x \ w + (x::'a::len word)" by unat_arith lemma word_le_minus_one_leq: "x < y \ x \ y - 1" for x :: "'a :: len word" by transfer (metis le_less_trans less_irrefl take_bit_decr_eq take_bit_nonnegative zle_diff1_eq) lemma word_less_sub_le[simp]: fixes x :: "'a :: len word" assumes nv: "n < LENGTH('a)" shows "(x \ 2 ^ n - 1) = (x < 2 ^ n)" using le_less_trans word_le_minus_one_leq nv power_2_ge_iff by blast lemma unat_of_nat_len: "x < 2 ^ LENGTH('a) \ unat (of_nat x :: 'a::len word) = x" by (simp add: unsigned_of_nat take_bit_nat_eq_self_iff) lemma unat_of_nat_eq: "x < 2 ^ LENGTH('a) \ unat (of_nat x ::'a::len word) = x" by (rule unat_of_nat_len) lemma unat_eq_of_nat: "n < 2 ^ LENGTH('a) \ (unat (x :: 'a::len word) = n) = (x = of_nat n)" by transfer (auto simp add: take_bit_of_nat nat_eq_iff take_bit_nat_eq_self_iff intro: sym) lemma alignUp_div_helper: fixes a :: "'a::len word" assumes kv: "k < 2 ^ (LENGTH('a) - n)" and xk: "x = 2 ^ n * of_nat k" and le: "a \ x" and sz: "n < LENGTH('a)" and anz: "a mod 2 ^ n \ 0" shows "a div 2 ^ n < of_nat k" proof - have kn: "unat (of_nat k :: 'a word) * unat ((2::'a word) ^ n) < 2 ^ LENGTH('a)" using xk kv sz apply (subst unat_of_nat_eq) apply (erule order_less_le_trans) apply simp apply (subst unat_power_lower, simp) apply (subst mult.commute) apply (rule nat_less_power_trans) apply simp apply simp done have "unat a div 2 ^ n * 2 ^ n \ unat a" proof - have "unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n" by (simp add: div_mult_mod_eq) also have "\ \ unat a div 2 ^ n * 2 ^ n" using sz anz by (simp add: unat_arith_simps) finally show ?thesis .. qed then have "a div 2 ^ n * 2 ^ n < a" using sz anz apply (subst word_less_nat_alt) apply (subst unat_word_ariths) apply (subst unat_div) apply simp apply (rule order_le_less_trans [OF mod_less_eq_dividend]) apply (erule order_le_neq_trans [OF div_mult_le]) done also from xk le have "\ \ of_nat k * 2 ^ n" by (simp add: field_simps) finally show ?thesis using sz kv apply - apply (erule word_mult_less_dest [OF _ _ kn]) apply (simp add: unat_div) apply (rule order_le_less_trans [OF div_mult_le]) apply (rule unat_lt2p) done qed lemma mask_out_sub_mask: "(x AND NOT (mask n)) = x - (x AND (mask n))" for x :: \'a::len word\ by (simp add: field_simps word_plus_and_or_coroll2) lemma subtract_mask: "p - (p AND mask n) = (p AND NOT (mask n))" "p - (p AND NOT (mask n)) = (p AND mask n)" for p :: \'a::len word\ by (simp add: field_simps word_plus_and_or_coroll2)+ lemma take_bit_word_eq_self_iff: \take_bit n w = w \ n \ LENGTH('a) \ w < 2 ^ n\ for w :: \'a::len word\ using take_bit_int_eq_self_iff [of n \take_bit LENGTH('a) (uint w)\] by (transfer fixing: n) auto lemma word_power_increasing: assumes x: "2 ^ x < (2 ^ y::'a::len word)" "x < LENGTH('a::len)" "y < LENGTH('a::len)" shows "x < y" using x using assms by transfer simp lemma mask_twice: "(x AND mask n) AND mask m = x AND mask (min m n)" for x :: \'a::len word\ by (simp flip: take_bit_eq_mask) lemma plus_one_helper[elim!]: "x < n + (1 :: 'a :: len word) \ x \ n" apply (simp add: word_less_nat_alt word_le_nat_alt field_simps) apply (case_tac "1 + n = 0") apply simp_all apply (subst(asm) unatSuc, assumption) apply arith done lemma plus_one_helper2: "\ x \ n; n + 1 \ 0 \ \ x < n + (1 :: 'a :: len word)" by (simp add: word_less_nat_alt word_le_nat_alt field_simps unatSuc) lemma less_x_plus_1: fixes x :: "'a :: len word" shows "x \ - 1 \ (y < (x + 1)) = (y < x \ y = x)" apply (rule iffI) apply (rule disjCI) apply (drule plus_one_helper) apply simp apply (subgoal_tac "x < x + 1") apply (erule disjE, simp_all) apply (rule plus_one_helper2 [OF order_refl]) apply (rule notI, drule max_word_wrap) apply simp done lemma word_Suc_leq: fixes k::"'a::len word" shows "k \ - 1 \ x < k + 1 \ x \ k" using less_x_plus_1 word_le_less_eq by auto lemma word_Suc_le: fixes k::"'a::len word" shows "x \ - 1 \ x + 1 \ k \ x < k" by (meson not_less word_Suc_leq) lemma word_lessThan_Suc_atMost: \{..< k + 1} = {..k}\ if \k \ - 1\ for k :: \'a::len word\ using that by (simp add: lessThan_def atMost_def word_Suc_leq) lemma word_atLeastLessThan_Suc_atLeastAtMost: \{l ..< u + 1} = {l..u}\ if \u \ - 1\ for l :: \'a::len word\ using that by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost) lemma word_atLeastAtMost_Suc_greaterThanAtMost: \{m<..u} = {m + 1..u}\ if \m \ - 1\ for m :: \'a::len word\ using that by (simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le) lemma word_atLeastLessThan_Suc_atLeastAtMost_union: fixes l::"'a::len word" assumes "m \ - 1" and "l \ m" and "m \ u" shows "{l..m} \ {m+1..u} = {l..u}" proof - from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} \ {m<..u}" by blast with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost) qed lemma max_word_less_eq_iff [simp]: \- 1 \ w \ w = - 1\ for w :: \'a::len word\ by (fact word_order.extremum_unique) lemma word_or_zero: "(a OR b = 0) = (a = 0 \ b = 0)" for a b :: \'a::len word\ by (fact or_eq_0_iff) lemma word_2p_mult_inc: assumes x: "2 * 2 ^ n < (2::'a::len word) * 2 ^ m" assumes suc_n: "Suc n < LENGTH('a::len)" shows "2^n < (2::'a::len word)^m" by (smt suc_n le_less_trans lessI nat_less_le nat_mult_less_cancel_disj p2_gt_0 power_Suc power_Suc unat_power_lower word_less_nat_alt x) lemma power_overflow: "n \ LENGTH('a) \ 2 ^ n = (0 :: 'a::len word)" by simp lemmas extra_sle_sless_unfolds [simp] = word_sle_eq[where a=0 and b=1] word_sle_eq[where a=0 and b="numeral n"] word_sle_eq[where a=1 and b=0] word_sle_eq[where a=1 and b="numeral n"] word_sle_eq[where a="numeral n" and b=0] word_sle_eq[where a="numeral n" and b=1] word_sless_alt[where a=0 and b=1] word_sless_alt[where a=0 and b="numeral n"] word_sless_alt[where a=1 and b=0] word_sless_alt[where a=1 and b="numeral n"] word_sless_alt[where a="numeral n" and b=0] word_sless_alt[where a="numeral n" and b=1] for n lemma word_sint_1: "sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)" by (fact signed_1) lemma ucast_of_nat: "is_down (ucast :: 'a :: len word \ 'b :: len word) \ ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)" by transfer simp lemma scast_1': "(scast (1::'a::len word) :: 'b::len word) = (word_of_int (signed_take_bit (LENGTH('a::len) - Suc 0) (1::int)))" by transfer simp lemma scast_1: "(scast (1::'a::len word) :: 'b::len word) = (if LENGTH('a) = 1 then -1 else 1)" by (fact signed_1) lemma unat_minus_one_word: "unat (-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1" by (simp add: mask_eq_exp_minus_1 unsigned_minus_1_eq_mask) lemmas word_diff_ls'' = word_diff_ls [where xa=x and x=x for x] lemmas word_diff_ls' = word_diff_ls'' [simplified] lemmas word_l_diffs' = word_l_diffs [where xa=x and x=x for x] lemmas word_l_diffs = word_l_diffs' [simplified] lemma two_power_increasing: "\ n \ m; m < LENGTH('a) \ \ (2 :: 'a :: len word) ^ n \ 2 ^ m" by (simp add: word_le_nat_alt) lemma word_leq_le_minus_one: "\ x \ y; x \ 0 \ \ x - 1 < (y :: 'a :: len word)" apply (simp add: word_less_nat_alt word_le_nat_alt) apply (subst unat_minus_one) apply assumption apply (cases "unat x") apply (simp add: unat_eq_zero) apply arith done lemma neg_mask_combine: "NOT(mask a) AND NOT(mask b) = NOT(mask (max a b) :: 'a::len word)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma neg_mask_twice: "x AND NOT(mask n) AND NOT(mask m) = x AND NOT(mask (max n m))" for x :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps) lemma multiple_mask_trivia: "n \ m \ (x AND NOT(mask n)) + (x AND mask n AND NOT(mask m)) = x AND NOT(mask m)" for x :: \'a::len word\ apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2) apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice max_absorb2) done lemma word_of_nat_less: "\ n < unat x \ \ of_nat n < x" apply (simp add: word_less_nat_alt) apply (erule order_le_less_trans[rotated]) apply (simp add: unsigned_of_nat take_bit_eq_mod) done lemma unat_mask: "unat (mask n :: 'a :: len word) = 2 ^ (min n (LENGTH('a))) - 1" apply (subst min.commute) apply (simp add: mask_eq_decr_exp not_less min_def split: if_split_asm) apply (intro conjI impI) apply (simp add: unat_sub_if_size) apply (simp add: power_overflow word_size) apply (simp add: unat_sub_if_size) done lemma mask_over_length: "LENGTH('a) \ n \ mask n = (-1::'a::len word)" by (simp add: mask_eq_decr_exp) lemma Suc_2p_unat_mask: "n < LENGTH('a) \ Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)" by (simp add: unat_mask) lemma sint_of_nat_ge_zero: "x < 2 ^ (LENGTH('a) - 1) \ sint (of_nat x :: 'a :: len word) \ 0" by (simp add: bit_iff_odd signed_of_nat) lemma int_eq_sint: "x < 2 ^ (LENGTH('a) - 1) \ sint (of_nat x :: 'a :: len word) = int x" apply transfer apply (rule signed_take_bit_int_eq_self) apply simp_all apply (metis negative_zle numeral_power_eq_of_nat_cancel_iff) done lemma sint_of_nat_le: "\ b < 2 ^ (LENGTH('a) - 1); a \ b \ \ sint (of_nat a :: 'a :: len word) \ sint (of_nat b :: 'a :: len word)" apply (cases \LENGTH('a)\) apply simp_all apply transfer apply (subst signed_take_bit_eq_if_positive) apply (simp add: bit_simps) apply (metis bit_take_bit_iff nat_less_le order_less_le_trans take_bit_nat_eq_self_iff) apply (subst signed_take_bit_eq_if_positive) apply (simp add: bit_simps) apply (metis bit_take_bit_iff nat_less_le take_bit_nat_eq_self_iff) apply (simp flip: of_nat_take_bit add: take_bit_nat_eq_self) done lemma word_le_not_less: "((b::'a::len word) \ a) = (\(a < b))" by fastforce lemma less_is_non_zero_p1: fixes a :: "'a :: len word" shows "a < k \ a + 1 \ 0" apply (erule contrapos_pn) apply (drule max_word_wrap) apply (simp add: not_less) done lemma unat_add_lem': "(unat x + unat y < 2 ^ LENGTH('a)) \ (unat (x + y :: 'a :: len word) = unat x + unat y)" by (subst unat_add_lem[symmetric], assumption) lemma word_less_two_pow_divI: "\ (x :: 'a::len word) < 2 ^ (n - m); m \ n; n < LENGTH('a) \ \ x < 2 ^ n div 2 ^ m" apply (simp add: word_less_nat_alt) apply (subst unat_word_ariths) apply (subst mod_less) apply (rule order_le_less_trans [OF div_le_dividend]) apply (rule unat_lt2p) apply (simp add: power_sub) done lemma word_less_two_pow_divD: "\ (x :: 'a::len word) < 2 ^ n div 2 ^ m \ \ n \ m \ (x < 2 ^ (n - m))" apply (cases "n < LENGTH('a)") apply (cases "m < LENGTH('a)") apply (simp add: word_less_nat_alt) apply (subst(asm) unat_word_ariths) apply (subst(asm) mod_less) apply (rule order_le_less_trans [OF div_le_dividend]) apply (rule unat_lt2p) apply (clarsimp dest!: less_two_pow_divD) apply (simp add: power_overflow) apply (simp add: word_div_def) apply (simp add: power_overflow word_div_def) done lemma of_nat_less_two_pow_div_set: "\ n < LENGTH('a) \ \ {x. x < (2 ^ n div 2 ^ m :: 'a::len word)} = of_nat ` {k. k < 2 ^ n div 2 ^ m}" apply (simp add: image_def) apply (safe dest!: word_less_two_pow_divD less_two_pow_divD intro!: word_less_two_pow_divI) apply (rule_tac x="unat x" in exI) apply (simp add: power_sub[symmetric]) apply (subst unat_power_lower[symmetric, where 'a='a]) apply simp apply (erule unat_mono) apply (subst word_unat_power) apply (rule of_nat_mono_maybe) apply (rule power_strict_increasing) apply simp apply simp apply assumption done lemma ucast_less: "LENGTH('b) < LENGTH('a) \ (ucast (x :: 'b :: len word) :: ('a :: len word)) < 2 ^ LENGTH('b)" by transfer simp lemma ucast_range_less: "LENGTH('a :: len) < LENGTH('b :: len) \ range (ucast :: 'a word \ 'b word) = {x. x < 2 ^ len_of TYPE ('a)}" apply safe apply (erule ucast_less) apply (simp add: image_def) apply (rule_tac x="ucast x" in exI) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) apply (metis bit_take_bit_iff take_bit_word_eq_self_iff) done lemma word_power_less_diff: "\2 ^ n * q < (2::'a::len word) ^ m; q < 2 ^ (LENGTH('a) - n)\ \ q < 2 ^ (m - n)" apply (case_tac "m \ LENGTH('a)") apply (simp add: power_overflow) apply (case_tac "n \ LENGTH('a)") apply (simp add: power_overflow) apply (cases "n = 0") apply simp apply (subst word_less_nat_alt) apply (subst unat_power_lower) apply simp apply (rule nat_power_less_diff) apply (simp add: word_less_nat_alt) apply (subst (asm) iffD1 [OF unat_mult_lem]) apply (simp add:nat_less_power_trans) apply simp done lemma word_less_sub_1: "x < (y :: 'a :: len word) \ x \ y - 1" by (fact word_le_minus_one_leq) lemma word_sub_mono2: "\ a + b \ c + d; c \ a; b \ a + b; d \ c + d \ \ b \ (d :: 'a :: len word)" apply (drule(1) word_sub_mono) apply simp apply simp apply simp done lemma word_not_le: "(\ x \ (y :: 'a :: len word)) = (y < x)" by fastforce lemma word_subset_less: "\ {x .. x + r - 1} \ {y .. y + s - 1}; x \ x + r - 1; y \ y + (s :: 'a :: len word) - 1; s \ 0 \ \ r \ s" apply (frule subsetD[where c=x]) apply simp apply (drule subsetD[where c="x + r - 1"]) apply simp apply (clarsimp simp: add_diff_eq[symmetric]) apply (drule(1) word_sub_mono2) apply (simp_all add: olen_add_eqv[symmetric]) apply (erule word_le_minus_cancel) apply (rule ccontr) apply (simp add: word_not_le) done lemma uint_power_lower: "n < LENGTH('a) \ uint (2 ^ n :: 'a :: len word) = (2 ^ n :: int)" by (rule uint_2p_alt) lemma power_le_mono: "\2 ^ n \ (2::'a::len word) ^ m; n < LENGTH('a); m < LENGTH('a)\ \ n \ m" apply (clarsimp simp add: le_less) apply safe apply (simp add: word_less_nat_alt) apply (simp only: uint_arith_simps(3)) apply (drule uint_power_lower)+ apply simp done lemma two_power_eq: "\n < LENGTH('a); m < LENGTH('a)\ \ ((2::'a::len word) ^ n = 2 ^ m) = (n = m)" apply safe apply (rule order_antisym) apply (simp add: power_le_mono[where 'a='a])+ done lemma unat_less_helper: "x < of_nat n \ unat x < n" apply (simp add: word_less_nat_alt) apply (erule order_less_le_trans) apply (simp add: take_bit_eq_mod unsigned_of_nat) done lemma nat_uint_less_helper: "nat (uint y) = z \ x < y \ nat (uint x) < z" apply (erule subst) apply (subst unat_eq_nat_uint [symmetric]) apply (subst unat_eq_nat_uint [symmetric]) by (simp add: unat_mono) lemma of_nat_0: "\of_nat n = (0::'a::len word); n < 2 ^ LENGTH('a)\ \ n = 0" by (auto simp add: word_of_nat_eq_0_iff) lemma of_nat_inj: "\x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\ \ (of_nat x = (of_nat y :: 'a :: len word)) = (x = y)" by (metis unat_of_nat_len) lemma div_to_mult_word_lt: "\ (x :: 'a :: len word) \ y div z \ \ x * z \ y" apply (cases "z = 0") apply simp apply (simp add: word_neq_0_conv) apply (rule order_trans) apply (erule(1) word_mult_le_mono1) apply (simp add: unat_div) apply (rule order_le_less_trans [OF div_mult_le]) apply simp apply (rule word_div_mult_le) done lemma ucast_ucast_mask: "(ucast :: 'a :: len word \ 'b :: len word) (ucast x) = x AND mask (len_of TYPE ('a))" apply (simp flip: take_bit_eq_mask) apply transfer apply (simp add: ac_simps) done lemma ucast_ucast_len: "\ x < 2 ^ LENGTH('b) \ \ ucast (ucast x::'b::len word) = (x::'a::len word)" apply (subst ucast_ucast_mask) apply (erule less_mask_eq) done lemma ucast_ucast_id: "LENGTH('a) < LENGTH('b) \ ucast (ucast (x::'a::len word)::'b::len word) = x" by (auto intro: ucast_up_ucast_id simp: is_up_def source_size_def target_size_def word_size) lemma unat_ucast: "unat (ucast x :: ('a :: len) word) = unat x mod 2 ^ (LENGTH('a))" proof - have \2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))\ by simp moreover have \unat (ucast x :: 'a word) = unat x mod nat (2 ^ LENGTH('a))\ by transfer (simp flip: nat_mod_distrib take_bit_eq_mod) ultimately show ?thesis by (simp only:) qed lemma ucast_less_ucast: "LENGTH('a) \ LENGTH('b) \ (ucast x < ((ucast (y :: 'a::len word)) :: 'b::len word)) = (x < y)" apply (simp add: word_less_nat_alt unat_ucast) apply (subst mod_less) apply(rule less_le_trans[OF unat_lt2p], simp) apply (subst mod_less) apply(rule less_le_trans[OF unat_lt2p], simp) apply simp done \ \This weaker version was previously called @{text ucast_less_ucast}. We retain it to support existing proofs.\ lemmas ucast_less_ucast_weak = ucast_less_ucast[OF order.strict_implies_order] lemma unat_Suc2: fixes n :: "'a :: len word" shows "n \ -1 \ unat (n + 1) = Suc (unat n)" apply (subst add.commute, rule unatSuc) apply (subst eq_diff_eq[symmetric], simp add: minus_equation_iff) done lemma word_div_1: "(n :: 'a :: len word) div 1 = n" by (fact bits_div_by_1) lemma word_minus_one_le: "-1 \ (x :: 'a :: len word) = (x = -1)" by (fact word_order.extremum_unique) lemma up_scast_inj: "\ scast x = (scast y :: 'b :: len word); size x \ LENGTH('b) \ \ x = y" apply transfer apply (cases \LENGTH('a)\) apply simp_all apply (metis order_refl take_bit_signed_take_bit take_bit_tightened) done lemma up_scast_inj_eq: "LENGTH('a) \ len_of TYPE ('b) \ (scast x = (scast y::'b::len word)) = (x = (y::'a::len word))" by (fastforce dest: up_scast_inj simp: word_size) lemma word_le_add: fixes x :: "'a :: len word" shows "x \ y \ \n. y = x + of_nat n" by (rule exI [where x = "unat (y - x)"]) simp lemma word_plus_mcs_4': fixes x :: "'a :: len word" shows "\x + v \ x + w; x \ x + v\ \ v \ w" apply (rule word_plus_mcs_4) apply (simp add: add.commute) apply (simp add: add.commute) done lemma unat_eq_1: \unat x = Suc 0 \ x = 1\ by (auto intro!: unsigned_word_eqI [where ?'a = nat]) lemma word_unat_Rep_inject1: \unat x = unat 1 \ x = 1\ by (simp add: unat_eq_1) lemma and_not_mask_twice: "(w AND NOT (mask n)) AND NOT (mask m) = w AND NOT (mask (max m n))" for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps) lemma word_less_cases: "x < y \ x = y - 1 \ x < y - (1 ::'a::len word)" apply (drule word_less_sub_1) apply (drule order_le_imp_less_or_eq) apply auto done lemma mask_and_mask: "mask a AND mask b = (mask (min a b) :: 'a::len word)" by (simp flip: take_bit_eq_mask ac_simps) lemma mask_eq_0_eq_x: "(x AND w = 0) = (x AND NOT w = x)" for x w :: \'a::len word\ using word_plus_and_or_coroll2[where x=x and w=w] by auto lemma mask_eq_x_eq_0: "(x AND w = x) = (x AND NOT w = 0)" for x w :: \'a::len word\ using word_plus_and_or_coroll2[where x=x and w=w] by auto lemma compl_of_1: "NOT 1 = (-2 :: 'a :: len word)" by (fact not_one_eq) lemma split_word_eq_on_mask: "(x = y) = (x AND m = y AND m \ x AND NOT m = y AND NOT m)" for x y m :: \'a::len word\ apply transfer apply (simp add: bit_eq_iff) apply (auto simp add: bit_simps ac_simps) done lemma word_FF_is_mask: "0xFF = (mask 8 :: 'a::len word)" by (simp add: mask_eq_decr_exp) lemma word_1FF_is_mask: "0x1FF = (mask 9 :: 'a::len word)" by (simp add: mask_eq_decr_exp) lemma ucast_of_nat_small: "x < 2 ^ LENGTH('a) \ ucast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)" apply transfer apply (auto simp add: take_bit_of_nat min_def not_le) apply (metis linorder_not_less min_def take_bit_nat_eq_self take_bit_take_bit) done lemma word_le_make_less: fixes x :: "'a :: len word" shows "y \ -1 \ (x \ y) = (x < (y + 1))" apply safe apply (erule plus_one_helper2) apply (simp add: eq_diff_eq[symmetric]) done lemmas finite_word = finite [where 'a="'a::len word"] lemma word_to_1_set: "{0 ..< (1 :: 'a :: len word)} = {0}" by fastforce lemma word_leq_minus_one_le: fixes x :: "'a::len word" shows "\y \ 0; x \ y - 1 \ \ x < y" using le_m1_iff_lt word_neq_0_conv by blast lemma word_count_from_top: "n \ 0 \ {0 ..< n :: 'a :: len word} = {0 ..< n - 1} \ {n - 1}" apply (rule set_eqI, rule iffI) apply simp apply (drule word_le_minus_one_leq) apply (rule disjCI) apply simp apply simp apply (erule word_leq_minus_one_le) apply fastforce done lemma word_minus_one_le_leq: "\ x - 1 < y \ \ x \ (y :: 'a :: len word)" apply (cases "x = 0") apply simp apply (simp add: word_less_nat_alt word_le_nat_alt) apply (subst(asm) unat_minus_one) apply (simp add: word_less_nat_alt) apply (cases "unat x") apply (simp add: unat_eq_zero) apply arith done lemma word_must_wrap: "\ x \ n - 1; n \ x \ \ n = (0 :: 'a :: len word)" using dual_order.trans sub_wrap word_less_1 by blast lemma range_subset_card: "\ {a :: 'a :: len word .. b} \ {c .. d}; b \ a \ \ d \ c \ d - c \ b - a" using word_sub_le word_sub_mono by fastforce lemma less_1_simp: "n - 1 < m = (n \ (m :: 'a :: len word) \ n \ 0)" by unat_arith lemma word_power_mod_div: fixes x :: "'a::len word" shows "\ n < LENGTH('a); m < LENGTH('a)\ \ x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)" apply (simp add: word_arith_nat_div unat_mod power_mod_div) apply (subst unat_arith_simps(3)) apply (subst unat_mod) apply (subst unat_of_nat)+ apply (simp add: mod_mod_power min.commute) done lemma word_range_minus_1': fixes a :: "'a :: len word" shows "a \ 0 \ {a - 1<..b} = {a..b}" by (simp add: greaterThanAtMost_def atLeastAtMost_def greaterThan_def atLeast_def less_1_simp) lemma word_range_minus_1: fixes a :: "'a :: len word" shows "b \ 0 \ {a..b - 1} = {a.. 'b :: len word) x" by transfer simp lemma overflow_plus_one_self: "(1 + p \ p) = (p = (-1 :: 'a :: len word))" apply rule apply (rule ccontr) apply (drule plus_one_helper2) apply (rule notI) apply (drule arg_cong[where f="\x. x - 1"]) apply simp apply (simp add: field_simps) apply simp done lemma plus_1_less: "(x + 1 \ (x :: 'a :: len word)) = (x = -1)" apply (rule iffI) apply (rule ccontr) apply (cut_tac plus_one_helper2[where x=x, OF order_refl]) apply simp apply clarsimp apply (drule arg_cong[where f="\x. x - 1"]) apply simp apply simp done lemma pos_mult_pos_ge: "[|x > (0::int); n>=0 |] ==> n * x >= n*1" apply (simp only: mult_left_mono) done lemma word_plus_strict_mono_right: fixes x :: "'a :: len word" shows "\y < z; x \ x + z\ \ x + y < x + z" by unat_arith lemma word_div_mult: "0 < c \ a < b * c \ a div c < b" for a b c :: "'a::len word" by (rule classical) (use div_to_mult_word_lt [of b a c] in \auto simp add: word_less_nat_alt word_le_nat_alt unat_div\) lemma word_less_power_trans_ofnat: "\n < 2 ^ (m - k); k \ m; m < LENGTH('a)\ \ of_nat n * 2 ^ k < (2::'a::len word) ^ m" apply (subst mult.commute) apply (rule word_less_power_trans) apply (simp_all add: word_less_nat_alt unsigned_of_nat) using take_bit_nat_less_eq_self apply (rule le_less_trans) apply assumption done lemma word_1_le_power: "n < LENGTH('a) \ (1 :: 'a :: len word) \ 2 ^ n" by (rule inc_le[where i=0, simplified], erule iffD2[OF p2_gt_0]) lemma unat_1_0: "1 \ (x::'a::len word) = (0 < unat x)" by (auto simp add: word_le_nat_alt) lemma x_less_2_0_1': fixes x :: "'a::len word" shows "\LENGTH('a) \ 1; x < 2\ \ x = 0 \ x = 1" apply (cases \2 \ LENGTH('a)\) apply simp_all apply transfer apply auto apply (metis add.commute add.right_neutral even_two_times_div_two mod_div_trivial mod_pos_pos_trivial mult.commute mult_zero_left not_less not_take_bit_negative odd_two_times_div_two_succ) done lemmas word_add_le_iff2 = word_add_le_iff [folded no_olen_add_nat] lemma of_nat_power: shows "\ p < 2 ^ x; x < len_of TYPE ('a) \ \ of_nat p < (2 :: 'a :: len word) ^ x" apply (rule order_less_le_trans) apply (rule of_nat_mono_maybe) apply (erule power_strict_increasing) apply simp apply assumption apply (simp add: word_unat_power del: of_nat_power) done lemma of_nat_n_less_equal_power_2: "n < LENGTH('a::len) \ ((of_nat n)::'a word) < 2 ^ n" apply (induct n) apply clarsimp apply clarsimp apply (metis of_nat_power n_less_equal_power_2 of_nat_Suc power_Suc) done lemma eq_mask_less: fixes w :: "'a::len word" assumes eqm: "w = w AND mask n" and sz: "n < len_of TYPE ('a)" shows "w < (2::'a word) ^ n" by (subst eqm, rule and_mask_less' [OF sz]) lemma of_nat_mono_maybe': fixes Y :: "nat" assumes xlt: "x < 2 ^ len_of TYPE ('a)" assumes ylt: "y < 2 ^ len_of TYPE ('a)" shows "(y < x) = (of_nat y < (of_nat x :: 'a :: len word))" apply (subst word_less_nat_alt) apply (subst unat_of_nat)+ apply (subst mod_less) apply (rule ylt) apply (subst mod_less) apply (rule xlt) apply simp done lemma of_nat_mono_maybe_le: "\x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\ \ (y \ x) = ((of_nat y :: 'a :: len word) \ of_nat x)" apply (clarsimp simp: le_less) apply (rule disj_cong) apply (rule of_nat_mono_maybe', assumption+) apply auto using of_nat_inj apply blast done lemma mask_AND_NOT_mask: "(w AND NOT (mask n)) AND mask n = 0" for w :: \'a::len word\ by (rule bit_word_eqI) (simp add: bit_simps) lemma AND_NOT_mask_plus_AND_mask_eq: "(w AND NOT (mask n)) + (w AND mask n) = w" for w :: \'a::len word\ apply (subst disjunctive_add) apply (auto simp add: bit_simps) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) done lemma mask_eqI: fixes x :: "'a :: len word" assumes m1: "x AND mask n = y AND mask n" and m2: "x AND NOT (mask n) = y AND NOT (mask n)" shows "x = y" proof - have *: \x = x AND mask n OR x AND NOT (mask n)\ for x :: \'a word\ by (rule bit_word_eqI) (auto simp add: bit_simps) from assms * [of x] * [of y] show ?thesis by simp qed lemma neq_0_no_wrap: fixes x :: "'a :: len word" shows "\ x \ x + y; x \ 0 \ \ x + y \ 0" by clarsimp lemma unatSuc2: fixes n :: "'a :: len word" shows "n + 1 \ 0 \ unat (n + 1) = Suc (unat n)" by (simp add: add.commute unatSuc) lemma word_of_nat_le: "n \ unat x \ of_nat n \ x" apply (simp add: word_le_nat_alt unat_of_nat) apply (erule order_trans[rotated]) apply (simp add: take_bit_eq_mod) done lemma word_unat_less_le: "a \ of_nat b \ unat a \ b" by (metis eq_iff le_cases le_unat_uoi word_of_nat_le) lemma mask_Suc_0 : "mask (Suc 0) = (1 :: 'a::len word)" by (simp add: mask_eq_decr_exp) lemma bool_mask': fixes x :: "'a :: len word" shows "2 < LENGTH('a) \ (0 < x AND 1) = (x AND 1 = 1)" by (simp add: and_one_eq mod_2_eq_odd) lemma ucast_ucast_add: fixes x :: "'a :: len word" fixes y :: "'b :: len word" shows "LENGTH('b) \ LENGTH('a) \ ucast (ucast x + y) = x + ucast y" apply transfer apply simp apply (subst (2) take_bit_add [symmetric]) apply (subst take_bit_add [symmetric]) apply simp done lemma lt1_neq0: fixes x :: "'a :: len word" shows "(1 \ x) = (x \ 0)" by unat_arith lemma word_plus_one_nonzero: fixes x :: "'a :: len word" shows "\x \ x + y; y \ 0\ \ x + 1 \ 0" apply (subst lt1_neq0 [symmetric]) apply (subst olen_add_eqv [symmetric]) apply (erule word_random) apply (simp add: lt1_neq0) done lemma word_sub_plus_one_nonzero: fixes n :: "'a :: len word" shows "\n' \ n; n' \ 0\ \ (n - n') + 1 \ 0" apply (subst lt1_neq0 [symmetric]) apply (subst olen_add_eqv [symmetric]) apply (rule word_random [where x' = n']) apply simp apply (erule word_sub_le) apply (simp add: lt1_neq0) done lemma word_le_minus_mono_right: fixes x :: "'a :: len word" shows "\ z \ y; y \ x; z \ x \ \ x - y \ x - z" apply (rule word_sub_mono) apply simp apply assumption apply (erule word_sub_le) apply (erule word_sub_le) done lemma word_0_sle_from_less: \0 \s x\ if \x < 2 ^ (LENGTH('a) - 1)\ for x :: \'a::len word\ using that apply transfer apply (cases \LENGTH('a)\) apply simp_all apply (metis bit_take_bit_iff min_def nat_less_le not_less_eq take_bit_int_eq_self_iff take_bit_take_bit) done lemma ucast_sub_ucast: fixes x :: "'a::len word" assumes "y \ x" assumes T: "LENGTH('a) \ LENGTH('b)" shows "ucast (x - y) = (ucast x - ucast y :: 'b::len word)" proof - from T have P: "unat x < 2 ^ LENGTH('b)" "unat y < 2 ^ LENGTH('b)" by (fastforce intro!: less_le_trans[OF unat_lt2p])+ then show ?thesis by (simp add: unat_arith_simps unat_ucast assms[simplified unat_arith_simps]) qed lemma word_1_0: "\a + (1::('a::len) word) \ b; a < of_nat x\ \ a < b" apply transfer apply (subst (asm) take_bit_incr_eq) apply (auto simp add: diff_less_eq) using take_bit_int_less_exp le_less_trans by blast lemma unat_of_nat_less:"\ a < b; unat b = c \ \ a < of_nat c" by fastforce lemma word_le_plus_1: "\ (y::('a::len) word) < y + n; a < n \ \ y + a \ y + a + 1" by unat_arith lemma word_le_plus:"\(a::('a::len) word) < a + b; c < b\ \ a \ a + c" by (metis order_less_imp_le word_random) lemma sint_minus1 [simp]: "(sint x = -1) = (x = -1)" apply (cases \LENGTH('a)\) apply simp_all apply transfer apply (simp only: flip: signed_take_bit_eq_iff_take_bit_eq) apply simp done lemma sint_0 [simp]: "(sint x = 0) = (x = 0)" by (fact signed_eq_0_iff) (* It is not always that case that "sint 1 = 1", because of 1-bit word sizes. * This lemma produces the different cases. *) lemma sint_1_cases: P if \\ len_of TYPE ('a::len) = 1; (a::'a word) = 0; sint a = 0 \ \ P\ \\ len_of TYPE ('a) = 1; a = 1; sint (1 :: 'a word) = -1 \ \ P\ \\ len_of TYPE ('a) > 1; sint (1 :: 'a word) = 1 \ \ P\ proof (cases \LENGTH('a) = 1\) case True then have \a = 0 \ a = 1\ by transfer auto with True that show ?thesis by auto next case False with that show ?thesis by (simp add: less_le Suc_le_eq) qed lemma sint_int_min: "sint (- (2 ^ (LENGTH('a) - Suc 0)) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))" apply (cases \LENGTH('a)\) apply simp_all apply transfer apply (simp add: signed_take_bit_int_eq_self) done lemma sint_int_max_plus_1: "sint (2 ^ (LENGTH('a) - Suc 0) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))" apply (cases \LENGTH('a)\) apply simp_all apply (subst word_of_int_2p [symmetric]) apply (subst int_word_sint) apply simp done lemma uint_range': \0 \ uint x \ uint x < 2 ^ LENGTH('a)\ for x :: \'a::len word\ by transfer simp lemma sint_of_int_eq: "\ - (2 ^ (LENGTH('a) - 1)) \ x; x < 2 ^ (LENGTH('a) - 1) \ \ sint (of_int x :: ('a::len) word) = x" by (simp add: signed_take_bit_int_eq_self signed_of_int) lemma of_int_sint: "of_int (sint a) = a" by simp lemma sint_ucast_eq_uint: "\ \ is_down (ucast :: ('a::len word \ 'b::len word)) \ \ sint ((ucast :: ('a::len word \ 'b::len word)) x) = uint x" apply transfer apply (simp add: signed_take_bit_take_bit) done lemma word_less_nowrapI': "(x :: 'a :: len word) \ z - k \ k \ z \ 0 < k \ x < x + k" by uint_arith lemma mask_plus_1: "mask n + 1 = (2 ^ n :: 'a::len word)" by (clarsimp simp: mask_eq_decr_exp) lemma unat_inj: "inj unat" by (metis eq_iff injI word_le_nat_alt) lemma unat_ucast_upcast: "is_up (ucast :: 'b word \ 'a word) \ unat (ucast x :: ('a::len) word) = unat (x :: ('b::len) word)" unfolding ucast_eq unat_eq_nat_uint apply transfer apply simp done lemma ucast_mono: "\ (x :: 'b :: len word) < y; y < 2 ^ LENGTH('a) \ \ ucast x < ((ucast y) :: 'a :: len word)" apply (simp only: flip: ucast_nat_def) apply (rule of_nat_mono_maybe) apply (rule unat_less_helper) apply simp apply (simp add: word_less_nat_alt) done lemma ucast_mono_le: "\x \ y; y < 2 ^ LENGTH('b)\ \ (ucast (x :: 'a :: len word) :: 'b :: len word) \ ucast y" apply (simp only: flip: ucast_nat_def) apply (subst of_nat_mono_maybe_le[symmetric]) apply (rule unat_less_helper) apply simp apply (rule unat_less_helper) apply (erule le_less_trans) apply (simp_all add: word_le_nat_alt) done lemma ucast_mono_le': "\ unat y < 2 ^ LENGTH('b); LENGTH('b::len) < LENGTH('a::len); x \ y \ \ ucast x \ (ucast y :: 'b word)" for x y :: \'a::len word\ by (auto simp: word_less_nat_alt intro: ucast_mono_le) lemma neg_mask_add_mask: "((x:: 'a :: len word) AND NOT (mask n)) + (2 ^ n - 1) = x OR mask n" unfolding mask_2pm1 [symmetric] apply (subst word_plus_and_or_coroll; rule bit_word_eqI) apply (auto simp add: bit_simps) done lemma le_step_down_word:"\(i::('a::len) word) \ n; i = n \ P; i \ n - 1 \ P\ \ P" by unat_arith lemma le_step_down_word_2: fixes x :: "'a::len word" shows "\x \ y; x \ y\ \ x \ y - 1" by (subst (asm) word_le_less_eq, clarsimp, simp add: word_le_minus_one_leq) lemma NOT_mask_AND_mask[simp]: "(w AND mask n) AND NOT (mask n) = 0" by (rule bit_eqI) (simp add: bit_simps) lemma and_and_not[simp]:"(a AND b) AND NOT b = 0" for a b :: \'a::len word\ apply (subst word_bw_assocs(1)) apply clarsimp done lemma ex_mask_1[simp]: "(\x. mask x = (1 :: 'a::len word))" apply (rule_tac x=1 in exI) apply (simp add:mask_eq_decr_exp) done lemma not_switch:"NOT a = x \ a = NOT x" by auto lemma test_bit_eq_iff: "bit u = bit v \ u = v" for u v :: "'a::len word" by (auto intro: bit_eqI simp add: fun_eq_iff) lemma test_bit_size: "bit w n \ n < size w" for w :: "'a::len word" by transfer simp lemma word_eq_iff: "x = y \ (\n?P \ ?Q\) for x y :: "'a::len word" by transfer (auto simp add: bit_eq_iff bit_take_bit_iff) lemma word_eqI: "(\n. n < size u \ bit u n = bit v n) \ u = v" for u :: "'a::len word" by (simp add: word_size word_eq_iff) lemma word_eqD: "u = v \ bit u x = bit v x" for u v :: "'a::len word" by simp lemma test_bit_bin': "bit w n \ n < size w \ bit (uint w) n" by transfer (simp add: bit_take_bit_iff) lemmas test_bit_bin = test_bit_bin' [unfolded word_size] lemma word_test_bit_def: \bit a = bit (uint a)\ by transfer (simp add: fun_eq_iff bit_take_bit_iff) lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] lemma word_test_bit_transfer [transfer_rule]: "(rel_fun pcr_word (rel_fun (=) (=))) (\x n. n < LENGTH('a) \ bit x n) (bit :: 'a::len word \ _)" by transfer_prover lemma test_bit_wi: "bit (word_of_int x :: 'a::len word) n \ n < LENGTH('a) \ bit x n" by transfer simp lemma word_ops_nth_size: "n < size x \ bit (x OR y) n = (bit x n | bit y n) \ bit (x AND y) n = (bit x n \ bit y n) \ bit (x XOR y) n = (bit x n \ bit y n) \ bit (NOT x) n = (\ bit x n)" for x :: "'a::len word" by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff) lemma word_ao_nth: "bit (x OR y) n = (bit x n | bit y n) \ bit (x AND y) n = (bit x n \ bit y n)" for x :: "'a::len word" by transfer (auto simp add: bit_or_iff bit_and_iff) lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]] lemma nth_sint: fixes w :: "'a::len word" defines "l \ LENGTH('a)" shows "bit (sint w) n = (if n < l - 1 then bit w n else bit w (l - 1))" unfolding sint_uint l_def by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def) lemma test_bit_2p: "bit (word_of_int (2 ^ n)::'a::len word) m \ m = n \ m < LENGTH('a)" by transfer (auto simp add: bit_exp_iff) lemma nth_w2p: "bit ((2::'a::len word) ^ n) m \ m = n \ m < LENGTH('a::len)" by transfer (auto simp add: bit_exp_iff) lemma bang_is_le: "bit x m \ 2 ^ m \ x" for x :: "'a::len word" apply (rule xtrans(3)) apply (rule_tac [2] y = "x" in le_word_or2) apply (rule word_eqI) apply (auto simp add: word_ao_nth nth_w2p word_size) done lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]] lemmas msb1 = msb0 [where i = 0] lemma test_bit_1 [iff]: "bit (1 :: 'a::len word) n \ n = 0" by transfer (auto simp add: bit_1_iff) lemma nth_0: "\ bit (0 :: 'a::len word) n" by transfer simp lemma nth_minus1: "bit (-1 :: 'a::len word) n \ n < LENGTH('a)" by transfer simp lemma nth_ucast: "bit (ucast w::'a::len word) n = (bit w n \ n < LENGTH('a))" by transfer (simp add: bit_take_bit_iff ac_simps) lemma drop_bit_numeral_bit0_1 [simp]: \drop_bit (Suc 0) (numeral k) = (word_of_int (drop_bit (Suc 0) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\ by (metis Word_eq_word_of_int drop_bit_word.abs_eq of_int_numeral) lemma nth_mask: \bit (mask n :: 'a::len word) i \ i < n \ i < size (mask n :: 'a word)\ by (auto simp add: word_size Word.bit_mask_iff) lemma nth_slice: "bit (slice n w :: 'a::len word) m = (bit w (m + n) \ m < LENGTH('a))" apply (auto simp add: bit_simps less_diff_conv dest: bit_imp_le_length) using bit_imp_le_length apply fastforce done lemma test_bit_cat [OF refl]: "wc = word_cat a b \ bit wc n = (n < size wc \ (if n < size b then bit b n else bit a (n - size b)))" apply (simp add: word_size not_less; transfer) apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff) done \ \keep quantifiers for use in simplification\ lemma test_bit_split': "word_split c = (a, b) \ (\n m. bit b n = (n < size b \ bit c n) \ bit a m = (m < size a \ bit c (m + size b)))" by (auto simp add: word_split_bin' bit_unsigned_iff word_size bit_drop_bit_eq ac_simps dest: bit_imp_le_length) lemma test_bit_split: "word_split c = (a, b) \ (\n::nat. bit b n \ n < size b \ bit c n) \ (\m::nat. bit a m \ m < size a \ bit c (m + size b))" by (simp add: test_bit_split') lemma test_bit_split_eq: "word_split c = (a, b) \ ((\n::nat. bit b n = (n < size b \ bit c n)) \ (\m::nat. bit a m = (m < size a \ bit c (m + size b))))" apply (rule_tac iffI) apply (rule_tac conjI) apply (erule test_bit_split [THEN conjunct1]) apply (erule test_bit_split [THEN conjunct2]) apply (case_tac "word_split c") apply (frule test_bit_split) apply (erule trans) apply (fastforce intro!: word_eqI simp add: word_size) done lemma test_bit_rcat: "sw = size (hd wl) \ rc = word_rcat wl \ bit rc n = (n < size rc \ n div sw < size wl \ bit ((rev wl) ! (n div sw)) (n mod sw))" for wl :: "'a::len word list" by (simp add: word_size word_rcat_def rev_map bit_horner_sum_uint_exp_iff bit_simps not_le) lemmas test_bit_cong = arg_cong [where f = "bit", THEN fun_cong] lemma max_test_bit: "bit (- 1::'a::len word) n \ n < LENGTH('a)" by (fact nth_minus1) lemma map_nth_0 [simp]: "map (bit (0::'a::len word)) xs = replicate (length xs) False" by (simp flip: map_replicate_const) lemma word_and_1: "n AND 1 = (if bit n 0 then 1 else 0)" for n :: "_ word" by (rule bit_word_eqI) (auto simp add: bit_and_iff bit_1_iff intro: gr0I) lemma test_bit_1': "bit (1 :: 'a :: len word) n \ 0 < LENGTH('a) \ n = 0" by simp lemma nth_w2p_same: "bit (2^n :: 'a :: len word) n = (n < LENGTH('a))" by (simp add: nth_w2p) lemma word_leI: "(\n. \n < size (u::'a::len word); bit u n \ \ bit (v::'a::len word) n) \ u <= v" apply (rule order_trans [of u \u AND v\ v]) apply (rule eq_refl) apply (rule bit_word_eqI) apply (auto simp add: bit_simps word_and_le1 word_size) done lemma bang_eq: fixes x :: "'a::len word" shows "(x = y) = (\n. bit x n = bit y n)" by (auto intro!: bit_eqI) lemma neg_mask_test_bit: "bit (NOT(mask n) :: 'a :: len word) m = (n \ m \ m < LENGTH('a))" by (auto simp add: bit_simps) lemma upper_bits_unset_is_l2p: \(\n' \ n. n' < LENGTH('a) \ \ bit p n') \ (p < 2 ^ n)\ (is \?P \ ?Q\) if \n < LENGTH('a)\ for p :: "'a :: len word" proof assume ?Q then show ?P by (meson bang_is_le le_less_trans not_le word_power_increasing) next assume ?P have \take_bit n p = p\ proof (rule bit_word_eqI) fix q assume \q < LENGTH('a)\ show \bit (take_bit n p) q \ bit p q\ proof (cases \q < n\) case True then show ?thesis by (auto simp add: bit_simps) next case False then have \n \ q\ by simp with \?P\ \q < LENGTH('a)\ have \\ bit p q\ by simp then show ?thesis by (simp add: bit_simps) qed qed with that show ?Q using take_bit_word_eq_self_iff [of n p] by auto qed lemma less_2p_is_upper_bits_unset: "p < 2 ^ n \ n < LENGTH('a) \ (\n' \ n. n' < LENGTH('a) \ \ bit p n')" for p :: "'a :: len word" by (meson le_less_trans le_mask_iff_lt_2n upper_bits_unset_is_l2p word_zero_le) lemma test_bit_over: "n \ size (x::'a::len word) \ (bit x n) = False" by transfer auto lemma le_mask_high_bits: "w \ mask n \ (\i \ {n ..< size w}. \ bit w i)" for w :: \'a::len word\ apply (auto simp add: bit_simps word_size less_eq_mask_iff_take_bit_eq_self) apply (metis bit_take_bit_iff leD) apply (metis atLeastLessThan_iff leI take_bit_word_eq_self_iff upper_bits_unset_is_l2p) done lemma test_bit_conj_lt: "(bit x m \ m < LENGTH('a)) = bit x m" for x :: "'a :: len word" using test_bit_bin by blast lemma neg_test_bit: "bit (NOT x) n = (\ bit x n \ n < LENGTH('a))" for x :: "'a::len word" by (cases "n < LENGTH('a)") (auto simp add: test_bit_over word_ops_nth_size word_size) lemma nth_bounded: "\bit (x :: 'a :: len word) n; x < 2 ^ m; m \ len_of TYPE ('a)\ \ n < m" apply (rule ccontr) apply (auto simp add: not_less) apply (meson bit_imp_le_length bit_uint_iff less_2p_is_upper_bits_unset test_bit_bin) done lemma and_neq_0_is_nth: \x AND y \ 0 \ bit x n\ if \y = 2 ^ n\ for x y :: \'a::len word\ apply (simp add: bit_eq_iff bit_simps) using that apply (simp add: bit_simps not_le) apply transfer apply auto done lemma nth_is_and_neq_0: "bit (x::'a::len word) n = (x AND 2 ^ n \ 0)" by (subst and_neq_0_is_nth; rule refl) lemma max_word_not_less [simp]: "\ - 1 < x" for x :: \'a::len word\ by (fact word_order.extremum_strict) lemma bit_twiddle_min: "(y::'a::len word) XOR (((x::'a::len word) XOR y) AND (if x < y then -1 else 0)) = min x y" by (rule bit_eqI) (auto simp add: bit_simps) lemma bit_twiddle_max: "(x::'a::len word) XOR (((x::'a::len word) XOR y) AND (if x < y then -1 else 0)) = max x y" by (rule bit_eqI) (auto simp add: bit_simps max_def) lemma swap_with_xor: "\(x::'a::len word) = a XOR b; y = b XOR x; z = x XOR y\ \ z = b \ y = a" by (auto intro: bit_word_eqI simp add: bit_simps) lemma le_mask_imp_and_mask: "(x::'a::len word) \ mask n \ x AND mask n = x" by (metis and_mask_eq_iff_le_mask) lemma or_not_mask_nop: "((x::'a::len word) OR NOT (mask n)) AND mask n = x AND mask n" by (metis word_and_not word_ao_dist2 word_bw_comms(1) word_log_esimps(3)) lemma mask_subsume: "\n \ m\ \ ((x::'a::len word) OR y AND mask n) AND NOT (mask m) = x AND NOT (mask m)" by (rule bit_word_eqI) (auto simp add: bit_simps word_size) lemma and_mask_0_iff_le_mask: fixes w :: "'a::len word" shows "(w AND NOT(mask n) = 0) = (w \ mask n)" by (simp add: mask_eq_0_eq_x le_mask_imp_and_mask and_mask_eq_iff_le_mask) lemma mask_twice2: "n \ m \ ((x::'a::len word) AND mask m) AND mask n = x AND mask n" by (metis mask_twice min_def) lemma uint_2_id: "LENGTH('a) \ 2 \ uint (2::('a::len) word) = 2" by simp lemma div_of_0_id[simp]:"(0::('a::len) word) div n = 0" by (simp add: word_div_def) lemma degenerate_word:"LENGTH('a) = 1 \ (x::('a::len) word) = 0 \ x = 1" by (metis One_nat_def less_irrefl_nat sint_1_cases) lemma div_by_0_word:"(x::('a::len) word) div 0 = 0" by (metis div_0 div_by_0 unat_0 word_arith_nat_defs(6) word_div_1) lemma div_less_dividend_word:"\x \ 0; n \ 1\ \ (x::('a::len) word) div n < x" apply (cases \n = 0\) apply clarsimp apply (simp add:word_neq_0_conv) apply (subst word_arith_nat_div) apply (rule word_of_nat_less) apply (rule div_less_dividend) using unat_eq_zero word_unat_Rep_inject1 apply force apply (simp add:unat_gt_0) done lemma word_less_div: fixes x :: "('a::len) word" and y :: "('a::len) word" shows "x div y = 0 \ y = 0 \ x < y" apply (case_tac "y = 0", clarsimp+) by (metis One_nat_def Suc_le_mono le0 le_div_geq not_less unat_0 unat_div unat_gt_0 word_less_nat_alt zero_less_one) lemma not_degenerate_imp_2_neq_0:"LENGTH('a) > 1 \ (2::('a::len) word) \ 0" by (metis numerals(1) power_not_zero power_zero_numeral) lemma word_overflow:"(x::('a::len) word) + 1 > x \ x + 1 = 0" apply clarsimp by (metis diff_0 eq_diff_eq less_x_plus_1) lemma word_overflow_unat:"unat ((x::('a::len) word) + 1) = unat x + 1 \ x + 1 = 0" by (metis Suc_eq_plus1 add.commute unatSuc) lemma even_word_imp_odd_next:"even (unat (x::('a::len) word)) \ x + 1 = 0 \ odd (unat (x + 1))" apply (cut_tac x=x in word_overflow_unat) apply clarsimp done lemma odd_word_imp_even_next:"odd (unat (x::('a::len) word)) \ x + 1 = 0 \ even (unat (x + 1))" apply (cut_tac x=x in word_overflow_unat) apply clarsimp done lemma overflow_imp_lsb:"(x::('a::len) word) + 1 = 0 \ bit x 0" using even_plus_one_iff [of x] by (simp add: bit_0) lemma odd_iff_lsb:"odd (unat (x::('a::len) word)) = bit x 0" by transfer (simp add: even_nat_iff bit_0) lemma of_nat_neq_iff_word: "x mod 2 ^ LENGTH('a) \ y mod 2 ^ LENGTH('a) \ (((of_nat x)::('a::len) word) \ of_nat y) = (x \ y)" apply (rule iffI) apply (case_tac "x = y") apply (subst (asm) of_nat_eq_iff[symmetric]) apply auto apply (case_tac "((of_nat x)::('a::len) word) = of_nat y") apply auto apply (metis unat_of_nat) done lemma lsb_this_or_next: "\ (bit ((x::('a::len) word) + 1) 0) \ bit x 0" by (simp add: bit_0) lemma mask_or_not_mask: "x AND mask n OR x AND NOT (mask n) = x" for x :: \'a::len word\ apply (subst word_oa_dist, simp) apply (subst word_oa_dist2, simp) done lemma word_gr0_conv_Suc: "(m::'a::len word) > 0 \ \n. m = n + 1" by (metis add.commute add_minus_cancel) lemma revcast_down_us [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = ucast (signed_drop_bit n w)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done lemma revcast_down_ss [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = scast (signed_drop_bit n w)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done lemma revcast_down_uu [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = ucast (drop_bit n w)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done lemma revcast_down_su [OF refl]: "rc = revcast \ source_size rc = target_size rc + n \ rc w = scast (drop_bit n w)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps ac_simps) done lemma cast_down_rev [OF refl]: "uc = ucast \ source_size uc = target_size uc + n \ uc w = revcast (push_bit n w)" for w :: "'a::len word" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps) done lemma revcast_up [OF refl]: "rc = revcast \ source_size rc + n = target_size rc \ rc w = push_bit n (ucast w :: 'a::len word)" apply (simp add: source_size_def target_size_def) apply (rule bit_word_eqI) apply (simp add: bit_simps) apply auto apply (metis add.commute add_diff_cancel_right) apply (metis diff_add_inverse2 diff_diff_add) done lemmas rc1 = revcast_up [THEN revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]] lemmas rc2 = revcast_down_uu [THEN revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]] lemma word_ops_nth: fixes x y :: \'a::len word\ shows word_or_nth: "bit (x OR y) n = (bit x n \ bit y n)" and word_and_nth: "bit (x AND y) n = (bit x n \ bit y n)" and word_xor_nth: "bit (x XOR y) n = (bit x n \ bit y n)" by (simp_all add: bit_simps) lemma word_power_nonzero: "\ (x :: 'a::len word) < 2 ^ (LENGTH('a) - n); n < LENGTH('a); x \ 0 \ \ x * 2 ^ n \ 0" by (metis Word.word_div_mult bits_div_0 len_gt_0 len_of_finite_2_def nat_mult_power_less_eq p2_gt_0 unat_mono unat_power_lower word_gt_a_gt_0) lemma less_1_helper: "n \ m \ (n - 1 :: int) < m" by arith lemma div_power_helper: "\ x \ y; y < LENGTH('a) \ \ (2 ^ y - 1) div (2 ^ x :: 'a::len word) = 2 ^ (y - x) - 1" apply (simp flip: mask_eq_exp_minus_1 drop_bit_eq_div) apply (rule bit_word_eqI) apply (auto simp add: bit_simps not_le) done lemma max_word_mask: "(- 1 :: 'a::len word) = mask LENGTH('a)" by (fact minus_1_eq_mask) lemmas mask_len_max = max_word_mask[symmetric] lemma mask_out_first_mask_some: "\ x AND NOT (mask n) = y; n \ m \ \ x AND NOT (mask m) = y AND NOT (mask m)" for x y :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps word_size) lemma mask_lower_twice: "n \ m \ (x AND NOT (mask n)) AND NOT (mask m) = x AND NOT (mask m)" for x :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps word_size) lemma mask_lower_twice2: "(a AND NOT (mask n)) AND NOT (mask m) = a AND NOT (mask (max n m))" for a :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps) lemma ucast_and_neg_mask: "ucast (x AND NOT (mask n)) = ucast x AND NOT (mask n)" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done lemma ucast_and_mask: "ucast (x AND mask n) = ucast x AND mask n" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done lemma ucast_mask_drop: "LENGTH('a :: len) \ n \ (ucast (x AND mask n) :: 'a word) = ucast x" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done lemma mask_exceed: "n \ LENGTH('a) \ (x::'a::len word) AND NOT (mask n) = 0" by (rule bit_word_eqI) (simp add: bit_simps) lemma word_add_no_overflow:"(x::'a::len word) < - 1 \ x < x + 1" using less_x_plus_1 order_less_le by blast lemma lt_plus_1_le_word: fixes x :: "'a::len word" assumes bound:"n < unat (maxBound::'a word)" shows "x < 1 + of_nat n = (x \ of_nat n)" by (metis add.commute bound max_word_max word_Suc_leq word_not_le word_of_nat_less) lemma unat_ucast_up_simp: fixes x :: "'a::len word" assumes "LENGTH('a) \ LENGTH('b)" shows "unat (ucast x :: 'b::len word) = unat x" apply (rule bit_eqI) using assms apply (auto simp add: bit_simps dest: bit_imp_le_length) done lemma unat_ucast_less_no_overflow: "\n < 2 ^ LENGTH('a); unat f < n\ \ (f::('a::len) word) < of_nat n" by (erule (1) order_le_less_trans[OF _ of_nat_mono_maybe,rotated]) simp lemma unat_ucast_less_no_overflow_simp: "n < 2 ^ LENGTH('a) \ (unat f < n) = ((f::('a::len) word) < of_nat n)" using unat_less_helper unat_ucast_less_no_overflow by blast lemma unat_ucast_no_overflow_le: assumes no_overflow: "unat b < (2 :: nat) ^ LENGTH('a)" and upward_cast: "LENGTH('a) < LENGTH('b)" shows "(ucast (f::'a::len word) < (b :: 'b :: len word)) = (unat f < unat b)" proof - have LR: "ucast f < b \ unat f < unat b" apply (rule unat_less_helper) apply (simp add:ucast_nat_def) apply (rule_tac 'b1 = 'b in ucast_less_ucast[OF order.strict_implies_order, THEN iffD1]) apply (rule upward_cast) apply (simp add: ucast_ucast_mask less_mask_eq word_less_nat_alt unat_power_lower[OF upward_cast] no_overflow) done have RL: "unat f < unat b \ ucast f < b" proof- assume ineq: "unat f < unat b" have "ucast (f::'a::len word) < ((ucast (ucast b ::'a::len word)) :: 'b :: len word)" apply (simp add: ucast_less_ucast[OF order.strict_implies_order] upward_cast) apply (simp only: flip: ucast_nat_def) apply (rule unat_ucast_less_no_overflow[OF no_overflow ineq]) done then show ?thesis apply (rule order_less_le_trans) apply (simp add:ucast_ucast_mask word_and_le2) done qed then show ?thesis by (simp add:RL LR iffI) qed lemmas ucast_up_mono = ucast_less_ucast[THEN iffD2] lemma minus_one_word: "(-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1" by simp lemma le_2p_upper_bits: "\ (p::'a::len word) \ 2^n - 1; n < LENGTH('a) \ \ \n'\n. n' < LENGTH('a) \ \ bit p n'" by (subst upper_bits_unset_is_l2p; simp) lemma le2p_bits_unset: "p \ 2 ^ n - 1 \ \n'\n. n' < LENGTH('a) \ \ bit (p::'a::len word) n'" using upper_bits_unset_is_l2p [where p=p] by (cases "n < LENGTH('a)") auto lemma complement_nth_w2p: shows "n' < LENGTH('a) \ bit (NOT (2 ^ n :: 'a::len word)) n' = (n' \ n)" by (fastforce simp: word_ops_nth_size word_size nth_w2p) lemma word_unat_and_lt: "unat x < n \ unat y < n \ unat (x AND y) < n" by (meson le_less_trans word_and_le1 word_and_le2 word_le_nat_alt) lemma word_unat_mask_lt: "m \ size w \ unat ((w::'a::len word) AND mask m) < 2 ^ m" by (rule word_unat_and_lt) (simp add: unat_mask word_size) lemma word_sless_sint_le:"x sint x \ sint y - 1" by (metis word_sless_alt zle_diff1_eq) lemma upper_trivial: fixes x :: "'a::len word" shows "x \ 2 ^ LENGTH('a) - 1 \ x < 2 ^ LENGTH('a) - 1" by (simp add: less_le) lemma constraint_expand: fixes x :: "'a::len word" shows "x \ {y. lower \ y \ y \ upper} = (lower \ x \ x \ upper)" by (rule mem_Collect_eq) lemma card_map_elide: "card ((of_nat :: nat \ 'a::len word) ` {0.. CARD('a::len word)" proof - let ?of_nat = "of_nat :: nat \ 'a word" have "inj_on ?of_nat {i. i < CARD('a word)}" by (rule inj_onI) (simp add: card_word of_nat_inj) moreover have "{0.. {i. i < CARD('a word)}" using that by auto ultimately have "inj_on ?of_nat {0.. CARD('a::len word) \ card ((of_nat::nat \ 'a::len word) ` {0.. LENGTH('a) \ x = ucast y \ ucast x = y" for x :: "'a::len word" and y :: "'b::len word" by transfer simp lemma le_ucast_ucast_le: "x \ ucast y \ ucast x \ y" for x :: "'a::len word" and y :: "'b::len word" by (smt le_unat_uoi linorder_not_less order_less_imp_le ucast_nat_def unat_arith_simps(1)) lemma less_ucast_ucast_less: "LENGTH('b) \ LENGTH('a) \ x < ucast y \ ucast x < y" for x :: "'a::len word" and y :: "'b::len word" by (metis ucast_nat_def unat_mono unat_ucast_up_simp word_of_nat_less) lemma ucast_le_ucast: "LENGTH('a) \ LENGTH('b) \ (ucast x \ (ucast y::'b::len word)) = (x \ y)" for x :: "'a::len word" by (simp add: unat_arith_simps(1) unat_ucast_up_simp) lemmas ucast_up_mono_le = ucast_le_ucast[THEN iffD2] lemma ucast_or_distrib: fixes x :: "'a::len word" fixes y :: "'a::len word" shows "(ucast (x OR y) :: ('b::len) word) = ucast x OR ucast y" by (fact unsigned_or_eq) lemma word_exists_nth: "(w::'a::len word) \ 0 \ \i. bit w i" by (auto simp add: bit_eq_iff) lemma max_word_not_0 [simp]: "- 1 \ (0 :: 'a::len word)" by simp lemma unat_max_word_pos[simp]: "0 < unat (- 1 :: 'a::len word)" using unat_gt_0 [of \- 1 :: 'a::len word\] by simp (* Miscellaneous conditional injectivity rules. *) lemma mult_pow2_inj: assumes ws: "m + n \ LENGTH('a)" assumes le: "x \ mask m" "y \ mask m" assumes eq: "x * 2 ^ n = y * (2 ^ n::'a::len word)" shows "x = y" proof (rule bit_word_eqI) fix q assume \q < LENGTH('a)\ from eq have \push_bit n x = push_bit n y\ by (simp add: push_bit_eq_mult) moreover from le have \take_bit m x = x\ \take_bit m y = y\ by (simp_all add: less_eq_mask_iff_take_bit_eq_self) ultimately have \push_bit n (take_bit m x) = push_bit n (take_bit m y)\ by simp_all with \q < LENGTH('a)\ ws show \bit x q \ bit y q\ apply (simp add: push_bit_take_bit) unfolding bit_eq_iff apply (simp add: bit_simps not_le) apply (metis (full_types) \take_bit m x = x\ \take_bit m y = y\ add.commute add_diff_cancel_right' add_less_cancel_right bit_take_bit_iff le_add2 less_le_trans) done qed lemma word_of_nat_inj: assumes bounded: "x < 2 ^ LENGTH('a)" "y < 2 ^ LENGTH('a)" assumes of_nats: "of_nat x = (of_nat y :: 'a::len word)" shows "x = y" by (rule contrapos_pp[OF of_nats]; cases "x < y"; cases "y < x") (auto dest: bounded[THEN of_nat_mono_maybe]) lemma word_of_int_bin_cat_eq_iff: "(word_of_int (concat_bit LENGTH('b) (uint b) (uint a))::'c::len word) = word_of_int (concat_bit LENGTH('b) (uint d) (uint c)) \ b = d \ a = c" if "LENGTH('a) + LENGTH('b) \ LENGTH('c)" for a::"'a::len word" and b::"'b::len word" proof - from that show ?thesis using that concat_bit_eq_iff [of \LENGTH('b)\ \uint b\ \uint a\ \uint d\ \uint c\] apply (simp add: word_of_int_eq_iff take_bit_int_eq_self flip: word_eq_iff_unsigned) apply (simp add: concat_bit_def take_bit_int_eq_self bintr_uint take_bit_push_bit) done qed lemma word_cat_inj: "(word_cat a b::'c::len word) = word_cat c d \ a = c \ b = d" if "LENGTH('a) + LENGTH('b) \ LENGTH('c)" for a::"'a::len word" and b::"'b::len word" using word_of_int_bin_cat_eq_iff [OF that, of b a d c] by (simp add: word_cat_eq' ac_simps) lemma p2_eq_1: "2 ^ n = (1::'a::len word) \ n = 0" proof - have "2 ^ n = (1::'a word) \ n = 0" by (metis One_nat_def not_less one_less_numeral_iff p2_eq_0 p2_gt_0 power_0 power_0 power_inject_exp semiring_norm(76) unat_power_lower zero_neq_one) then show ?thesis by auto qed end lemmas word_div_less = div_word_less (* FIXME: move to Word distribution? *) lemma bin_nth_minus_Bit0[simp]: "0 < n \ bit (numeral (num.Bit0 w) :: int) n = bit (numeral w :: int) (n - 1)" by (cases n; simp) lemma bin_nth_minus_Bit1[simp]: "0 < n \ bit (numeral (num.Bit1 w) :: int) n = bit (numeral w :: int) (n - 1)" by (cases n; simp) lemma word_mod_by_0: "k mod (0::'a::len word) = k" by (simp add: word_arith_nat_mod) end