merged
authorhaftmann
Mon May 11 19:51:21 2009 +0200 (2009-05-11)
changeset 31104ac8a12b0ed3c
parent 31099 03314c427b34
parent 31103 9820999467a7
child 31110 ef8210e58ad7
merged
src/HOL/NSA/hypreal_arith.ML
src/HOL/Nat_Numeral.thy
src/HOL/Tools/rat_arith.ML
src/HOL/Tools/real_arith.ML
     1.1 --- a/doc-src/HOL/HOL.tex	Tue May 05 17:09:18 2009 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon May 11 19:51:21 2009 +0200
     1.3 @@ -1427,7 +1427,7 @@
     1.4  provides a decision procedure for \emph{linear arithmetic}: formulae involving
     1.5  addition and subtraction. The simplifier invokes a weak version of this
     1.6  decision procedure automatically. If this is not sufficent, you can invoke the
     1.7 -full procedure \ttindex{linear_arith_tac} explicitly.  It copes with arbitrary
     1.8 +full procedure \ttindex{Lin_Arith.tac} explicitly.  It copes with arbitrary
     1.9  formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
    1.10    min}, {\tt max} and numerical constants. Other subterms are treated as
    1.11  atomic, while subformulae not involving numerical types are ignored. Quantified
    1.12 @@ -1438,10 +1438,10 @@
    1.13  If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
    1.14  {\tt k dvd} are also supported. The former two are eliminated
    1.15  by case distinctions, again blowing up the running time.
    1.16 -If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
    1.17 +If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
    1.18  super-exponential time and space.
    1.19  
    1.20 -If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
    1.21 +If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
    1.22  the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
    1.23  theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
    1.24  Theory \texttt{Divides} contains theorems about \texttt{div} and
     2.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Tue May 05 17:09:18 2009 +0200
     2.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon May 11 19:51:21 2009 +0200
     2.3 @@ -443,7 +443,7 @@
     2.4  --{* 32 subgoals left *}
     2.5  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
     2.6  
     2.7 -apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
     2.8 +apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
     2.9  --{* 9 subgoals left *}
    2.10  apply (force simp add:less_Suc_eq)
    2.11  apply(drule sym)
     3.1 --- a/src/HOL/Int.thy	Tue May 05 17:09:18 2009 +0200
     3.2 +++ b/src/HOL/Int.thy	Mon May 11 19:51:21 2009 +0200
     3.3 @@ -1521,6 +1521,7 @@
     3.4  use "Tools/numeral_simprocs.ML"
     3.5  
     3.6  use "Tools/int_arith.ML"
     3.7 +setup {* Int_Arith.global_setup *}
     3.8  declaration {* K Int_Arith.setup *}
     3.9  
    3.10  setup {*
     4.1 --- a/src/HOL/IsaMakefile	Tue May 05 17:09:18 2009 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Mon May 11 19:51:21 2009 +0200
     4.3 @@ -295,8 +295,6 @@
     4.4    Real.thy \
     4.5    RealVector.thy \
     4.6    Tools/float_syntax.ML \
     4.7 -  Tools/rat_arith.ML \
     4.8 -  Tools/real_arith.ML \
     4.9    Tools/Qelim/ferrante_rackoff_data.ML \
    4.10    Tools/Qelim/ferrante_rackoff.ML \
    4.11    Tools/Qelim/langford_data.ML \
    4.12 @@ -1051,7 +1049,6 @@
    4.13    NSA/HyperDef.thy \
    4.14    NSA/HyperNat.thy \
    4.15    NSA/Hyperreal.thy \
    4.16 -  NSA/hypreal_arith.ML \
    4.17    NSA/Filter.thy \
    4.18    NSA/NatStar.thy \
    4.19    NSA/NSA.thy \
     5.1 --- a/src/HOL/NSA/HyperDef.thy	Tue May 05 17:09:18 2009 +0200
     5.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon May 11 19:51:21 2009 +0200
     5.3 @@ -8,7 +8,6 @@
     5.4  
     5.5  theory HyperDef
     5.6  imports HyperNat Real
     5.7 -uses ("hypreal_arith.ML")
     5.8  begin
     5.9  
    5.10  types hypreal = "real star"
    5.11 @@ -343,8 +342,17 @@
    5.12  Addsimps [symmetric hypreal_diff_def]
    5.13  *)
    5.14  
    5.15 -use "hypreal_arith.ML"
    5.16 -declaration {* K hypreal_arith_setup *}
    5.17 +declaration {*
    5.18 +  K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
    5.19 +    @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
    5.20 +  #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
    5.21 +      @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
    5.22 +      @{thm star_of_diff}, @{thm star_of_mult}]
    5.23 +  #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
    5.24 +  #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
    5.25 +      "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    5.26 +      (K Lin_Arith.simproc)]))
    5.27 +*}
    5.28  
    5.29  
    5.30  subsection {* Exponentials on the Hyperreals *}
     6.1 --- a/src/HOL/NSA/hypreal_arith.ML	Tue May 05 17:09:18 2009 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,45 +0,0 @@
     6.4 -(*  Title:      HOL/NSA/hypreal_arith.ML
     6.5 -    Author:     Tobias Nipkow, TU Muenchen
     6.6 -    Copyright   1999 TU Muenchen
     6.7 -
     6.8 -Simprocs for common factor cancellation & Rational coefficient handling
     6.9 -
    6.10 -Instantiation of the generic linear arithmetic package for type hypreal.
    6.11 -*)
    6.12 -
    6.13 -local
    6.14 -
    6.15 -val simps = [thm "star_of_zero",
    6.16 -             thm "star_of_one",
    6.17 -             thm "star_of_number_of",
    6.18 -             thm "star_of_add",
    6.19 -             thm "star_of_minus",
    6.20 -             thm "star_of_diff",
    6.21 -             thm "star_of_mult"]
    6.22 -
    6.23 -val real_inj_thms = [thm "star_of_le" RS iffD2,
    6.24 -                     thm "star_of_less" RS iffD2,
    6.25 -                     thm "star_of_eq" RS iffD2]
    6.26 -
    6.27 -in
    6.28 -
    6.29 -val hyprealT = Type (@{type_name StarDef.star}, [HOLogic.realT]);
    6.30 -
    6.31 -val fast_hypreal_arith_simproc =
    6.32 -    Simplifier.simproc (the_context ())
    6.33 -      "fast_hypreal_arith" 
    6.34 -      ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    6.35 -    (K Lin_Arith.lin_arith_simproc);
    6.36 -
    6.37 -val hypreal_arith_setup =
    6.38 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    6.39 -   {add_mono_thms = add_mono_thms,
    6.40 -    mult_mono_thms = mult_mono_thms,
    6.41 -    inj_thms = real_inj_thms @ inj_thms,
    6.42 -    lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
    6.43 -    neqE = neqE,
    6.44 -    simpset = simpset addsimps simps}) #>
    6.45 -  Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, HOLogic.realT --> hyprealT) #>
    6.46 -  Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
    6.47 -
    6.48 -end;
     7.1 --- a/src/HOL/Nat.thy	Tue May 05 17:09:18 2009 +0200
     7.2 +++ b/src/HOL/Nat.thy	Mon May 11 19:51:21 2009 +0200
     7.3 @@ -1410,6 +1410,7 @@
     7.4  declaration {* K Nat_Arith.setup *}
     7.5  
     7.6  use "Tools/lin_arith.ML"
     7.7 +setup {* Lin_Arith.global_setup *}
     7.8  declaration {* K Lin_Arith.setup *}
     7.9  
    7.10  lemmas [arith_split] = nat_diff_split split_min split_max
     8.1 --- a/src/HOL/Nat_Numeral.thy	Tue May 05 17:09:18 2009 +0200
     8.2 +++ b/src/HOL/Nat_Numeral.thy	Mon May 11 19:51:21 2009 +0200
     8.3 @@ -874,33 +874,21 @@
     8.4  
     8.5  use "Tools/nat_numeral_simprocs.ML"
     8.6  
     8.7 -declaration {*
     8.8 -let
     8.9 -
    8.10 -val less_eq_rules = @{thms ring_distribs} @
    8.11 -  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
    8.12 -   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    8.13 -   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    8.14 -   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    8.15 -   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    8.16 -   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    8.17 -   @{thm mult_Suc}, @{thm mult_Suc_right},
    8.18 -   @{thm add_Suc}, @{thm add_Suc_right},
    8.19 -   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    8.20 -   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
    8.21 -
    8.22 -val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
    8.23 -
    8.24 -in
    8.25 -
    8.26 -K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    8.27 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    8.28 -    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    8.29 -    simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    8.30 -      addsimps less_eq_rules
    8.31 -      addsimprocs simprocs}))
    8.32 -
    8.33 -end
    8.34 +declaration {* 
    8.35 +  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    8.36 +  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
    8.37 +     @{thm nat_0}, @{thm nat_1},
    8.38 +     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    8.39 +     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    8.40 +     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    8.41 +     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    8.42 +     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    8.43 +     @{thm mult_Suc}, @{thm mult_Suc_right},
    8.44 +     @{thm add_Suc}, @{thm add_Suc_right},
    8.45 +     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    8.46 +     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
    8.47 +     @{thm if_True}, @{thm if_False}])
    8.48 +  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
    8.49  *}
    8.50  
    8.51  
     9.1 --- a/src/HOL/Rational.thy	Tue May 05 17:09:18 2009 +0200
     9.2 +++ b/src/HOL/Rational.thy	Mon May 11 19:51:21 2009 +0200
     9.3 @@ -6,7 +6,6 @@
     9.4  
     9.5  theory Rational
     9.6  imports GCD Archimedean_Field
     9.7 -uses ("Tools/rat_arith.ML")
     9.8  begin
     9.9  
    9.10  subsection {* Rational numbers as quotient *}
    9.11 @@ -582,10 +581,25 @@
    9.12    by (simp add: floor_unique)
    9.13  
    9.14  
    9.15 -subsection {* Arithmetic setup *}
    9.16 +subsection {* Linear arithmetic setup *}
    9.17  
    9.18 -use "Tools/rat_arith.ML"
    9.19 -declaration {* K rat_arith_setup *}
    9.20 +declaration {*
    9.21 +  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
    9.22 +    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
    9.23 +  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
    9.24 +    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
    9.25 +  #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
    9.26 +      @{thm True_implies_equals},
    9.27 +      read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
    9.28 +      @{thm divide_1}, @{thm divide_zero_left},
    9.29 +      @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    9.30 +      @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    9.31 +      @{thm of_int_minus}, @{thm of_int_diff},
    9.32 +      @{thm of_int_of_nat_eq}]
    9.33 +  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
    9.34 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
    9.35 +  #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
    9.36 +*}
    9.37  
    9.38  
    9.39  subsection {* Embedding from Rationals to other Fields *}
    10.1 --- a/src/HOL/RealDef.thy	Tue May 05 17:09:18 2009 +0200
    10.2 +++ b/src/HOL/RealDef.thy	Mon May 11 19:51:21 2009 +0200
    10.3 @@ -9,7 +9,6 @@
    10.4  
    10.5  theory RealDef
    10.6  imports PReal
    10.7 -uses ("Tools/real_arith.ML")
    10.8  begin
    10.9  
   10.10  definition
   10.11 @@ -960,10 +959,20 @@
   10.12          (if neg (number_of v :: int) then 0  
   10.13           else (number_of v :: real))"
   10.14  by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of)
   10.15 - 
   10.16  
   10.17 -use "Tools/real_arith.ML"
   10.18 -declaration {* K real_arith_setup *}
   10.19 +declaration {*
   10.20 +  K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
   10.21 +    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
   10.22 +  #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
   10.23 +    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
   10.24 +  #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
   10.25 +      @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
   10.26 +      @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
   10.27 +      @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
   10.28 +      @{thm real_of_nat_number_of}, @{thm real_number_of}]
   10.29 +  #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT)
   10.30 +  #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT))
   10.31 +*}
   10.32  
   10.33  
   10.34  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
    11.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue May 05 17:09:18 2009 +0200
    11.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 11 19:51:21 2009 +0200
    11.3 @@ -172,7 +172,7 @@
    11.4  
    11.5      (* Canonical linear form for terms, formulae etc.. *)
    11.6  fun provelin ctxt t = Goal.prove ctxt [] [] t 
    11.7 -  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
    11.8 +  (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
    11.9  fun linear_cmul 0 tm = zero 
   11.10    | linear_cmul n tm = case tm of  
   11.11        Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
    12.1 --- a/src/HOL/Tools/int_arith.ML	Tue May 05 17:09:18 2009 +0200
    12.2 +++ b/src/HOL/Tools/int_arith.ML	Mon May 11 19:51:21 2009 +0200
    12.3 @@ -5,8 +5,8 @@
    12.4  
    12.5  signature INT_ARITH =
    12.6  sig
    12.7 -  val fast_int_arith_simproc: simproc
    12.8    val setup: Context.generic -> Context.generic
    12.9 +  val global_setup: theory -> theory
   12.10  end
   12.11  
   12.12  structure Int_Arith : INT_ARITH =
   12.13 @@ -49,17 +49,15 @@
   12.14    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   12.15    proc = proc1, identifier = []};
   12.16  
   12.17 -val allowed_consts =
   12.18 -  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
   12.19 -   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
   12.20 -   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
   12.21 -   @{const_name "HOL.less_eq"}];
   12.22 -
   12.23 -fun check t = case t of
   12.24 -   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
   12.25 -                else s mem_string allowed_consts
   12.26 - | a$b => check a andalso check b
   12.27 - | _ => false;
   12.28 +fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
   12.29 +  | check (Const (@{const_name "HOL.one"}, _)) = true
   12.30 +  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
   12.31 +      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
   12.32 +      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
   12.33 +      @{const_name "HOL.zero"},
   12.34 +      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
   12.35 +  | check (a $ b) = check a andalso check b
   12.36 +  | check _ = false;
   12.37  
   12.38  val conv =
   12.39    Simplifier.rewrite
   12.40 @@ -80,35 +78,24 @@
   12.41    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   12.42    proc = sproc, identifier = []}
   12.43  
   12.44 -val add_rules =
   12.45 -    simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
   12.46 -    @{thms int_arith_rules}
   12.47 +val fast_int_arith_simproc =
   12.48 +  Simplifier.simproc @{theory} "fast_int_arith"
   12.49 +     ["(m::'a::{ordered_idom,number_ring}) < n",
   12.50 +      "(m::'a::{ordered_idom,number_ring}) <= n",
   12.51 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
   12.52  
   12.53 -val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   12.54 -
   12.55 -val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   12.56 -  :: Numeral_Simprocs.combine_numerals
   12.57 -  :: Numeral_Simprocs.cancel_numerals;
   12.58 +val global_setup = Simplifier.map_simpset
   12.59 +  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
   12.60  
   12.61  val setup =
   12.62 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   12.63 -   {add_mono_thms = add_mono_thms,
   12.64 -    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
   12.65 -    inj_thms = nat_inj_thms @ inj_thms,
   12.66 -    lessD = lessD @ [@{thm zless_imp_add1_zle}],
   12.67 -    neqE = neqE,
   12.68 -    simpset = simpset addsimps add_rules
   12.69 -                      addsimprocs numeral_base_simprocs}) #>
   12.70 -  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   12.71 -  Lin_Arith.add_discrete_type @{type_name Int.int}
   12.72 -
   12.73 -val fast_int_arith_simproc =
   12.74 -  Simplifier.simproc (the_context ())
   12.75 -  "fast_int_arith" 
   12.76 -     ["(m::'a::{ordered_idom,number_ring}) < n",
   12.77 -      "(m::'a::{ordered_idom,number_ring}) <= n",
   12.78 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
   12.79 +  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   12.80 +  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
   12.81 +  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
   12.82 +      @ @{thms arith_special} @ @{thms int_arith_rules})
   12.83 +  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   12.84 +      :: Numeral_Simprocs.combine_numerals
   12.85 +      :: Numeral_Simprocs.cancel_numerals)
   12.86 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
   12.87 +  #> Lin_Arith.add_discrete_type @{type_name Int.int}
   12.88  
   12.89  end;
   12.90 -
   12.91 -Addsimprocs [Int_Arith.fast_int_arith_simproc];
    13.1 --- a/src/HOL/Tools/lin_arith.ML	Tue May 05 17:09:18 2009 +0200
    13.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon May 11 19:51:21 2009 +0200
    13.3 @@ -4,29 +4,20 @@
    13.4  HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
    13.5  *)
    13.6  
    13.7 -signature BASIC_LIN_ARITH =
    13.8 -sig
    13.9 -  val arith_split_add: attribute
   13.10 -  val lin_arith_pre_tac: Proof.context -> int -> tactic
   13.11 -  val fast_arith_tac: Proof.context -> int -> tactic
   13.12 -  val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
   13.13 -  val lin_arith_simproc: simpset -> term -> thm option
   13.14 -  val fast_nat_arith_simproc: simproc
   13.15 -  val linear_arith_tac: Proof.context -> int -> tactic
   13.16 -end;
   13.17 -
   13.18  signature LIN_ARITH =
   13.19  sig
   13.20 -  include BASIC_LIN_ARITH
   13.21 -  val add_discrete_type: string -> Context.generic -> Context.generic
   13.22 +  val pre_tac: Proof.context -> int -> tactic
   13.23 +  val simple_tac: Proof.context -> int -> tactic
   13.24 +  val tac: Proof.context -> int -> tactic
   13.25 +  val simproc: simpset -> term -> thm option
   13.26 +  val add_inj_thms: thm list -> Context.generic -> Context.generic
   13.27 +  val add_lessD: thm -> Context.generic -> Context.generic
   13.28 +  val add_simps: thm list -> Context.generic -> Context.generic
   13.29 +  val add_simprocs: simproc list -> Context.generic -> Context.generic
   13.30    val add_inj_const: string * typ -> Context.generic -> Context.generic
   13.31 -  val map_data:
   13.32 -    ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   13.33 -      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} ->
   13.34 -     {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   13.35 -      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ->
   13.36 -    Context.generic -> Context.generic
   13.37 +  val add_discrete_type: string -> Context.generic -> Context.generic
   13.38    val setup: Context.generic -> Context.generic
   13.39 +  val global_setup: theory -> theory
   13.40    val split_limit: int Config.T
   13.41    val neq_limit: int Config.T
   13.42    val warning_count: int ref
   13.43 @@ -47,37 +38,38 @@
   13.44  val sym = sym;
   13.45  val not_lessD = @{thm linorder_not_less} RS iffD1;
   13.46  val not_leD = @{thm linorder_not_le} RS iffD1;
   13.47 -val le0 = thm "le0";
   13.48  
   13.49 -fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   13.50 +fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI;
   13.51  
   13.52  val mk_Trueprop = HOLogic.mk_Trueprop;
   13.53  
   13.54  fun atomize thm = case Thm.prop_of thm of
   13.55 -    Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
   13.56 -    atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
   13.57 +    Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
   13.58 +    atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   13.59    | _ => [thm];
   13.60  
   13.61 -fun neg_prop ((TP as Const("Trueprop",_)) $ (Const("Not",_) $ t)) = TP $ t
   13.62 -  | neg_prop ((TP as Const("Trueprop",_)) $ t) = TP $ (HOLogic.Not $t)
   13.63 +fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
   13.64 +  | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
   13.65    | neg_prop t = raise TERM ("neg_prop", [t]);
   13.66  
   13.67  fun is_False thm =
   13.68    let val _ $ t = Thm.prop_of thm
   13.69 -  in t = Const("False",HOLogic.boolT) end;
   13.70 +  in t = HOLogic.false_const end;
   13.71  
   13.72  fun is_nat t = (fastype_of1 t = HOLogic.natT);
   13.73  
   13.74 -fun mk_nat_thm sg t =
   13.75 -  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   13.76 -  in instantiate ([],[(cn,ct)]) le0 end;
   13.77 +fun mk_nat_thm thy t =
   13.78 +  let
   13.79 +    val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
   13.80 +    and ct = cterm_of thy t
   13.81 +  in instantiate ([], [(cn, ct)]) @{thm le0} end;
   13.82  
   13.83  end;
   13.84  
   13.85  
   13.86  (* arith context data *)
   13.87  
   13.88 -structure ArithContextData = GenericDataFun
   13.89 +structure Lin_Arith_Data = GenericDataFun
   13.90  (
   13.91    type T = {splits: thm list,
   13.92              inj_consts: (string * typ) list,
   13.93 @@ -92,27 +84,25 @@
   13.94      discrete = Library.merge (op =) (discrete1, discrete2)};
   13.95  );
   13.96  
   13.97 -val get_arith_data = ArithContextData.get o Context.Proof;
   13.98 +val get_arith_data = Lin_Arith_Data.get o Context.Proof;
   13.99  
  13.100 -val arith_split_add = Thm.declaration_attribute (fn thm =>
  13.101 -  ArithContextData.map (fn {splits, inj_consts, discrete} =>
  13.102 -    {splits = update Thm.eq_thm_prop thm splits,
  13.103 -     inj_consts = inj_consts, discrete = discrete}));
  13.104 +fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
  13.105 +  {splits = update Thm.eq_thm_prop thm splits,
  13.106 +   inj_consts = inj_consts, discrete = discrete});
  13.107  
  13.108 -fun add_discrete_type d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
  13.109 +fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
  13.110    {splits = splits, inj_consts = inj_consts,
  13.111     discrete = update (op =) d discrete});
  13.112  
  13.113 -fun add_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
  13.114 +fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
  13.115    {splits = splits, inj_consts = update (op =) c inj_consts,
  13.116     discrete = discrete});
  13.117  
  13.118 -val (split_limit, setup1) = Attrib.config_int "linarith_split_limit" 9;
  13.119 -val (neq_limit, setup2) = Attrib.config_int "linarith_neq_limit" 9;
  13.120 -val setup_options = setup1 #> setup2;
  13.121 +val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
  13.122 +val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
  13.123  
  13.124  
  13.125 -structure LA_Data_Ref =
  13.126 +structure LA_Data =
  13.127  struct
  13.128  
  13.129  val fast_arith_neq_limit = neq_limit;
  13.130 @@ -243,15 +233,12 @@
  13.131  end handle Rat.DIVZERO => NONE;
  13.132  
  13.133  fun of_lin_arith_sort thy U =
  13.134 -  Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]);
  13.135 +  Sign.of_sort thy (U, @{sort Ring_and_Field.ordered_idom});
  13.136  
  13.137 -fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
  13.138 -  if of_lin_arith_sort sg U then
  13.139 -    (true, D mem discrete)
  13.140 -  else (* special cases *)
  13.141 -    if D mem discrete then  (true, true)  else  (false, false)
  13.142 -  | allows_lin_arith sg discrete U =
  13.143 -  (of_lin_arith_sort sg U, false);
  13.144 +fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
  13.145 +      if of_lin_arith_sort thy U then (true, member (op =) discrete D)
  13.146 +      else if member (op =) discrete D then (true, true) else (false, false)
  13.147 +  | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
  13.148  
  13.149  fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
  13.150    case T of
  13.151 @@ -287,7 +274,7 @@
  13.152    | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
  13.153    | domain_is_nat _                                                 = false;
  13.154  
  13.155 -fun number_of (n, T) = HOLogic.mk_number T n;
  13.156 +val mk_number = HOLogic.mk_number;
  13.157  
  13.158  (*---------------------------------------------------------------------------*)
  13.159  (* the following code performs splitting of certain constants (e.g. min,     *)
  13.160 @@ -756,17 +743,34 @@
  13.161    )
  13.162  end;
  13.163  
  13.164 -end;  (* LA_Data_Ref *)
  13.165 +end;  (* LA_Data *)
  13.166  
  13.167  
  13.168 -val lin_arith_pre_tac = LA_Data_Ref.pre_tac;
  13.169 +val pre_tac = LA_Data.pre_tac;
  13.170  
  13.171 -structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data_Ref);
  13.172 +structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
  13.173  
  13.174  val map_data = Fast_Arith.map_data;
  13.175  
  13.176 -fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
  13.177 -val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
  13.178 +fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
  13.179 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
  13.180 +    lessD = lessD, neqE = neqE, simpset = simpset};
  13.181 +
  13.182 +fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
  13.183 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
  13.184 +    lessD = f lessD, neqE = neqE, simpset = simpset};
  13.185 +
  13.186 +fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
  13.187 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
  13.188 +    lessD = lessD, neqE = neqE, simpset = f simpset};
  13.189 +
  13.190 +fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
  13.191 +fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
  13.192 +fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
  13.193 +fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
  13.194 +
  13.195 +fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
  13.196 +val lin_arith_tac = Fast_Arith.lin_arith_tac;
  13.197  val trace = Fast_Arith.trace;
  13.198  val warning_count = Fast_Arith.warning_count;
  13.199  
  13.200 @@ -774,7 +778,7 @@
  13.201     Most of the work is done by the cancel tactics. *)
  13.202  
  13.203  val init_arith_data =
  13.204 - map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
  13.205 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
  13.206     {add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
  13.207      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
  13.208      inj_thms = inj_thms,
  13.209 @@ -797,17 +801,7 @@
  13.210  fun add_arith_facts ss =
  13.211    add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
  13.212  
  13.213 -val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
  13.214 -
  13.215 -val fast_nat_arith_simproc =
  13.216 -  Simplifier.simproc (the_context ()) "fast_nat_arith"
  13.217 -    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
  13.218 -
  13.219 -(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
  13.220 -useful to detect inconsistencies among the premises for subgoals which are
  13.221 -*not* themselves (in)equalities, because the latter activate
  13.222 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
  13.223 -solver all the time rather than add the additional check. *)
  13.224 +val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
  13.225  
  13.226  
  13.227  (* generic refutation procedure *)
  13.228 @@ -857,7 +851,7 @@
  13.229  
  13.230  local
  13.231  
  13.232 -fun raw_arith_tac ctxt ex =
  13.233 +fun raw_tac ctxt ex =
  13.234    (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
  13.235       decomp sg"? -- but note that the test is applied to terms already before
  13.236       they are split/normalized) to speed things up in case there are lots of
  13.237 @@ -866,21 +860,21 @@
  13.238       (l <= min m n + k) = (l <= m+k & l <= n+k)
  13.239    *)
  13.240    refute_tac (K true)
  13.241 -    (* Splitting is also done inside fast_arith_tac, but not completely --   *)
  13.242 +    (* Splitting is also done inside simple_tac, but not completely --   *)
  13.243      (* split_tac may use split theorems that have not been implemented in    *)
  13.244 -    (* fast_arith_tac (cf. pre_decomp and split_once_items above), and       *)
  13.245 +    (* simple_tac (cf. pre_decomp and split_once_items above), and       *)
  13.246      (* split_limit may trigger.                                   *)
  13.247 -    (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
  13.248 -    (* some goals that fast_arith_tac alone would fail on.                   *)
  13.249 +    (* Therefore splitting outside of simple_tac may allow us to prove   *)
  13.250 +    (* some goals that simple_tac alone would fail on.                   *)
  13.251      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
  13.252 -    (fast_ex_arith_tac ctxt ex);
  13.253 +    (lin_arith_tac ctxt ex);
  13.254  
  13.255  in
  13.256  
  13.257 -fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
  13.258 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
  13.259 +fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
  13.260 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
  13.261  
  13.262 -val linear_arith_tac = gen_linear_arith_tac true;
  13.263 +val tac = gen_tac true;
  13.264  
  13.265  end;
  13.266  
  13.267 @@ -889,21 +883,25 @@
  13.268  
  13.269  val setup =
  13.270    init_arith_data #>
  13.271 -  Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
  13.272 +  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
  13.273 +    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
  13.274 +    (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
  13.275 +    useful to detect inconsistencies among the premises for subgoals which are
  13.276 +    *not* themselves (in)equalities, because the latter activate
  13.277 +    fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
  13.278 +    solver all the time rather than add the additional check. *)
  13.279      addSolver (mk_solver' "lin_arith"
  13.280 -      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
  13.281 -  Context.mapping
  13.282 -   (setup_options #>
  13.283 -    Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
  13.284 -    Method.setup @{binding linarith}
  13.285 -      (Args.bang_facts >> (fn prems => fn ctxt =>
  13.286 -        METHOD (fn facts =>
  13.287 -          HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
  13.288 -            THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
  13.289 -    Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
  13.290 -      "declaration of split rules for arithmetic procedure") I;
  13.291 +      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
  13.292 +
  13.293 +val global_setup =
  13.294 +  setup_split_limit #> setup_neq_limit #>
  13.295 +  Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
  13.296 +    "declaration of split rules for arithmetic procedure" #>
  13.297 +  Method.setup @{binding linarith}
  13.298 +    (Args.bang_facts >> (fn prems => fn ctxt =>
  13.299 +      METHOD (fn facts =>
  13.300 +        HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
  13.301 +          THEN' tac ctxt)))) "linear arithmetic" #>
  13.302 +  Arith_Data.add_tactic "linear arithmetic" gen_tac;
  13.303  
  13.304  end;
  13.305 -
  13.306 -structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
  13.307 -open Basic_Lin_Arith;
    14.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Tue May 05 17:09:18 2009 +0200
    14.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon May 11 19:51:21 2009 +0200
    14.3 @@ -516,7 +516,7 @@
    14.4        val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
    14.5        val pos = less $ zero $ t and neg = less $ t $ zero
    14.6        fun prove p =
    14.7 -        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
    14.8 +        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
    14.9          handle THM _ => NONE
   14.10      in case prove pos of
   14.11           SOME th => SOME(th RS pos_th)
    15.1 --- a/src/HOL/Tools/rat_arith.ML	Tue May 05 17:09:18 2009 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,46 +0,0 @@
    15.4 -(*  Title:      HOL/Real/rat_arith.ML
    15.5 -    Author:     Lawrence C Paulson
    15.6 -    Copyright   2004 University of Cambridge
    15.7 -
    15.8 -Simprocs for common factor cancellation & Rational coefficient handling
    15.9 -
   15.10 -Instantiation of the generic linear arithmetic package for type rat.
   15.11 -*)
   15.12 -
   15.13 -local
   15.14 -
   15.15 -val simps =
   15.16 - [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
   15.17 -  read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
   15.18 -  @{thm divide_1}, @{thm divide_zero_left},
   15.19 -  @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   15.20 -  @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   15.21 -  @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
   15.22 -  @{thm of_int_minus}, @{thm of_int_diff},
   15.23 -  @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
   15.24 -
   15.25 -val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
   15.26 -                    @{thm of_nat_eq_iff} RS iffD2]
   15.27 -(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
   15.28 -                    of_nat_less_iff RS iffD2 *)
   15.29 -
   15.30 -val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
   15.31 -                    @{thm of_int_eq_iff} RS iffD2]
   15.32 -(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
   15.33 -                    of_int_less_iff RS iffD2 *)
   15.34 -
   15.35 -in
   15.36 -
   15.37 -val rat_arith_setup =
   15.38 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   15.39 -   {add_mono_thms = add_mono_thms,
   15.40 -    mult_mono_thms = mult_mono_thms,
   15.41 -    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
   15.42 -    lessD = lessD,  (*Can't change lessD: the rats are dense!*)
   15.43 -    neqE =  neqE,
   15.44 -    simpset = simpset addsimps simps
   15.45 -                      addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
   15.46 -  Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
   15.47 -  Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})
   15.48 -
   15.49 -end;
    16.1 --- a/src/HOL/Tools/real_arith.ML	Tue May 05 17:09:18 2009 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,42 +0,0 @@
    16.4 -(*  Title:      HOL/Real/real_arith.ML
    16.5 -    ID:         $Id$
    16.6 -    Author:     Tobias Nipkow, TU Muenchen
    16.7 -    Copyright   1999 TU Muenchen
    16.8 -
    16.9 -Simprocs for common factor cancellation & Rational coefficient handling
   16.10 -
   16.11 -Instantiation of the generic linear arithmetic package for type real.
   16.12 -*)
   16.13 -
   16.14 -local
   16.15 -
   16.16 -val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
   16.17 -             @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
   16.18 -             @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
   16.19 -             @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
   16.20 -             @{thm real_of_nat_number_of}, @{thm real_number_of}]
   16.21 -
   16.22 -val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
   16.23 -                    @{thm real_of_nat_inject} RS iffD2]
   16.24 -(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
   16.25 -                    real_of_nat_less_iff RS iffD2 *)
   16.26 -
   16.27 -val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
   16.28 -                    @{thm real_of_int_inject} RS iffD2]
   16.29 -(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
   16.30 -                    real_of_int_less_iff RS iffD2 *)
   16.31 -
   16.32 -in
   16.33 -
   16.34 -val real_arith_setup =
   16.35 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   16.36 -   {add_mono_thms = add_mono_thms,
   16.37 -    mult_mono_thms = mult_mono_thms,
   16.38 -    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
   16.39 -    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
   16.40 -    neqE = neqE,
   16.41 -    simpset = simpset addsimps simps}) #>
   16.42 -  Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
   16.43 -  Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
   16.44 -
   16.45 -end;
    17.1 --- a/src/HOL/ex/Arith_Examples.thy	Tue May 05 17:09:18 2009 +0200
    17.2 +++ b/src/HOL/ex/Arith_Examples.thy	Mon May 11 19:51:21 2009 +0200
    17.3 @@ -13,18 +13,18 @@
    17.4    distribution.  This file merely contains some additional tests and special
    17.5    corner cases.  Some rather technical remarks:
    17.6  
    17.7 -  @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
    17.8 +  @{ML Lin_Arith.simple_tac} is a very basic version of the tactic.  It performs no
    17.9    meta-to-object-logic conversion, and only some splitting of operators.
   17.10 -  @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
   17.11 +  @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
   17.12    splitting of operators, and NNF normalization of the goal.  The @{text arith}
   17.13    method combines them both, and tries other methods (e.g.~@{text presburger})
   17.14    as well.  This is the one that you should use in your proofs!
   17.15  
   17.16    An @{text arith}-based simproc is available as well (see @{ML
   17.17 -  Lin_Arith.lin_arith_simproc}), which---for performance
   17.18 -  reasons---however does even less splitting than @{ML fast_arith_tac}
   17.19 +  Lin_Arith.simproc}), which---for performance
   17.20 +  reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
   17.21    at the moment (namely inequalities only).  (On the other hand, it
   17.22 -  does take apart conjunctions, which @{ML fast_arith_tac} currently
   17.23 +  does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
   17.24    does not do.)
   17.25  *}
   17.26  
   17.27 @@ -123,12 +123,12 @@
   17.28    (* FIXME: need to replace 1 by its numeral representation *)
   17.29    apply (subst numeral_1_eq_1 [symmetric])
   17.30    (* FIXME: arith does not know about iszero *)
   17.31 -  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
   17.32 +  apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
   17.33  oops
   17.34  
   17.35  lemma "(i::int) mod 42 <= 41"
   17.36    (* FIXME: arith does not know about iszero *)
   17.37 -  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
   17.38 +  apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
   17.39  oops
   17.40  
   17.41  lemma "-(i::int) * 1 = 0 ==> i = 0"
   17.42 @@ -208,13 +208,13 @@
   17.43  (*        preprocessing negates the goal and tries to compute its negation *)
   17.44  (*        normal form, which creates lots of separate cases for this       *)
   17.45  (*        disjunction of conjunctions                                      *)
   17.46 -(* by (tactic {* linear_arith_tac 1 *}) *)
   17.47 +(* by (tactic {* Lin_Arith.tac 1 *}) *)
   17.48  oops
   17.49  
   17.50  lemma "2 * (x::nat) ~= 1"
   17.51  (* FIXME: this is beyond the scope of the decision procedure at the moment, *)
   17.52  (*        because its negation is satisfiable in the rationals?             *)
   17.53 -(* by (tactic {* fast_arith_tac 1 *}) *)
   17.54 +(* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
   17.55  oops
   17.56  
   17.57  text {* Constants. *}
    18.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue May 05 17:09:18 2009 +0200
    18.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 11 19:51:21 2009 +0200
    18.3 @@ -56,7 +56,7 @@
    18.4  
    18.5    (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
    18.6    val pre_tac: Proof.context -> int -> tactic
    18.7 -  val number_of: int * typ -> term
    18.8 +  val mk_number: typ -> int -> term
    18.9  
   18.10    (*the limit on the number of ~= allowed; because each ~= is split
   18.11      into two cases, this can lead to an explosion*)
   18.12 @@ -86,6 +86,9 @@
   18.13  
   18.14  signature FAST_LIN_ARITH =
   18.15  sig
   18.16 +  val cut_lin_arith_tac: simpset -> int -> tactic
   18.17 +  val lin_arith_tac: Proof.context -> bool -> int -> tactic
   18.18 +  val lin_arith_simproc: simpset -> term -> thm option
   18.19    val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   18.20                   lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
   18.21                   -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   18.22 @@ -93,9 +96,6 @@
   18.23                  -> Context.generic -> Context.generic
   18.24    val trace: bool ref
   18.25    val warning_count: int ref;
   18.26 -  val cut_lin_arith_tac: simpset -> int -> tactic
   18.27 -  val lin_arith_tac: Proof.context -> bool -> int -> tactic
   18.28 -  val lin_arith_simproc: simpset -> term -> thm option
   18.29  end;
   18.30  
   18.31  functor Fast_Lin_Arith
   18.32 @@ -429,7 +429,7 @@
   18.33  
   18.34  (* FIXME OPTIMIZE!!!! (partly done already)
   18.35     Addition/Multiplication need i*t representation rather than t+t+...
   18.36 -   Get rid of Mulitplied(2). For Nat LA_Data.number_of should return Suc^n
   18.37 +   Get rid of Mulitplied(2). For Nat LA_Data.mk_number should return Suc^n
   18.38     because Numerals are not known early enough.
   18.39  
   18.40  Simplification may detect a contradiction 'prematurely' due to type
   18.41 @@ -480,7 +480,7 @@
   18.42                get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
   18.43              fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
   18.44              val cv = cvar(mth, hd(prems_of mth));
   18.45 -            val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv)))
   18.46 +            val ct = cterm_of thy (LA_Data.mk_number (#T (rep_cterm cv)) n)
   18.47          in instantiate ([],[(cv,ct)]) mth end
   18.48  
   18.49        fun simp thm =