# HG changeset patch # User Manuel Eberl # Date 1617786300 -7200 # Node ID 56db8559eadb0c2577fb1c4c5d36510cf09b42f9 # Parent 5131c388a9b07c8a6e5249d65398b598074cf059 fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes) diff -r 5131c388a9b0 -r 56db8559eadb src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Wed Apr 07 12:28:19 2021 +0000 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 07 11:05:00 2021 +0200 @@ -115,7 +115,7 @@ fun approx approx' :: "nat \ floatarith \ (float interval) option list \ (float interval) option" where "approx' prec a bs = (case (approx prec a bs) of Some ivl \ Some (round_interval prec ivl) | None \ None)" | - "approx prec (Add a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (+)" | + "approx prec (Add a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (plus_float_interval prec)" | "approx prec (Minus a) bs = lift_un' (approx' prec a bs) uminus" | "approx prec (Mult a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (mult_float_interval prec)" | "approx prec (Inverse a) bs = lift_un (approx' prec a bs) (inverse_float_interval prec)" | @@ -153,7 +153,7 @@ using \bounded_by xs vs\[THEN bounded_byE] by (induct arith arbitrary: ivl) (force split: option.splits if_splits - intro!: plus_in_float_intervalI mult_float_intervalI uminus_in_float_intervalI + intro!: plus_float_intervalI mult_float_intervalI uminus_in_float_intervalI inverse_float_interval_eqI abs_in_float_intervalI min_intervalI max_intervalI cos_float_intervalI diff -r 5131c388a9b0 -r 56db8559eadb src/HOL/Decision_Procs/Approximation_Bounds.thy --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed Apr 07 12:28:19 2021 +0000 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed Apr 07 11:05:00 2021 +0200 @@ -235,6 +235,54 @@ section \Approximation utility functions\ +lift_definition plus_float_interval::"nat \ float interval \ float interval \ float interval" + is "\prec. \(a1, a2). \(b1, b2). (float_plus_down prec a1 b1, float_plus_up prec a2 b2)" + by (auto intro!: add_mono simp: float_plus_down_le float_plus_up_le) + +lemma lower_plus_float_interval: + "lower (plus_float_interval prec ivl ivl') = float_plus_down prec (lower ivl) (lower ivl')" + by transfer auto +lemma upper_plus_float_interval: + "upper (plus_float_interval prec ivl ivl') = float_plus_up prec (upper ivl) (upper ivl')" + by transfer auto + +lemma mult_float_interval_ge: + "real_interval A + real_interval B \ real_interval (plus_float_interval prec A B)" + unfolding less_eq_interval_def + by transfer + (auto simp: lower_plus_float_interval upper_plus_float_interval + intro!: order.trans[OF float_plus_down] order.trans[OF _ float_plus_up]) + +lemma plus_float_interval: + "set_of (real_interval A) + set_of (real_interval B) \ + set_of (real_interval (plus_float_interval prec A B))" +proof - + have "set_of (real_interval A) + set_of (real_interval B) \ + set_of (real_interval A + real_interval B)" + by (simp add: set_of_plus) + also have "\ \ set_of (real_interval (plus_float_interval prec A B))" + using mult_float_interval_ge[of A B prec] by (simp add: set_of_subset_iff') + finally show ?thesis . +qed + +lemma plus_float_intervalI: + "x + y \\<^sub>r plus_float_interval prec A B" + if "x \\<^sub>i real_interval A" "y \\<^sub>i real_interval B" + using plus_float_interval[of A B] that by auto + +lemma plus_float_interval_mono: + "plus_float_interval prec A B \ plus_float_interval prec X Y" + if "A \ X" "B \ Y" + using that + by (auto simp: less_eq_interval_def lower_plus_float_interval upper_plus_float_interval + float_plus_down.rep_eq float_plus_up.rep_eq plus_down_mono plus_up_mono) + +lemma plus_float_interval_monotonic: + "set_of (ivl + ivl') \ set_of (plus_float_interval prec ivl ivl')" + using float_plus_down_le float_plus_up_le lower_plus_float_interval upper_plus_float_interval + by (simp add: set_of_subset_iff) + + definition bnds_mult :: "nat \ float \ float \ float \ float \ float \ float" where "bnds_mult prec a1 a2 b1 b2 = (float_plus_down prec (nprt a1 * pprt b2) @@ -287,7 +335,7 @@ using mult_float_interval[of A B] that by (auto simp: ) -lemma mult_float_interval_mono: +lemma mult_float_interval_mono': "set_of (mult_float_interval prec A B) \ set_of (mult_float_interval prec X Y)" if "set_of A \ set_of X" "set_of B \ set_of Y" using that @@ -295,6 +343,12 @@ unfolding bnds_mult_def atLeastatMost_subset_iff float_plus_down.rep_eq float_plus_up.rep_eq by (auto simp: float_plus_down.rep_eq float_plus_up.rep_eq mult_float_mono1 mult_float_mono2) +lemma mult_float_interval_mono: + "mult_float_interval prec A B \ mult_float_interval prec X Y" + if "A \ X" "B \ Y" + using mult_float_interval_mono'[of A X B Y prec] that + by (simp add: set_of_subset_iff') + definition map_bnds :: "(nat \ float \ float) \ (nat \ float \ float) \ nat \ (float \ float) \ (float \ float)" where diff -r 5131c388a9b0 -r 56db8559eadb src/HOL/Library/Interval_Float.thy --- a/src/HOL/Library/Interval_Float.thy Wed Apr 07 12:28:19 2021 +0000 +++ b/src/HOL/Library/Interval_Float.thy Wed Apr 07 11:05:00 2021 +0200 @@ -184,6 +184,10 @@ for X Y::"'a::linorder interval" by (auto simp: set_of_eq subset_iff) +lemma set_of_subset_iff': + "set_of a \ set_of (b :: 'a :: linorder interval) \ a \ b" + unfolding less_eq_interval_def set_of_subset_iff .. + lemma bounds_of_interval_eq_lower_upper: "bounds_of_interval ivl = (lower ivl, upper ivl)" if "lower ivl \ upper ivl" using that