lin_arith_prover splits certain operators (e.g. min, max, abs)
--- a/src/HOL/Complex/NSCA.thy Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy Sun Jul 30 05:53:10 2006 +0200
@@ -764,8 +764,10 @@
apply (subgoal_tac "0 < v")
prefer 2 apply arith
apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
-apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
apply (simp add: power2_eq_square)
+ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
+apply (rule_tac lemma_sqrt_hcomplex_capprox, auto)
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
done
lemma CFinite_HFinite_iff:
--- a/src/HOL/Hyperreal/Integration.thy Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Sun Jul 30 05:53:10 2006 +0200
@@ -173,7 +173,10 @@
prefer 2 apply assumption
apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
prefer 2 apply arith
-apply (drule_tac x = "psize D - Suc n" in spec, simp)
+apply (drule_tac x = "psize D - Suc n" in spec)
+ML {* fast_arith_split_limit := 0; *} (* FIXME *)
+apply simp
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
done
lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
@@ -436,6 +439,8 @@
apply (simp add: right_diff_distrib)
done
+ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
+
lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
==> Integral(a,b) f' (f(b) - f(a))"
apply (drule order_le_imp_less_or_eq, auto)
@@ -467,6 +472,7 @@
fine_def)
done
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
by simp
--- a/src/HOL/Hyperreal/Ln.thy Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Sun Jul 30 05:53:10 2006 +0200
@@ -394,7 +394,7 @@
apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
apply force
apply assumption
- apply (simp add: power2_eq_square mult_compare_simps)
+ apply (simp (asm_lr) add: power2_eq_square mult_compare_simps)
apply (rule mult_imp_div_pos_less)
apply (rule mult_pos_pos, assumption, assumption)
apply (subgoal_tac "xa * xa = abs xa * abs xa")
@@ -408,6 +408,7 @@
apply (subst diff_minus [THEN sym])+
apply (subst ln_div [THEN sym])
apply arith
+ apply assumption
apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq
add_divide_distrib power2_eq_square)
apply (rule mult_pos_pos, assumption)+
--- a/src/HOL/Hyperreal/Poly.thy Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Sun Jul 30 05:53:10 2006 +0200
@@ -425,7 +425,7 @@
lemma poly_add_length [rule_format]:
"\<forall>p2. length (p1 +++ p2) =
(if (length p1 < length p2) then length p2 else length p1)"
-apply (induct "p1", simp_all, arith)
+apply (induct "p1", simp_all)
done
lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
--- a/src/HOL/Hyperreal/Transcendental.thy Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Sun Jul 30 05:53:10 2006 +0200
@@ -400,8 +400,6 @@
apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le)
apply (auto simp add: mult_assoc power_abs abs_mult)
- prefer 2
- apply (drule_tac x = 0 in spec, force)
apply (auto simp add: power_abs mult_ac)
apply (rule_tac a2 = "z ^ n"
in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
@@ -578,8 +576,6 @@
text{* FIXME: Long proofs*}
-ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *} (* FIXME: rewrite proofs *)
-
lemma termdiffs_aux:
"[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
==> (\<lambda>h. \<Sum>n. c n *
@@ -593,56 +589,59 @@
and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h)
- (real n * (x ^ (n - Suc 0))))"
in lemma_termdiff5)
-apply (auto simp add: add_commute)
-apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
-apply (rule_tac [2] x = K in powser_insidea, auto)
-apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
-apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
-apply (simp add: diffs_def mult_assoc [symmetric])
-apply (subgoal_tac
- "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n)
- = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ")
-apply (auto simp add: abs_mult)
-apply (drule diffs_equiv)
-apply (drule sums_summable)
-apply (simp_all add: diffs_def)
-apply (simp add: diffs_def mult_ac)
-apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
-apply auto
+ -- "3 subgoals"
+ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
+ apply (auto simp add: add_commute)
+ apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
+ apply (rule_tac [2] x = K in powser_insidea, auto)
+ apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
+ apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
+ apply (simp add: diffs_def mult_assoc [symmetric])
+ apply (subgoal_tac
+ "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n)
+ = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ")
+ apply (auto simp add: abs_mult)
+ apply (drule diffs_equiv)
+ apply (drule sums_summable)
+ apply (simp_all add: diffs_def)
+ apply (simp add: diffs_def mult_ac)
+ apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
+ apply auto
prefer 2
apply (rule ext)
- apply (simp add: diffs_def)
+ apply (simp add: diffs_def)
apply (case_tac "n", auto)
txt{*23*}
apply (drule abs_ge_zero [THEN order_le_less_trans])
- apply (simp add: mult_ac)
+ apply (simp add: mult_ac)
apply (drule abs_ge_zero [THEN order_le_less_trans])
- apply (simp add: mult_ac)
+ apply (simp add: mult_ac)
apply (drule diffs_equiv)
apply (drule sums_summable)
-apply (subgoal_tac
- "summable
- (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
- r ^ (n - Suc 0)) =
- summable
- (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
-apply simp
-apply (rule_tac f = summable in arg_cong, rule ext)
+ apply (subgoal_tac
+ "summable
+ (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
+ r ^ (n - Suc 0)) =
+ summable
+ (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
+ apply simp
+ apply (rule_tac f = summable in arg_cong, rule ext)
txt{*33*}
-apply (case_tac "n", auto)
-apply (case_tac "nat", auto)
-apply (drule abs_ge_zero [THEN order_le_less_trans], auto)
+ apply (case_tac "n", auto)
+ apply (case_tac "nat", auto)
+ apply (drule abs_ge_zero [THEN order_le_less_trans], auto)
apply (drule abs_ge_zero [THEN order_le_less_trans])
apply (simp add: mult_assoc)
apply (rule mult_left_mono)
- prefer 2 apply arith
+ prefer 2 apply arith
apply (subst add_commute)
apply (simp (no_asm) add: mult_assoc [symmetric])
apply (rule lemma_termdiff3)
-apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
+ apply (auto intro: abs_triangle_ineq [THEN order_trans])
+apply arith
done
-ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
lemma termdiffs:
"[| summable(%n. c(n) * (K ^ n));
@@ -656,7 +655,7 @@
apply (simp add: LIM_def, safe)
apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
apply (auto simp add: less_diff_eq)
-apply (drule abs_triangle_ineq [THEN order_le_less_trans])
+apply (frule abs_triangle_ineq [THEN order_le_less_trans])
apply (rule_tac y = 0 in order_le_less_trans, auto)
apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (\<Sum>n. (c n) * (x ^ n)) & (%n. (c n) * ((x + xa) ^ n)) sums (\<Sum>n. (c n) * ( (x + xa) ^ n))")
apply (auto intro!: summable_sums)
@@ -668,11 +667,11 @@
apply (simp add: diff_def divide_inverse add_ac mult_ac)
apply (rule LIM_zero_cancel)
apply (rule_tac g = "%h. \<Sum>n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))" in LIM_trans)
- prefer 2 apply (blast intro: termdiffs_aux)
+ prefer 2 apply (blast intro: termdiffs_aux)
apply (simp add: LIM_def, safe)
apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
apply (auto simp add: less_diff_eq)
-apply (drule abs_triangle_ineq [THEN order_le_less_trans])
+apply (frule abs_triangle_ineq [THEN order_le_less_trans])
apply (rule_tac y = 0 in order_le_less_trans, auto)
apply (subgoal_tac "summable (%n. (diffs c) (n) * (x ^ n))")
apply (rule_tac [2] powser_inside, auto)
@@ -2581,5 +2580,5 @@
apply (drule_tac [3] LIM_fun_gt_zero)
apply force+
done
-
+
end