linear arithmetic splits certain operators (e.g. min, max, abs)
1.1 --- a/NEWS Wed Jul 26 13:31:07 2006 +0200
1.2 +++ b/NEWS Wed Jul 26 19:23:04 2006 +0200
1.3 @@ -510,6 +510,12 @@
1.4 (i.e. a boolean expression) by compiling it to ML. The goal is
1.5 "proved" (via the oracle "Evaluation") if it evaluates to True.
1.6
1.7 +* Linear arithmetic now splits certain operators (e.g. min, max, abs) also
1.8 +when invoked by the simplifier. This results in the simplifier being more
1.9 +powerful on arithmetic goals.
1.10 +INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain
1.11 +the old behavior.
1.12 +
1.13 * Support for hex (0x20) and binary (0b1001) numerals.
1.14
1.15 *** HOL-Algebra ***
2.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy Wed Jul 26 13:31:07 2006 +0200
2.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Jul 26 19:23:04 2006 +0200
2.3 @@ -90,19 +90,10 @@
2.4
2.5 \noindent
2.6 The inclusion remains to be proved. After unfolding some definitions,
2.7 -we are left with simple arithmetic:
2.8 +we are left with simple arithmetic that is dispatched automatically.
2.9 *}
2.10
2.11 -apply (clarify, simp add: measure_def inv_image_def)
2.12 -
2.13 -txt{*
2.14 -@{subgoals[display,indent=0,margin=65]}
2.15 -
2.16 -\noindent
2.17 -And that is dispatched automatically:
2.18 -*}
2.19 -
2.20 -by arith
2.21 +by (clarify, simp add: measure_def inv_image_def)
2.22
2.23 text{*\noindent
2.24
3.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Jul 26 13:31:07 2006 +0200
3.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Jul 26 19:23:04 2006 +0200
3.3 @@ -119,22 +119,11 @@
3.4
3.5 \noindent
3.6 The inclusion remains to be proved. After unfolding some definitions,
3.7 -we are left with simple arithmetic:%
3.8 -\end{isamarkuptxt}%
3.9 -\isamarkuptrue%
3.10 -\isacommand{apply}\isamarkupfalse%
3.11 -\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
3.12 -\begin{isamarkuptxt}%
3.13 -\begin{isabelle}%
3.14 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
3.15 -\end{isabelle}
3.16 -
3.17 -\noindent
3.18 -And that is dispatched automatically:%
3.19 +we are left with simple arithmetic that is dispatched automatically.%
3.20 \end{isamarkuptxt}%
3.21 \isamarkuptrue%
3.22 \isacommand{by}\isamarkupfalse%
3.23 -\ arith%
3.24 +\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
3.25 \endisatagproof
3.26 {\isafoldproof}%
3.27 %
4.1 --- a/src/HOL/Algebra/UnivPoly.thy Wed Jul 26 13:31:07 2006 +0200
4.2 +++ b/src/HOL/Algebra/UnivPoly.thy Wed Jul 26 19:23:04 2006 +0200
4.3 @@ -972,13 +972,13 @@
4.4 next
4.5 case (Suc j)
4.6 have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
4.7 - using Suc by (auto intro!: funcset_mem [OF Rg]) arith
4.8 + using Suc by (auto intro!: funcset_mem [OF Rg])
4.9 have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
4.10 - using Suc by (auto intro!: funcset_mem [OF Rg]) arith
4.11 + using Suc by (auto intro!: funcset_mem [OF Rg])
4.12 have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
4.13 using Suc by (auto intro!: funcset_mem [OF Rf])
4.14 have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
4.15 - using Suc by (auto intro!: funcset_mem [OF Rg]) arith
4.16 + using Suc by (auto intro!: funcset_mem [OF Rg])
4.17 have R11: "g 0 \<in> carrier R"
4.18 using Suc by (auto intro!: funcset_mem [OF Rg])
4.19 from Suc show ?case
5.1 --- a/src/HOL/Auth/Guard/Extensions.thy Wed Jul 26 13:31:07 2006 +0200
5.2 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed Jul 26 19:23:04 2006 +0200
5.3 @@ -231,7 +231,7 @@
5.4 "greatest_msg other = 0"
5.5
5.6 lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
5.7 -by (induct X, auto, arith+)
5.8 +by (induct X, auto)
5.9
5.10 subsubsection{*sets of keys*}
5.11
6.1 --- a/src/HOL/Auth/Guard/Guard_Public.thy Wed Jul 26 13:31:07 2006 +0200
6.2 +++ b/src/HOL/Auth/Guard/Guard_Public.thy Wed Jul 26 19:23:04 2006 +0200
6.3 @@ -95,7 +95,7 @@
6.4 apply (induct evs, auto simp: initState.simps)
6.5 apply (drule used_sub_parts_used, safe)
6.6 apply (drule greatest_msg_is_greatest, arith)
6.7 -by (simp, arith)
6.8 +by simp
6.9
6.10 subsubsection{*function giving a new nonce*}
6.11
6.12 @@ -171,4 +171,4 @@
6.13 apply (frule_tac A=A in priK_analz_iff_bad)
6.14 by (simp add: knows_decomp)+
6.15
6.16 -end
6.17 \ No newline at end of file
6.18 +end
7.1 --- a/src/HOL/Bali/AxCompl.thy Wed Jul 26 13:31:07 2006 +0200
7.2 +++ b/src/HOL/Bali/AxCompl.thy Wed Jul 26 19:23:04 2006 +0200
7.3 @@ -1421,7 +1421,6 @@
7.4 apply (drule finite_subset)
7.5 apply (erule finite_imageI)
7.6 apply auto
7.7 -apply arith
7.8 done
7.9
7.10
8.1 --- a/src/HOL/Binomial.thy Wed Jul 26 13:31:07 2006 +0200
8.2 +++ b/src/HOL/Binomial.thy Wed Jul 26 19:23:04 2006 +0200
8.3 @@ -33,9 +33,8 @@
8.4 by simp
8.5
8.6 lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
8.7 -apply (induct "n", auto)
8.8 -apply (erule allE)
8.9 -apply (erule mp, arith)
8.10 +apply (induct "n")
8.11 +apply auto
8.12 done
8.13
8.14 declare binomial_0 [simp del] binomial_Suc [simp del]
9.1 --- a/src/HOL/Complex/CLim.thy Wed Jul 26 13:31:07 2006 +0200
9.2 +++ b/src/HOL/Complex/CLim.thy Wed Jul 26 19:23:04 2006 +0200
9.3 @@ -178,7 +178,7 @@
9.4 apply (simp add: CInfinitesimal_hcmod_iff star_of_def
9.5 Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod, blast)
9.6 apply (drule_tac x = r in spec, clarify)
9.7 -apply (drule FreeUltrafilterNat_all, ultra, arith)
9.8 +apply (drule FreeUltrafilterNat_all, ultra)
9.9 done
9.10
9.11
10.1 --- a/src/HOL/Divides.thy Wed Jul 26 13:31:07 2006 +0200
10.2 +++ b/src/HOL/Divides.thy Wed Jul 26 19:23:04 2006 +0200
10.3 @@ -710,8 +710,7 @@
10.4 apply (rule iffI)
10.5 apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
10.6 prefer 3; apply assumption
10.7 - apply (simp_all add: quorem_def)
10.8 - apply arith
10.9 + apply (simp_all add: quorem_def) apply arith
10.10 apply (rule conjI)
10.11 apply (rule_tac P="%x. n * (m div n) \<le> x" in
10.12 subst [OF mod_div_equality [of _ n]])
11.1 --- a/src/HOL/HoareParallel/Graph.thy Wed Jul 26 13:31:07 2006 +0200
11.2 +++ b/src/HOL/HoareParallel/Graph.thy Wed Jul 26 19:23:04 2006 +0200
11.3 @@ -126,7 +126,6 @@
11.4 apply(case_tac "j=R")
11.5 apply(erule_tac x = "Suc i" in allE)
11.6 apply simp
11.7 - apply arith
11.8 apply (force simp add:nth_list_update)
11.9 apply simp
11.10 apply(erule exE)
11.11 @@ -154,7 +153,6 @@
11.12 apply simp
11.13 apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
11.14 prefer 2 apply arith
11.15 -apply simp
11.16 apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
11.17 prefer 2 apply arith
11.18 apply simp
11.19 @@ -175,24 +173,16 @@
11.20 prefer 2 apply arith
11.21 apply(drule_tac n = "Suc nata" in Compl_lemma)
11.22 apply clarify
11.23 + ML {* fast_arith_split_limit := 0; *} (*FIXME*)
11.24 apply force
11.25 + ML {* fast_arith_split_limit := 9; *} (*FIXME*)
11.26 apply(drule leI)
11.27 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
11.28 apply(erule_tac x = "m - (Suc nata)" in allE)
11.29 apply(case_tac "m")
11.30 apply simp
11.31 apply simp
11.32 - apply(subgoal_tac "natb - nata < Suc natb")
11.33 - prefer 2 apply(erule thin_rl)+ apply arith
11.34 - apply simp
11.35 - apply(case_tac "length path")
11.36 - apply force
11.37 -apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
11.38 apply simp
11.39 -apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
11.40 -apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
11.41 -apply simp
11.42 -apply arith
11.43 done
11.44
11.45
11.46 @@ -253,8 +243,6 @@
11.47 apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
11.48 prefer 2 apply arith
11.49 apply simp
11.50 - apply(erule mp)
11.51 - apply arith
11.52 --{* T is a root *}
11.53 apply(case_tac "m=0")
11.54 apply force
12.1 --- a/src/HOL/HoareParallel/OG_Examples.thy Wed Jul 26 13:31:07 2006 +0200
12.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy Wed Jul 26 19:23:04 2006 +0200
12.3 @@ -298,7 +298,6 @@
12.4 --{* 98 verification conditions *}
12.5 apply auto
12.6 --{* auto takes about 3 minutes !! *}
12.7 -apply arith+
12.8 done
12.9
12.10 text {* Easier Version: without AWAIT. Apt and Olderog. page 256: *}
12.11 @@ -332,7 +331,6 @@
12.12 --{* 20 vc *}
12.13 apply auto
12.14 --{* auto takes aprox. 2 minutes. *}
12.15 -apply arith+
12.16 done
12.17
12.18 subsection {* Producer/Consumer *}
13.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 26 13:31:07 2006 +0200
13.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 26 19:23:04 2006 +0200
13.3 @@ -361,11 +361,8 @@
13.4 apply clarify
13.5 apply(frule_tac j=0 and k="j" and p=pre in stability)
13.6 apply simp_all
13.7 - apply arith
13.8 apply(erule_tac x=i in allE,simp)
13.9 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
13.10 - apply arith
13.11 - apply arith
13.12 apply(case_tac "x!j")
13.13 apply clarify
13.14 apply simp
13.15 @@ -492,11 +489,8 @@
13.16 apply(simp add:assum_def)
13.17 apply clarify
13.18 apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
13.19 - apply arith
13.20 apply(erule_tac x=i in allE,simp)
13.21 apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
13.22 - apply arith
13.23 - apply arith
13.24 apply(case_tac "x!j")
13.25 apply clarify
13.26 apply simp
13.27 @@ -543,7 +537,6 @@
13.28 apply(simp add:assum_def)
13.29 apply(simp add:assum_def)
13.30 apply(erule_tac m="length x" in etran_or_ctran,simp+)
13.31 - apply(case_tac x,simp+)
13.32 apply(case_tac x, (simp add:last_length)+)
13.33 apply(erule exE)
13.34 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
13.35 @@ -555,18 +548,7 @@
13.36 apply(erule_tac x="sa" in allE)
13.37 apply(drule_tac c="drop (Suc m) x" in subsetD)
13.38 apply simp
13.39 - apply(rule conjI)
13.40 - apply force
13.41 apply clarify
13.42 - apply(subgoal_tac "(Suc m) + i \<le> length x")
13.43 - apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
13.44 - apply(rotate_tac -2)
13.45 - apply simp
13.46 - apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
13.47 - apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
13.48 - apply arith
13.49 - apply arith
13.50 - apply arith
13.51 apply simp
13.52 apply clarify
13.53 apply(case_tac "i\<le>m")
13.54 @@ -575,49 +557,33 @@
13.55 apply(erule_tac x=i in allE, erule impE, assumption)
13.56 apply simp+
13.57 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
13.58 - apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
13.59 - apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
13.60 - apply(rotate_tac -2)
13.61 - apply simp
13.62 - apply(erule mp)
13.63 - apply arith
13.64 - apply arith
13.65 - apply arith
13.66 - apply(case_tac "length (drop (Suc m) x)",simp)
13.67 - apply(erule_tac x="sa" in allE)
13.68 - back
13.69 - apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
13.70 - apply(rule conjI)
13.71 - apply force
13.72 - apply clarify
13.73 - apply(subgoal_tac "(Suc m) + i \<le> length x")
13.74 - apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
13.75 - apply(rotate_tac -2)
13.76 - apply simp
13.77 - apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
13.78 - apply(subgoal_tac "Suc (Suc (m + i)) < length x")
13.79 - apply simp
13.80 - apply arith
13.81 - apply arith
13.82 - apply arith
13.83 - apply simp
13.84 - apply clarify
13.85 - apply(case_tac "i\<le>m")
13.86 - apply(drule le_imp_less_or_eq)
13.87 - apply(erule disjE)
13.88 - apply(erule_tac x=i in allE, erule impE, assumption)
13.89 - apply simp
13.90 + apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
13.91 + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
13.92 + apply(rotate_tac -2)
13.93 apply simp
13.94 - apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
13.95 - apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
13.96 - apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
13.97 - apply(rotate_tac -2)
13.98 - apply simp
13.99 - apply(erule mp)
13.100 - apply arith
13.101 apply arith
13.102 apply arith
13.103 - done
13.104 +apply(case_tac "length (drop (Suc m) x)",simp)
13.105 +apply(erule_tac x="sa" in allE)
13.106 +back
13.107 +apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
13.108 + apply clarify
13.109 +apply simp
13.110 +apply clarify
13.111 +apply(case_tac "i\<le>m")
13.112 + apply(drule le_imp_less_or_eq)
13.113 + apply(erule disjE)
13.114 + apply(erule_tac x=i in allE, erule impE, assumption)
13.115 + apply simp
13.116 + apply simp
13.117 +apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
13.118 +apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
13.119 + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
13.120 + apply(rotate_tac -2)
13.121 + apply simp
13.122 + apply arith
13.123 +apply arith
13.124 +done
13.125
13.126 subsubsection{* Soundness of the Sequential rule *}
13.127
13.128 @@ -862,8 +828,6 @@
13.129 apply simp
13.130 apply(erule mp)
13.131 apply(case_tac ys,simp+)
13.132 - apply arith
13.133 - apply arith
13.134 apply force
13.135 apply arith
13.136 apply force
14.1 --- a/src/HOL/Hyperreal/HTranscendental.thy Wed Jul 26 13:31:07 2006 +0200
14.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy Wed Jul 26 19:23:04 2006 +0200
14.3 @@ -364,7 +364,7 @@
14.4 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
14.5 apply (rule bexI [OF _ Rep_star_star_n], auto)
14.6 apply (rule_tac x = "exp u" in exI)
14.7 -apply (ultra, arith)
14.8 +apply ultra
14.9 done
14.10
14.11 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
15.1 --- a/src/HOL/Hyperreal/Integration.thy Wed Jul 26 13:31:07 2006 +0200
15.2 +++ b/src/HOL/Hyperreal/Integration.thy Wed Jul 26 19:23:04 2006 +0200
15.3 @@ -323,7 +323,6 @@
15.4 apply (drule add_strict_mono, assumption)
15.5 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
15.6 mult_less_cancel_right)
15.7 -apply arith
15.8 done
15.9
15.10 lemma Integral_zero [simp]: "Integral(a,a) f 0"
15.11 @@ -423,7 +422,7 @@
15.12 \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
15.13 in order_trans)
15.14 apply (rule abs_triangle_ineq [THEN [2] order_trans])
15.15 -apply (simp add: right_diff_distrib, arith)
15.16 +apply (simp add: right_diff_distrib)
15.17 apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
15.18 apply (rule add_mono)
15.19 apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
15.20 @@ -434,7 +433,7 @@
15.21 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
15.22 apply (rule order_trans)
15.23 apply (auto simp add: abs_le_interval_iff)
15.24 -apply (simp add: right_diff_distrib, arith)
15.25 +apply (simp add: right_diff_distrib)
15.26 done
15.27
15.28 lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
15.29 @@ -577,7 +576,7 @@
15.30 apply (auto dest: partition_lt_cancel)
15.31 apply (rule_tac x=N and y=n in linorder_cases)
15.32 apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
15.33 -apply (drule_tac n = n in partition_lt_gen, auto, arith)
15.34 +apply (drule_tac n = n in partition_lt_gen, auto)
15.35 apply (drule_tac x = n in spec)
15.36 apply (simp split: split_if_asm)
15.37 done
15.38 @@ -741,7 +740,6 @@
15.39 ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
15.40 apply (simp add: tpart_def partition_def, safe)
15.41 apply (rule_tac x = "N - n" in exI, auto)
15.42 -apply (drule_tac x = "na + n" in spec, arith)+
15.43 done
15.44
15.45 lemma fine_right1:
15.46 @@ -752,7 +750,7 @@
15.47 ==> fine ga (%x. D(x + n),%x. p(x + n))"
15.48 apply (auto simp add: fine_def gauge_def)
15.49 apply (drule_tac x = "na + n" in spec)
15.50 -apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
15.51 +apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto)
15.52 apply (simp add: tpart_def, safe)
15.53 apply (subgoal_tac "D n \<le> p (na + n)")
15.54 apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
15.55 @@ -783,7 +781,7 @@
15.56 apply ((drule spec)+, auto)
15.57 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)
15.58 apply (auto simp only: rsum_add left_distrib [symmetric]
15.59 - mult_2_right [symmetric] real_mult_less_iff1, arith)
15.60 + mult_2_right [symmetric] real_mult_less_iff1)
15.61 done
15.62
15.63 lemma partition_lt_gen2:
15.64 @@ -834,7 +832,7 @@
15.65 apply arith
15.66 apply (drule add_strict_mono, assumption)
15.67 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
15.68 - real_mult_less_iff1, arith)
15.69 + real_mult_less_iff1)
15.70 done
15.71
15.72 lemma Integral_imp_Cauchy:
15.73 @@ -853,7 +851,7 @@
15.74 apply (erule_tac V = "0 < e" in thin_rl)
15.75 apply (drule add_strict_mono, assumption)
15.76 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
15.77 - real_mult_less_iff1, arith)
15.78 + real_mult_less_iff1)
15.79 done
15.80
15.81 lemma Cauchy_iff2:
16.1 --- a/src/HOL/Hyperreal/Lim.thy Wed Jul 26 13:31:07 2006 +0200
16.2 +++ b/src/HOL/Hyperreal/Lim.thy Wed Jul 26 19:23:04 2006 +0200
16.3 @@ -1484,7 +1484,7 @@
16.4 apply (rule_tac x = s in exI, clarify)
16.5 apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
16.6 apply (drule_tac x = "xa-x" in spec)
16.7 -apply (auto simp add: abs_ge_self, arith+)
16.8 +apply (auto simp add: abs_ge_self)
16.9 done
16.10
16.11 text{*Refine the above to existence of least upper bound*}
16.12 @@ -2236,6 +2236,8 @@
16.13 thus ?thesis by simp
16.14 qed
16.15
16.16 +ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
16.17 +
16.18 lemma LIMSEQ_SEQ_conv2:
16.19 assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
16.20 shows "X -- a --> L"
16.21 @@ -2316,6 +2318,7 @@
16.22 ultimately show False by simp
16.23 qed
16.24
16.25 +ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
16.26
16.27 lemma LIMSEQ_SEQ_conv:
16.28 "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
17.1 --- a/src/HOL/Hyperreal/MacLaurin.thy Wed Jul 26 13:31:07 2006 +0200
17.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Jul 26 19:23:04 2006 +0200
17.3 @@ -390,7 +390,7 @@
17.4
17.5 lemma mod_exhaust_less_4:
17.6 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
17.7 -by (case_tac "m mod 4", auto, arith)
17.8 +by auto
17.9
17.10 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
17.11 "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
18.1 --- a/src/HOL/Hyperreal/NSA.thy Wed Jul 26 13:31:07 2006 +0200
18.2 +++ b/src/HOL/Hyperreal/NSA.thy Wed Jul 26 19:23:04 2006 +0200
18.3 @@ -1349,7 +1349,8 @@
18.4 ==> hypreal_of_real x + u < hypreal_of_real y"
18.5 apply (simp add: Infinitesimal_def)
18.6 apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
18.7 -apply (simp add: abs_less_iff)
18.8 +(* FIXME: arith simproc bug with apply (simp add: abs_less_iff) *)
18.9 +apply simp
18.10 done
18.11
18.12 lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
19.1 --- a/src/HOL/Hyperreal/Poly.thy Wed Jul 26 13:31:07 2006 +0200
19.2 +++ b/src/HOL/Hyperreal/Poly.thy Wed Jul 26 19:23:04 2006 +0200
19.3 @@ -1023,7 +1023,7 @@
19.4 apply (induct "p", auto)
19.5 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
19.6 apply (rule abs_triangle_ineq)
19.7 -apply (auto intro!: mult_mono simp add: abs_mult, arith)
19.8 +apply (auto intro!: mult_mono simp add: abs_mult)
19.9 done
19.10
19.11 end
20.1 --- a/src/HOL/Hyperreal/SEQ.thy Wed Jul 26 13:31:07 2006 +0200
20.2 +++ b/src/HOL/Hyperreal/SEQ.thy Wed Jul 26 19:23:04 2006 +0200
20.3 @@ -745,7 +745,6 @@
20.4 apply (simp add: Bseq_def, safe)
20.5 apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
20.6 apply auto
20.7 -apply arith
20.8 apply (rule_tac x = N in exI, safe)
20.9 apply (drule_tac x = n in spec, arith)
20.10 apply (auto simp add: Bseq_iff2)
20.11 @@ -754,7 +753,7 @@
20.12 lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
20.13 apply (simp add: Bseq_def)
20.14 apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
20.15 -apply (drule_tac [2] x = n in spec, arith+)
20.16 +apply (drule_tac x = n in spec, arith)
20.17 done
20.18
20.19
20.20 @@ -824,9 +823,7 @@
20.21
20.22 lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
20.23 ==> \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
20.24 -apply safe
20.25 -apply (drule spec, auto, arith)
20.26 -done
20.27 +by auto
20.28
20.29 lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
20.30 by auto
21.1 --- a/src/HOL/Hyperreal/Series.thy Wed Jul 26 13:31:07 2006 +0200
21.2 +++ b/src/HOL/Hyperreal/Series.thy Wed Jul 26 19:23:04 2006 +0200
21.3 @@ -274,10 +274,6 @@
21.4 apply (induct "no", auto)
21.5 apply (drule_tac x = "Suc no" in spec)
21.6 apply (simp add: add_ac)
21.7 -(* FIXME why does simp require a separate step to prove the (pure arithmetic)
21.8 - left-over? With del cong: strong_setsum_cong it works!
21.9 -*)
21.10 -apply simp
21.11 done
21.12
21.13 lemma sumr_pos_lt_pair:
21.14 @@ -299,15 +295,7 @@
21.15 apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
21.16 prefer 3 apply assumption
21.17 apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
21.18 -apply simp_all
21.19 -apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
21.20 -apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
21.21 -prefer 3 apply simp
21.22 -apply (drule_tac [2] x = 0 in spec)
21.23 - prefer 2 apply simp
21.24 -apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
21.25 -apply (simp add: abs_if)
21.26 -apply (auto simp add: linorder_not_less [symmetric])
21.27 +apply simp_all
21.28 done
21.29
21.30 text{*A summable series of positive terms has limit that is at least as
22.1 --- a/src/HOL/Hyperreal/Transcendental.thy Wed Jul 26 13:31:07 2006 +0200
22.2 +++ b/src/HOL/Hyperreal/Transcendental.thy Wed Jul 26 19:23:04 2006 +0200
22.3 @@ -526,7 +526,7 @@
22.4 apply (rule setsum_abs [THEN real_le_trans])
22.5 apply (rule real_setsum_nat_ivl_bounded)
22.6 apply (auto dest!: less_add_one intro!: mult_mono simp add: power_add abs_mult)
22.7 -apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
22.8 +apply (auto intro!: power_mono zero_le_power simp add: power_abs)
22.9 done
22.10
22.11 lemma lemma_termdiff4:
22.12 @@ -576,9 +576,10 @@
22.13 done
22.14
22.15
22.16 -
22.17 text{* FIXME: Long proofs*}
22.18
22.19 +ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *} (* FIXME: rewrite proofs *)
22.20 +
22.21 lemma termdiffs_aux:
22.22 "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
22.23 ==> (\<lambda>h. \<Sum>n. c n *
22.24 @@ -641,6 +642,8 @@
22.25 apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
22.26 done
22.27
22.28 +ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
22.29 +
22.30 lemma termdiffs:
22.31 "[| summable(%n. c(n) * (K ^ n));
22.32 summable(%n. (diffs c)(n) * (K ^ n));
22.33 @@ -748,7 +751,7 @@
22.34 apply (subst lemma_exp_ext)
22.35 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)")
22.36 apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
22.37 -apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
22.38 +apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs)
22.39 done
22.40
22.41 lemma lemma_sin_ext:
22.42 @@ -769,14 +772,14 @@
22.43 apply (subst lemma_sin_ext)
22.44 apply (auto simp add: sin_fdiffs2 [symmetric])
22.45 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
22.46 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
22.47 +apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
22.48 done
22.49
22.50 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
22.51 apply (subst lemma_cos_ext)
22.52 apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
22.53 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
22.54 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
22.55 +apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
22.56 done
22.57
22.58
22.59 @@ -2533,7 +2536,7 @@
22.60 apply (rule_tac x = ea in exI, auto)
22.61 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)
22.62 apply auto
22.63 -apply (drule sym, auto, arith)
22.64 +apply (drule sym, auto)
22.65 done
22.66
22.67 lemma isCont_inv_fun_inv:
23.1 --- a/src/HOL/IMP/Compiler.thy Wed Jul 26 13:31:07 2006 +0200
23.2 +++ b/src/HOL/IMP/Compiler.thy Wed Jul 26 19:23:04 2006 +0200
23.3 @@ -101,7 +101,6 @@
23.4 apply(rule ccontr)
23.5 apply(drule_tac f = length in arg_cong)
23.6 apply simp
23.7 -apply arith
23.8 done
23.9
23.10 lemma reduce_exec1:
23.11 @@ -293,6 +292,6 @@
23.12 with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
23.13 qed
23.14
23.15 -(* To Do: connect with Machine 0 using M_equiv *)
23.16 +(* TODO: connect with Machine 0 using M_equiv *)
23.17
23.18 -end
23.19 \ No newline at end of file
23.20 +end
24.1 --- a/src/HOL/IMP/Machines.thy Wed Jul 26 13:31:07 2006 +0200
24.2 +++ b/src/HOL/IMP/Machines.thy Wed Jul 26 19:23:04 2006 +0200
24.3 @@ -168,11 +168,10 @@
24.4 apply fastsimp
24.5 apply simp
24.6 apply simp
24.7 - apply arith
24.8 apply simp
24.9 - apply arith
24.10 apply(fastsimp simp add:exec01.JMPB)
24.11 done
24.12 +
24.13 (*
24.14 lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
24.15 apply(induct xs)
24.16 @@ -188,6 +187,7 @@
24.17 apply simp_all
24.18 done
24.19 *)
24.20 +
24.21 lemma direction2:
24.22 "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
24.23 rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
25.1 --- a/src/HOL/IMPP/Hoare.thy Wed Jul 26 13:31:07 2006 +0200
25.2 +++ b/src/HOL/IMPP/Hoare.thy Wed Jul 26 19:23:04 2006 +0200
25.3 @@ -381,7 +381,6 @@
25.4 apply (drule finite_subset)
25.5 apply (erule finite_imageI)
25.6 apply (simp (no_asm_simp))
25.7 -apply arith
25.8 done
25.9
25.10 lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>
26.1 --- a/src/HOL/Integ/IntArith.thy Wed Jul 26 13:31:07 2006 +0200
26.2 +++ b/src/HOL/Integ/IntArith.thy Wed Jul 26 19:23:04 2006 +0200
26.3 @@ -324,9 +324,6 @@
26.4 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
26.5 in int_val_lemma)
26.6 apply simp
26.7 -apply (erule impE)
26.8 - apply (intro strip)
26.9 - apply (erule_tac x = "i+m" in allE, arith)
26.10 apply (erule exE)
26.11 apply (rule_tac x = "i+m" in exI, arith)
26.12 done
27.1 --- a/src/HOL/Integ/IntDef.thy Wed Jul 26 13:31:07 2006 +0200
27.2 +++ b/src/HOL/Integ/IntDef.thy Wed Jul 26 19:23:04 2006 +0200
27.3 @@ -387,7 +387,7 @@
27.4 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
27.5 proof -
27.6 have "(\<lambda>(x,y). {x-y}) respects intrel"
27.7 - by (simp add: congruent_def, arith)
27.8 + by (simp add: congruent_def, arith)
27.9 thus ?thesis
27.10 by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
27.11 qed
28.1 --- a/src/HOL/Integ/NatBin.thy Wed Jul 26 13:31:07 2006 +0200
28.2 +++ b/src/HOL/Integ/NatBin.thy Wed Jul 26 19:23:04 2006 +0200
28.3 @@ -88,12 +88,11 @@
28.4
28.5 text{*Suggested by Matthias Daum*}
28.6 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
28.7 -apply (subgoal_tac "nat x div nat k < nat x")
28.8 - apply (simp add: nat_div_distrib [symmetric])
28.9 +apply (subgoal_tac "nat x div nat k < nat x")
28.10 + apply (simp (asm_lr) add: nat_div_distrib [symmetric])
28.11 apply (rule Divides.div_less_dividend, simp_all)
28.12 done
28.13
28.14 -
28.15 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
28.16
28.17 (*"neg" is used in rewrite rules for binary comparisons*)
28.18 @@ -148,7 +147,6 @@
28.19 else let d = z-z' in
28.20 if neg d then 0 else nat d)"
28.21 apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
28.22 -apply (simp add: diff_is_0_eq nat_le_eq_zle)
28.23 done
28.24
28.25 lemma diff_nat_number_of [simp]:
28.26 @@ -628,7 +626,6 @@
28.27
28.28 lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
28.29 apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
28.30 - apply (simp add: neg_nat)
28.31 done
28.32
28.33 lemma nat_number_of_BIT_1:
28.34 @@ -676,7 +673,7 @@
28.35 by (simp only: mult_2 nat_add_distrib of_nat_add)
28.36
28.37 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
28.38 -by (simp only: nat_number_of_def, simp)
28.39 +by (simp only: nat_number_of_def)
28.40
28.41 lemma of_nat_number_of_lemma:
28.42 "of_nat (number_of v :: nat) =
29.1 --- a/src/HOL/Integ/Presburger.thy Wed Jul 26 13:31:07 2006 +0200
29.2 +++ b/src/HOL/Integ/Presburger.thy Wed Jul 26 19:23:04 2006 +0200
29.3 @@ -558,17 +558,13 @@
29.4 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
29.5 apply(induct rule: int_gr_induct)
29.6 apply simp
29.7 - apply arith
29.8 apply (simp add:int_distrib)
29.9 -apply arith
29.10 done
29.11
29.12 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
29.13 apply(induct rule: int_gr_induct)
29.14 apply simp
29.15 - apply arith
29.16 apply (simp add:int_distrib)
29.17 -apply arith
29.18 done
29.19
29.20 lemma minusinfinity:
30.1 --- a/src/HOL/Lambda/Eta.thy Wed Jul 26 13:31:07 2006 +0200
30.2 +++ b/src/HOL/Lambda/Eta.thy Wed Jul 26 19:23:04 2006 +0200
30.3 @@ -50,8 +50,7 @@
30.4 lemma free_lift [simp]:
30.5 "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
30.6 apply (induct t fixing: i k)
30.7 - apply (auto cong: conj_cong)
30.8 - apply arith
30.9 + apply (auto cong: conj_cong)
30.10 done
30.11
30.12 lemma free_subst [simp]:
31.1 --- a/src/HOL/Library/Word.thy Wed Jul 26 13:31:07 2006 +0200
31.2 +++ b/src/HOL/Library/Word.thy Wed Jul 26 19:23:04 2006 +0200
31.3 @@ -1383,7 +1383,7 @@
31.4 proof (rule ccontr)
31.5 from w0 wk
31.6 have k1: "1 < k"
31.7 - by (cases "k - 1",simp_all,arith)
31.8 + by (cases "k - 1",simp_all)
31.9 assume "~ length (int_to_bv i) \<le> k"
31.10 hence "k < length (int_to_bv i)"
31.11 by simp
31.12 @@ -1512,7 +1512,7 @@
31.13 proof (rule ccontr)
31.14 from w1 wk
31.15 have k1: "1 < k"
31.16 - by (cases "k - 1",simp_all,arith)
31.17 + by (cases "k - 1",simp_all)
31.18 assume "~ length (int_to_bv i) \<le> k"
31.19 hence "k < length (int_to_bv i)"
31.20 by simp
31.21 @@ -1731,8 +1731,6 @@
31.22 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)"
31.23 apply (cases "length w1 \<le> length w2")
31.24 apply (auto simp add: max_def)
31.25 - apply arith
31.26 - apply arith
31.27 done
31.28 also have "... = 2 ^ max (length w1) (length w2)"
31.29 proof -
31.30 @@ -1982,7 +1980,6 @@
31.31 apply simp
31.32 apply (subst zpower_zadd_distrib [symmetric])
31.33 apply simp
31.34 - apply arith
31.35 done
31.36 finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
31.37 .
31.38 @@ -2030,10 +2027,6 @@
31.39 apply simp
31.40 apply (subst zpower_zadd_distrib [symmetric])
31.41 apply simp
31.42 - apply (cut_tac lmw)
31.43 - apply arith
31.44 - apply (cut_tac p)
31.45 - apply arith
31.46 done
31.47 hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
31.48 by simp
31.49 @@ -2278,13 +2271,13 @@
31.50 by (simp add: bv_chop_def Let_def)
31.51
31.52 lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
31.53 - by (simp add: bv_chop_def Let_def,arith)
31.54 + by (simp add: bv_chop_def Let_def)
31.55
31.56 lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
31.57 - by (simp add: bv_chop_def Let_def,arith)
31.58 + by (simp add: bv_chop_def Let_def)
31.59
31.60 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
31.61 - by (auto simp add: bv_slice_def,arith)
31.62 + by (auto simp add: bv_slice_def)
31.63
31.64 definition
31.65 length_nat :: "nat => nat"
31.66 @@ -2337,7 +2330,6 @@
31.67 apply (drule norm_empty_bv_to_nat_zero)
31.68 using prems
31.69 apply simp
31.70 - apply arith
31.71 apply (cases "norm_unsigned (nat_to_bv (nat i))")
31.72 apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
31.73 using prems
31.74 @@ -2439,7 +2431,6 @@
31.75 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])
31.76 apply simp_all
31.77 apply (simp_all add: w_defs min_def)
31.78 - apply arith+
31.79 done
31.80 qed
31.81
31.82 @@ -2514,11 +2505,7 @@
31.83 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
31.84 by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle)
31.85
31.86 -lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
31.87 - apply (cases "y = 0",simp_all add: length_int_lt0)
31.88 - apply (subgoal_tac "nat (- y) - Suc 0 \<le> nat (- x) - Suc 0")
31.89 - apply (simp add: length_nat_mono)
31.90 - apply arith
31.91 +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)
31.92 done
31.93
31.94 lemmas [simp] = length_nat_non0
32.1 --- a/src/HOL/List.thy Wed Jul 26 13:31:07 2006 +0200
32.2 +++ b/src/HOL/List.thy Wed Jul 26 19:23:04 2006 +0200
32.3 @@ -1691,7 +1691,6 @@
32.4 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
32.5 apply(induct j)
32.6 apply auto
32.7 -apply arith
32.8 done
32.9
32.10 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
33.1 --- a/src/HOL/Matrix/MatrixGeneral.thy Wed Jul 26 13:31:07 2006 +0200
33.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Jul 26 19:23:04 2006 +0200
33.3 @@ -994,8 +994,6 @@
33.4 apply (subst foldseq_almostzero[of _ j])
33.5 apply (simp add: prems)+
33.6 apply (auto)
33.7 - apply (insert ncols_le[of A j])
33.8 - apply (arith)
33.9 proof -
33.10 fix k
33.11 fix l
34.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Jul 26 13:31:07 2006 +0200
34.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Jul 26 19:23:04 2006 +0200
34.3 @@ -454,8 +454,10 @@
34.4 apply (simp add: max_of_list_def)
34.5 apply (induct xs)
34.6 apply simp
34.7 +ML {* fast_arith_split_limit := 0; *} (* FIXME *)
34.8 apply simp
34.9 apply arith
34.10 +ML {* fast_arith_split_limit := 9; *} (* FIXME *)
34.11 done
34.12
34.13
34.14 @@ -520,16 +522,7 @@
34.15 lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
34.16 \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
34.17 apply (induct i)
34.18 -apply simp+
34.19 - (* case Goto *)
34.20 -apply arith
34.21 - (* case Ifcmpeq *)
34.22 -apply simp
34.23 -apply (erule disjE)
34.24 -apply arith
34.25 -apply arith
34.26 - (* case Throw *)
34.27 -apply simp
34.28 +apply (arith|simp)+
34.29 done
34.30
34.31
34.32 @@ -537,16 +530,7 @@
34.33 \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk>
34.34 \<Longrightarrow> n \<le> pc'"
34.35 apply (induct i)
34.36 -apply simp+
34.37 - (* case Goto *)
34.38 -apply arith
34.39 - (* case Ifcmpeq *)
34.40 -apply simp
34.41 -apply (erule disjE)
34.42 -apply simp
34.43 -apply arith
34.44 - (* case Throw *)
34.45 -apply simp
34.46 +apply (arith|simp)+
34.47 done
34.48
34.49
34.50 @@ -975,7 +959,6 @@
34.51 apply (simp (no_asm_simp))+
34.52 apply simp
34.53 apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
34.54 -apply (simp (no_asm_simp))+
34.55
34.56 (* show check_type \<dots> *)
34.57 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
34.58 @@ -2100,7 +2083,6 @@
34.59 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
34.60 apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
34.61 (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
34.62 - apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
34.63 apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
34.64 apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
34.65 apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
35.1 --- a/src/HOL/NumberTheory/Finite2.thy Wed Jul 26 13:31:07 2006 +0200
35.2 +++ b/src/HOL/NumberTheory/Finite2.thy Wed Jul 26 19:23:04 2006 +0200
35.3 @@ -179,10 +179,6 @@
35.4 lemma int_card_bdd_int_set_l_l: "0 < n ==>
35.5 int(card {x. 0 < x & x < n}) = n - 1"
35.6 apply (auto simp add: card_bdd_int_set_l_l)
35.7 - apply (subgoal_tac "Suc 0 \<le> nat n")
35.8 - apply (auto simp add: zdiff_int [symmetric])
35.9 - apply (subgoal_tac "0 < nat n", arith)
35.10 - apply (simp add: zero_less_nat_eq)
35.11 done
35.12
35.13 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
36.1 --- a/src/HOL/NumberTheory/Gauss.thy Wed Jul 26 13:31:07 2006 +0200
36.2 +++ b/src/HOL/NumberTheory/Gauss.thy Wed Jul 26 19:23:04 2006 +0200
36.3 @@ -104,8 +104,6 @@
36.4 apply (auto simp add: A_def ResSet_def)
36.5 apply (rule_tac m = p in zcong_less_eq)
36.6 apply (insert p_g_2, auto)
36.7 - apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
36.8 - apply (auto, auto simp add: p_minus_one_l)
36.9 done
36.10
36.11 lemma (in GAUSS) B_res: "ResSet p B"
36.12 @@ -255,6 +253,8 @@
36.13 lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
36.14 by (auto simp add: D_eq)
36.15
36.16 +ML {* fast_arith_split_limit := 0; *} (*FIXME*)
36.17 +
36.18 lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
36.19 apply (auto simp add: F_eq A_def)
36.20 proof -
36.21 @@ -270,6 +270,8 @@
36.22 using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
36.23 qed
36.24
36.25 +ML {* fast_arith_split_limit := 9; *} (*FIXME*)
36.26 +
36.27 lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
36.28 using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
36.29
37.1 --- a/src/HOL/NumberTheory/Int2.thy Wed Jul 26 13:31:07 2006 +0200
37.2 +++ b/src/HOL/NumberTheory/Int2.thy Wed Jul 26 19:23:04 2006 +0200
37.3 @@ -191,7 +191,7 @@
37.4 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
37.5 by auto
37.6 also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
37.7 - by (simp only: nat_add_distrib, auto)
37.8 + by (simp only: nat_add_distrib)
37.9 also have "p - 2 + 1 = p - 1" by arith
37.10 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
37.11 by (rule ssubst, auto)
38.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jul 26 13:31:07 2006 +0200
38.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jul 26 19:23:04 2006 +0200
38.3 @@ -193,6 +193,8 @@
38.4 then show ?thesis by auto
38.5 qed
38.6
38.7 +ML {* fast_arith_split_limit := 0; *} (*FIXME*)
38.8 +
38.9 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
38.10 (p * b \<noteq> q * a)"
38.11 proof
38.12 @@ -234,6 +236,8 @@
38.13 with q_g_2 show False by auto
38.14 qed
38.15
38.16 +ML {* fast_arith_split_limit := 9; *} (*FIXME*)
38.17 +
38.18 lemma (in QRTEMP) P_set_finite: "finite (P_set)"
38.19 using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
38.20
39.1 --- a/src/HOL/Presburger.thy Wed Jul 26 13:31:07 2006 +0200
39.2 +++ b/src/HOL/Presburger.thy Wed Jul 26 19:23:04 2006 +0200
39.3 @@ -558,17 +558,13 @@
39.4 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
39.5 apply(induct rule: int_gr_induct)
39.6 apply simp
39.7 - apply arith
39.8 apply (simp add:int_distrib)
39.9 -apply arith
39.10 done
39.11
39.12 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
39.13 apply(induct rule: int_gr_induct)
39.14 apply simp
39.15 - apply arith
39.16 apply (simp add:int_distrib)
39.17 -apply arith
39.18 done
39.19
39.20 lemma minusinfinity:
40.1 --- a/src/HOL/Real/Float.thy Wed Jul 26 13:31:07 2006 +0200
40.2 +++ b/src/HOL/Real/Float.thy Wed Jul 26 19:23:04 2006 +0200
40.3 @@ -28,9 +28,7 @@
40.4 apply (auto, induct_tac n)
40.5 apply (simp_all add: pow2_def)
40.6 apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
40.7 - apply (auto simp add: h)
40.8 - apply arith
40.9 - done
40.10 + by (auto simp add: h)
40.11 show ?thesis
40.12 proof (induct a)
40.13 case (1 n)
41.1 --- a/src/HOL/Real/RComplete.thy Wed Jul 26 13:31:07 2006 +0200
41.2 +++ b/src/HOL/Real/RComplete.thy Wed Jul 26 19:23:04 2006 +0200
41.3 @@ -1066,10 +1066,7 @@
41.4 apply (subgoal_tac "real a = real (int a)")
41.5 apply (erule ssubst)
41.6 apply simp
41.7 - apply (subst nat_diff_distrib)
41.8 apply simp
41.9 - apply (rule le_floor)
41.10 - apply simp_all
41.11 done
41.12
41.13 lemma natceiling_zero [simp]: "natceiling 0 = 0"
41.14 @@ -1206,13 +1203,7 @@
41.15 apply (subgoal_tac "real a = real (int a)")
41.16 apply (erule ssubst)
41.17 apply simp
41.18 - apply (subst nat_diff_distrib)
41.19 apply simp
41.20 - apply (rule order_trans)
41.21 - prefer 2
41.22 - apply (rule ceiling_mono2)
41.23 - apply assumption
41.24 - apply simp_all
41.25 done
41.26
41.27 lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>
42.1 --- a/src/HOL/Real/RealDef.thy Wed Jul 26 13:31:07 2006 +0200
42.2 +++ b/src/HOL/Real/RealDef.thy Wed Jul 26 19:23:04 2006 +0200
42.3 @@ -1024,15 +1024,9 @@
42.4 by (simp add: real_of_nat_ge_zero)
42.5
42.6 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
42.7 -apply (simp add: linorder_not_less)
42.8 -apply (auto intro: abs_ge_self [THEN order_trans])
42.9 -done
42.10 +by simp
42.11
42.12 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
42.13 -apply (simp add: real_add_assoc)
42.14 -apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
42.15 -apply (rule real_add_assoc [THEN subst])
42.16 -apply (rule abs_triangle_ineq)
42.17 -done
42.18 +by simp
42.19
42.20 end
43.1 --- a/src/HOL/Set.thy Wed Jul 26 13:31:07 2006 +0200
43.2 +++ b/src/HOL/Set.thy Wed Jul 26 19:23:04 2006 +0200
43.3 @@ -33,6 +33,7 @@
43.4 Pow :: "'a set => 'a set set" -- "powerset"
43.5 Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
43.6 Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
43.7 + Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers"
43.8 image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90)
43.9 "op :" :: "'a => 'a set => bool" -- "membership"
43.10
43.11 @@ -117,11 +118,13 @@
43.12 "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10)
43.13 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
43.14 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
43.15 + "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3EX! _:_./ _)" [0, 0, 10] 10)
43.16 "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10)
43.17
43.18 syntax (HOL)
43.19 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10)
43.20 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)
43.21 + "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3?! _:_./ _)" [0, 0, 10] 10)
43.22
43.23 translations
43.24 "{x, xs}" == "insert x {xs}"
43.25 @@ -138,16 +141,19 @@
43.26 "INT x:A. B" == "INTER A (%x. B)"
43.27 "ALL x:A. P" == "Ball A (%x. P)"
43.28 "EX x:A. P" == "Bex A (%x. P)"
43.29 + "EX! x:A. P" == "Bex1 A (%x. P)"
43.30 "LEAST x:A. P" => "LEAST x. x:A & P"
43.31
43.32 syntax (xsymbols)
43.33 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
43.34 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
43.35 + "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
43.36 "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
43.37
43.38 syntax (HTML output)
43.39 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
43.40 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
43.41 + "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
43.42
43.43 syntax (xsymbols)
43.44 "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
43.45 @@ -178,30 +184,35 @@
43.46 "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
43.47 "_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
43.48 "_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
43.49 + "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3EX! _<=_./ _)" [0, 0, 10] 10)
43.50
43.51 syntax (xsymbols)
43.52 "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10)
43.53 "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10)
43.54 "_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
43.55 "_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
43.56 + "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
43.57
43.58 syntax (HOL output)
43.59 "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
43.60 "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
43.61 "_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
43.62 "_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
43.63 + "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3?! _<=_./ _)" [0, 0, 10] 10)
43.64
43.65 syntax (HTML output)
43.66 "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10)
43.67 "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10)
43.68 "_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
43.69 "_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
43.70 + "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
43.71
43.72 translations
43.73 "\<forall>A\<subset>B. P" => "ALL A. A \<subset> B --> P"
43.74 - "\<exists>A\<subset>B. P" => "EX A. A \<subset> B & P"
43.75 - "\<forall>A\<subseteq>B. P" => "ALL A. A \<subseteq> B --> P"
43.76 + "\<exists>A\<subset>B. P" => "EX A. A \<subset> B & P"
43.77 + "\<forall>A\<subseteq>B. P" => "ALL A. A \<subseteq> B --> P"
43.78 "\<exists>A\<subseteq>B. P" => "EX A. A \<subseteq> B & P"
43.79 + "\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P"
43.80
43.81 print_translation {*
43.82 let
43.83 @@ -316,6 +327,7 @@
43.84 defs
43.85 Ball_def: "Ball A P == ALL x. x:A --> P(x)"
43.86 Bex_def: "Bex A P == EX x. x:A & P(x)"
43.87 + Bex1_def: "Bex1 A P == EX! x. x:A & P(x)"
43.88
43.89 defs (overloaded)
43.90 subset_def: "A <= B == ALL x:A. x:B"
44.1 --- a/src/HOL/SetInterval.thy Wed Jul 26 13:31:07 2006 +0200
44.2 +++ b/src/HOL/SetInterval.thy Wed Jul 26 19:23:04 2006 +0200
44.3 @@ -301,7 +301,7 @@
44.4 show "?B \<subseteq> ?A"
44.5 proof
44.6 fix n assume a: "n : ?B"
44.7 - hence "n - k : {i..j}" by auto arith+
44.8 + hence "n - k : {i..j}" by auto
44.9 moreover have "n = (n - k) + k" using a by auto
44.10 ultimately show "n : ?A" by blast
44.11 qed
44.12 @@ -315,7 +315,7 @@
44.13 show "?B \<subseteq> ?A"
44.14 proof
44.15 fix n assume a: "n : ?B"
44.16 - hence "n - k : {i..<j}" by auto arith+
44.17 + hence "n - k : {i..<j}" by auto
44.18 moreover have "n = (n - k) + k" using a by auto
44.19 ultimately show "n : ?A" by blast
44.20 qed
44.21 @@ -384,7 +384,6 @@
44.22 apply (rule card_image)
44.23 apply (simp add: inj_on_def)
44.24 apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
44.25 - apply arith
44.26 apply (rule_tac x = "x - l" in exI)
44.27 apply arith
44.28 done
45.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy Wed Jul 26 13:31:07 2006 +0200
45.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed Jul 26 19:23:04 2006 +0200
45.3 @@ -35,7 +35,6 @@
45.4 setsum f (lessThan n) <= setsum g (lessThan n)"
45.5 apply (induct_tac "n")
45.6 apply (auto simp add: lessThan_Suc)
45.7 -apply (drule_tac x = n in spec, arith)
45.8 done
45.9
45.10 lemma tokens_mono_prefix [rule_format]:
46.1 --- a/src/HOL/ZF/HOLZF.thy Wed Jul 26 13:31:07 2006 +0200
46.2 +++ b/src/HOL/ZF/HOLZF.thy Wed Jul 26 19:23:04 2006 +0200
46.3 @@ -578,7 +578,6 @@
46.4 apply (insert n_less_u)
46.5 apply (insert u)
46.6 apply auto
46.7 - apply arith
46.8 done
46.9 ultimately show False by auto
46.10 qed
47.1 --- a/src/HOL/arith_data.ML Wed Jul 26 13:31:07 2006 +0200
47.2 +++ b/src/HOL/arith_data.ML Wed Jul 26 19:23:04 2006 +0200
47.3 @@ -29,7 +29,6 @@
47.4 funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
47.5 end;
47.6
47.7 -
47.8 (* dest_sum *)
47.9
47.10 val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
47.11 @@ -44,7 +43,6 @@
47.12 SOME (t, u) => dest_sum t @ dest_sum u
47.13 | NONE => [tm]));
47.14
47.15 -
47.16 (** generic proof tools **)
47.17
47.18 (* prove conversions *)
47.19 @@ -57,7 +55,6 @@
47.20 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
47.21 (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
47.22
47.23 -
47.24 (* rewriting *)
47.25
47.26 fun simp_all_tac rules =
47.27 @@ -70,7 +67,8 @@
47.28 fun prep_simproc (name, pats, proc) =
47.29 Simplifier.simproc (the_context ()) name pats proc;
47.30
47.31 -end;
47.32 +end; (* NatArithUtils *)
47.33 +
47.34
47.35 signature ARITH_DATA =
47.36 sig
47.37 @@ -78,12 +76,12 @@
47.38 val nat_cancel_sums: simproc list
47.39 end;
47.40
47.41 +
47.42 structure ArithData: ARITH_DATA =
47.43 struct
47.44
47.45 open NatArithUtils;
47.46
47.47 -
47.48 (** cancel common summands **)
47.49
47.50 structure Sum =
47.51 @@ -99,7 +97,6 @@
47.52 fun gen_uncancel_tac rule ct =
47.53 rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
47.54
47.55 -
47.56 (* nat eq *)
47.57
47.58 structure EqCancelSums = CancelSumsFun
47.59 @@ -110,7 +107,6 @@
47.60 val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
47.61 end);
47.62
47.63 -
47.64 (* nat less *)
47.65
47.66 structure LessCancelSums = CancelSumsFun
47.67 @@ -121,7 +117,6 @@
47.68 val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
47.69 end);
47.70
47.71 -
47.72 (* nat le *)
47.73
47.74 structure LeCancelSums = CancelSumsFun
47.75 @@ -132,7 +127,6 @@
47.76 val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
47.77 end);
47.78
47.79 -
47.80 (* nat diff *)
47.81
47.82 structure DiffCancelSums = CancelSumsFun
47.83 @@ -143,8 +137,6 @@
47.84 val uncancel_tac = gen_uncancel_tac diff_cancel;
47.85 end);
47.86
47.87 -
47.88 -
47.89 (** prepare nat_cancel simprocs **)
47.90
47.91 val nat_cancel_sums_add = map prep_simproc
47.92 @@ -159,7 +151,7 @@
47.93 [prep_simproc ("natdiff_cancel_sums",
47.94 ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
47.95
47.96 -end;
47.97 +end; (* ArithData *)
47.98
47.99 open ArithData;
47.100
47.101 @@ -172,6 +164,7 @@
47.102
47.103 structure LA_Logic: LIN_ARITH_LOGIC =
47.104 struct
47.105 +
47.106 val ccontr = ccontr;
47.107 val conjI = conjI;
47.108 val notI = notI;
47.109 @@ -179,7 +172,6 @@
47.110 val not_lessD = linorder_not_less RS iffD1;
47.111 val not_leD = linorder_not_le RS iffD1;
47.112
47.113 -
47.114 fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
47.115
47.116 val mk_Trueprop = HOLogic.mk_Trueprop;
47.117 @@ -202,7 +194,7 @@
47.118 let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
47.119 in instantiate ([],[(cn,ct)]) le0 end;
47.120
47.121 -end;
47.122 +end; (* LA_Logic *)
47.123
47.124
47.125 (* arith theory data *)
47.126 @@ -235,9 +227,18 @@
47.127 {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
47.128
47.129
47.130 -structure LA_Data_Ref: LIN_ARITH_DATA =
47.131 +signature HOL_LIN_ARITH_DATA =
47.132 +sig
47.133 + include LIN_ARITH_DATA
47.134 + val fast_arith_split_limit : int ref
47.135 +end;
47.136 +
47.137 +structure LA_Data_Ref: HOL_LIN_ARITH_DATA =
47.138 struct
47.139
47.140 +(* internal representation of linear (in-)equations *)
47.141 +type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
47.142 +
47.143 (* Decomposition of terms *)
47.144
47.145 fun nT (Type("fun",[N,_])) = N = HOLogic.natT
47.146 @@ -370,16 +371,425 @@
47.147
47.148 fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n)
47.149
47.150 +(*---------------------------------------------------------------------------*)
47.151 +(* code that performs certain goal transformations for linear arithmetic *)
47.152 +(*---------------------------------------------------------------------------*)
47.153 +
47.154 +(* A "do nothing" variant of pre_decomp and pre_tac:
47.155 +
47.156 +fun pre_decomp sg Ts termitems = [termitems];
47.157 +fun pre_tac i = all_tac;
47.158 +*)
47.159 +
47.160 +(*---------------------------------------------------------------------------*)
47.161 +(* the following code performs splitting of certain constants (e.g. min, *)
47.162 +(* max) in a linear arithmetic problem; similar to what split_tac later does *)
47.163 +(* to the proof state *)
47.164 +(*---------------------------------------------------------------------------*)
47.165 +
47.166 +val fast_arith_split_limit = ref 9;
47.167 +
47.168 +(* checks whether splitting with 'thm' is implemented *)
47.169 +
47.170 +(* Thm.thm -> bool *)
47.171 +
47.172 +fun is_split_thm thm =
47.173 + case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
47.174 + (case head_of lhs of
47.175 + Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"]
47.176 + | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false))
47.177 + | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false);
47.178 +
47.179 +(* substitute new for occurrences of old in a term, incrementing bound *)
47.180 +(* variables as needed when substituting inside an abstraction *)
47.181 +
47.182 +(* (term * term) list -> term -> term *)
47.183 +
47.184 +fun subst_term [] t = t
47.185 + | subst_term pairs t =
47.186 + (case AList.lookup (op aconv) pairs t of
47.187 + SOME new =>
47.188 + new
47.189 + | NONE =>
47.190 + (case t of Abs (a, T, body) =>
47.191 + let val pairs' = map (pairself (incr_boundvars 1)) pairs
47.192 + in Abs (a, T, subst_term pairs' body) end
47.193 + | t1 $ t2 =>
47.194 + subst_term pairs t1 $ subst_term pairs t2
47.195 + | _ => t));
47.196 +
47.197 +(* approximates the effect of one application of split_tac (followed by NNF *)
47.198 +(* normalization) on the subgoal represented by '(Ts, terms)'; returns a *)
47.199 +(* list of new subgoals (each again represented by a typ list for bound *)
47.200 +(* variables and a term list for premises), or NONE if split_tac would fail *)
47.201 +(* on the subgoal *)
47.202 +
47.203 +(* theory -> typ list * term list -> (typ list * term list) list option *)
47.204 +
47.205 +(* FIXME: currently only the effect of certain split theorems is reproduced *)
47.206 +(* (which is why we need 'is_split_thm'). A more canonical *)
47.207 +(* implementation should analyze the right-hand side of the split *)
47.208 +(* theorem that can be applied, and modify the subgoal accordingly. *)
47.209 +
47.210 +fun split_once_items sg (Ts, terms) =
47.211 +let
47.212 + (* takes a list [t1, ..., tn] to the term *)
47.213 + (* tn' --> ... --> t1' --> False , *)
47.214 + (* where ti' = HOLogic.dest_Trueprop ti *)
47.215 + (* term list -> term *)
47.216 + fun REPEAT_DETERM_etac_rev_mp terms' =
47.217 + fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
47.218 + val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
47.219 + val cmap = Splitter.cmap_of_split_thms split_thms
47.220 + val splits = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
47.221 +in
47.222 + if length splits > !fast_arith_split_limit then (
47.223 + tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")");
47.224 + NONE
47.225 + ) else (
47.226 + case splits of [] =>
47.227 + NONE (* split_tac would fail: no possible split *)
47.228 + | ((_, _, _, split_type, split_term) :: _) => ( (* ignore all but the first possible split *)
47.229 + case strip_comb split_term of
47.230 + (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
47.231 + (Const ("Orderings.max", _), [t1, t2]) =>
47.232 + let
47.233 + val rev_terms = rev terms
47.234 + val terms1 = map (subst_term [(split_term, t1)]) rev_terms
47.235 + val terms2 = map (subst_term [(split_term, t2)]) rev_terms
47.236 + val t1_leq_t2 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
47.237 + val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
47.238 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.239 + val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
47.240 + val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
47.241 + in
47.242 + SOME [(Ts, subgoal1), (Ts, subgoal2)]
47.243 + end
47.244 + (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
47.245 + | (Const ("Orderings.min", _), [t1, t2]) =>
47.246 + let
47.247 + val rev_terms = rev terms
47.248 + val terms1 = map (subst_term [(split_term, t1)]) rev_terms
47.249 + val terms2 = map (subst_term [(split_term, t2)]) rev_terms
47.250 + val t1_leq_t2 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
47.251 + val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
47.252 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.253 + val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
47.254 + val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
47.255 + in
47.256 + SOME [(Ts, subgoal1), (Ts, subgoal2)]
47.257 + end
47.258 + (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
47.259 + | (Const ("HOL.abs", _), [t1]) =>
47.260 + let
47.261 + val rev_terms = rev terms
47.262 + val terms1 = map (subst_term [(split_term, t1)]) rev_terms
47.263 + val terms2 = map (subst_term [(split_term, Const ("HOL.uminus", split_type --> split_type) $ t1)]) rev_terms
47.264 + val zero = Const ("0", split_type)
47.265 + val zero_leq_t1 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ t1
47.266 + val t1_lt_zero = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
47.267 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.268 + val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
47.269 + val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
47.270 + in
47.271 + SOME [(Ts, subgoal1), (Ts, subgoal2)]
47.272 + end
47.273 + (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
47.274 + | (Const ("HOL.minus", _), [t1, t2]) =>
47.275 + let
47.276 + (* "d" in the above theorem becomes a new bound variable after NNF *)
47.277 + (* transformation, therefore some adjustment of indices is necessary *)
47.278 + val rev_terms = rev terms
47.279 + val zero = Const ("0", split_type)
47.280 + val d = Bound 0
47.281 + val terms1 = map (subst_term [(split_term, zero)]) rev_terms
47.282 + val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms)
47.283 + val t1' = incr_boundvars 1 t1
47.284 + val t2' = incr_boundvars 1 t2
47.285 + val t1_lt_t2 = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
47.286 + 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)
47.287 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.288 + val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
47.289 + val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
47.290 + in
47.291 + SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
47.292 + end
47.293 + (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
47.294 + | (Const ("IntDef.nat", _), [t1]) =>
47.295 + let
47.296 + val rev_terms = rev terms
47.297 + val zero_int = Const ("0", HOLogic.intT)
47.298 + val zero_nat = Const ("0", HOLogic.natT)
47.299 + val n = Bound 0
47.300 + val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms)
47.301 + val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
47.302 + val t1' = incr_boundvars 1 t1
47.303 + val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
47.304 + val t1_lt_zero = Const ("Orderings.less", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
47.305 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.306 + val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
47.307 + val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
47.308 + in
47.309 + SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
47.310 + end
47.311 + (* "?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))) *)
47.312 + | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
47.313 + let
47.314 + val rev_terms = rev terms
47.315 + val zero = Const ("0", split_type)
47.316 + val i = Bound 1
47.317 + val j = Bound 0
47.318 + val terms1 = map (subst_term [(split_term, t1)]) rev_terms
47.319 + val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
47.320 + val t1' = incr_boundvars 2 t1
47.321 + val t2' = incr_boundvars 2 t2
47.322 + val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
47.323 + val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
47.324 + val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
47.325 + val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
47.326 + (Const ("HOL.plus", split_type --> split_type --> split_type) $
47.327 + (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
47.328 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.329 + val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
47.330 + val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
47.331 + in
47.332 + SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
47.333 + end
47.334 + (* "?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))) *)
47.335 + | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
47.336 + let
47.337 + val rev_terms = rev terms
47.338 + val zero = Const ("0", split_type)
47.339 + val i = Bound 1
47.340 + val j = Bound 0
47.341 + val terms1 = map (subst_term [(split_term, zero)]) rev_terms
47.342 + val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
47.343 + val t1' = incr_boundvars 2 t1
47.344 + val t2' = incr_boundvars 2 t2
47.345 + val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
47.346 + val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
47.347 + val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
47.348 + val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
47.349 + (Const ("HOL.plus", split_type --> split_type --> split_type) $
47.350 + (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
47.351 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.352 + val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
47.353 + val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
47.354 + in
47.355 + SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
47.356 + end
47.357 + (* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) --> ?P ?n) &
47.358 + (neg (number_of (bin_minus ?k)) --> (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
47.359 + (neg (number_of ?k) --> (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
47.360 + | (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
47.361 + let
47.362 + val rev_terms = rev terms
47.363 + val zero = Const ("0", split_type)
47.364 + val i = Bound 1
47.365 + val j = Bound 0
47.366 + val terms1 = map (subst_term [(split_term, t1)]) rev_terms
47.367 + val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
47.368 + val t1' = incr_boundvars 2 t1
47.369 + val (t2' as (_ $ k')) = incr_boundvars 2 t2
47.370 + val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
47.371 + val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
47.372 + (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
47.373 + val zero_leq_j = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
47.374 + val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
47.375 + val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
47.376 + (Const ("HOL.plus", split_type --> split_type --> split_type) $
47.377 + (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
47.378 + val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
47.379 + val t2_lt_j = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
47.380 + val j_leq_zero = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
47.381 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.382 + val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
47.383 + val subgoal2 = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
47.384 + @ hd terms2_3
47.385 + :: (if tl terms2_3 = [] then [not_false] else [])
47.386 + @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
47.387 + @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
47.388 + val subgoal3 = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
47.389 + @ hd terms2_3
47.390 + :: (if tl terms2_3 = [] then [not_false] else [])
47.391 + @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
47.392 + @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
47.393 + val Ts' = split_type :: split_type :: Ts
47.394 + in
47.395 + SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
47.396 + end
47.397 + (* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) --> ?P 0) &
47.398 + (neg (number_of (bin_minus ?k)) --> (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
47.399 + (neg (number_of ?k) --> (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
47.400 + | (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
47.401 + let
47.402 + val rev_terms = rev terms
47.403 + val zero = Const ("0", split_type)
47.404 + val i = Bound 1
47.405 + val j = Bound 0
47.406 + val terms1 = map (subst_term [(split_term, zero)]) rev_terms
47.407 + val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
47.408 + val t1' = incr_boundvars 2 t1
47.409 + val (t2' as (_ $ k')) = incr_boundvars 2 t2
47.410 + val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
47.411 + val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
47.412 + (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
47.413 + val zero_leq_j = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
47.414 + val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
47.415 + val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
47.416 + (Const ("HOL.plus", split_type --> split_type --> split_type) $
47.417 + (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
47.418 + val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
47.419 + val t2_lt_j = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
47.420 + val j_leq_zero = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
47.421 + val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
47.422 + val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
47.423 + val subgoal2 = (HOLogic.mk_Trueprop neg_minus_k)
47.424 + :: terms2_3
47.425 + @ not_false
47.426 + :: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
47.427 + val subgoal3 = (HOLogic.mk_Trueprop neg_t2)
47.428 + :: terms2_3
47.429 + @ not_false
47.430 + :: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
47.431 + val Ts' = split_type :: split_type :: Ts
47.432 + in
47.433 + SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
47.434 + end
47.435 + (* this will only happen if a split theorem can be applied for which no code exists above -- *)
47.436 + (* in which case either the split theorem should be implemented above, or 'is_split_thm' *)
47.437 + (* should be modified to filter it out *)
47.438 + | (t, ts) => (
47.439 + warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^
47.440 + " argument(s)) not implemented; proof reconstruction is likely to fail");
47.441 + NONE
47.442 + ))
47.443 + )
47.444 end;
47.445
47.446 +(* remove terms that do not satisfy p; change the order of the remaining *)
47.447 +(* terms in the same way as filter_prems_tac does *)
47.448 +
47.449 +(* (term -> bool) -> term list -> term list *)
47.450 +
47.451 +fun filter_prems_tac_items p terms =
47.452 +let
47.453 + fun filter_prems (t, (left, right)) =
47.454 + if p t then (left, right @ [t]) else (left @ right, [])
47.455 + val (left, right) = foldl filter_prems ([], []) terms
47.456 +in
47.457 + right @ left
47.458 +end;
47.459 +
47.460 +(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *)
47.461 +(* subgoal that has 'terms' as premises *)
47.462 +
47.463 +(* term list -> bool *)
47.464 +
47.465 +fun negated_term_occurs_positively terms =
47.466 + List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t) | _ => false) terms;
47.467 +
47.468 +(* theory -> typ list * term list -> (typ list * term list) list *)
47.469 +
47.470 +fun pre_decomp sg (Ts, terms) =
47.471 +let
47.472 + (* repeatedly split (including newly emerging subgoals) until no further *)
47.473 + (* splitting is possible *)
47.474 + (* (typ list * term list) list -> (typ list * term list) list *)
47.475 + fun split_loop [] = []
47.476 + | split_loop (subgoal::subgoals) = (
47.477 + case split_once_items sg subgoal of
47.478 + SOME new_subgoals => split_loop (new_subgoals @ subgoals)
47.479 + | NONE => subgoal :: split_loop subgoals
47.480 + )
47.481 + fun is_relevant t = isSome (decomp sg t)
47.482 + val relevant_terms = filter_prems_tac_items is_relevant terms (* filter_prems_tac is_relevant *)
47.483 + val split_goals = split_loop [(Ts, relevant_terms)] (* split_tac, NNF normalization *)
47.484 + val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals (* necessary because split_once_tac may normalize terms *)
47.485 + val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm (* TRY (etac notE) THEN eq_assume_tac *)
47.486 +in
47.487 + result
47.488 +end;
47.489 +
47.490 +(* takes the i-th subgoal [| A1; ...; An |] ==> B to *)
47.491 +(* An --> ... --> A1 --> B, performs splitting with the given 'split_thms' *)
47.492 +(* (resulting in a different subgoal P), takes P to ~P ==> False, *)
47.493 +(* performs NNF-normalization of ~P, and eliminates conjunctions, *)
47.494 +(* disjunctions and existential quantifiers from the premises, possibly (in *)
47.495 +(* the case of disjunctions) resulting in several new subgoals, each of the *)
47.496 +(* general form [| Q1; ...; Qm |] ==> False. Fails if more than *)
47.497 +(* !fast_arith_split_limit splits are possible. *)
47.498 +
47.499 +(* Thm.thm list -> int -> Tactical.tactic *)
47.500 +
47.501 +fun split_once_tac split_thms i =
47.502 +let
47.503 + val nnf_simpset =
47.504 + empty_ss setmkeqTrue mk_eq_True
47.505 + setmksimps (mksimps mksimps_pairs)
47.506 + addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
47.507 + not_all, not_ex, not_not]
47.508 + fun prem_nnf_tac i st =
47.509 + full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
47.510 + fun cond_split_tac i st =
47.511 + let
47.512 + val subgoal = Logic.nth_prem (i, Thm.prop_of st)
47.513 + val Ts = rev (map snd (Logic.strip_params subgoal))
47.514 + val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
47.515 + val cmap = Splitter.cmap_of_split_thms split_thms
47.516 + val splits = Splitter.split_posns cmap (theory_of_thm st) Ts concl
47.517 + in
47.518 + if length splits > !fast_arith_split_limit then
47.519 + no_tac st
47.520 + else
47.521 + split_tac split_thms i st
47.522 + end
47.523 +in
47.524 + EVERY' [
47.525 + REPEAT_DETERM o etac rev_mp,
47.526 + cond_split_tac,
47.527 + rtac ccontr,
47.528 + prem_nnf_tac,
47.529 + TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
47.530 + ] i
47.531 +end;
47.532 +
47.533 +(* remove irrelevant premises, then split the i-th subgoal (and all new *)
47.534 +(* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *)
47.535 +(* subgoals and finally attempt to solve them by finding an immediate *)
47.536 +(* contradiction (i.e. a term and its negation) in their premises. *)
47.537 +
47.538 +(* int -> Tactical.tactic *)
47.539 +
47.540 +fun pre_tac i st =
47.541 +let
47.542 + val sg = theory_of_thm st
47.543 + val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
47.544 + fun is_relevant t = isSome (decomp sg t)
47.545 +in
47.546 + DETERM (
47.547 + TRY (filter_prems_tac is_relevant i)
47.548 + THEN (
47.549 + (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
47.550 + THEN_ALL_NEW
47.551 + ((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
47.552 + THEN'
47.553 + (TRY o (etac notE THEN' eq_assume_tac)))
47.554 + ) i
47.555 + ) st
47.556 +end;
47.557 +
47.558 +end; (* LA_Data_Ref *)
47.559 +
47.560
47.561 structure Fast_Arith =
47.562 Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
47.563
47.564 -val fast_arith_tac = Fast_Arith.lin_arith_tac false
47.565 -and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
47.566 -and trace_arith = Fast_Arith.trace
47.567 -and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
47.568 +val fast_arith_tac = Fast_Arith.lin_arith_tac false;
47.569 +val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
47.570 +val trace_arith = Fast_Arith.trace;
47.571 +val fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
47.572 +val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
47.573
47.574 local
47.575
47.576 @@ -439,7 +849,6 @@
47.577 Simplifier.simproc (the_context ()) "fast_nat_arith"
47.578 ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
47.579
47.580 -
47.581 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
47.582 useful to detect inconsistencies among the premises for subgoals which are
47.583 *not* themselves (in)equalities, because the latter activate
47.584 @@ -449,58 +858,24 @@
47.585
47.586 (* arith proof method *)
47.587
47.588 -(* FIXME: K true should be replaced by a sensible test to speed things up
47.589 - in case there are lots of irrelevant terms involved;
47.590 - elimination of min/max can be optimized:
47.591 - (max m n + k <= r) = (m+k <= r & n+k <= r)
47.592 - (l <= min m n + k) = (l <= m+k & l <= n+k)
47.593 -*)
47.594 local
47.595 -(* a simpset for computations subject to optimization !!! *)
47.596 -(*
47.597 -val binarith = map thm
47.598 - ["Pls_0_eq", "Min_1_eq",
47.599 - "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
47.600 - "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
47.601 - "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
47.602 - "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1",
47.603 - "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0",
47.604 - "bin_add_Pls_right", "bin_add_Min_right"];
47.605 - val intarithrel =
47.606 - (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT",
47.607 - "int_le_number_of_eq","int_iszero_number_of_0",
47.608 - "int_less_number_of_eq_neg"]) @
47.609 - (map (fn s => thm s RS thm "lift_bool")
47.610 - ["int_iszero_number_of_Pls","int_iszero_number_of_1",
47.611 - "int_neg_number_of_Min"])@
47.612 - (map (fn s => thm s RS thm "nlift_bool")
47.613 - ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
47.614 -
47.615 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
47.616 - "int_number_of_diff_sym", "int_number_of_mult_sym"];
47.617 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
47.618 - "mult_nat_number_of", "eq_nat_number_of",
47.619 - "less_nat_number_of"]
47.620 -val powerarith =
47.621 - (map thm ["nat_number_of", "zpower_number_of_even",
47.622 - "zpower_Pls", "zpower_Min"]) @
47.623 - [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
47.624 - thm "one_eq_Numeral1_nring"]
47.625 - (thm "zpower_number_of_odd"))]
47.626
47.627 -val comp_arith = binarith @ intarith @ intarithrel @ natarith
47.628 - @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
47.629 -
47.630 -val comp_ss = HOL_basic_ss addsimps comp_arith addsimps simp_thms;
47.631 -*)
47.632 fun raw_arith_tac ex i st =
47.633 + (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
47.634 + decomp sg"?) to speed things up in case there are lots of irrelevant
47.635 + terms involved; elimination of min/max can be optimized:
47.636 + (max m n + k <= r) = (m+k <= r & n+k <= r)
47.637 + (l <= min m n + k) = (l <= m+k & l <= n+k)
47.638 + *)
47.639 refute_tac (K true)
47.640 - (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
47.641 -(* (REPEAT o
47.642 - (fn i =>(split_tac (#splits (ArithTheoryData.get(Thm.theory_of_thm st))) i)
47.643 - THEN (simp_tac comp_ss i))) *)
47.644 - ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
47.645 - i st;
47.646 + (* Splitting is also done inside fast_arith_tac, but not completely -- *)
47.647 + (* split_tac may use split theorems that have not been implemented in *)
47.648 + (* fast_arith_tac (cf. pre_decomp and split_once_items above). *)
47.649 + (* Therefore splitting outside of fast_arith_tac may allow us to prove *)
47.650 + (* some goals that fast_arith_tac alone would fail on. *)
47.651 + (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
47.652 + (fast_ex_arith_tac ex)
47.653 + i st;
47.654
47.655 fun presburger_tac i st =
47.656 (case ArithTheoryData.get (Thm.theory_of_thm st) of
47.657 @@ -510,19 +885,19 @@
47.658
47.659 in
47.660
47.661 -val simple_arith_tac = FIRST' [fast_arith_tac,
47.662 - ObjectLogic.atomize_tac THEN' raw_arith_tac true];
47.663 + val simple_arith_tac = FIRST' [fast_arith_tac,
47.664 + ObjectLogic.atomize_tac THEN' raw_arith_tac true];
47.665
47.666 -val arith_tac = FIRST' [fast_arith_tac,
47.667 - ObjectLogic.atomize_tac THEN' raw_arith_tac true,
47.668 - presburger_tac];
47.669 + val arith_tac = FIRST' [fast_arith_tac,
47.670 + ObjectLogic.atomize_tac THEN' raw_arith_tac true,
47.671 + presburger_tac];
47.672
47.673 -val silent_arith_tac = FIRST' [fast_arith_tac,
47.674 - ObjectLogic.atomize_tac THEN' raw_arith_tac false,
47.675 - presburger_tac];
47.676 + val silent_arith_tac = FIRST' [fast_arith_tac,
47.677 + ObjectLogic.atomize_tac THEN' raw_arith_tac false,
47.678 + presburger_tac];
47.679
47.680 -fun arith_method prems =
47.681 - Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
47.682 + fun arith_method prems =
47.683 + Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
47.684
47.685 end;
47.686
48.1 --- a/src/HOL/ex/Adder.thy Wed Jul 26 13:31:07 2006 +0200
48.2 +++ b/src/HOL/ex/Adder.thy Wed Jul 26 19:23:04 2006 +0200
48.3 @@ -80,22 +80,7 @@
48.4 lemma cca_length [rule_format]:
48.5 "\<forall>bs. length as = length bs -->
48.6 length (carry_chain_adder as bs c) = Suc (length bs)"
48.7 - (is "?P as")
48.8 -proof (induct as,auto simp add: Let_def)
48.9 - fix as :: "bit list"
48.10 - fix xs :: "bit list"
48.11 - assume ind: "?P as"
48.12 - assume len: "Suc (length as) = length xs"
48.13 - thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs"
48.14 - proof (cases xs,simp_all)
48.15 - fix b bs
48.16 - assume [simp]: "xs = b # bs"
48.17 - assume "length as = length bs"
48.18 - with ind
48.19 - show "length (carry_chain_adder as bs c) - Suc 0 = length bs"
48.20 - by auto
48.21 - qed
48.22 -qed
48.23 + by (induct as,auto simp add: Let_def)
48.24
48.25 lemma cca_correct [rule_format]:
48.26 "\<forall>bs. length as = length bs -->
49.1 --- a/src/HOL/simpdata.ML Wed Jul 26 13:31:07 2006 +0200
49.2 +++ b/src/HOL/simpdata.ML Wed Jul 26 19:23:04 2006 +0200
49.3 @@ -166,8 +166,6 @@
49.4 end;
49.5
49.6
49.7 -
49.8 -
49.9 (*** Simproc for Let ***)
49.10
49.11 val use_let_simproc = ref true;
50.1 --- a/src/Provers/Arith/fast_lin_arith.ML Wed Jul 26 13:31:07 2006 +0200
50.2 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jul 26 19:23:04 2006 +0200
50.3 @@ -23,12 +23,12 @@
50.4
50.5 signature LIN_ARITH_LOGIC =
50.6 sig
50.7 - val conjI: thm (* P ==> Q ==> P & Q *)
50.8 + val conjI: thm (* P ==> Q ==> P & Q *)
50.9 val ccontr: thm (* (~ P ==> False) ==> P *)
50.10 val notI: thm (* (P ==> False) ==> ~ P *)
50.11 val not_lessD: thm (* ~(m < n) ==> n <= m *)
50.12 val not_leD: thm (* ~(m <= n) ==> n < m *)
50.13 - val sym: thm (* x = y ==> y = x *)
50.14 + val sym: thm (* x = y ==> y = x *)
50.15 val mk_Eq: thm -> thm
50.16 val atomize: thm -> thm list
50.17 val mk_Trueprop: term -> term
50.18 @@ -52,16 +52,26 @@
50.19
50.20 signature LIN_ARITH_DATA =
50.21 sig
50.22 - val decomp:
50.23 - theory -> term -> ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool) option
50.24 + type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool (* internal representation of linear (in-)equations *)
50.25 + val decomp: theory -> term -> decompT option
50.26 + val pre_decomp: theory -> typ list * term list -> (typ list * term list) list (* preprocessing, performed on a representation of subgoals as list of premises *)
50.27 + val pre_tac : int -> Tactical.tactic (* preprocessing, performed on the goal -- must do the same as 'pre_decomp' *)
50.28 val number_of: IntInf.int * typ -> term
50.29 end;
50.30 (*
50.31 decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
50.32 where Rel is one of "<", "~<", "<=", "~<=" and "=" and
50.33 - p/q is the decomposition of the sum terms x/y into a list
50.34 - of summand * multiplicity pairs and a constant summand and
50.35 - d indicates if the domain is discrete.
50.36 + p (q, respectively) is the decomposition of the sum term x
50.37 + (y, respectively) into a list of summand * multiplicity
50.38 + pairs and a constant summand and d indicates if the domain
50.39 + is discrete.
50.40 +
50.41 +The relationship between pre_decomp and pre_tac is somewhat tricky. The
50.42 +internal representation of a subgoal and the corresponding theorem must
50.43 +be modified by pre_decomp (pre_tac, resp.) in a corresponding way. See
50.44 +the comment for split_items below. (This is even necessary for eta- and
50.45 +beta-equivalent modifications, as some of the lin. arith. code is not
50.46 +insensitive to them.)
50.47
50.48 ss must reduce contradictory <= to False.
50.49 It should also cancel common summands to keep <= reduced;
50.50 @@ -192,32 +202,32 @@
50.51
50.52 fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2));
50.53
50.54 -fun choose2 d ((lb,exactl),(ub,exactu)) =
50.55 - if Rat.le(lb,Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
50.56 - Rat.le(Rat.zero,ub) andalso (ub <> Rat.zero orelse exactu)
50.57 +fun choose2 d ((lb, exactl), (ub, exactu)) =
50.58 + if Rat.le (lb, Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
50.59 + Rat.le (Rat.zero, ub) andalso (ub <> Rat.zero orelse exactu)
50.60 then Rat.zero else
50.61 if not d
50.62 then (if Rat.ge0 lb
50.63 - then if exactl then lb else ratmiddle(lb,ub)
50.64 - else if exactu then ub else ratmiddle(lb,ub))
50.65 + then if exactl then lb else ratmiddle (lb, ub)
50.66 + else if exactu then ub else ratmiddle (lb, ub))
50.67 else (* discrete domain, both bounds must be exact *)
50.68 if Rat.ge0 lb then let val lb' = Rat.roundup lb
50.69 - in if Rat.le(lb',ub) then lb' else raise NoEx end
50.70 + in if Rat.le (lb', ub) then lb' else raise NoEx end
50.71 else let val ub' = Rat.rounddown ub
50.72 - in if Rat.le(lb,ub') then ub' else raise NoEx end;
50.73 + in if Rat.le (lb, ub') then ub' else raise NoEx end;
50.74
50.75 -fun findex1 discr (ex,(v,lineqs)) =
50.76 +fun findex1 discr (ex, (v, lineqs)) =
50.77 let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs;
50.78 val ineqs = Library.foldl elim_eqns ([],nz)
50.79 val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
50.80 - val lb = ratrelmax(map (eval ex v) ge)
50.81 - val ub = ratrelmin(map (eval ex v) le)
50.82 + val lb = ratrelmax (map (eval ex v) ge)
50.83 + val ub = ratrelmin (map (eval ex v) le)
50.84 in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
50.85
50.86 fun findex discr = Library.foldl (findex1 discr);
50.87
50.88 fun elim1 v x =
50.89 - map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le,
50.90 + map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
50.91 nth_update (v, Rat.zero) bs));
50.92
50.93 fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
50.94 @@ -327,7 +337,7 @@
50.95 (* ------------------------------------------------------------------------- *)
50.96
50.97 fun allpairs f xs ys =
50.98 - maps (fn x => map (fn y => f x y) ys) xs;
50.99 + List.concat (map (fn x => map (fn y => f x y) ys) xs);
50.100
50.101 fun extract_first p =
50.102 let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
50.103 @@ -346,25 +356,25 @@
50.104 type history = (int * lineq list) list;
50.105 datatype result = Success of injust | Failure of history;
50.106
50.107 -fun elim(ineqs,hist) =
50.108 - let val dummy = print_ineqs ineqs;
50.109 - val (triv,nontriv) = List.partition is_trivial ineqs in
50.110 - if not(null triv)
50.111 +fun elim (ineqs, hist) =
50.112 + let val dummy = print_ineqs ineqs
50.113 + val (triv, nontriv) = List.partition is_trivial ineqs in
50.114 + if not (null triv)
50.115 then case Library.find_first is_answer triv of
50.116 - NONE => elim(nontriv,hist)
50.117 + NONE => elim (nontriv, hist)
50.118 | SOME(Lineq(_,_,_,j)) => Success j
50.119 else
50.120 - if null nontriv then Failure(hist)
50.121 + if null nontriv then Failure hist
50.122 else
50.123 - let val (eqs,noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
50.124 - if not(null eqs) then
50.125 + let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
50.126 + if not (null eqs) then
50.127 let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
50.128 val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
50.129 (List.filter (fn i => i<>0) clist)
50.130 val c = hd sclist
50.131 val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
50.132 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
50.133 - val v = find_index (fn x => x = c) ceq
50.134 + val v = find_index_eq c ceq
50.135 val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
50.136 (othereqs @ noneqs)
50.137 val others = map (elim_var v eq) roth @ ioth
50.138 @@ -390,10 +400,12 @@
50.139 (* Translate back a proof. *)
50.140 (* ------------------------------------------------------------------------- *)
50.141
50.142 -fun trace_thm msg th =
50.143 - if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th;
50.144 +(* string -> Thm.thm -> Thm.thm *)
50.145 +fun trace_thm msg th =
50.146 + (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
50.147
50.148 -fun trace_msg msg =
50.149 +(* string -> unit *)
50.150 +fun trace_msg msg =
50.151 if !trace then tracing msg else ();
50.152
50.153 (* FIXME OPTIMIZE!!!! (partly done already)
50.154 @@ -408,21 +420,21 @@
50.155 local
50.156 exception FalseE of thm
50.157 in
50.158 +(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> injust -> Thm.thm *)
50.159 fun mkthm (sg, ss) asms just =
50.160 let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
50.161 Data.get sg;
50.162 val simpset' = Simplifier.inherit_context ss simpset;
50.163 - val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
50.164 + val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
50.165 map fst lhs union (map fst rhs union ats))
50.166 - ([], map_filter (fn thm => if Thm.no_prems thm
50.167 - then LA_Data.decomp sg (concl_of thm)
50.168 - else NONE) asms)
50.169 + ([], List.mapPartial (fn thm => if Thm.no_prems thm
50.170 + then LA_Data.decomp sg (concl_of thm)
50.171 + else NONE) asms)
50.172
50.173 fun add2 thm1 thm2 =
50.174 let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
50.175 in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms
50.176 end;
50.177 -
50.178 fun try_add [] _ = NONE
50.179 | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
50.180 NONE => try_add thm1s thm2 | some => some;
50.181 @@ -430,23 +442,18 @@
50.182 fun addthms thm1 thm2 =
50.183 case add2 thm1 thm2 of
50.184 NONE => (case try_add ([thm1] RL inj_thms) thm2 of
50.185 - NONE => (the (try_add ([thm2] RL inj_thms) thm1)
50.186 + NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
50.187 handle Option =>
50.188 (trace_thm "" thm1; trace_thm "" thm2;
50.189 - sys_error "Lin.arith. failed to add thms"))
50.190 + sys_error "Lin.arith. failed to add thms")
50.191 + )
50.192 | SOME thm => thm)
50.193 | SOME thm => thm;
50.194
50.195 fun multn(n,thm) =
50.196 let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
50.197 in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
50.198 -(*
50.199 - fun multn2(n,thm) =
50.200 - let val SOME(mth,cv) =
50.201 - get_first (fn (th,cv) => SOME(thm RS th,cv) handle THM _ => NONE) mult_mono_thms
50.202 - val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
50.203 - in instantiate ([],[(cv,ct)]) mth end
50.204 -*)
50.205 +
50.206 fun multn2(n,thm) =
50.207 let val SOME(mth) =
50.208 get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
50.209 @@ -459,15 +466,15 @@
50.210 let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
50.211 in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
50.212
50.213 - fun mk(Asm i) = trace_thm "Asm" (nth asms i)
50.214 - | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth atoms i))
50.215 - | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
50.216 - | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
50.217 - | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
50.218 - | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
50.219 - | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
50.220 - | mk(Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
50.221 - | mk(Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
50.222 + fun mk (Asm i) = trace_thm "Asm" (nth asms i)
50.223 + | mk (Nat i) = trace_thm "Nat" (LA_Logic.mk_nat_thm sg (nth atoms i))
50.224 + | mk (LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
50.225 + | mk (NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
50.226 + | mk (NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
50.227 + | mk (NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
50.228 + | mk (Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
50.229 + | mk (Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
50.230 + | mk (Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
50.231
50.232 in trace_msg "mkthm";
50.233 let val thm = trace_thm "Final thm:" (mk just)
50.234 @@ -475,19 +482,20 @@
50.235 in trace_thm "After simplification:" fls;
50.236 if LA_Logic.is_False fls then fls
50.237 else
50.238 - (tracing "Assumptions:"; List.app print_thm asms;
50.239 - tracing "Proved:"; print_thm fls;
50.240 + (tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms;
50.241 + tracing "Proved:"; tracing (Display.string_of_thm fls);
50.242 warning "Linear arithmetic should have refuted the assumptions.\n\
50.243 \Please inform Tobias Nipkow (nipkow@in.tum.de).";
50.244 fls)
50.245 end
50.246 - end handle FalseE thm => (trace_thm "False reached early:" thm; thm)
50.247 + end handle FalseE thm => trace_thm "False reached early:" thm
50.248 end
50.249 end;
50.250
50.251 fun coeff poly atom : IntInf.int =
50.252 AList.lookup (op =) poly atom |> the_default 0;
50.253
50.254 +(* int list -> int *)
50.255 fun lcms is = Library.foldl lcm (1, is);
50.256
50.257 fun integ(rlhs,r,rel,rrhs,s,d) =
50.258 @@ -499,8 +507,8 @@
50.259 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
50.260
50.261 fun mklineq n atoms =
50.262 - fn (item,k) =>
50.263 - let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
50.264 + fn (item, k) =>
50.265 + let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item
50.266 val lhsa = map (coeff lhs) atoms
50.267 and rhsa = map (coeff rhs) atoms
50.268 val diff = map2 (curry (op -)) rhsa lhsa
50.269 @@ -535,28 +543,33 @@
50.270 curry (op ~~) sds
50.271 #> map print_atom
50.272 #> commas
50.273 - #> curry (op ^) "Counter example:\n";
50.274 + #> curry (op ^) "Counter example (possibly spurious):\n";
50.275
50.276 -fun trace_ex(sg,params,atoms,discr,n,hist:history) =
50.277 - if null hist then ()
50.278 - else let val frees = map Free params;
50.279 - fun s_of_t t = Sign.string_of_term sg (subst_bounds(frees,t));
50.280 - val (v,lineqs) :: hist' = hist
50.281 - val start = if v = ~1 then (findex0 discr n lineqs,hist')
50.282 - else (replicate n Rat.zero,hist)
50.283 - val ex = SOME (produce_ex ((map s_of_t atoms)~~discr) (findex discr start))
50.284 - handle NoEx => NONE;
50.285 - in
50.286 - (case ex of
50.287 - SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
50.288 - | NONE => warning "arith failed")
50.289 - end;
50.290 +fun trace_ex (sg, params, atoms, discr, n, hist : history) =
50.291 + case hist of
50.292 + [] => ()
50.293 + | (v, lineqs) :: hist' =>
50.294 + let val frees = map Free params
50.295 + fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
50.296 + val start = if v = ~1 then (findex0 discr n lineqs, hist')
50.297 + else (replicate n Rat.zero, hist)
50.298 + val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) (findex discr start))
50.299 + handle NoEx => NONE
50.300 + in
50.301 + case ex of
50.302 + SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
50.303 + | NONE => warning "arith failed"
50.304 + end;
50.305
50.306 -fun mknat pTs ixs (atom,i) =
50.307 - if LA_Logic.is_nat(pTs,atom)
50.308 +(* ------------------------------------------------------------------------- *)
50.309 +
50.310 +(* Term.typ list -> int list -> Term.term * int -> lineq option *)
50.311 +
50.312 +fun mknat pTs ixs (atom, i) =
50.313 + if LA_Logic.is_nat (pTs, atom)
50.314 then let val l = map (fn j => if j=i then 1 else 0) ixs
50.315 - in SOME(Lineq(0,Le,l,Nat(i))) end
50.316 - else NONE
50.317 + in SOME (Lineq (0, Le, l, Nat i)) end
50.318 + else NONE;
50.319
50.320 (* This code is tricky. It takes a list of premises in the order they occur
50.321 in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical
50.322 @@ -570,95 +583,184 @@
50.323
50.324 For variables n of type nat, a constraint 0 <= n is added.
50.325 *)
50.326 -fun split_items(items) =
50.327 - let fun elim_neq front _ [] = [rev front]
50.328 - | elim_neq front n (NONE::ineqs) = elim_neq front (n+1) ineqs
50.329 - | elim_neq front n (SOME(ineq as (l,i,rel,r,j,d))::ineqs) =
50.330 - if rel = "~=" then elim_neq front n (ineqs @ [SOME(l,i,"<",r,j,d)]) @
50.331 - elim_neq front n (ineqs @ [SOME(r,j,"<",l,i,d)])
50.332 - else elim_neq ((ineq,n) :: front) (n+1) ineqs
50.333 - in elim_neq [] 0 items end;
50.334
50.335 -fun add_atoms(ats,((lhs,_,_,rhs,_,_),_)) =
50.336 - (map fst lhs) union ((map fst rhs) union ats)
50.337 +(* FIXME: To optimize, the splitting of cases and the search for refutations *)
50.338 +(* should be intertwined: separate the first (fully split) case, *)
50.339 +(* refute it, continue with splitting and refuting. Terminate with *)
50.340 +(* failure as soon as a case could not be refuted; i.e. delay further *)
50.341 +(* splitting until after a refutation for other cases has been found. *)
50.342
50.343 -fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) =
50.344 - (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats)
50.345 +(* Theory.theory -> bool -> typ list * term list -> (typ list * (decompT * int) list) list *)
50.346 +
50.347 +fun split_items sg do_pre (Ts, terms) =
50.348 + let
50.349 +(*
50.350 + val _ = trace_msg ("split_items: do_pre is " ^ Bool.toString do_pre ^ "\n" ^
50.351 + " Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
50.352 + " terms = " ^ string_of_list (Sign.string_of_term sg) terms)
50.353 +*)
50.354 + (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
50.355 + (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *)
50.356 + (* level *)
50.357 + (* decompT option list -> decompT option list list *)
50.358 + fun elim_neq [] = [[]]
50.359 + | elim_neq (NONE :: ineqs) = map (cons NONE) (elim_neq ineqs)
50.360 + | elim_neq (SOME(ineq as (l,i,rel,r,j,d)) :: ineqs) =
50.361 + if rel = "~=" then elim_neq (ineqs @ [SOME (l, i, "<", r, j, d)]) @
50.362 + elim_neq (ineqs @ [SOME (r, j, "<", l, i, d)])
50.363 + else map (cons (SOME ineq)) (elim_neq ineqs)
50.364 + (* int -> decompT option list -> (decompT * int) list *)
50.365 + fun number_hyps _ [] = []
50.366 + | number_hyps n (NONE::xs) = number_hyps (n+1) xs
50.367 + | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs
50.368 +
50.369 + val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *)
50.370 + (* (typ list * term list) list *)
50.371 + (if do_pre then LA_Data.pre_decomp sg else Library.single)
50.372 + |> (* compute the internal encoding of (in-)equalities *)
50.373 + (* (typ list * decompT option list) list *)
50.374 + map (apsnd (map (LA_Data.decomp sg)))
50.375 + |> (* splitting of inequalities *)
50.376 + (* (typ list * decompT option list) list list *)
50.377 + map (fn (Ts, items) => map (pair Ts) (elim_neq items))
50.378 + |> (* combine the list of lists of subgoals into a single list *)
50.379 + (* (typ list * decompT option list) list *)
50.380 + List.concat
50.381 + |> (* numbering of hypotheses, ignoring irrelevant ones *)
50.382 + (* (typ list * (decompT * int) list) list *)
50.383 + map (apsnd (number_hyps 0))
50.384 +(*
50.385 + val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^ " subgoal(s)"
50.386 + ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
50.387 + (" " ^ Int.toString n ^ ". Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
50.388 + " items = " ^ string_of_list
50.389 + (string_of_pair
50.390 + (fn (l, i, rel, r, j, d) =>
50.391 + enclose "(" ")" (commas
50.392 + [string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
50.393 + Rat.string_of_rat i,
50.394 + rel,
50.395 + string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
50.396 + Rat.string_of_rat j,
50.397 + Bool.toString d]))
50.398 + Int.toString) items, n+1)) result 1))
50.399 +*)
50.400 + in result end;
50.401 +
50.402 +(* term list * (decompT * int) -> term list *)
50.403 +
50.404 +fun add_atoms (ats, ((lhs,_,_,rhs,_,_),_)) =
50.405 + (map fst lhs) union ((map fst rhs) union ats);
50.406 +
50.407 +(* (bool * term) list * (decompT * int) -> (bool * term) list *)
50.408 +
50.409 +fun add_datoms (dats, ((lhs,_,_,rhs,_,d),_)) =
50.410 + (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
50.411 +
50.412 +(* (decompT * int) list -> bool list *)
50.413
50.414 fun discr initems = map fst (Library.foldl add_datoms ([],initems));
50.415
50.416 -fun refutes sg (pTs,params) ex =
50.417 +(* Theory.theory -> (string * typ) list -> bool -> (typ list * (decompT * int) list) list -> injust list -> injust list option *)
50.418 +
50.419 +fun refutes sg params show_ex =
50.420 let
50.421 - fun refute (initems::initemss) js =
50.422 - let val atoms = Library.foldl add_atoms ([],initems)
50.423 + (* (typ list * (decompT * int) list) list -> injust list -> injust list option *)
50.424 + fun refute ((Ts, initems)::initemss) js =
50.425 + let val atoms = Library.foldl add_atoms ([], initems)
50.426 val n = length atoms
50.427 val mkleq = mklineq n atoms
50.428 val ixs = 0 upto (n-1)
50.429 val iatoms = atoms ~~ ixs
50.430 - val natlineqs = map_filter (mknat pTs ixs) iatoms
50.431 + val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
50.432 val ineqs = map mkleq initems @ natlineqs
50.433 - in case elim(ineqs,[]) of
50.434 - Success(j) =>
50.435 - (trace_msg "Contradiction!"; refute initemss (js@[j]))
50.436 - | Failure(hist) =>
50.437 - (if not ex then ()
50.438 - else trace_ex(sg,params,atoms,discr initems,n,hist);
50.439 - NONE)
50.440 + in case elim (ineqs, []) of
50.441 + Success j =>
50.442 + (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); refute initemss (js@[j]))
50.443 + | Failure hist =>
50.444 + (if not show_ex then
50.445 + ()
50.446 + else let
50.447 + (* invent names for bound variables that are new, i.e. in Ts, but not in params *)
50.448 + (* we assume that Ts still contains (map snd params) as a suffix *)
50.449 + val new_count = length Ts - length params - 1
50.450 + val new_names = map Name.bound (0 upto new_count)
50.451 + val params' = (new_names @ map fst params) ~~ Ts
50.452 + in
50.453 + trace_ex (sg, params', atoms, discr initems, n, hist)
50.454 + end; NONE)
50.455 end
50.456 | refute [] js = SOME js
50.457 in refute end;
50.458
50.459 -fun refute sg ps ex items = refutes sg ps ex (split_items items) [];
50.460 +(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *)
50.461
50.462 -fun refute_tac ss (i,justs) =
50.463 +fun refute sg params show_ex do_pre terms =
50.464 + refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
50.465 +
50.466 +(* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *)
50.467 +
50.468 +fun refute_tac ss (i, justs) =
50.469 fn state =>
50.470 - let val sg = #sign(rep_thm state)
50.471 - val {neqE, ...} = Data.get sg;
50.472 - fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
50.473 - METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
50.474 - in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
50.475 - EVERY(map just1 justs)
50.476 - end
50.477 - state;
50.478 + let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ Int.toString (length justs) ^ " justification(s)):") state
50.479 + val sg = theory_of_thm state
50.480 + val {neqE, ...} = Data.get sg
50.481 + fun just1 j =
50.482 + REPEAT_DETERM (eresolve_tac neqE i) THEN (* eliminate inequalities *)
50.483 + METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i (* use theorems generated from the actual justifications *)
50.484 + in DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
50.485 + DETERM (LA_Data.pre_tac i) THEN (* user-defined preprocessing of the subgoal *)
50.486 + PRIMITIVE (trace_thm "State after pre_tac:") THEN
50.487 + EVERY (map just1 justs) (* prove every resulting subgoal, using its justification *)
50.488 + end state;
50.489
50.490 -fun count P xs = length(List.filter P xs);
50.491 +(* ('a -> bool) -> 'a list -> int *)
50.492 +
50.493 +fun count P xs = length (List.filter P xs);
50.494
50.495 (* The limit on the number of ~= allowed.
50.496 Because each ~= is split into two cases, this can lead to an explosion.
50.497 *)
50.498 val fast_arith_neq_limit = ref 9;
50.499
50.500 -fun prove sg ps ex Hs concl =
50.501 -let val Hitems = map (LA_Data.decomp sg) Hs
50.502 -in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems
50.503 - > !fast_arith_neq_limit then NONE
50.504 - else
50.505 - case LA_Data.decomp sg concl of
50.506 - NONE => refute sg ps ex (Hitems@[NONE])
50.507 - | SOME(citem as (r,i,rel,l,j,d)) =>
50.508 - let val neg::rel0 = explode rel
50.509 - val nrel = if neg = "~" then implode rel0 else "~"^rel
50.510 - in refute sg ps ex (Hitems @ [SOME(r,i,nrel,l,j,d)]) end
50.511 -end;
50.512 +(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *)
50.513 +
50.514 +fun prove sg params show_ex do_pre Hs concl =
50.515 + let
50.516 + (* append the negated conclusion to 'Hs' -- this corresponds to *)
50.517 + (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
50.518 + (* theorem/tactic level *)
50.519 + val Hs' = Hs @ [LA_Logic.neg_prop concl]
50.520 + (* decompT option -> bool *)
50.521 + fun is_neq NONE = false
50.522 + | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
50.523 + in
50.524 + trace_msg "prove";
50.525 + if count is_neq (map (LA_Data.decomp sg) Hs')
50.526 + > !fast_arith_neq_limit then (
50.527 + trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")");
50.528 + NONE
50.529 + ) else
50.530 + refute sg params show_ex do_pre Hs'
50.531 + end;
50.532
50.533 (*
50.534 Fast but very incomplete decider. Only premises and conclusions
50.535 that are already (negated) (in)equations are taken into account.
50.536 *)
50.537 -fun simpset_lin_arith_tac ss ex i st = SUBGOAL (fn (A,_) =>
50.538 - let val params = rev(Logic.strip_params A)
50.539 - val pTs = map snd params
50.540 - val Hs = Logic.strip_assums_hyp A
50.541 - val concl = Logic.strip_assums_concl A
50.542 +fun simpset_lin_arith_tac ss show_ex i st = SUBGOAL (fn (A,_) =>
50.543 + let val params = rev (Logic.strip_params A)
50.544 + val Hs = Logic.strip_assums_hyp A
50.545 + val concl = Logic.strip_assums_concl A
50.546 in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
50.547 - case prove (Thm.sign_of_thm st) (pTs,params) ex Hs concl of
50.548 + case prove (Thm.sign_of_thm st) params show_ex true Hs concl of
50.549 NONE => (trace_msg "Refutation failed."; no_tac)
50.550 - | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
50.551 + | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
50.552 end) i st;
50.553
50.554 -fun lin_arith_tac ex i st =
50.555 +fun lin_arith_tac show_ex i st =
50.556 simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
50.557 - ex i st;
50.558 + show_ex i st;
50.559
50.560 fun cut_lin_arith_tac ss i =
50.561 cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
50.562 @@ -673,47 +775,77 @@
50.563 datatype splittree = Tip of thm list
50.564 | Spl of thm * cterm * splittree * cterm * splittree
50.565
50.566 +(* the cterm "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *)
50.567 +
50.568 +(* Thm.cterm -> Thm.cterm * Thm.cterm *)
50.569 +
50.570 fun extract imp =
50.571 -let val (Il,r) = Thm.dest_comb imp
50.572 - val (_,imp1) = Thm.dest_comb Il
50.573 - val (Ict1,_) = Thm.dest_comb imp1
50.574 - val (_,ct1) = Thm.dest_comb Ict1
50.575 - val (Ir,_) = Thm.dest_comb r
50.576 - val (_,Ict2r) = Thm.dest_comb Ir
50.577 - val (Ict2,_) = Thm.dest_comb Ict2r
50.578 - val (_,ct2) = Thm.dest_comb Ict2
50.579 -in (ct1,ct2) end;
50.580 +let val (Il, r) = Thm.dest_comb imp
50.581 + val (_, imp1) = Thm.dest_comb Il
50.582 + val (Ict1, _) = Thm.dest_comb imp1
50.583 + val (_, ct1) = Thm.dest_comb Ict1
50.584 + val (Ir, _) = Thm.dest_comb r
50.585 + val (_, Ict2r) = Thm.dest_comb Ir
50.586 + val (Ict2, _) = Thm.dest_comb Ict2r
50.587 + val (_, ct2) = Thm.dest_comb Ict2
50.588 +in (ct1, ct2) end;
50.589 +
50.590 +(* Theory.theory -> Thm.thm list -> splittree *)
50.591
50.592 fun splitasms sg asms =
50.593 -let val {neqE, ...} = Data.get sg;
50.594 - fun split(asms',[]) = Tip(rev asms')
50.595 - | split(asms',asm::asms) =
50.596 - (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
50.597 - of SOME spl =>
50.598 - let val (ct1,ct2) = extract(cprop_of spl)
50.599 - val thm1 = assume ct1 and thm2 = assume ct2
50.600 - in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2]))
50.601 +let val {neqE, ...} = Data.get sg
50.602 + fun elim_neq (asms', []) = Tip (rev asms')
50.603 + | elim_neq (asms', asm::asms) =
50.604 + (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
50.605 + SOME spl =>
50.606 + let val (ct1, ct2) = extract (cprop_of spl)
50.607 + val thm1 = assume ct1
50.608 + val thm2 = assume ct2
50.609 + in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
50.610 end
50.611 - | NONE => split(asm::asms', asms))
50.612 -in split([],asms) end;
50.613 + | NONE => elim_neq (asm::asms', asms))
50.614 +in elim_neq ([], asms) end;
50.615 +
50.616 +(* Theory.theory * MetaSimplifier.simpset -> splittree -> injust list -> (Thm.thm, injust list) *)
50.617
50.618 fun fwdproof ctxt (Tip asms) (j::js) = (mkthm ctxt asms j, js)
50.619 - | fwdproof ctxt (Spl(thm,ct1,tree1,ct2,tree2)) js =
50.620 - let val (thm1,js1) = fwdproof ctxt tree1 js
50.621 - val (thm2,js2) = fwdproof ctxt tree2 js1
50.622 + | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js =
50.623 + let val (thm1, js1) = fwdproof ctxt tree1 js
50.624 + val (thm2, js2) = fwdproof ctxt tree2 js1
50.625 val thm1' = implies_intr ct1 thm1
50.626 val thm2' = implies_intr ct2 thm2
50.627 in (thm2' COMP (thm1' COMP thm), js2) end;
50.628 (* needs handle THM _ => NONE ? *)
50.629
50.630 -fun prover (ctxt as (sg, _)) thms Tconcl js pos =
50.631 -let val nTconcl = LA_Logic.neg_prop Tconcl
50.632 - val cnTconcl = cterm_of sg nTconcl
50.633 - val nTconclthm = assume cnTconcl
50.634 - val tree = splitasms sg (thms @ [nTconclthm])
50.635 - val (thm,_) = fwdproof ctxt tree js
50.636 - val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
50.637 -in SOME(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end
50.638 +(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *)
50.639 +
50.640 +fun prover (ctxt as (sg, ss)) thms Tconcl js pos =
50.641 +let
50.642 +(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *)
50.643 +(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *)
50.644 + (* There is no "forward version" of 'pre_tac'. Therefore we combine the *)
50.645 + (* available theorems into a single proof state and perform "backward proof" *)
50.646 + (* using 'refute_tac'. *)
50.647 +(*
50.648 + val Hs = map prop_of thms
50.649 + val Prop = fold (curry Logic.mk_implies) (rev Hs) Tconcl
50.650 + val cProp = cterm_of sg Prop
50.651 + val concl = Goal.init cProp
50.652 + |> refute_tac ss (1, js)
50.653 + |> Seq.hd
50.654 + |> Goal.finish
50.655 + |> fold (fn thA => fn thAB => implies_elim thAB thA) thms
50.656 +*)
50.657 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
50.658 + val nTconcl = LA_Logic.neg_prop Tconcl
50.659 + val cnTconcl = cterm_of sg nTconcl
50.660 + val nTconclthm = assume cnTconcl
50.661 + val tree = splitasms sg (thms @ [nTconclthm])
50.662 + val (Falsethm, _) = fwdproof ctxt tree js
50.663 + val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
50.664 + val concl = implies_intr cnTconcl Falsethm COMP contr
50.665 +in SOME (trace_thm "Proved by lin. arith. prover:"
50.666 + (LA_Logic.mk_Eq concl)) end
50.667 (* in case concl contains ?-var, which makes assume fail: *)
50.668 handle THM _ => NONE;
50.669
50.670 @@ -723,15 +855,22 @@
50.671 2. lin_arith_prover is applied by the simplifier which
50.672 dives into terms and will thus try the non-negated concl anyway.
50.673 *)
50.674 +
50.675 +(* Theory.theory -> MetaSimplifier.simpset -> Term.term -> Thm.thm option *)
50.676 +
50.677 fun lin_arith_prover sg ss concl =
50.678 -let
50.679 - val thms = maps LA_Logic.atomize (prems_of_ss ss);
50.680 - val Hs = map (#prop o rep_thm) thms
50.681 +let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
50.682 + val Hs = map prop_of thms
50.683 val Tconcl = LA_Logic.mk_Trueprop concl
50.684 -in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
50.685 +(*
50.686 + val _ = trace_msg "lin_arith_prover"
50.687 + val _ = map (trace_thm "thms:") thms
50.688 + val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl)
50.689 +*)
50.690 +in case prove sg [] false false Hs Tconcl of (* concl provable? *)
50.691 SOME js => prover (sg, ss) thms Tconcl js true
50.692 | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl
50.693 - in case prove sg ([],[]) false Hs nTconcl of (* ~concl provable? *)
50.694 + in case prove sg [] false false Hs nTconcl of (* ~concl provable? *)
50.695 SOME js => prover (sg, ss) thms nTconcl js false
50.696 | NONE => NONE
50.697 end
51.1 --- a/src/Provers/splitter.ML Wed Jul 26 13:31:07 2006 +0200
51.2 +++ b/src/Provers/splitter.ML Wed Jul 26 19:23:04 2006 +0200
51.3 @@ -13,18 +13,23 @@
51.4 signature SPLITTER_DATA =
51.5 sig
51.6 val mk_eq : thm -> thm
51.7 - val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
51.8 - val iffD : thm (* "[| P = Q; Q |] ==> P" *)
51.9 - val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
51.10 - val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
51.11 - val exE : thm (* "[| x. P x; !!x. P x ==> Q |] ==> Q" *)
51.12 - val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *)
51.13 - val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *)
51.14 - val notnotD : thm (* "~ ~ P ==> P" *)
51.15 + val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
51.16 + val iffD : thm (* "[| P = Q; Q |] ==> P" *)
51.17 + val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
51.18 + val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
51.19 + val exE : thm (* "[| EX x. P x; !!x. P x ==> Q |] ==> Q" *)
51.20 + val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *)
51.21 + val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *)
51.22 + val notnotD : thm (* "~ ~ P ==> P" *)
51.23 end
51.24
51.25 signature SPLITTER =
51.26 sig
51.27 + (* somewhat more internal functions *)
51.28 + val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list
51.29 + val split_posns : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term ->
51.30 + (thm * (typ * typ * int list) list * int list * typ * term) list (* first argument is a "cmap", returns a list of "split packs" *)
51.31 + (* the "real" interface, providing a number of tactics *)
51.32 val split_tac : thm list -> int -> tactic
51.33 val split_inside_tac: thm list -> int -> tactic
51.34 val split_asm_tac : thm list -> int -> tactic
51.35 @@ -52,18 +57,42 @@
51.36 val const_Trueprop = ObjectLogic.judgment_name (the_context ());
51.37
51.38
51.39 -fun split_format_err() = error("Wrong format for split rule");
51.40 +fun split_format_err () = error "Wrong format for split rule";
51.41
51.42 +(* thm -> (string * typ) * bool *)
51.43 fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
51.44 Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
51.45 (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
51.46 | _ => split_format_err ())
51.47 | _ => split_format_err ();
51.48
51.49 +(* thm list -> (string * (typ * term * thm * typ * int) list) list *)
51.50 +fun cmap_of_split_thms thms =
51.51 +let
51.52 + val splits = map Data.mk_eq thms
51.53 + fun add_thm (cmap, thm) =
51.54 + (case concl_of thm of _$(t as _$lhs)$_ =>
51.55 + (case strip_comb lhs of (Const(a,aT),args) =>
51.56 + let val info = (aT,lhs,thm,fastype_of t,length args)
51.57 + in case AList.lookup (op =) cmap a of
51.58 + SOME infos => AList.update (op =) (a, info::infos) cmap
51.59 + | NONE => (a,[info])::cmap
51.60 + end
51.61 + | _ => split_format_err())
51.62 + | _ => split_format_err())
51.63 +in
51.64 + Library.foldl add_thm ([], splits)
51.65 +end;
51.66 +
51.67 +(* ------------------------------------------------------------------------- *)
51.68 +(* mk_case_split_tac *)
51.69 +(* ------------------------------------------------------------------------- *)
51.70 +
51.71 +(* (int * int -> order) -> thm list -> int -> tactic * <split_posns> *)
51.72 +
51.73 fun mk_case_split_tac order =
51.74 let
51.75
51.76 -
51.77 (************************************************************
51.78 Create lift-theorem "trlift" :
51.79
51.80 @@ -71,7 +100,8 @@
51.81
51.82 *************************************************************)
51.83
51.84 -val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
51.85 +val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
51.86 +
51.87 val lift =
51.88 let val ct = read_cterm Pure.thy
51.89 ("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
51.90 @@ -129,12 +159,12 @@
51.91
51.92
51.93 (* add all loose bound variables in t to list is *)
51.94 -fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
51.95 +fun add_lbnos (is,t) = add_loose_bnos (t,0,is);
51.96
51.97 (* check if the innermost abstraction that needs to be removed
51.98 has a body of type T; otherwise the expansion thm will fail later on
51.99 *)
51.100 -fun type_test(T,lbnos,apsns) =
51.101 +fun type_test (T,lbnos,apsns) =
51.102 let val (_,U,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
51.103 in T=U end;
51.104
51.105 @@ -166,7 +196,7 @@
51.106 lifting is required before applying the split-theorem.
51.107 ******************************************************************************)
51.108
51.109 -fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) =
51.110 +fun mk_split_pack (thm, T, T', n, ts, apsns, pos, TB, t) =
51.111 if n > length ts then []
51.112 else let val lev = length apsns
51.113 val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
51.114 @@ -198,26 +228,34 @@
51.115 see Pure/pattern.ML for the full version;
51.116 *)
51.117 local
51.118 -exception MATCH
51.119 + exception MATCH
51.120 in
51.121 -fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
51.122 - handle Type.TYPE_MATCH => raise MATCH;
51.123 -fun fomatch sg args =
51.124 - let
51.125 - fun mtch tyinsts = fn
51.126 - (Ts,Var(_,T), t) => typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
51.127 - | (_,Free (a,T), Free (b,U)) =>
51.128 - if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
51.129 - | (_,Const (a,T), Const (b,U)) =>
51.130 - if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
51.131 - | (_,Bound i, Bound j) => if i=j then tyinsts else raise MATCH
51.132 - | (Ts,Abs(_,T,t), Abs(_,U,u)) =>
51.133 - mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
51.134 - | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
51.135 - | _ => raise MATCH
51.136 - in (mtch Vartab.empty args; true) handle MATCH => false end;
51.137 -end
51.138 + (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *)
51.139 + fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
51.140 + handle Type.TYPE_MATCH => raise MATCH
51.141 + (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *)
51.142 + fun fomatch sg args =
51.143 + let
51.144 + (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *)
51.145 + fun mtch tyinsts = fn
51.146 + (Ts, Var(_,T), t) =>
51.147 + typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
51.148 + | (_, Free (a,T), Free (b,U)) =>
51.149 + if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
51.150 + | (_, Const (a,T), Const (b,U)) =>
51.151 + if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
51.152 + | (_, Bound i, Bound j) =>
51.153 + if i=j then tyinsts else raise MATCH
51.154 + | (Ts, Abs(_,T,t), Abs(_,U,u)) =>
51.155 + mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
51.156 + | (Ts, f$t, g$u) =>
51.157 + mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
51.158 + | _ => raise MATCH
51.159 + in (mtch Vartab.empty args; true) handle MATCH => false end;
51.160 +end (* local *)
51.161
51.162 +(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term ->
51.163 + (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *)
51.164 fun split_posns cmap sg Ts t =
51.165 let
51.166 val T' = fastype_of1 (Ts, t);
51.167 @@ -243,15 +281,13 @@
51.168 in snd(Library.foldl iter ((0, a), ts)) end
51.169 in posns Ts [] [] t end;
51.170
51.171 +fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
51.172
51.173 -fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
51.174 -
51.175 -fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
51.176 +fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
51.177 prod_ord (int_ord o pairself length) (order o pairself length)
51.178 ((ps, pos), (qs, qos));
51.179
51.180
51.181 -
51.182 (************************************************************
51.183 call split_posns with appropriate parameters
51.184 *************************************************************)
51.185 @@ -261,8 +297,10 @@
51.186 val goali = nth_subgoal i state
51.187 val Ts = rev(map #2 (Logic.strip_params goali))
51.188 val _ $ t $ _ = Logic.strip_assums_concl goali;
51.189 - in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
51.190 + in (Ts, t, sort shorter (split_posns cmap sg Ts t)) end;
51.191
51.192 +fun exported_split_posns cmap sg Ts t =
51.193 + sort shorter (split_posns cmap sg Ts t);
51.194
51.195 (*************************************************************
51.196 instantiate lift theorem
51.197 @@ -322,20 +360,11 @@
51.198 i : number of subgoal the tactic should be applied to
51.199 *****************************************************************************)
51.200
51.201 +(* thm list -> int -> tactic *)
51.202 +
51.203 fun split_tac [] i = no_tac
51.204 | split_tac splits i =
51.205 - let val splits = map Data.mk_eq splits;
51.206 - fun add_thm(cmap,thm) =
51.207 - (case concl_of thm of _$(t as _$lhs)$_ =>
51.208 - (case strip_comb lhs of (Const(a,aT),args) =>
51.209 - let val info = (aT,lhs,thm,fastype_of t,length args)
51.210 - in case AList.lookup (op =) cmap a of
51.211 - SOME infos => AList.update (op =) (a, info::infos) cmap
51.212 - | NONE => (a,[info])::cmap
51.213 - end
51.214 - | _ => split_format_err())
51.215 - | _ => split_format_err())
51.216 - val cmap = Library.foldl add_thm ([],splits);
51.217 + let val cmap = cmap_of_split_thms splits
51.218 fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
51.219 fun lift_split_tac state =
51.220 let val (Ts, t, splits) = select cmap state i
51.221 @@ -352,12 +381,12 @@
51.222 (rtac meta_iffD i THEN lift_split_tac)
51.223 end;
51.224
51.225 -in split_tac end;
51.226 +in (split_tac, exported_split_posns) end; (* mk_case_split_tac *)
51.227
51.228
51.229 -val split_tac = mk_case_split_tac int_ord;
51.230 +val (split_tac, split_posns) = mk_case_split_tac int_ord;
51.231
51.232 -val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
51.233 +val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord);
51.234
51.235
51.236 (*****************************************************************************
51.237 @@ -378,7 +407,7 @@
51.238 | first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
51.239 first_prem_is_disj t
51.240 | first_prem_is_disj _ = false;
51.241 - (* does not work properly if the split variable is bound by a quantfier *)
51.242 + (* does not work properly if the split variable is bound by a quantifier *)
51.243 fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
51.244 (if first_prem_is_disj t
51.245 then EVERY[etac Data.disjE i,rotate_tac ~1 i,
51.246 @@ -387,11 +416,11 @@
51.247 else all_tac)
51.248 THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
51.249 THEN REPEAT (dresolve_tac [Data.notnotD] i)) i;
51.250 - in if n<0 then no_tac else DETERM (EVERY'
51.251 + in if n<0 then no_tac else (DETERM (EVERY'
51.252 [rotate_tac n, etac Data.contrapos2,
51.253 split_tac splits,
51.254 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
51.255 - flat_prems_tac] i)
51.256 + flat_prems_tac] i))
51.257 end;
51.258 in SUBGOAL tac
51.259 end;