--- a/src/HOL/Algebra/Exponent.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/Exponent.thy Wed Aug 30 03:19:08 2006 +0200
@@ -327,6 +327,7 @@
apply (subst times_binomial_minus1_eq, simp, simp)
apply (subst exponent_mult_add, simp)
apply (simp (no_asm_simp) add: zero_less_binomial_iff)
+apply arith
apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
done
--- a/src/HOL/Algebra/UnivPoly.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Aug 30 03:19:08 2006 +0200
@@ -513,7 +513,7 @@
have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: Pi_def)
from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
- by (simp cong: R.finsum_cong add: Pi_def)
+ by (simp cong: R.finsum_cong add: Pi_def) arith
have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
show ?thesis
--- a/src/HOL/Algebra/poly/LongDiv.ML Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.ML Wed Aug 30 03:19:08 2006 +0200
@@ -24,8 +24,6 @@
val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma";
-fast_arith_split_limit := 0; (* FIXME: rewrite proofs *)
-
Goal
"!! f::(nat=>'a::ring). \
\ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
@@ -279,5 +277,3 @@
by (rtac long_div_quo_unique 1);
by (REPEAT (atac 1));
qed "long_div_rem_unique";
-
-fast_arith_split_limit := 9; (* FIXME *)
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Aug 30 03:19:08 2006 +0200
@@ -187,8 +187,6 @@
by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
qed
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
-
lemma coeff_mult [simp]:
"coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
proof -
@@ -228,8 +226,6 @@
by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
qed
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
-
lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
by (unfold up_uminus_def) (simp add: ring_simps)
--- a/src/HOL/Complex/NSCA.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy Wed Aug 30 03:19:08 2006 +0200
@@ -764,10 +764,8 @@
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/Divides.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Divides.thy Wed Aug 30 03:19:08 2006 +0200
@@ -710,7 +710,7 @@
apply (rule iffI)
apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
prefer 3; apply assumption
- apply (simp_all add: quorem_def)
+ apply (simp_all add: quorem_def) apply arith
apply (rule conjI)
apply (rule_tac P="%x. n * (m div n) \<le> x" in
subst [OF mod_div_equality [of _ n]])
--- a/src/HOL/HoareParallel/Graph.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Wed Aug 30 03:19:08 2006 +0200
@@ -111,8 +111,6 @@
apply(erule Ex_first_occurrence)
done
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
-
lemma Graph2:
"\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
apply (unfold Reach_def)
@@ -128,7 +126,6 @@
apply(case_tac "j=R")
apply(erule_tac x = "Suc i" in allE)
apply simp
- apply arith
apply (force simp add:nth_list_update)
apply simp
apply(erule exE)
@@ -156,7 +153,6 @@
apply simp
apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
prefer 2 apply arith
-apply simp
apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
prefer 2 apply arith
apply simp
@@ -177,26 +173,19 @@
prefer 2 apply arith
apply(drule_tac n = "Suc nata" in Compl_lemma)
apply clarify
+ ML {* fast_arith_split_limit := 0; *} (*FIXME*)
apply force
+ ML {* fast_arith_split_limit := 9; *} (*FIXME*)
apply(drule leI)
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
apply(erule_tac x = "m - (Suc nata)" in allE)
apply(case_tac "m")
apply simp
apply simp
- apply(subgoal_tac "natb - nata < Suc natb")
- prefer 2 apply(erule thin_rl)+ apply arith
- apply simp
- apply(case_tac "length path")
- apply force
-apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
apply simp
-apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
-apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
-apply simp
-apply arith
done
+
subsubsection{* Graph 3 *}
lemma Graph3:
@@ -254,8 +243,6 @@
apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
prefer 2 apply arith
apply simp
- apply(erule mp)
- apply arith
--{* T is a root *}
apply(case_tac "m=0")
apply force
@@ -282,8 +269,6 @@
apply(force simp add: nth_list_update)
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
-
subsubsection{* Graph 4 *}
lemma Graph4:
--- a/src/HOL/HoareParallel/RG_Hoare.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Wed Aug 30 03:19:08 2006 +0200
@@ -329,7 +329,7 @@
apply(rule_tac x=0 in exI,simp)
done
-lemma Basic_sound:
+lemma Basic_sound:
" \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar;
stable pre rely; stable post rely\<rbrakk>
\<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
@@ -369,15 +369,16 @@
apply(drule_tac s="Some (Basic f)" in sym,simp)
apply(case_tac "x!Suc j",simp)
apply(rule ctran.elims,simp)
- apply(simp_all)
+apply(simp_all)
apply(drule_tac c=sa in subsetD,simp)
apply clarify
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
- apply(case_tac x,simp+)
+ apply(case_tac x,simp+)
apply(erule_tac x=i in allE)
- apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
+apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
+ apply arith+
apply(case_tac x)
- apply(simp add:last_length)+
+apply(simp add:last_length)+
done
subsubsection{* Soundness of the Await rule *}
@@ -496,7 +497,7 @@
apply(drule_tac s="Some (Await b P)" in sym,simp)
apply(case_tac "x!Suc j",simp)
apply(rule ctran.elims,simp)
- apply(simp_all)
+apply(simp_all)
apply(drule Star_imp_cptn)
apply clarify
apply(erule_tac x=sa in allE)
@@ -510,17 +511,16 @@
apply simp
apply clarify
apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
- apply(case_tac x,simp+)
+ apply(case_tac x,simp+)
apply(erule_tac x=i in allE)
- apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
+apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
+ apply arith+
apply(case_tac x)
- apply(simp add:last_length)+
+apply(simp add:last_length)+
done
subsubsection{* Soundness of the Conditional rule *}
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
-
lemma Cond_sound:
"\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post];
\<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
@@ -537,7 +537,6 @@
apply(simp add:assum_def)
apply(simp add:assum_def)
apply(erule_tac m="length x" in etran_or_ctran,simp+)
- apply(case_tac x,simp+)
apply(case_tac x, (simp add:last_length)+)
apply(erule exE)
apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
@@ -549,18 +548,7 @@
apply(erule_tac x="sa" in allE)
apply(drule_tac c="drop (Suc m) x" in subsetD)
apply simp
- apply(rule conjI)
- apply force
apply clarify
- apply(subgoal_tac "(Suc m) + i \<le> length x")
- apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
- apply(rotate_tac -2)
- apply simp
- apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
- apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
- apply arith
- apply arith
- apply arith
apply simp
apply clarify
apply(case_tac "i\<le>m")
@@ -569,52 +557,34 @@
apply(erule_tac x=i in allE, erule impE, assumption)
apply simp+
apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
- apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
- apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
- apply(rotate_tac -2)
- apply simp
- apply(erule mp)
- apply arith
- apply arith
- apply arith
- apply(case_tac "length (drop (Suc m) x)",simp)
- apply(erule_tac x="sa" in allE)
- back
- apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
- apply(rule conjI)
- apply force
- apply clarify
- apply(subgoal_tac "(Suc m) + i \<le> length x")
- apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
- apply(rotate_tac -2)
- apply simp
- apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
- apply(subgoal_tac "Suc (Suc (m + i)) < length x")
- apply simp
- apply arith
- apply arith
- apply arith
- apply simp
- apply clarify
- apply(case_tac "i\<le>m")
- apply(drule le_imp_less_or_eq)
- apply(erule disjE)
- apply(erule_tac x=i in allE, erule impE, assumption)
- apply simp
+ apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+ apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+ apply(rotate_tac -2)
apply simp
- apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
- apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
- apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
- apply(rotate_tac -2)
- apply simp
- apply(erule mp)
- apply arith
apply arith
apply arith
+apply(case_tac "length (drop (Suc m) x)",simp)
+apply(erule_tac x="sa" in allE)
+back
+apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
+ apply clarify
+apply simp
+apply clarify
+apply(case_tac "i\<le>m")
+ apply(drule le_imp_less_or_eq)
+ apply(erule disjE)
+ apply(erule_tac x=i in allE, erule impE, assumption)
+ apply simp
+ apply simp
+apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+ apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+ apply(rotate_tac -2)
+ apply simp
+ apply arith
+apply arith
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
-
subsubsection{* Soundness of the Sequential rule *}
inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
@@ -656,7 +626,6 @@
apply(simp add:lift_def)
apply simp
done
-
declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
lemma Seq_sound2 [rule_format]:
@@ -714,7 +683,6 @@
apply simp+
apply(simp add:lift_def)
done
-
(*
lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
apply(simp only:last_length [THEN sym])
@@ -737,8 +705,6 @@
apply simp
done
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
-
lemma Seq_sound:
"\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
\<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
@@ -862,8 +828,6 @@
apply simp
apply(erule mp)
apply(case_tac ys,simp+)
- apply arith
- apply arith
apply force
apply arith
apply force
@@ -877,8 +841,6 @@
apply(case_tac ys,simp+)
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
-
subsubsection{* Soundness of the While rule *}
lemma last_append[rule_format]:
@@ -924,8 +886,6 @@
apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
done
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
-
lemma While_sound_aux [rule_format]:
"\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
stable pre rely; stable post rely; x \<in> cptn_mod \<rbrakk>
@@ -1092,8 +1052,6 @@
apply simp
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
-
lemma While_sound:
"\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
\<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
--- a/src/HOL/Hyperreal/Integration.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Wed Aug 30 03:19:08 2006 +0200
@@ -173,10 +173,7 @@
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)
-ML {* fast_arith_split_limit := 0; *} (* FIXME *)
-apply simp
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
+apply (drule_tac x = "psize D - Suc n" in spec, simp)
done
lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
@@ -439,8 +436,6 @@
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)
@@ -472,7 +467,6 @@
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/Lim.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Aug 30 03:19:08 2006 +0200
@@ -2239,7 +2239,7 @@
thus ?thesis by simp
qed
-ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
+ML {* fast_arith_split_limit := 0; *} (* FIXME *)
lemma LIMSEQ_SEQ_conv2:
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
@@ -2321,7 +2321,7 @@
ultimately show False by simp
qed
-ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
--- a/src/HOL/Hyperreal/Ln.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Wed Aug 30 03:19:08 2006 +0200
@@ -394,7 +394,7 @@
apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
apply force
apply assumption
- apply (simp (asm_lr) add: power2_eq_square mult_compare_simps)
+ apply (simp 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,7 +408,6 @@
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/NSA.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Aug 30 03:19:08 2006 +0200
@@ -329,7 +329,7 @@
apply (rule InfinitesimalI)
apply (drule HFiniteD, clarify)
apply (simp only: abs_mult)
-apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp)
+apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp add: split_if)
apply (subgoal_tac "0 < r / t")
apply (rule mult_strict_mono)
apply (simp add: InfinitesimalD SReal_divide)
--- a/src/HOL/Hyperreal/Poly.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Wed Aug 30 03:19:08 2006 +0200
@@ -426,6 +426,7 @@
"\<forall>p2. length (p1 +++ p2) =
(if (length p1 < length p2) then length p2 else length p1)"
apply (induct "p1", simp_all)
+apply arith
done
lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
--- a/src/HOL/Hyperreal/Series.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Wed Aug 30 03:19:08 2006 +0200
@@ -323,8 +323,6 @@
lemmas sumr_geometric = geometric_sum [where 'a = real]
-ML {* fast_arith_split_limit := 0; *} (* FIXME: needed because otherwise a premise gets simplified away *)
-
lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
apply (case_tac "x = 1")
apply (auto dest!: LIMSEQ_rabs_realpow_zero2
@@ -335,8 +333,6 @@
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
-
text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
lemma summable_convergent_sumr_iff:
--- a/src/HOL/Hyperreal/Transcendental.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed Aug 30 03:19:08 2006 +0200
@@ -400,6 +400,8 @@
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])
@@ -576,6 +578,8 @@
text{* FIXME: Long proofs*}
+ML {* 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 *
@@ -589,56 +593,53 @@
and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h)
- (real n * (x ^ (n - Suc 0))))"
in lemma_termdiff5)
- -- "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
+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])
-apply arith
+apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
done
ML {* fast_arith_split_limit := 9; *} (* FIXME *)
@@ -655,7 +656,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 (frule abs_triangle_ineq [THEN order_le_less_trans])
+apply (drule 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)
@@ -667,11 +668,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 (frule abs_triangle_ineq [THEN order_le_less_trans])
+apply (drule 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)
@@ -2580,5 +2581,5 @@
apply (drule_tac [3] LIM_fun_gt_zero)
apply force+
done
-
+
end
--- a/src/HOL/Import/HOL4Compat.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Wed Aug 30 03:19:08 2006 +0200
@@ -221,7 +221,7 @@
by simp
lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
- by simp
+ by (simp, arith)
lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
by (simp add: max_def)
--- a/src/HOL/Integ/IntDef.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Aug 30 03:19:08 2006 +0200
@@ -387,7 +387,7 @@
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
have "(\<lambda>(x,y). {x-y}) respects intrel"
- by (simp add: congruent_def)
+ by (simp add: congruent_def) arith
thus ?thesis
by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
qed
--- a/src/HOL/Isar_examples/HoareEx.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy Wed Aug 30 03:19:08 2006 +0200
@@ -317,6 +317,7 @@
apply simp
apply clarsimp
apply clarsimp
+ apply arith
prefer 2
apply clarsimp
apply (clarsimp simp: nat_distrib)
--- a/src/HOL/Matrix/MatrixGeneral.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Aug 30 03:19:08 2006 +0200
@@ -934,10 +934,11 @@
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (case_tac "j + int u < 0")
- apply simp
+ apply (simp, arith)
apply (case_tac "i + int v < 0")
+ apply (simp add: neg_def, arith)
apply (simp add: neg_def)
- apply (simp add: neg_def)
+ apply arith
done
lemma Rep_take_columns[simp]:
--- a/src/HOL/Matrix/SparseMatrix.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Wed Aug 30 03:19:08 2006 +0200
@@ -338,12 +338,17 @@
apply (subst Rep_matrix_mult)
apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
apply (simp_all)
+ apply (intro strip, rule conjI)
apply (intro strip)
+ apply (drule_tac max_helper)
+ apply (simp)
+ apply (auto)
apply (rule zero_imp_mult_zero)
apply (rule disjI2)
apply (rule nrows)
apply (rule order_trans[of _ 1])
- apply auto
+ apply (simp)
+ apply (simp)
done
qed
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Wed Aug 30 03:19:08 2006 +0200
@@ -968,14 +968,14 @@
apply fast
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp
+apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
apply (rule progression_refl)
(* case b= False *)
apply simp
apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
apply fast
(* case exit Loop *)
@@ -1003,7 +1003,7 @@
apply fast
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
-apply simp
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
apply (rule progression_refl)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 30 03:19:08 2006 +0200
@@ -663,7 +663,7 @@
(* show P x of bspec *)
apply simp
apply (subgoal_tac "length mt_pre \<le> pc'")
- apply (simp add: nth_append)
+ apply (simp add: nth_append) apply arith
(* subgoals *)
apply (simp add: eff_def xcpt_eff_def)
@@ -965,6 +965,7 @@
apply (simp only:)
apply (rule check_type_mono) apply assumption
apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append max_ac)
+apply arith
apply (simp add: nth_append)
apply (erule conjE)+
@@ -1282,7 +1283,6 @@
apply auto
done
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G;
max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
@@ -1319,7 +1319,6 @@
apply (simp add: max_def)
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc;
0 \<le> (int pc + i); nat (int pc + i) < max_pc;
@@ -1644,7 +1643,7 @@
done
-ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
+
lemma wt_method_compTpExpr_Exprs_corresp: "
\<lbrakk> jmb = (pns,lvars,blk,res);
@@ -1923,7 +1922,6 @@
done
-ML {* fast_arith_split_limit := 9; *} (* FIXME *)
lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] =
wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]
--- a/src/HOL/NumberTheory/Chinese.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Wed Aug 30 03:19:08 2006 +0200
@@ -175,6 +175,11 @@
apply (rule_tac [!] funprod_zgcd)
apply safe
apply simp_all
+ apply (subgoal_tac "i<n")
+ prefer 2
+ apply arith
+ apply (case_tac [2] i)
+ apply simp_all
done
lemma x_sol_lin_aux:
--- a/src/HOL/NumberTheory/Fib.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Wed Aug 30 03:19:08 2006 +0200
@@ -72,6 +72,7 @@
apply (simp add: fib.Suc_Suc mod_Suc)
apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
mod_Suc zmult_int [symmetric])
+ apply (presburger (no_abs))
done
text{*We now obtain a version for the natural numbers via the coercion
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Aug 30 03:19:08 2006 +0200
@@ -193,8 +193,6 @@
then show ?thesis by auto
qed
-ML {* fast_arith_split_limit := 0; *} (*FIXME*)
-
lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
(p * b \<noteq> q * a)"
proof
@@ -236,8 +234,6 @@
with q_g_2 show False by auto
qed
-ML {* fast_arith_split_limit := 9; *} (*FIXME*)
-
lemma (in QRTEMP) P_set_finite: "finite (P_set)"
using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)