linear arithmetic splits certain operators (e.g. min, max, abs)
--- a/NEWS Wed Jul 26 13:31:07 2006 +0200
+++ b/NEWS Wed Jul 26 19:23:04 2006 +0200
@@ -510,6 +510,12 @@
(i.e. a boolean expression) by compiling it to ML. The goal is
"proved" (via the oracle "Evaluation") if it evaluates to True.
+* Linear arithmetic now splits certain operators (e.g. min, max, abs) also
+when invoked by the simplifier. This results in the simplifier being more
+powerful on arithmetic goals.
+INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain
+the old behavior.
+
* Support for hex (0x20) and binary (0b1001) numerals.
*** HOL-Algebra ***
--- a/doc-src/TutorialI/Advanced/WFrec.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Jul 26 19:23:04 2006 +0200
@@ -90,19 +90,10 @@
\noindent
The inclusion remains to be proved. After unfolding some definitions,
-we are left with simple arithmetic:
+we are left with simple arithmetic that is dispatched automatically.
*}
-apply (clarify, simp add: measure_def inv_image_def)
-
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-
-\noindent
-And that is dispatched automatically:
-*}
-
-by arith
+by (clarify, simp add: measure_def inv_image_def)
text{*\noindent
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Jul 26 13:31:07 2006 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Jul 26 19:23:04 2006 +0200
@@ -119,22 +119,11 @@
\noindent
The inclusion remains to be proved. After unfolding some definitions,
-we are left with simple arithmetic:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
-\end{isabelle}
-
-\noindent
-And that is dispatched automatically:%
+we are left with simple arithmetic that is dispatched automatically.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{by}\isamarkupfalse%
-\ arith%
+\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
--- a/src/HOL/Algebra/UnivPoly.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Jul 26 19:23:04 2006 +0200
@@ -972,13 +972,13 @@
next
case (Suc j)
have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+ using Suc by (auto intro!: funcset_mem [OF Rg])
have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+ using Suc by (auto intro!: funcset_mem [OF Rg])
have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
using Suc by (auto intro!: funcset_mem [OF Rf])
have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+ using Suc by (auto intro!: funcset_mem [OF Rg])
have R11: "g 0 \<in> carrier R"
using Suc by (auto intro!: funcset_mem [OF Rg])
from Suc show ?case
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Wed Jul 26 19:23:04 2006 +0200
@@ -231,7 +231,7 @@
"greatest_msg other = 0"
lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
-by (induct X, auto, arith+)
+by (induct X, auto)
subsubsection{*sets of keys*}
--- a/src/HOL/Auth/Guard/Guard_Public.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Wed Jul 26 19:23:04 2006 +0200
@@ -95,7 +95,7 @@
apply (induct evs, auto simp: initState.simps)
apply (drule used_sub_parts_used, safe)
apply (drule greatest_msg_is_greatest, arith)
-by (simp, arith)
+by simp
subsubsection{*function giving a new nonce*}
@@ -171,4 +171,4 @@
apply (frule_tac A=A in priK_analz_iff_bad)
by (simp add: knows_decomp)+
-end
\ No newline at end of file
+end
--- a/src/HOL/Bali/AxCompl.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Bali/AxCompl.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1421,7 +1421,6 @@
apply (drule finite_subset)
apply (erule finite_imageI)
apply auto
-apply arith
done
--- a/src/HOL/Binomial.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Binomial.thy Wed Jul 26 19:23:04 2006 +0200
@@ -33,9 +33,8 @@
by simp
lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
-apply (induct "n", auto)
-apply (erule allE)
-apply (erule mp, arith)
+apply (induct "n")
+apply auto
done
declare binomial_0 [simp del] binomial_Suc [simp del]
--- a/src/HOL/Complex/CLim.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Complex/CLim.thy Wed Jul 26 19:23:04 2006 +0200
@@ -178,7 +178,7 @@
apply (simp add: CInfinitesimal_hcmod_iff star_of_def
Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod, blast)
apply (drule_tac x = r in spec, clarify)
-apply (drule FreeUltrafilterNat_all, ultra, arith)
+apply (drule FreeUltrafilterNat_all, ultra)
done
--- a/src/HOL/Divides.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Divides.thy Wed Jul 26 19:23:04 2006 +0200
@@ -710,8 +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 arith
+ 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 Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Wed Jul 26 19:23:04 2006 +0200
@@ -126,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)
@@ -154,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
@@ -175,24 +173,16 @@
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
@@ -253,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
--- a/src/HOL/HoareParallel/OG_Examples.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Wed Jul 26 19:23:04 2006 +0200
@@ -298,7 +298,6 @@
--{* 98 verification conditions *}
apply auto
--{* auto takes about 3 minutes !! *}
-apply arith+
done
text {* Easier Version: without AWAIT. Apt and Olderog. page 256: *}
@@ -332,7 +331,6 @@
--{* 20 vc *}
apply auto
--{* auto takes aprox. 2 minutes. *}
-apply arith+
done
subsection {* Producer/Consumer *}
--- a/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 26 19:23:04 2006 +0200
@@ -361,11 +361,8 @@
apply clarify
apply(frule_tac j=0 and k="j" and p=pre in stability)
apply simp_all
- apply arith
apply(erule_tac x=i in allE,simp)
apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
- apply arith
- apply arith
apply(case_tac "x!j")
apply clarify
apply simp
@@ -492,11 +489,8 @@
apply(simp add:assum_def)
apply clarify
apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
- apply arith
apply(erule_tac x=i in allE,simp)
apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
- apply arith
- apply arith
apply(case_tac "x!j")
apply clarify
apply simp
@@ -543,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)
@@ -555,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")
@@ -575,49 +557,33 @@
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
- done
+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
subsubsection{* Soundness of the Sequential rule *}
@@ -862,8 +828,6 @@
apply simp
apply(erule mp)
apply(case_tac ys,simp+)
- apply arith
- apply arith
apply force
apply arith
apply force
--- a/src/HOL/Hyperreal/HTranscendental.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Wed Jul 26 19:23:04 2006 +0200
@@ -364,7 +364,7 @@
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
apply (rule bexI [OF _ Rep_star_star_n], auto)
apply (rule_tac x = "exp u" in exI)
-apply (ultra, arith)
+apply ultra
done
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
--- a/src/HOL/Hyperreal/Integration.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Wed Jul 26 19:23:04 2006 +0200
@@ -323,7 +323,6 @@
apply (drule add_strict_mono, assumption)
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
mult_less_cancel_right)
-apply arith
done
lemma Integral_zero [simp]: "Integral(a,a) f 0"
@@ -423,7 +422,7 @@
\<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
in order_trans)
apply (rule abs_triangle_ineq [THEN [2] order_trans])
-apply (simp add: right_diff_distrib, arith)
+apply (simp add: right_diff_distrib)
apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
apply (rule add_mono)
apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
@@ -434,7 +433,7 @@
apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
apply (rule order_trans)
apply (auto simp add: abs_le_interval_iff)
-apply (simp add: right_diff_distrib, arith)
+apply (simp add: right_diff_distrib)
done
lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
@@ -577,7 +576,7 @@
apply (auto dest: partition_lt_cancel)
apply (rule_tac x=N and y=n in linorder_cases)
apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
-apply (drule_tac n = n in partition_lt_gen, auto, arith)
+apply (drule_tac n = n in partition_lt_gen, auto)
apply (drule_tac x = n in spec)
apply (simp split: split_if_asm)
done
@@ -741,7 +740,6 @@
==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
apply (simp add: tpart_def partition_def, safe)
apply (rule_tac x = "N - n" in exI, auto)
-apply (drule_tac x = "na + n" in spec, arith)+
done
lemma fine_right1:
@@ -752,7 +750,7 @@
==> fine ga (%x. D(x + n),%x. p(x + n))"
apply (auto simp add: fine_def gauge_def)
apply (drule_tac x = "na + n" in spec)
-apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
+apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto)
apply (simp add: tpart_def, safe)
apply (subgoal_tac "D n \<le> p (na + n)")
apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
@@ -783,7 +781,7 @@
apply ((drule spec)+, auto)
apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption)
apply (auto simp only: rsum_add left_distrib [symmetric]
- mult_2_right [symmetric] real_mult_less_iff1, arith)
+ mult_2_right [symmetric] real_mult_less_iff1)
done
lemma partition_lt_gen2:
@@ -834,7 +832,7 @@
apply arith
apply (drule add_strict_mono, assumption)
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
- real_mult_less_iff1, arith)
+ real_mult_less_iff1)
done
lemma Integral_imp_Cauchy:
@@ -853,7 +851,7 @@
apply (erule_tac V = "0 < e" in thin_rl)
apply (drule add_strict_mono, assumption)
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
- real_mult_less_iff1, arith)
+ real_mult_less_iff1)
done
lemma Cauchy_iff2:
--- a/src/HOL/Hyperreal/Lim.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1484,7 +1484,7 @@
apply (rule_tac x = s in exI, clarify)
apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
apply (drule_tac x = "xa-x" in spec)
-apply (auto simp add: abs_ge_self, arith+)
+apply (auto simp add: abs_ge_self)
done
text{*Refine the above to existence of least upper bound*}
@@ -2236,6 +2236,8 @@
thus ?thesis by simp
qed
+ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
+
lemma LIMSEQ_SEQ_conv2:
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "X -- a --> L"
@@ -2316,6 +2318,7 @@
ultimately show False by simp
qed
+ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
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/MacLaurin.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Jul 26 19:23:04 2006 +0200
@@ -390,7 +390,7 @@
lemma mod_exhaust_less_4:
"m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
-by (case_tac "m mod 4", auto, arith)
+by auto
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
"0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
--- a/src/HOL/Hyperreal/NSA.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1349,7 +1349,8 @@
==> hypreal_of_real x + u < hypreal_of_real y"
apply (simp add: Infinitesimal_def)
apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
-apply (simp add: abs_less_iff)
+(* FIXME: arith simproc bug with apply (simp add: abs_less_iff) *)
+apply simp
done
lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
--- a/src/HOL/Hyperreal/Poly.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1023,7 +1023,7 @@
apply (induct "p", auto)
apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono simp add: abs_mult, arith)
+apply (auto intro!: mult_mono simp add: abs_mult)
done
end
--- a/src/HOL/Hyperreal/SEQ.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Wed Jul 26 19:23:04 2006 +0200
@@ -745,7 +745,6 @@
apply (simp add: Bseq_def, safe)
apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
apply auto
-apply arith
apply (rule_tac x = N in exI, safe)
apply (drule_tac x = n in spec, arith)
apply (auto simp add: Bseq_iff2)
@@ -754,7 +753,7 @@
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
apply (simp add: Bseq_def)
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
-apply (drule_tac [2] x = n in spec, arith+)
+apply (drule_tac x = n in spec, arith)
done
@@ -824,9 +823,7 @@
lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
==> \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
-apply safe
-apply (drule spec, auto, arith)
-done
+by auto
lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
by auto
--- a/src/HOL/Hyperreal/Series.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Wed Jul 26 19:23:04 2006 +0200
@@ -274,10 +274,6 @@
apply (induct "no", auto)
apply (drule_tac x = "Suc no" in spec)
apply (simp add: add_ac)
-(* FIXME why does simp require a separate step to prove the (pure arithmetic)
- left-over? With del cong: strong_setsum_cong it works!
-*)
-apply simp
done
lemma sumr_pos_lt_pair:
@@ -299,15 +295,7 @@
apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
prefer 3 apply assumption
apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
-apply simp_all
-apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
-apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
-prefer 3 apply simp
-apply (drule_tac [2] x = 0 in spec)
- prefer 2 apply simp
-apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
-apply (simp add: abs_if)
-apply (auto simp add: linorder_not_less [symmetric])
+apply simp_all
done
text{*A summable series of positive terms has limit that is at least as
--- a/src/HOL/Hyperreal/Transcendental.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed Jul 26 19:23:04 2006 +0200
@@ -526,7 +526,7 @@
apply (rule setsum_abs [THEN real_le_trans])
apply (rule real_setsum_nat_ivl_bounded)
apply (auto dest!: less_add_one intro!: mult_mono simp add: power_add abs_mult)
-apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
+apply (auto intro!: power_mono zero_le_power simp add: power_abs)
done
lemma lemma_termdiff4:
@@ -576,9 +576,10 @@
done
-
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 *
@@ -641,6 +642,8 @@
apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
done
+ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+
lemma termdiffs:
"[| summable(%n. c(n) * (K ^ n));
summable(%n. (diffs c)(n) * (K ^ n));
@@ -748,7 +751,7 @@
apply (subst lemma_exp_ext)
apply (subgoal_tac "DERIV (%u. \<Sum>n. inverse (real (fact n)) * u ^ n) x :> (\<Sum>n. diffs (%n. inverse (real (fact n))) n * x ^ n)")
apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
-apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
+apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs)
done
lemma lemma_sin_ext:
@@ -769,14 +772,14 @@
apply (subst lemma_sin_ext)
apply (auto simp add: sin_fdiffs2 [symmetric])
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
-apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
+apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
done
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
apply (subst lemma_cos_ext)
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
-apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
+apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
done
@@ -2533,7 +2536,7 @@
apply (rule_tac x = ea in exI, auto)
apply (drule_tac x = "f (x) + xa" and P = "%y. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)" in spec)
apply auto
-apply (drule sym, auto, arith)
+apply (drule sym, auto)
done
lemma isCont_inv_fun_inv:
--- a/src/HOL/IMP/Compiler.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMP/Compiler.thy Wed Jul 26 19:23:04 2006 +0200
@@ -101,7 +101,6 @@
apply(rule ccontr)
apply(drule_tac f = length in arg_cong)
apply simp
-apply arith
done
lemma reduce_exec1:
@@ -293,6 +292,6 @@
with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
qed
-(* To Do: connect with Machine 0 using M_equiv *)
+(* TODO: connect with Machine 0 using M_equiv *)
-end
\ No newline at end of file
+end
--- a/src/HOL/IMP/Machines.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMP/Machines.thy Wed Jul 26 19:23:04 2006 +0200
@@ -168,11 +168,10 @@
apply fastsimp
apply simp
apply simp
- apply arith
apply simp
- apply arith
apply(fastsimp simp add:exec01.JMPB)
done
+
(*
lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
apply(induct xs)
@@ -188,6 +187,7 @@
apply simp_all
done
*)
+
lemma direction2:
"rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
--- a/src/HOL/IMPP/Hoare.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMPP/Hoare.thy Wed Jul 26 19:23:04 2006 +0200
@@ -381,7 +381,6 @@
apply (drule finite_subset)
apply (erule finite_imageI)
apply (simp (no_asm_simp))
-apply arith
done
lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>
--- a/src/HOL/Integ/IntArith.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy Wed Jul 26 19:23:04 2006 +0200
@@ -324,9 +324,6 @@
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
in int_val_lemma)
apply simp
-apply (erule impE)
- apply (intro strip)
- apply (erule_tac x = "i+m" in allE, arith)
apply (erule exE)
apply (rule_tac x = "i+m" in exI, arith)
done
--- a/src/HOL/Integ/IntDef.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Jul 26 19:23:04 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, arith)
+ by (simp add: congruent_def, arith)
thus ?thesis
by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
qed
--- a/src/HOL/Integ/NatBin.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Wed Jul 26 19:23:04 2006 +0200
@@ -88,12 +88,11 @@
text{*Suggested by Matthias Daum*}
lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp add: nat_div_distrib [symmetric])
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
apply (rule Divides.div_less_dividend, simp_all)
done
-
subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
(*"neg" is used in rewrite rules for binary comparisons*)
@@ -148,7 +147,6 @@
else let d = z-z' in
if neg d then 0 else nat d)"
apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-apply (simp add: diff_is_0_eq nat_le_eq_zle)
done
lemma diff_nat_number_of [simp]:
@@ -628,7 +626,6 @@
lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
- apply (simp add: neg_nat)
done
lemma nat_number_of_BIT_1:
@@ -676,7 +673,7 @@
by (simp only: mult_2 nat_add_distrib of_nat_add)
lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
-by (simp only: nat_number_of_def, simp)
+by (simp only: nat_number_of_def)
lemma of_nat_number_of_lemma:
"of_nat (number_of v :: nat) =
--- a/src/HOL/Integ/Presburger.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/Presburger.thy Wed Jul 26 19:23:04 2006 +0200
@@ -558,17 +558,13 @@
lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
apply(induct rule: int_gr_induct)
apply simp
- apply arith
apply (simp add:int_distrib)
-apply arith
done
lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
apply(induct rule: int_gr_induct)
apply simp
- apply arith
apply (simp add:int_distrib)
-apply arith
done
lemma minusinfinity:
--- a/src/HOL/Lambda/Eta.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy Wed Jul 26 19:23:04 2006 +0200
@@ -50,8 +50,7 @@
lemma free_lift [simp]:
"free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
apply (induct t fixing: i k)
- apply (auto cong: conj_cong)
- apply arith
+ apply (auto cong: conj_cong)
done
lemma free_subst [simp]:
--- a/src/HOL/Library/Word.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Library/Word.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1383,7 +1383,7 @@
proof (rule ccontr)
from w0 wk
have k1: "1 < k"
- by (cases "k - 1",simp_all,arith)
+ by (cases "k - 1",simp_all)
assume "~ length (int_to_bv i) \<le> k"
hence "k < length (int_to_bv i)"
by simp
@@ -1512,7 +1512,7 @@
proof (rule ccontr)
from w1 wk
have k1: "1 < k"
- by (cases "k - 1",simp_all,arith)
+ by (cases "k - 1",simp_all)
assume "~ length (int_to_bv i) \<le> k"
hence "k < length (int_to_bv i)"
by simp
@@ -1731,8 +1731,6 @@
have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
apply (cases "length w1 \<le> length w2")
apply (auto simp add: max_def)
- apply arith
- apply arith
done
also have "... = 2 ^ max (length w1) (length w2)"
proof -
@@ -1982,7 +1980,6 @@
apply simp
apply (subst zpower_zadd_distrib [symmetric])
apply simp
- apply arith
done
finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
.
@@ -2030,10 +2027,6 @@
apply simp
apply (subst zpower_zadd_distrib [symmetric])
apply simp
- apply (cut_tac lmw)
- apply arith
- apply (cut_tac p)
- apply arith
done
hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
by simp
@@ -2278,13 +2271,13 @@
by (simp add: bv_chop_def Let_def)
lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
- by (simp add: bv_chop_def Let_def,arith)
+ by (simp add: bv_chop_def Let_def)
lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
- by (simp add: bv_chop_def Let_def,arith)
+ by (simp add: bv_chop_def Let_def)
lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
- by (auto simp add: bv_slice_def,arith)
+ by (auto simp add: bv_slice_def)
definition
length_nat :: "nat => nat"
@@ -2337,7 +2330,6 @@
apply (drule norm_empty_bv_to_nat_zero)
using prems
apply simp
- apply arith
apply (cases "norm_unsigned (nat_to_bv (nat i))")
apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
using prems
@@ -2439,7 +2431,6 @@
apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
apply simp_all
apply (simp_all add: w_defs min_def)
- apply arith+
done
qed
@@ -2514,11 +2505,7 @@
lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle)
-lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
- apply (cases "y = 0",simp_all add: length_int_lt0)
- apply (subgoal_tac "nat (- y) - Suc 0 \<le> nat (- x) - Suc 0")
- apply (simp add: length_nat_mono)
- apply arith
+lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x" apply (cases "y = 0",simp_all add: length_int_lt0)
done
lemmas [simp] = length_nat_non0
--- a/src/HOL/List.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/List.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1691,7 +1691,6 @@
lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
apply(induct j)
apply auto
-apply arith
done
lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
--- a/src/HOL/Matrix/MatrixGeneral.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Jul 26 19:23:04 2006 +0200
@@ -994,8 +994,6 @@
apply (subst foldseq_almostzero[of _ j])
apply (simp add: prems)+
apply (auto)
- apply (insert ncols_le[of A j])
- apply (arith)
proof -
fix k
fix l
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Jul 26 19:23:04 2006 +0200
@@ -454,8 +454,10 @@
apply (simp add: max_of_list_def)
apply (induct xs)
apply simp
+ML {* fast_arith_split_limit := 0; *} (* FIXME *)
apply simp
apply arith
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
done
@@ -520,16 +522,7 @@
lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
\<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
apply (induct i)
-apply simp+
- (* case Goto *)
-apply arith
- (* case Ifcmpeq *)
-apply simp
-apply (erule disjE)
-apply arith
-apply arith
- (* case Throw *)
-apply simp
+apply (arith|simp)+
done
@@ -537,16 +530,7 @@
\<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk>
\<Longrightarrow> n \<le> pc'"
apply (induct i)
-apply simp+
- (* case Goto *)
-apply arith
- (* case Ifcmpeq *)
-apply simp
-apply (erule disjE)
-apply simp
-apply arith
- (* case Throw *)
-apply simp
+apply (arith|simp)+
done
@@ -975,7 +959,6 @@
apply (simp (no_asm_simp))+
apply simp
apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
-apply (simp (no_asm_simp))+
(* show check_type \<dots> *)
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
@@ -2100,7 +2083,6 @@
apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
(* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
- apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
--- a/src/HOL/NumberTheory/Finite2.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy Wed Jul 26 19:23:04 2006 +0200
@@ -179,10 +179,6 @@
lemma int_card_bdd_int_set_l_l: "0 < n ==>
int(card {x. 0 < x & x < n}) = n - 1"
apply (auto simp add: card_bdd_int_set_l_l)
- apply (subgoal_tac "Suc 0 \<le> nat n")
- apply (auto simp add: zdiff_int [symmetric])
- apply (subgoal_tac "0 < nat n", arith)
- apply (simp add: zero_less_nat_eq)
done
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
--- a/src/HOL/NumberTheory/Gauss.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Wed Jul 26 19:23:04 2006 +0200
@@ -104,8 +104,6 @@
apply (auto simp add: A_def ResSet_def)
apply (rule_tac m = p in zcong_less_eq)
apply (insert p_g_2, auto)
- apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
- apply (auto, auto simp add: p_minus_one_l)
done
lemma (in GAUSS) B_res: "ResSet p B"
@@ -255,6 +253,8 @@
lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
by (auto simp add: D_eq)
+ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+
lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
apply (auto simp add: F_eq A_def)
proof -
@@ -270,6 +270,8 @@
using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
qed
+ML {* fast_arith_split_limit := 9; *} (*FIXME*)
+
lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
--- a/src/HOL/NumberTheory/Int2.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Int2.thy Wed Jul 26 19:23:04 2006 +0200
@@ -191,7 +191,7 @@
have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
by auto
also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
- by (simp only: nat_add_distrib, auto)
+ by (simp only: nat_add_distrib)
also have "p - 2 + 1 = p - 1" by arith
finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
by (rule ssubst, auto)
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jul 26 19:23:04 2006 +0200
@@ -193,6 +193,8 @@
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
@@ -234,6 +236,8 @@
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)
--- a/src/HOL/Presburger.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Presburger.thy Wed Jul 26 19:23:04 2006 +0200
@@ -558,17 +558,13 @@
lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
apply(induct rule: int_gr_induct)
apply simp
- apply arith
apply (simp add:int_distrib)
-apply arith
done
lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
apply(induct rule: int_gr_induct)
apply simp
- apply arith
apply (simp add:int_distrib)
-apply arith
done
lemma minusinfinity:
--- a/src/HOL/Real/Float.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Real/Float.thy Wed Jul 26 19:23:04 2006 +0200
@@ -28,9 +28,7 @@
apply (auto, induct_tac n)
apply (simp_all add: pow2_def)
apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
- apply (auto simp add: h)
- apply arith
- done
+ by (auto simp add: h)
show ?thesis
proof (induct a)
case (1 n)
--- a/src/HOL/Real/RComplete.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Real/RComplete.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1066,10 +1066,7 @@
apply (subgoal_tac "real a = real (int a)")
apply (erule ssubst)
apply simp
- apply (subst nat_diff_distrib)
apply simp
- apply (rule le_floor)
- apply simp_all
done
lemma natceiling_zero [simp]: "natceiling 0 = 0"
@@ -1206,13 +1203,7 @@
apply (subgoal_tac "real a = real (int a)")
apply (erule ssubst)
apply simp
- apply (subst nat_diff_distrib)
apply simp
- apply (rule order_trans)
- prefer 2
- apply (rule ceiling_mono2)
- apply assumption
- apply simp_all
done
lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>
--- a/src/HOL/Real/RealDef.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Real/RealDef.thy Wed Jul 26 19:23:04 2006 +0200
@@ -1024,15 +1024,9 @@
by (simp add: real_of_nat_ge_zero)
lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
-apply (simp add: linorder_not_less)
-apply (auto intro: abs_ge_self [THEN order_trans])
-done
+by simp
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
-apply (simp add: real_add_assoc)
-apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
-apply (rule real_add_assoc [THEN subst])
-apply (rule abs_triangle_ineq)
-done
+by simp
end
--- a/src/HOL/Set.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Set.thy Wed Jul 26 19:23:04 2006 +0200
@@ -33,6 +33,7 @@
Pow :: "'a set => 'a set set" -- "powerset"
Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
+ Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers"
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90)
"op :" :: "'a => 'a set => bool" -- "membership"
@@ -117,11 +118,13 @@
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3EX! _:_./ _)" [0, 0, 10] 10)
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10)
syntax (HOL)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3?! _:_./ _)" [0, 0, 10] 10)
translations
"{x, xs}" == "insert x {xs}"
@@ -138,16 +141,19 @@
"INT x:A. B" == "INTER A (%x. B)"
"ALL x:A. P" == "Ball A (%x. P)"
"EX x:A. P" == "Bex A (%x. P)"
+ "EX! x:A. P" == "Bex1 A (%x. P)"
"LEAST x:A. P" => "LEAST x. x:A & P"
syntax (xsymbols)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
syntax (HTML output)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
syntax (xsymbols)
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
@@ -178,30 +184,35 @@
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3EX! _<=_./ _)" [0, 0, 10] 10)
syntax (xsymbols)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
syntax (HOL output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3?! _<=_./ _)" [0, 0, 10] 10)
syntax (HTML output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
translations
"\<forall>A\<subset>B. P" => "ALL A. A \<subset> B --> P"
- "\<exists>A\<subset>B. P" => "EX A. A \<subset> B & P"
- "\<forall>A\<subseteq>B. P" => "ALL A. A \<subseteq> B --> P"
+ "\<exists>A\<subset>B. P" => "EX A. A \<subset> B & P"
+ "\<forall>A\<subseteq>B. P" => "ALL A. A \<subseteq> B --> P"
"\<exists>A\<subseteq>B. P" => "EX A. A \<subseteq> B & P"
+ "\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P"
print_translation {*
let
@@ -316,6 +327,7 @@
defs
Ball_def: "Ball A P == ALL x. x:A --> P(x)"
Bex_def: "Bex A P == EX x. x:A & P(x)"
+ Bex1_def: "Bex1 A P == EX! x. x:A & P(x)"
defs (overloaded)
subset_def: "A <= B == ALL x:A. x:B"
--- a/src/HOL/SetInterval.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/SetInterval.thy Wed Jul 26 19:23:04 2006 +0200
@@ -301,7 +301,7 @@
show "?B \<subseteq> ?A"
proof
fix n assume a: "n : ?B"
- hence "n - k : {i..j}" by auto arith+
+ hence "n - k : {i..j}" by auto
moreover have "n = (n - k) + k" using a by auto
ultimately show "n : ?A" by blast
qed
@@ -315,7 +315,7 @@
show "?B \<subseteq> ?A"
proof
fix n assume a: "n : ?B"
- hence "n - k : {i..<j}" by auto arith+
+ hence "n - k : {i..<j}" by auto
moreover have "n = (n - k) + k" using a by auto
ultimately show "n : ?A" by blast
qed
@@ -384,7 +384,6 @@
apply (rule card_image)
apply (simp add: inj_on_def)
apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
- apply arith
apply (rule_tac x = "x - l" in exI)
apply arith
done
--- a/src/HOL/UNITY/Comp/AllocBase.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed Jul 26 19:23:04 2006 +0200
@@ -35,7 +35,6 @@
setsum f (lessThan n) <= setsum g (lessThan n)"
apply (induct_tac "n")
apply (auto simp add: lessThan_Suc)
-apply (drule_tac x = n in spec, arith)
done
lemma tokens_mono_prefix [rule_format]:
--- a/src/HOL/ZF/HOLZF.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/ZF/HOLZF.thy Wed Jul 26 19:23:04 2006 +0200
@@ -578,7 +578,6 @@
apply (insert n_less_u)
apply (insert u)
apply auto
- apply arith
done
ultimately show False by auto
qed
--- a/src/HOL/arith_data.ML Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/arith_data.ML Wed Jul 26 19:23:04 2006 +0200
@@ -29,7 +29,6 @@
funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
end;
-
(* dest_sum *)
val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
@@ -44,7 +43,6 @@
SOME (t, u) => dest_sum t @ dest_sum u
| NONE => [tm]));
-
(** generic proof tools **)
(* prove conversions *)
@@ -57,7 +55,6 @@
val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
-
(* rewriting *)
fun simp_all_tac rules =
@@ -70,7 +67,8 @@
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context ()) name pats proc;
-end;
+end; (* NatArithUtils *)
+
signature ARITH_DATA =
sig
@@ -78,12 +76,12 @@
val nat_cancel_sums: simproc list
end;
+
structure ArithData: ARITH_DATA =
struct
open NatArithUtils;
-
(** cancel common summands **)
structure Sum =
@@ -99,7 +97,6 @@
fun gen_uncancel_tac rule ct =
rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
-
(* nat eq *)
structure EqCancelSums = CancelSumsFun
@@ -110,7 +107,6 @@
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
end);
-
(* nat less *)
structure LessCancelSums = CancelSumsFun
@@ -121,7 +117,6 @@
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
end);
-
(* nat le *)
structure LeCancelSums = CancelSumsFun
@@ -132,7 +127,6 @@
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
end);
-
(* nat diff *)
structure DiffCancelSums = CancelSumsFun
@@ -143,8 +137,6 @@
val uncancel_tac = gen_uncancel_tac diff_cancel;
end);
-
-
(** prepare nat_cancel simprocs **)
val nat_cancel_sums_add = map prep_simproc
@@ -159,7 +151,7 @@
[prep_simproc ("natdiff_cancel_sums",
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
-end;
+end; (* ArithData *)
open ArithData;
@@ -172,6 +164,7 @@
structure LA_Logic: LIN_ARITH_LOGIC =
struct
+
val ccontr = ccontr;
val conjI = conjI;
val notI = notI;
@@ -179,7 +172,6 @@
val not_lessD = linorder_not_less RS iffD1;
val not_leD = linorder_not_le RS iffD1;
-
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
val mk_Trueprop = HOLogic.mk_Trueprop;
@@ -202,7 +194,7 @@
let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
in instantiate ([],[(cn,ct)]) le0 end;
-end;
+end; (* LA_Logic *)
(* arith theory data *)
@@ -235,9 +227,18 @@
{splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
-structure LA_Data_Ref: LIN_ARITH_DATA =
+signature HOL_LIN_ARITH_DATA =
+sig
+ include LIN_ARITH_DATA
+ val fast_arith_split_limit : int ref
+end;
+
+structure LA_Data_Ref: HOL_LIN_ARITH_DATA =
struct
+(* internal representation of linear (in-)equations *)
+type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
+
(* Decomposition of terms *)
fun nT (Type("fun",[N,_])) = N = HOLogic.natT
@@ -370,16 +371,425 @@
fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n)
+(*---------------------------------------------------------------------------*)
+(* code that performs certain goal transformations for linear arithmetic *)
+(*---------------------------------------------------------------------------*)
+
+(* A "do nothing" variant of pre_decomp and pre_tac:
+
+fun pre_decomp sg Ts termitems = [termitems];
+fun pre_tac i = all_tac;
+*)
+
+(*---------------------------------------------------------------------------*)
+(* the following code performs splitting of certain constants (e.g. min, *)
+(* max) in a linear arithmetic problem; similar to what split_tac later does *)
+(* to the proof state *)
+(*---------------------------------------------------------------------------*)
+
+val fast_arith_split_limit = ref 9;
+
+(* checks whether splitting with 'thm' is implemented *)
+
+(* Thm.thm -> bool *)
+
+fun is_split_thm thm =
+ case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
+ (case head_of lhs of
+ Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"]
+ | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false))
+ | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false);
+
+(* substitute new for occurrences of old in a term, incrementing bound *)
+(* variables as needed when substituting inside an abstraction *)
+
+(* (term * term) list -> term -> term *)
+
+fun subst_term [] t = t
+ | subst_term pairs t =
+ (case AList.lookup (op aconv) pairs t of
+ SOME new =>
+ new
+ | NONE =>
+ (case t of Abs (a, T, body) =>
+ let val pairs' = map (pairself (incr_boundvars 1)) pairs
+ in Abs (a, T, subst_term pairs' body) end
+ | t1 $ t2 =>
+ subst_term pairs t1 $ subst_term pairs t2
+ | _ => t));
+
+(* approximates the effect of one application of split_tac (followed by NNF *)
+(* normalization) on the subgoal represented by '(Ts, terms)'; returns a *)
+(* list of new subgoals (each again represented by a typ list for bound *)
+(* variables and a term list for premises), or NONE if split_tac would fail *)
+(* on the subgoal *)
+
+(* theory -> typ list * term list -> (typ list * term list) list option *)
+
+(* FIXME: currently only the effect of certain split theorems is reproduced *)
+(* (which is why we need 'is_split_thm'). A more canonical *)
+(* implementation should analyze the right-hand side of the split *)
+(* theorem that can be applied, and modify the subgoal accordingly. *)
+
+fun split_once_items sg (Ts, terms) =
+let
+ (* takes a list [t1, ..., tn] to the term *)
+ (* tn' --> ... --> t1' --> False , *)
+ (* where ti' = HOLogic.dest_Trueprop ti *)
+ (* term list -> term *)
+ fun REPEAT_DETERM_etac_rev_mp terms' =
+ fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
+ val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
+ val cmap = Splitter.cmap_of_split_thms split_thms
+ val splits = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
+in
+ if length splits > !fast_arith_split_limit then (
+ tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")");
+ NONE
+ ) else (
+ case splits of [] =>
+ NONE (* split_tac would fail: no possible split *)
+ | ((_, _, _, split_type, split_term) :: _) => ( (* ignore all but the first possible split *)
+ case strip_comb split_term of
+ (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
+ (Const ("Orderings.max", _), [t1, t2]) =>
+ let
+ val rev_terms = rev terms
+ val terms1 = map (subst_term [(split_term, t1)]) rev_terms
+ val terms2 = map (subst_term [(split_term, t2)]) rev_terms
+ val t1_leq_t2 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+ val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
+ in
+ SOME [(Ts, subgoal1), (Ts, subgoal2)]
+ end
+ (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
+ | (Const ("Orderings.min", _), [t1, t2]) =>
+ let
+ val rev_terms = rev terms
+ val terms1 = map (subst_term [(split_term, t1)]) rev_terms
+ val terms2 = map (subst_term [(split_term, t2)]) rev_terms
+ val t1_leq_t2 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+ val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
+ in
+ SOME [(Ts, subgoal1), (Ts, subgoal2)]
+ end
+ (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
+ | (Const ("HOL.abs", _), [t1]) =>
+ let
+ val rev_terms = rev terms
+ val terms1 = map (subst_term [(split_term, t1)]) rev_terms
+ val terms2 = map (subst_term [(split_term, Const ("HOL.uminus", split_type --> split_type) $ t1)]) rev_terms
+ val zero = Const ("0", split_type)
+ val zero_leq_t1 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ t1
+ val t1_lt_zero = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
+ in
+ SOME [(Ts, subgoal1), (Ts, subgoal2)]
+ end
+ (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
+ | (Const ("HOL.minus", _), [t1, t2]) =>
+ let
+ (* "d" in the above theorem becomes a new bound variable after NNF *)
+ (* transformation, therefore some adjustment of indices is necessary *)
+ val rev_terms = rev terms
+ val zero = Const ("0", split_type)
+ val d = Bound 0
+ val terms1 = map (subst_term [(split_term, zero)]) rev_terms
+ val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms)
+ val t1' = incr_boundvars 1 t1
+ val t2' = incr_boundvars 1 t2
+ val t1_lt_t2 = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+ val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const ("HOL.plus", split_type --> split_type --> split_type) $ t2' $ d)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
+ in
+ SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
+ end
+ (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
+ | (Const ("IntDef.nat", _), [t1]) =>
+ let
+ val rev_terms = rev terms
+ val zero_int = Const ("0", HOLogic.intT)
+ val zero_nat = Const ("0", HOLogic.natT)
+ val n = Bound 0
+ val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms)
+ val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
+ val t1' = incr_boundvars 1 t1
+ val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+ val t1_lt_zero = Const ("Orderings.less", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
+ in
+ SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
+ end
+ (* "?P ((?n::nat) mod (number_of ?k)) = ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
+ | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ let
+ val rev_terms = rev terms
+ val zero = Const ("0", split_type)
+ val i = Bound 1
+ val j = Bound 0
+ val terms1 = map (subst_term [(split_term, t1)]) rev_terms
+ val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+ val t1' = incr_boundvars 2 t1
+ val t2' = incr_boundvars 2 t2
+ val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+ val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+ val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ (Const ("HOL.plus", split_type --> split_type --> split_type) $
+ (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+ in
+ SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
+ end
+ (* "?P ((?n::nat) div (number_of ?k)) = ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
+ | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ let
+ val rev_terms = rev terms
+ val zero = Const ("0", split_type)
+ val i = Bound 1
+ val j = Bound 0
+ val terms1 = map (subst_term [(split_term, zero)]) rev_terms
+ val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+ val t1' = incr_boundvars 2 t1
+ val t2' = incr_boundvars 2 t2
+ val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+ val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+ val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ (Const ("HOL.plus", split_type --> split_type --> split_type) $
+ (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+ in
+ SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
+ end
+ (* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) --> ?P ?n) &
+ (neg (number_of (bin_minus ?k)) --> (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
+ (neg (number_of ?k) --> (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
+ | (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ let
+ val rev_terms = rev terms
+ val zero = Const ("0", split_type)
+ val i = Bound 1
+ val j = Bound 0
+ val terms1 = map (subst_term [(split_term, t1)]) rev_terms
+ val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+ val t1' = incr_boundvars 2 t1
+ val (t2' as (_ $ k')) = incr_boundvars 2 t2
+ val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
+ val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+ (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
+ val zero_leq_j = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
+ val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ (Const ("HOL.plus", split_type --> split_type --> split_type) $
+ (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+ val t2_lt_j = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+ val j_leq_zero = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
+ @ hd terms2_3
+ :: (if tl terms2_3 = [] then [not_false] else [])
+ @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
+ @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
+ val subgoal3 = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
+ @ hd terms2_3
+ :: (if tl terms2_3 = [] then [not_false] else [])
+ @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
+ @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
+ val Ts' = split_type :: split_type :: Ts
+ in
+ SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
+ end
+ (* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) --> ?P 0) &
+ (neg (number_of (bin_minus ?k)) --> (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
+ (neg (number_of ?k) --> (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
+ | (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ let
+ val rev_terms = rev terms
+ val zero = Const ("0", split_type)
+ val i = Bound 1
+ val j = Bound 0
+ val terms1 = map (subst_term [(split_term, zero)]) rev_terms
+ val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+ val t1' = incr_boundvars 2 t1
+ val (t2' as (_ $ k')) = incr_boundvars 2 t2
+ val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
+ val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+ (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
+ val zero_leq_j = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
+ val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ (Const ("HOL.plus", split_type --> split_type --> split_type) $
+ (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+ val t2_lt_j = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+ val j_leq_zero = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop neg_minus_k)
+ :: terms2_3
+ @ not_false
+ :: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
+ val subgoal3 = (HOLogic.mk_Trueprop neg_t2)
+ :: terms2_3
+ @ not_false
+ :: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
+ val Ts' = split_type :: split_type :: Ts
+ in
+ SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
+ end
+ (* this will only happen if a split theorem can be applied for which no code exists above -- *)
+ (* in which case either the split theorem should be implemented above, or 'is_split_thm' *)
+ (* should be modified to filter it out *)
+ | (t, ts) => (
+ warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^
+ " argument(s)) not implemented; proof reconstruction is likely to fail");
+ NONE
+ ))
+ )
end;
+(* remove terms that do not satisfy p; change the order of the remaining *)
+(* terms in the same way as filter_prems_tac does *)
+
+(* (term -> bool) -> term list -> term list *)
+
+fun filter_prems_tac_items p terms =
+let
+ fun filter_prems (t, (left, right)) =
+ if p t then (left, right @ [t]) else (left @ right, [])
+ val (left, right) = foldl filter_prems ([], []) terms
+in
+ right @ left
+end;
+
+(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *)
+(* subgoal that has 'terms' as premises *)
+
+(* term list -> bool *)
+
+fun negated_term_occurs_positively terms =
+ List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t) | _ => false) terms;
+
+(* theory -> typ list * term list -> (typ list * term list) list *)
+
+fun pre_decomp sg (Ts, terms) =
+let
+ (* repeatedly split (including newly emerging subgoals) until no further *)
+ (* splitting is possible *)
+ (* (typ list * term list) list -> (typ list * term list) list *)
+ fun split_loop [] = []
+ | split_loop (subgoal::subgoals) = (
+ case split_once_items sg subgoal of
+ SOME new_subgoals => split_loop (new_subgoals @ subgoals)
+ | NONE => subgoal :: split_loop subgoals
+ )
+ fun is_relevant t = isSome (decomp sg t)
+ val relevant_terms = filter_prems_tac_items is_relevant terms (* filter_prems_tac is_relevant *)
+ val split_goals = split_loop [(Ts, relevant_terms)] (* split_tac, NNF normalization *)
+ val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals (* necessary because split_once_tac may normalize terms *)
+ val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm (* TRY (etac notE) THEN eq_assume_tac *)
+in
+ result
+end;
+
+(* takes the i-th subgoal [| A1; ...; An |] ==> B to *)
+(* An --> ... --> A1 --> B, performs splitting with the given 'split_thms' *)
+(* (resulting in a different subgoal P), takes P to ~P ==> False, *)
+(* performs NNF-normalization of ~P, and eliminates conjunctions, *)
+(* disjunctions and existential quantifiers from the premises, possibly (in *)
+(* the case of disjunctions) resulting in several new subgoals, each of the *)
+(* general form [| Q1; ...; Qm |] ==> False. Fails if more than *)
+(* !fast_arith_split_limit splits are possible. *)
+
+(* Thm.thm list -> int -> Tactical.tactic *)
+
+fun split_once_tac split_thms i =
+let
+ val nnf_simpset =
+ empty_ss setmkeqTrue mk_eq_True
+ setmksimps (mksimps mksimps_pairs)
+ addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
+ not_all, not_ex, not_not]
+ fun prem_nnf_tac i st =
+ full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
+ fun cond_split_tac i st =
+ let
+ val subgoal = Logic.nth_prem (i, Thm.prop_of st)
+ val Ts = rev (map snd (Logic.strip_params subgoal))
+ val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
+ val cmap = Splitter.cmap_of_split_thms split_thms
+ val splits = Splitter.split_posns cmap (theory_of_thm st) Ts concl
+ in
+ if length splits > !fast_arith_split_limit then
+ no_tac st
+ else
+ split_tac split_thms i st
+ end
+in
+ EVERY' [
+ REPEAT_DETERM o etac rev_mp,
+ cond_split_tac,
+ rtac ccontr,
+ prem_nnf_tac,
+ TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
+ ] i
+end;
+
+(* remove irrelevant premises, then split the i-th subgoal (and all new *)
+(* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *)
+(* subgoals and finally attempt to solve them by finding an immediate *)
+(* contradiction (i.e. a term and its negation) in their premises. *)
+
+(* int -> Tactical.tactic *)
+
+fun pre_tac i st =
+let
+ val sg = theory_of_thm st
+ val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
+ fun is_relevant t = isSome (decomp sg t)
+in
+ DETERM (
+ TRY (filter_prems_tac is_relevant i)
+ THEN (
+ (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
+ THEN_ALL_NEW
+ ((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
+ THEN'
+ (TRY o (etac notE THEN' eq_assume_tac)))
+ ) i
+ ) st
+end;
+
+end; (* LA_Data_Ref *)
+
structure Fast_Arith =
Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
-val fast_arith_tac = Fast_Arith.lin_arith_tac false
-and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
-and trace_arith = Fast_Arith.trace
-and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
+val fast_arith_tac = Fast_Arith.lin_arith_tac false;
+val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
+val trace_arith = Fast_Arith.trace;
+val fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
+val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
local
@@ -439,7 +849,6 @@
Simplifier.simproc (the_context ()) "fast_nat_arith"
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
-
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
useful to detect inconsistencies among the premises for subgoals which are
*not* themselves (in)equalities, because the latter activate
@@ -449,58 +858,24 @@
(* arith proof method *)
-(* FIXME: K true should be replaced by a sensible test to speed things up
- in case there are lots of irrelevant terms involved;
- elimination of min/max can be optimized:
- (max m n + k <= r) = (m+k <= r & n+k <= r)
- (l <= min m n + k) = (l <= m+k & l <= n+k)
-*)
local
-(* a simpset for computations subject to optimization !!! *)
-(*
-val binarith = map thm
- ["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
- "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
- "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
- "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1",
- "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0",
- "bin_add_Pls_right", "bin_add_Min_right"];
- val intarithrel =
- (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
- "int_le_number_of_eq","int_iszero_number_of_0",
- "int_less_number_of_eq_neg"]) @
- (map (fn s => thm s RS thm "lift_bool")
- ["int_iszero_number_of_Pls","int_iszero_number_of_1",
- "int_neg_number_of_Min"])@
- (map (fn s => thm s RS thm "nlift_bool")
- ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
-
-val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
- "int_number_of_diff_sym", "int_number_of_mult_sym"];
-val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
- "mult_nat_number_of", "eq_nat_number_of",
- "less_nat_number_of"]
-val powerarith =
- (map thm ["nat_number_of", "zpower_number_of_even",
- "zpower_Pls", "zpower_Min"]) @
- [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
- thm "one_eq_Numeral1_nring"]
- (thm "zpower_number_of_odd"))]
-val comp_arith = binarith @ intarith @ intarithrel @ natarith
- @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
-
-val comp_ss = HOL_basic_ss addsimps comp_arith addsimps simp_thms;
-*)
fun raw_arith_tac ex i st =
+ (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
+ decomp sg"?) to speed things up in case there are lots of irrelevant
+ terms involved; elimination of min/max can be optimized:
+ (max m n + k <= r) = (m+k <= r & n+k <= r)
+ (l <= min m n + k) = (l <= m+k & l <= n+k)
+ *)
refute_tac (K true)
- (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
-(* (REPEAT o
- (fn i =>(split_tac (#splits (ArithTheoryData.get(Thm.theory_of_thm st))) i)
- THEN (simp_tac comp_ss i))) *)
- ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
- i st;
+ (* Splitting is also done inside fast_arith_tac, but not completely -- *)
+ (* split_tac may use split theorems that have not been implemented in *)
+ (* fast_arith_tac (cf. pre_decomp and split_once_items above). *)
+ (* Therefore splitting outside of fast_arith_tac may allow us to prove *)
+ (* some goals that fast_arith_tac alone would fail on. *)
+ (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
+ (fast_ex_arith_tac ex)
+ i st;
fun presburger_tac i st =
(case ArithTheoryData.get (Thm.theory_of_thm st) of
@@ -510,19 +885,19 @@
in
-val simple_arith_tac = FIRST' [fast_arith_tac,
- ObjectLogic.atomize_tac THEN' raw_arith_tac true];
+ val simple_arith_tac = FIRST' [fast_arith_tac,
+ ObjectLogic.atomize_tac THEN' raw_arith_tac true];
-val arith_tac = FIRST' [fast_arith_tac,
- ObjectLogic.atomize_tac THEN' raw_arith_tac true,
- presburger_tac];
+ val arith_tac = FIRST' [fast_arith_tac,
+ ObjectLogic.atomize_tac THEN' raw_arith_tac true,
+ presburger_tac];
-val silent_arith_tac = FIRST' [fast_arith_tac,
- ObjectLogic.atomize_tac THEN' raw_arith_tac false,
- presburger_tac];
+ val silent_arith_tac = FIRST' [fast_arith_tac,
+ ObjectLogic.atomize_tac THEN' raw_arith_tac false,
+ presburger_tac];
-fun arith_method prems =
- Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
+ fun arith_method prems =
+ Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
end;
--- a/src/HOL/ex/Adder.thy Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/ex/Adder.thy Wed Jul 26 19:23:04 2006 +0200
@@ -80,22 +80,7 @@
lemma cca_length [rule_format]:
"\<forall>bs. length as = length bs -->
length (carry_chain_adder as bs c) = Suc (length bs)"
- (is "?P as")
-proof (induct as,auto simp add: Let_def)
- fix as :: "bit list"
- fix xs :: "bit list"
- assume ind: "?P as"
- assume len: "Suc (length as) = length xs"
- thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs"
- proof (cases xs,simp_all)
- fix b bs
- assume [simp]: "xs = b # bs"
- assume "length as = length bs"
- with ind
- show "length (carry_chain_adder as bs c) - Suc 0 = length bs"
- by auto
- qed
-qed
+ by (induct as,auto simp add: Let_def)
lemma cca_correct [rule_format]:
"\<forall>bs. length as = length bs -->
--- a/src/HOL/simpdata.ML Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/simpdata.ML Wed Jul 26 19:23:04 2006 +0200
@@ -166,8 +166,6 @@
end;
-
-
(*** Simproc for Let ***)
val use_let_simproc = ref true;
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Jul 26 13:31:07 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jul 26 19:23:04 2006 +0200
@@ -23,12 +23,12 @@
signature LIN_ARITH_LOGIC =
sig
- val conjI: thm (* P ==> Q ==> P & Q *)
+ val conjI: thm (* P ==> Q ==> P & Q *)
val ccontr: thm (* (~ P ==> False) ==> P *)
val notI: thm (* (P ==> False) ==> ~ P *)
val not_lessD: thm (* ~(m < n) ==> n <= m *)
val not_leD: thm (* ~(m <= n) ==> n < m *)
- val sym: thm (* x = y ==> y = x *)
+ val sym: thm (* x = y ==> y = x *)
val mk_Eq: thm -> thm
val atomize: thm -> thm list
val mk_Trueprop: term -> term
@@ -52,16 +52,26 @@
signature LIN_ARITH_DATA =
sig
- val decomp:
- theory -> term -> ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool) option
+ type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool (* internal representation of linear (in-)equations *)
+ val decomp: theory -> term -> decompT option
+ val pre_decomp: theory -> typ list * term list -> (typ list * term list) list (* preprocessing, performed on a representation of subgoals as list of premises *)
+ val pre_tac : int -> Tactical.tactic (* preprocessing, performed on the goal -- must do the same as 'pre_decomp' *)
val number_of: IntInf.int * typ -> term
end;
(*
decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
where Rel is one of "<", "~<", "<=", "~<=" and "=" and
- p/q is the decomposition of the sum terms x/y into a list
- of summand * multiplicity pairs and a constant summand and
- d indicates if the domain is discrete.
+ p (q, respectively) is the decomposition of the sum term x
+ (y, respectively) into a list of summand * multiplicity
+ pairs and a constant summand and d indicates if the domain
+ is discrete.
+
+The relationship between pre_decomp and pre_tac is somewhat tricky. The
+internal representation of a subgoal and the corresponding theorem must
+be modified by pre_decomp (pre_tac, resp.) in a corresponding way. See
+the comment for split_items below. (This is even necessary for eta- and
+beta-equivalent modifications, as some of the lin. arith. code is not
+insensitive to them.)
ss must reduce contradictory <= to False.
It should also cancel common summands to keep <= reduced;
@@ -192,32 +202,32 @@
fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2));
-fun choose2 d ((lb,exactl),(ub,exactu)) =
- if Rat.le(lb,Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
- Rat.le(Rat.zero,ub) andalso (ub <> Rat.zero orelse exactu)
+fun choose2 d ((lb, exactl), (ub, exactu)) =
+ if Rat.le (lb, Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
+ Rat.le (Rat.zero, ub) andalso (ub <> Rat.zero orelse exactu)
then Rat.zero else
if not d
then (if Rat.ge0 lb
- then if exactl then lb else ratmiddle(lb,ub)
- else if exactu then ub else ratmiddle(lb,ub))
+ then if exactl then lb else ratmiddle (lb, ub)
+ else if exactu then ub else ratmiddle (lb, ub))
else (* discrete domain, both bounds must be exact *)
if Rat.ge0 lb then let val lb' = Rat.roundup lb
- in if Rat.le(lb',ub) then lb' else raise NoEx end
+ in if Rat.le (lb', ub) then lb' else raise NoEx end
else let val ub' = Rat.rounddown ub
- in if Rat.le(lb,ub') then ub' else raise NoEx end;
+ in if Rat.le (lb, ub') then ub' else raise NoEx end;
-fun findex1 discr (ex,(v,lineqs)) =
+fun findex1 discr (ex, (v, lineqs)) =
let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs;
val ineqs = Library.foldl elim_eqns ([],nz)
val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
- val lb = ratrelmax(map (eval ex v) ge)
- val ub = ratrelmin(map (eval ex v) le)
+ val lb = ratrelmax (map (eval ex v) ge)
+ val ub = ratrelmin (map (eval ex v) le)
in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
fun findex discr = Library.foldl (findex1 discr);
fun elim1 v x =
- map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le,
+ map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
nth_update (v, Rat.zero) bs));
fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
@@ -327,7 +337,7 @@
(* ------------------------------------------------------------------------- *)
fun allpairs f xs ys =
- maps (fn x => map (fn y => f x y) ys) xs;
+ List.concat (map (fn x => map (fn y => f x y) ys) xs);
fun extract_first p =
let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
@@ -346,25 +356,25 @@
type history = (int * lineq list) list;
datatype result = Success of injust | Failure of history;
-fun elim(ineqs,hist) =
- let val dummy = print_ineqs ineqs;
- val (triv,nontriv) = List.partition is_trivial ineqs in
- if not(null triv)
+fun elim (ineqs, hist) =
+ let val dummy = print_ineqs ineqs
+ val (triv, nontriv) = List.partition is_trivial ineqs in
+ if not (null triv)
then case Library.find_first is_answer triv of
- NONE => elim(nontriv,hist)
+ NONE => elim (nontriv, hist)
| SOME(Lineq(_,_,_,j)) => Success j
else
- if null nontriv then Failure(hist)
+ if null nontriv then Failure hist
else
- let val (eqs,noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
- if not(null eqs) then
+ let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
+ if not (null eqs) then
let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
(List.filter (fn i => i<>0) clist)
val c = hd sclist
val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
- val v = find_index (fn x => x = c) ceq
+ val v = find_index_eq c ceq
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
(othereqs @ noneqs)
val others = map (elim_var v eq) roth @ ioth
@@ -390,10 +400,12 @@
(* Translate back a proof. *)
(* ------------------------------------------------------------------------- *)
-fun trace_thm msg th =
- if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th;
+(* string -> Thm.thm -> Thm.thm *)
+fun trace_thm msg th =
+ (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
-fun trace_msg msg =
+(* string -> unit *)
+fun trace_msg msg =
if !trace then tracing msg else ();
(* FIXME OPTIMIZE!!!! (partly done already)
@@ -408,21 +420,21 @@
local
exception FalseE of thm
in
+(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> injust -> Thm.thm *)
fun mkthm (sg, ss) asms just =
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
Data.get sg;
val simpset' = Simplifier.inherit_context ss simpset;
- val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
+ val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
map fst lhs union (map fst rhs union ats))
- ([], map_filter (fn thm => if Thm.no_prems thm
- then LA_Data.decomp sg (concl_of thm)
- else NONE) asms)
+ ([], List.mapPartial (fn thm => if Thm.no_prems thm
+ then LA_Data.decomp sg (concl_of thm)
+ else NONE) asms)
fun add2 thm1 thm2 =
let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms
end;
-
fun try_add [] _ = NONE
| try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
NONE => try_add thm1s thm2 | some => some;
@@ -430,23 +442,18 @@
fun addthms thm1 thm2 =
case add2 thm1 thm2 of
NONE => (case try_add ([thm1] RL inj_thms) thm2 of
- NONE => (the (try_add ([thm2] RL inj_thms) thm1)
+ NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
handle Option =>
(trace_thm "" thm1; trace_thm "" thm2;
- sys_error "Lin.arith. failed to add thms"))
+ sys_error "Lin.arith. failed to add thms")
+ )
| SOME thm => thm)
| SOME thm => thm;
fun multn(n,thm) =
let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
-(*
- fun multn2(n,thm) =
- let val SOME(mth,cv) =
- get_first (fn (th,cv) => SOME(thm RS th,cv) handle THM _ => NONE) mult_mono_thms
- val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
- in instantiate ([],[(cv,ct)]) mth end
-*)
+
fun multn2(n,thm) =
let val SOME(mth) =
get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
@@ -459,15 +466,15 @@
let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
- fun mk(Asm i) = trace_thm "Asm" (nth asms i)
- | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth atoms i))
- | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
- | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
- | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
- | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
- | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
- | mk(Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
- | mk(Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
+ fun mk (Asm i) = trace_thm "Asm" (nth asms i)
+ | mk (Nat i) = trace_thm "Nat" (LA_Logic.mk_nat_thm sg (nth atoms i))
+ | mk (LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
+ | mk (NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
+ | mk (NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
+ | mk (NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
+ | mk (Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
+ | mk (Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
+ | mk (Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
in trace_msg "mkthm";
let val thm = trace_thm "Final thm:" (mk just)
@@ -475,19 +482,20 @@
in trace_thm "After simplification:" fls;
if LA_Logic.is_False fls then fls
else
- (tracing "Assumptions:"; List.app print_thm asms;
- tracing "Proved:"; print_thm fls;
+ (tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms;
+ tracing "Proved:"; tracing (Display.string_of_thm fls);
warning "Linear arithmetic should have refuted the assumptions.\n\
\Please inform Tobias Nipkow (nipkow@in.tum.de).";
fls)
end
- end handle FalseE thm => (trace_thm "False reached early:" thm; thm)
+ end handle FalseE thm => trace_thm "False reached early:" thm
end
end;
fun coeff poly atom : IntInf.int =
AList.lookup (op =) poly atom |> the_default 0;
+(* int list -> int *)
fun lcms is = Library.foldl lcm (1, is);
fun integ(rlhs,r,rel,rrhs,s,d) =
@@ -499,8 +507,8 @@
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
fun mklineq n atoms =
- fn (item,k) =>
- let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
+ fn (item, k) =>
+ let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item
val lhsa = map (coeff lhs) atoms
and rhsa = map (coeff rhs) atoms
val diff = map2 (curry (op -)) rhsa lhsa
@@ -535,28 +543,33 @@
curry (op ~~) sds
#> map print_atom
#> commas
- #> curry (op ^) "Counter example:\n";
+ #> curry (op ^) "Counter example (possibly spurious):\n";
-fun trace_ex(sg,params,atoms,discr,n,hist:history) =
- if null hist then ()
- else let val frees = map Free params;
- fun s_of_t t = Sign.string_of_term sg (subst_bounds(frees,t));
- val (v,lineqs) :: hist' = hist
- val start = if v = ~1 then (findex0 discr n lineqs,hist')
- else (replicate n Rat.zero,hist)
- val ex = SOME (produce_ex ((map s_of_t atoms)~~discr) (findex discr start))
- handle NoEx => NONE;
- in
- (case ex of
- SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
- | NONE => warning "arith failed")
- end;
+fun trace_ex (sg, params, atoms, discr, n, hist : history) =
+ case hist of
+ [] => ()
+ | (v, lineqs) :: hist' =>
+ let val frees = map Free params
+ fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
+ val start = if v = ~1 then (findex0 discr n lineqs, hist')
+ else (replicate n Rat.zero, hist)
+ val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) (findex discr start))
+ handle NoEx => NONE
+ in
+ case ex of
+ SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
+ | NONE => warning "arith failed"
+ end;
-fun mknat pTs ixs (atom,i) =
- if LA_Logic.is_nat(pTs,atom)
+(* ------------------------------------------------------------------------- *)
+
+(* Term.typ list -> int list -> Term.term * int -> lineq option *)
+
+fun mknat pTs ixs (atom, i) =
+ if LA_Logic.is_nat (pTs, atom)
then let val l = map (fn j => if j=i then 1 else 0) ixs
- in SOME(Lineq(0,Le,l,Nat(i))) end
- else NONE
+ in SOME (Lineq (0, Le, l, Nat i)) end
+ else NONE;
(* This code is tricky. It takes a list of premises in the order they occur
in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical
@@ -570,95 +583,184 @@
For variables n of type nat, a constraint 0 <= n is added.
*)
-fun split_items(items) =
- let fun elim_neq front _ [] = [rev front]
- | elim_neq front n (NONE::ineqs) = elim_neq front (n+1) ineqs
- | elim_neq front n (SOME(ineq as (l,i,rel,r,j,d))::ineqs) =
- if rel = "~=" then elim_neq front n (ineqs @ [SOME(l,i,"<",r,j,d)]) @
- elim_neq front n (ineqs @ [SOME(r,j,"<",l,i,d)])
- else elim_neq ((ineq,n) :: front) (n+1) ineqs
- in elim_neq [] 0 items end;
+
+(* FIXME: To optimize, the splitting of cases and the search for refutations *)
+(* should be intertwined: separate the first (fully split) case, *)
+(* refute it, continue with splitting and refuting. Terminate with *)
+(* failure as soon as a case could not be refuted; i.e. delay further *)
+(* splitting until after a refutation for other cases has been found. *)
+
+(* Theory.theory -> bool -> typ list * term list -> (typ list * (decompT * int) list) list *)
+
+fun split_items sg do_pre (Ts, terms) =
+ let
+(*
+ val _ = trace_msg ("split_items: do_pre is " ^ Bool.toString do_pre ^ "\n" ^
+ " Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
+ " terms = " ^ string_of_list (Sign.string_of_term sg) terms)
+*)
+ (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
+ (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *)
+ (* level *)
+ (* decompT option list -> decompT option list list *)
+ fun elim_neq [] = [[]]
+ | elim_neq (NONE :: ineqs) = map (cons NONE) (elim_neq ineqs)
+ | elim_neq (SOME(ineq as (l,i,rel,r,j,d)) :: ineqs) =
+ if rel = "~=" then elim_neq (ineqs @ [SOME (l, i, "<", r, j, d)]) @
+ elim_neq (ineqs @ [SOME (r, j, "<", l, i, d)])
+ else map (cons (SOME ineq)) (elim_neq ineqs)
+ (* int -> decompT option list -> (decompT * int) list *)
+ fun number_hyps _ [] = []
+ | number_hyps n (NONE::xs) = number_hyps (n+1) xs
+ | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs
-fun add_atoms(ats,((lhs,_,_,rhs,_,_),_)) =
- (map fst lhs) union ((map fst rhs) union ats)
+ val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *)
+ (* (typ list * term list) list *)
+ (if do_pre then LA_Data.pre_decomp sg else Library.single)
+ |> (* compute the internal encoding of (in-)equalities *)
+ (* (typ list * decompT option list) list *)
+ map (apsnd (map (LA_Data.decomp sg)))
+ |> (* splitting of inequalities *)
+ (* (typ list * decompT option list) list list *)
+ map (fn (Ts, items) => map (pair Ts) (elim_neq items))
+ |> (* combine the list of lists of subgoals into a single list *)
+ (* (typ list * decompT option list) list *)
+ List.concat
+ |> (* numbering of hypotheses, ignoring irrelevant ones *)
+ (* (typ list * (decompT * int) list) list *)
+ map (apsnd (number_hyps 0))
+(*
+ val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^ " subgoal(s)"
+ ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
+ (" " ^ Int.toString n ^ ". Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
+ " items = " ^ string_of_list
+ (string_of_pair
+ (fn (l, i, rel, r, j, d) =>
+ enclose "(" ")" (commas
+ [string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
+ Rat.string_of_rat i,
+ rel,
+ string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
+ Rat.string_of_rat j,
+ Bool.toString d]))
+ Int.toString) items, n+1)) result 1))
+*)
+ in result end;
-fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) =
- (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats)
+(* term list * (decompT * int) -> term list *)
+
+fun add_atoms (ats, ((lhs,_,_,rhs,_,_),_)) =
+ (map fst lhs) union ((map fst rhs) union ats);
+
+(* (bool * term) list * (decompT * int) -> (bool * term) list *)
+
+fun add_datoms (dats, ((lhs,_,_,rhs,_,d),_)) =
+ (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
+
+(* (decompT * int) list -> bool list *)
fun discr initems = map fst (Library.foldl add_datoms ([],initems));
-fun refutes sg (pTs,params) ex =
+(* Theory.theory -> (string * typ) list -> bool -> (typ list * (decompT * int) list) list -> injust list -> injust list option *)
+
+fun refutes sg params show_ex =
let
- fun refute (initems::initemss) js =
- let val atoms = Library.foldl add_atoms ([],initems)
+ (* (typ list * (decompT * int) list) list -> injust list -> injust list option *)
+ fun refute ((Ts, initems)::initemss) js =
+ let val atoms = Library.foldl add_atoms ([], initems)
val n = length atoms
val mkleq = mklineq n atoms
val ixs = 0 upto (n-1)
val iatoms = atoms ~~ ixs
- val natlineqs = map_filter (mknat pTs ixs) iatoms
+ val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
val ineqs = map mkleq initems @ natlineqs
- in case elim(ineqs,[]) of
- Success(j) =>
- (trace_msg "Contradiction!"; refute initemss (js@[j]))
- | Failure(hist) =>
- (if not ex then ()
- else trace_ex(sg,params,atoms,discr initems,n,hist);
- NONE)
+ in case elim (ineqs, []) of
+ Success j =>
+ (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); refute initemss (js@[j]))
+ | Failure hist =>
+ (if not show_ex then
+ ()
+ else let
+ (* invent names for bound variables that are new, i.e. in Ts, but not in params *)
+ (* we assume that Ts still contains (map snd params) as a suffix *)
+ val new_count = length Ts - length params - 1
+ val new_names = map Name.bound (0 upto new_count)
+ val params' = (new_names @ map fst params) ~~ Ts
+ in
+ trace_ex (sg, params', atoms, discr initems, n, hist)
+ end; NONE)
end
| refute [] js = SOME js
in refute end;
-fun refute sg ps ex items = refutes sg ps ex (split_items items) [];
+(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *)
-fun refute_tac ss (i,justs) =
+fun refute sg params show_ex do_pre terms =
+ refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
+
+(* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *)
+
+fun refute_tac ss (i, justs) =
fn state =>
- let val sg = #sign(rep_thm state)
- val {neqE, ...} = Data.get sg;
- fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
- METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
- in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
- EVERY(map just1 justs)
- end
- state;
+ let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ Int.toString (length justs) ^ " justification(s)):") state
+ val sg = theory_of_thm state
+ val {neqE, ...} = Data.get sg
+ fun just1 j =
+ REPEAT_DETERM (eresolve_tac neqE i) THEN (* eliminate inequalities *)
+ METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i (* use theorems generated from the actual justifications *)
+ in DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
+ DETERM (LA_Data.pre_tac i) THEN (* user-defined preprocessing of the subgoal *)
+ PRIMITIVE (trace_thm "State after pre_tac:") THEN
+ EVERY (map just1 justs) (* prove every resulting subgoal, using its justification *)
+ end state;
-fun count P xs = length(List.filter P xs);
+(* ('a -> bool) -> 'a list -> int *)
+
+fun count P xs = length (List.filter P xs);
(* The limit on the number of ~= allowed.
Because each ~= is split into two cases, this can lead to an explosion.
*)
val fast_arith_neq_limit = ref 9;
-fun prove sg ps ex Hs concl =
-let val Hitems = map (LA_Data.decomp sg) Hs
-in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems
- > !fast_arith_neq_limit then NONE
- else
- case LA_Data.decomp sg concl of
- NONE => refute sg ps ex (Hitems@[NONE])
- | SOME(citem as (r,i,rel,l,j,d)) =>
- let val neg::rel0 = explode rel
- val nrel = if neg = "~" then implode rel0 else "~"^rel
- in refute sg ps ex (Hitems @ [SOME(r,i,nrel,l,j,d)]) end
-end;
+(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *)
+
+fun prove sg params show_ex do_pre Hs concl =
+ let
+ (* append the negated conclusion to 'Hs' -- this corresponds to *)
+ (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
+ (* theorem/tactic level *)
+ val Hs' = Hs @ [LA_Logic.neg_prop concl]
+ (* decompT option -> bool *)
+ fun is_neq NONE = false
+ | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
+ in
+ trace_msg "prove";
+ if count is_neq (map (LA_Data.decomp sg) Hs')
+ > !fast_arith_neq_limit then (
+ trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")");
+ NONE
+ ) else
+ refute sg params show_ex do_pre Hs'
+ end;
(*
Fast but very incomplete decider. Only premises and conclusions
that are already (negated) (in)equations are taken into account.
*)
-fun simpset_lin_arith_tac ss ex i st = SUBGOAL (fn (A,_) =>
- let val params = rev(Logic.strip_params A)
- val pTs = map snd params
- val Hs = Logic.strip_assums_hyp A
- val concl = Logic.strip_assums_concl A
+fun simpset_lin_arith_tac ss show_ex i st = SUBGOAL (fn (A,_) =>
+ let val params = rev (Logic.strip_params A)
+ val Hs = Logic.strip_assums_hyp A
+ val concl = Logic.strip_assums_concl A
in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
- case prove (Thm.sign_of_thm st) (pTs,params) ex Hs concl of
+ case prove (Thm.sign_of_thm st) params show_ex true Hs concl of
NONE => (trace_msg "Refutation failed."; no_tac)
- | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
+ | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
end) i st;
-fun lin_arith_tac ex i st =
+fun lin_arith_tac show_ex i st =
simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
- ex i st;
+ show_ex i st;
fun cut_lin_arith_tac ss i =
cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
@@ -673,47 +775,77 @@
datatype splittree = Tip of thm list
| Spl of thm * cterm * splittree * cterm * splittree
+(* the cterm "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *)
+
+(* Thm.cterm -> Thm.cterm * Thm.cterm *)
+
fun extract imp =
-let val (Il,r) = Thm.dest_comb imp
- val (_,imp1) = Thm.dest_comb Il
- val (Ict1,_) = Thm.dest_comb imp1
- val (_,ct1) = Thm.dest_comb Ict1
- val (Ir,_) = Thm.dest_comb r
- val (_,Ict2r) = Thm.dest_comb Ir
- val (Ict2,_) = Thm.dest_comb Ict2r
- val (_,ct2) = Thm.dest_comb Ict2
-in (ct1,ct2) end;
+let val (Il, r) = Thm.dest_comb imp
+ val (_, imp1) = Thm.dest_comb Il
+ val (Ict1, _) = Thm.dest_comb imp1
+ val (_, ct1) = Thm.dest_comb Ict1
+ val (Ir, _) = Thm.dest_comb r
+ val (_, Ict2r) = Thm.dest_comb Ir
+ val (Ict2, _) = Thm.dest_comb Ict2r
+ val (_, ct2) = Thm.dest_comb Ict2
+in (ct1, ct2) end;
+
+(* Theory.theory -> Thm.thm list -> splittree *)
fun splitasms sg asms =
-let val {neqE, ...} = Data.get sg;
- fun split(asms',[]) = Tip(rev asms')
- | split(asms',asm::asms) =
- (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
- of SOME spl =>
- let val (ct1,ct2) = extract(cprop_of spl)
- val thm1 = assume ct1 and thm2 = assume ct2
- in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2]))
+let val {neqE, ...} = Data.get sg
+ fun elim_neq (asms', []) = Tip (rev asms')
+ | elim_neq (asms', asm::asms) =
+ (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
+ SOME spl =>
+ let val (ct1, ct2) = extract (cprop_of spl)
+ val thm1 = assume ct1
+ val thm2 = assume ct2
+ in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
end
- | NONE => split(asm::asms', asms))
-in split([],asms) end;
+ | NONE => elim_neq (asm::asms', asms))
+in elim_neq ([], asms) end;
+
+(* Theory.theory * MetaSimplifier.simpset -> splittree -> injust list -> (Thm.thm, injust list) *)
fun fwdproof ctxt (Tip asms) (j::js) = (mkthm ctxt asms j, js)
- | fwdproof ctxt (Spl(thm,ct1,tree1,ct2,tree2)) js =
- let val (thm1,js1) = fwdproof ctxt tree1 js
- val (thm2,js2) = fwdproof ctxt tree2 js1
+ | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js =
+ let val (thm1, js1) = fwdproof ctxt tree1 js
+ val (thm2, js2) = fwdproof ctxt tree2 js1
val thm1' = implies_intr ct1 thm1
val thm2' = implies_intr ct2 thm2
in (thm2' COMP (thm1' COMP thm), js2) end;
(* needs handle THM _ => NONE ? *)
-fun prover (ctxt as (sg, _)) thms Tconcl js pos =
-let val nTconcl = LA_Logic.neg_prop Tconcl
- val cnTconcl = cterm_of sg nTconcl
- val nTconclthm = assume cnTconcl
- val tree = splitasms sg (thms @ [nTconclthm])
- val (thm,_) = fwdproof ctxt tree js
- val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
-in SOME(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end
+(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *)
+
+fun prover (ctxt as (sg, ss)) thms Tconcl js pos =
+let
+(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *)
+(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *)
+ (* There is no "forward version" of 'pre_tac'. Therefore we combine the *)
+ (* available theorems into a single proof state and perform "backward proof" *)
+ (* using 'refute_tac'. *)
+(*
+ val Hs = map prop_of thms
+ val Prop = fold (curry Logic.mk_implies) (rev Hs) Tconcl
+ val cProp = cterm_of sg Prop
+ val concl = Goal.init cProp
+ |> refute_tac ss (1, js)
+ |> Seq.hd
+ |> Goal.finish
+ |> fold (fn thA => fn thAB => implies_elim thAB thA) thms
+*)
+(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
+ val nTconcl = LA_Logic.neg_prop Tconcl
+ val cnTconcl = cterm_of sg nTconcl
+ val nTconclthm = assume cnTconcl
+ val tree = splitasms sg (thms @ [nTconclthm])
+ val (Falsethm, _) = fwdproof ctxt tree js
+ val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
+ val concl = implies_intr cnTconcl Falsethm COMP contr
+in SOME (trace_thm "Proved by lin. arith. prover:"
+ (LA_Logic.mk_Eq concl)) end
(* in case concl contains ?-var, which makes assume fail: *)
handle THM _ => NONE;
@@ -723,15 +855,22 @@
2. lin_arith_prover is applied by the simplifier which
dives into terms and will thus try the non-negated concl anyway.
*)
+
+(* Theory.theory -> MetaSimplifier.simpset -> Term.term -> Thm.thm option *)
+
fun lin_arith_prover sg ss concl =
-let
- val thms = maps LA_Logic.atomize (prems_of_ss ss);
- val Hs = map (#prop o rep_thm) thms
+let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
+ val Hs = map prop_of thms
val Tconcl = LA_Logic.mk_Trueprop concl
-in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
+(*
+ val _ = trace_msg "lin_arith_prover"
+ val _ = map (trace_thm "thms:") thms
+ val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl)
+*)
+in case prove sg [] false false Hs Tconcl of (* concl provable? *)
SOME js => prover (sg, ss) thms Tconcl js true
| NONE => let val nTconcl = LA_Logic.neg_prop Tconcl
- in case prove sg ([],[]) false Hs nTconcl of (* ~concl provable? *)
+ in case prove sg [] false false Hs nTconcl of (* ~concl provable? *)
SOME js => prover (sg, ss) thms nTconcl js false
| NONE => NONE
end
--- a/src/Provers/splitter.ML Wed Jul 26 13:31:07 2006 +0200
+++ b/src/Provers/splitter.ML Wed Jul 26 19:23:04 2006 +0200
@@ -13,18 +13,23 @@
signature SPLITTER_DATA =
sig
val mk_eq : thm -> thm
- val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
- val iffD : thm (* "[| P = Q; Q |] ==> P" *)
- val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
- val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
- val exE : thm (* "[| x. P x; !!x. P x ==> Q |] ==> Q" *)
- val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *)
- val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *)
- val notnotD : thm (* "~ ~ P ==> P" *)
+ val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
+ val iffD : thm (* "[| P = Q; Q |] ==> P" *)
+ val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
+ val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
+ val exE : thm (* "[| EX x. P x; !!x. P x ==> Q |] ==> Q" *)
+ val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *)
+ val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *)
+ val notnotD : thm (* "~ ~ P ==> P" *)
end
signature SPLITTER =
sig
+ (* somewhat more internal functions *)
+ val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list
+ val split_posns : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term ->
+ (thm * (typ * typ * int list) list * int list * typ * term) list (* first argument is a "cmap", returns a list of "split packs" *)
+ (* the "real" interface, providing a number of tactics *)
val split_tac : thm list -> int -> tactic
val split_inside_tac: thm list -> int -> tactic
val split_asm_tac : thm list -> int -> tactic
@@ -52,18 +57,42 @@
val const_Trueprop = ObjectLogic.judgment_name (the_context ());
-fun split_format_err() = error("Wrong format for split rule");
+fun split_format_err () = error "Wrong format for split rule";
+(* thm -> (string * typ) * bool *)
fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
(Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
| _ => split_format_err ())
| _ => split_format_err ();
+(* thm list -> (string * (typ * term * thm * typ * int) list) list *)
+fun cmap_of_split_thms thms =
+let
+ val splits = map Data.mk_eq thms
+ fun add_thm (cmap, thm) =
+ (case concl_of thm of _$(t as _$lhs)$_ =>
+ (case strip_comb lhs of (Const(a,aT),args) =>
+ let val info = (aT,lhs,thm,fastype_of t,length args)
+ in case AList.lookup (op =) cmap a of
+ SOME infos => AList.update (op =) (a, info::infos) cmap
+ | NONE => (a,[info])::cmap
+ end
+ | _ => split_format_err())
+ | _ => split_format_err())
+in
+ Library.foldl add_thm ([], splits)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* mk_case_split_tac *)
+(* ------------------------------------------------------------------------- *)
+
+(* (int * int -> order) -> thm list -> int -> tactic * <split_posns> *)
+
fun mk_case_split_tac order =
let
-
(************************************************************
Create lift-theorem "trlift" :
@@ -71,7 +100,8 @@
*************************************************************)
-val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
+val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
+
val lift =
let val ct = read_cterm Pure.thy
("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
@@ -129,12 +159,12 @@
(* add all loose bound variables in t to list is *)
-fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
+fun add_lbnos (is,t) = add_loose_bnos (t,0,is);
(* check if the innermost abstraction that needs to be removed
has a body of type T; otherwise the expansion thm will fail later on
*)
-fun type_test(T,lbnos,apsns) =
+fun type_test (T,lbnos,apsns) =
let val (_,U,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
in T=U end;
@@ -166,7 +196,7 @@
lifting is required before applying the split-theorem.
******************************************************************************)
-fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) =
+fun mk_split_pack (thm, T, T', n, ts, apsns, pos, TB, t) =
if n > length ts then []
else let val lev = length apsns
val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
@@ -198,26 +228,34 @@
see Pure/pattern.ML for the full version;
*)
local
-exception MATCH
+ exception MATCH
in
-fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
- handle Type.TYPE_MATCH => raise MATCH;
-fun fomatch sg args =
- let
- fun mtch tyinsts = fn
- (Ts,Var(_,T), t) => typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
- | (_,Free (a,T), Free (b,U)) =>
- if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
- | (_,Const (a,T), Const (b,U)) =>
- if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
- | (_,Bound i, Bound j) => if i=j then tyinsts else raise MATCH
- | (Ts,Abs(_,T,t), Abs(_,U,u)) =>
- mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
- | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
- | _ => raise MATCH
- in (mtch Vartab.empty args; true) handle MATCH => false end;
-end
+ (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *)
+ fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
+ handle Type.TYPE_MATCH => raise MATCH
+ (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *)
+ fun fomatch sg args =
+ let
+ (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *)
+ fun mtch tyinsts = fn
+ (Ts, Var(_,T), t) =>
+ typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
+ | (_, Free (a,T), Free (b,U)) =>
+ if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
+ | (_, Const (a,T), Const (b,U)) =>
+ if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
+ | (_, Bound i, Bound j) =>
+ if i=j then tyinsts else raise MATCH
+ | (Ts, Abs(_,T,t), Abs(_,U,u)) =>
+ mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
+ | (Ts, f$t, g$u) =>
+ mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
+ | _ => raise MATCH
+ in (mtch Vartab.empty args; true) handle MATCH => false end;
+end (* local *)
+(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term ->
+ (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *)
fun split_posns cmap sg Ts t =
let
val T' = fastype_of1 (Ts, t);
@@ -243,15 +281,13 @@
in snd(Library.foldl iter ((0, a), ts)) end
in posns Ts [] [] t end;
+fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
-fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
-
-fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
+fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
prod_ord (int_ord o pairself length) (order o pairself length)
((ps, pos), (qs, qos));
-
(************************************************************
call split_posns with appropriate parameters
*************************************************************)
@@ -261,8 +297,10 @@
val goali = nth_subgoal i state
val Ts = rev(map #2 (Logic.strip_params goali))
val _ $ t $ _ = Logic.strip_assums_concl goali;
- in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
+ in (Ts, t, sort shorter (split_posns cmap sg Ts t)) end;
+fun exported_split_posns cmap sg Ts t =
+ sort shorter (split_posns cmap sg Ts t);
(*************************************************************
instantiate lift theorem
@@ -322,20 +360,11 @@
i : number of subgoal the tactic should be applied to
*****************************************************************************)
+(* thm list -> int -> tactic *)
+
fun split_tac [] i = no_tac
| split_tac splits i =
- let val splits = map Data.mk_eq splits;
- fun add_thm(cmap,thm) =
- (case concl_of thm of _$(t as _$lhs)$_ =>
- (case strip_comb lhs of (Const(a,aT),args) =>
- let val info = (aT,lhs,thm,fastype_of t,length args)
- in case AList.lookup (op =) cmap a of
- SOME infos => AList.update (op =) (a, info::infos) cmap
- | NONE => (a,[info])::cmap
- end
- | _ => split_format_err())
- | _ => split_format_err())
- val cmap = Library.foldl add_thm ([],splits);
+ let val cmap = cmap_of_split_thms splits
fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
fun lift_split_tac state =
let val (Ts, t, splits) = select cmap state i
@@ -352,12 +381,12 @@
(rtac meta_iffD i THEN lift_split_tac)
end;
-in split_tac end;
+in (split_tac, exported_split_posns) end; (* mk_case_split_tac *)
-val split_tac = mk_case_split_tac int_ord;
+val (split_tac, split_posns) = mk_case_split_tac int_ord;
-val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
+val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord);
(*****************************************************************************
@@ -378,7 +407,7 @@
| first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
first_prem_is_disj t
| first_prem_is_disj _ = false;
- (* does not work properly if the split variable is bound by a quantfier *)
+ (* does not work properly if the split variable is bound by a quantifier *)
fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
(if first_prem_is_disj t
then EVERY[etac Data.disjE i,rotate_tac ~1 i,
@@ -387,11 +416,11 @@
else all_tac)
THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
THEN REPEAT (dresolve_tac [Data.notnotD] i)) i;
- in if n<0 then no_tac else DETERM (EVERY'
+ in if n<0 then no_tac else (DETERM (EVERY'
[rotate_tac n, etac Data.contrapos2,
split_tac splits,
rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
- flat_prems_tac] i)
+ flat_prems_tac] i))
end;
in SUBGOAL tac
end;