tuned interface of Lin_Arith
authorhaftmann
Mon May 11 15:18:32 2009 +0200 (2009-05-11)
changeset 311006a2e67fe4488
parent 31092 27a6558e64b6
child 31101 26c7bb764a38
tuned interface of Lin_Arith
src/HOL/Int.thy
src/HOL/IsaMakefile
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/hypreal_arith.ML
src/HOL/Nat.thy
src/HOL/Nat_Numeral.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/rat_arith.ML
src/HOL/Tools/real_arith.ML
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/src/HOL/Int.thy	Mon May 11 11:53:21 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon May 11 15:18:32 2009 +0200
     1.3 @@ -1521,6 +1521,7 @@
     1.4  use "Tools/numeral_simprocs.ML"
     1.5  
     1.6  use "Tools/int_arith.ML"
     1.7 +setup {* Int_Arith.global_setup *}
     1.8  declaration {* K Int_Arith.setup *}
     1.9  
    1.10  setup {*
     2.1 --- a/src/HOL/IsaMakefile	Mon May 11 11:53:21 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon May 11 15:18:32 2009 +0200
     2.3 @@ -295,8 +295,6 @@
     2.4    Real.thy \
     2.5    RealVector.thy \
     2.6    Tools/float_syntax.ML \
     2.7 -  Tools/rat_arith.ML \
     2.8 -  Tools/real_arith.ML \
     2.9    Tools/Qelim/ferrante_rackoff_data.ML \
    2.10    Tools/Qelim/ferrante_rackoff.ML \
    2.11    Tools/Qelim/langford_data.ML \
    2.12 @@ -1051,7 +1049,6 @@
    2.13    NSA/HyperDef.thy \
    2.14    NSA/HyperNat.thy \
    2.15    NSA/Hyperreal.thy \
    2.16 -  NSA/hypreal_arith.ML \
    2.17    NSA/Filter.thy \
    2.18    NSA/NatStar.thy \
    2.19    NSA/NSA.thy \
     3.1 --- a/src/HOL/NSA/HyperDef.thy	Mon May 11 11:53:21 2009 +0200
     3.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon May 11 15:18:32 2009 +0200
     3.3 @@ -8,7 +8,6 @@
     3.4  
     3.5  theory HyperDef
     3.6  imports HyperNat Real
     3.7 -uses ("hypreal_arith.ML")
     3.8  begin
     3.9  
    3.10  types hypreal = "real star"
    3.11 @@ -343,8 +342,17 @@
    3.12  Addsimps [symmetric hypreal_diff_def]
    3.13  *)
    3.14  
    3.15 -use "hypreal_arith.ML"
    3.16 -declaration {* K hypreal_arith_setup *}
    3.17 +declaration {*
    3.18 +  K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
    3.19 +    @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
    3.20 +  #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
    3.21 +      @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
    3.22 +      @{thm star_of_diff}, @{thm star_of_mult}]
    3.23 +  #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
    3.24 +  #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
    3.25 +      "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    3.26 +      (K Lin_Arith.lin_arith_simproc)]))
    3.27 +*}
    3.28  
    3.29  
    3.30  subsection {* Exponentials on the Hyperreals *}
     4.1 --- a/src/HOL/NSA/hypreal_arith.ML	Mon May 11 11:53:21 2009 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,45 +0,0 @@
     4.4 -(*  Title:      HOL/NSA/hypreal_arith.ML
     4.5 -    Author:     Tobias Nipkow, TU Muenchen
     4.6 -    Copyright   1999 TU Muenchen
     4.7 -
     4.8 -Simprocs for common factor cancellation & Rational coefficient handling
     4.9 -
    4.10 -Instantiation of the generic linear arithmetic package for type hypreal.
    4.11 -*)
    4.12 -
    4.13 -local
    4.14 -
    4.15 -val simps = [thm "star_of_zero",
    4.16 -             thm "star_of_one",
    4.17 -             thm "star_of_number_of",
    4.18 -             thm "star_of_add",
    4.19 -             thm "star_of_minus",
    4.20 -             thm "star_of_diff",
    4.21 -             thm "star_of_mult"]
    4.22 -
    4.23 -val real_inj_thms = [thm "star_of_le" RS iffD2,
    4.24 -                     thm "star_of_less" RS iffD2,
    4.25 -                     thm "star_of_eq" RS iffD2]
    4.26 -
    4.27 -in
    4.28 -
    4.29 -val hyprealT = Type (@{type_name StarDef.star}, [HOLogic.realT]);
    4.30 -
    4.31 -val fast_hypreal_arith_simproc =
    4.32 -    Simplifier.simproc (the_context ())
    4.33 -      "fast_hypreal_arith" 
    4.34 -      ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    4.35 -    (K Lin_Arith.lin_arith_simproc);
    4.36 -
    4.37 -val hypreal_arith_setup =
    4.38 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    4.39 -   {add_mono_thms = add_mono_thms,
    4.40 -    mult_mono_thms = mult_mono_thms,
    4.41 -    inj_thms = real_inj_thms @ inj_thms,
    4.42 -    lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
    4.43 -    neqE = neqE,
    4.44 -    simpset = simpset addsimps simps}) #>
    4.45 -  Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, HOLogic.realT --> hyprealT) #>
    4.46 -  Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
    4.47 -
    4.48 -end;
     5.1 --- a/src/HOL/Nat.thy	Mon May 11 11:53:21 2009 +0200
     5.2 +++ b/src/HOL/Nat.thy	Mon May 11 15:18:32 2009 +0200
     5.3 @@ -1410,6 +1410,7 @@
     5.4  declaration {* K Nat_Arith.setup *}
     5.5  
     5.6  use "Tools/lin_arith.ML"
     5.7 +setup {* Lin_Arith.global_setup *}
     5.8  declaration {* K Lin_Arith.setup *}
     5.9  
    5.10  lemmas [arith_split] = nat_diff_split split_min split_max
     6.1 --- a/src/HOL/Nat_Numeral.thy	Mon May 11 11:53:21 2009 +0200
     6.2 +++ b/src/HOL/Nat_Numeral.thy	Mon May 11 15:18:32 2009 +0200
     6.3 @@ -874,33 +874,21 @@
     6.4  
     6.5  use "Tools/nat_numeral_simprocs.ML"
     6.6  
     6.7 -declaration {*
     6.8 -let
     6.9 -
    6.10 -val less_eq_rules = @{thms ring_distribs} @
    6.11 -  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
    6.12 -   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    6.13 -   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    6.14 -   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    6.15 -   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    6.16 -   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    6.17 -   @{thm mult_Suc}, @{thm mult_Suc_right},
    6.18 -   @{thm add_Suc}, @{thm add_Suc_right},
    6.19 -   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    6.20 -   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
    6.21 -
    6.22 -val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
    6.23 -
    6.24 -in
    6.25 -
    6.26 -K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    6.27 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    6.28 -    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    6.29 -    simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    6.30 -      addsimps less_eq_rules
    6.31 -      addsimprocs simprocs}))
    6.32 -
    6.33 -end
    6.34 +declaration {* 
    6.35 +  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    6.36 +  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
    6.37 +     @{thm nat_0}, @{thm nat_1},
    6.38 +     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    6.39 +     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    6.40 +     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    6.41 +     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    6.42 +     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    6.43 +     @{thm mult_Suc}, @{thm mult_Suc_right},
    6.44 +     @{thm add_Suc}, @{thm add_Suc_right},
    6.45 +     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    6.46 +     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
    6.47 +     @{thm if_True}, @{thm if_False}])
    6.48 +  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
    6.49  *}
    6.50  
    6.51  
     7.1 --- a/src/HOL/Rational.thy	Mon May 11 11:53:21 2009 +0200
     7.2 +++ b/src/HOL/Rational.thy	Mon May 11 15:18:32 2009 +0200
     7.3 @@ -6,7 +6,6 @@
     7.4  
     7.5  theory Rational
     7.6  imports GCD Archimedean_Field
     7.7 -uses ("Tools/rat_arith.ML")
     7.8  begin
     7.9  
    7.10  subsection {* Rational numbers as quotient *}
    7.11 @@ -582,10 +581,25 @@
    7.12    by (simp add: floor_unique)
    7.13  
    7.14  
    7.15 -subsection {* Arithmetic setup *}
    7.16 +subsection {* Linear arithmetic setup *}
    7.17  
    7.18 -use "Tools/rat_arith.ML"
    7.19 -declaration {* K rat_arith_setup *}
    7.20 +declaration {*
    7.21 +  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
    7.22 +    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
    7.23 +  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
    7.24 +    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
    7.25 +  #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
    7.26 +      @{thm True_implies_equals},
    7.27 +      read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
    7.28 +      @{thm divide_1}, @{thm divide_zero_left},
    7.29 +      @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    7.30 +      @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    7.31 +      @{thm of_int_minus}, @{thm of_int_diff},
    7.32 +      @{thm of_int_of_nat_eq}]
    7.33 +  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
    7.34 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
    7.35 +  #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
    7.36 +*}
    7.37  
    7.38  
    7.39  subsection {* Embedding from Rationals to other Fields *}
     8.1 --- a/src/HOL/RealDef.thy	Mon May 11 11:53:21 2009 +0200
     8.2 +++ b/src/HOL/RealDef.thy	Mon May 11 15:18:32 2009 +0200
     8.3 @@ -9,7 +9,6 @@
     8.4  
     8.5  theory RealDef
     8.6  imports PReal
     8.7 -uses ("Tools/real_arith.ML")
     8.8  begin
     8.9  
    8.10  definition
    8.11 @@ -960,10 +959,20 @@
    8.12          (if neg (number_of v :: int) then 0  
    8.13           else (number_of v :: real))"
    8.14  by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of)
    8.15 - 
    8.16  
    8.17 -use "Tools/real_arith.ML"
    8.18 -declaration {* K real_arith_setup *}
    8.19 +declaration {*
    8.20 +  K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
    8.21 +    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
    8.22 +  #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
    8.23 +    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
    8.24 +  #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
    8.25 +      @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
    8.26 +      @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
    8.27 +      @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
    8.28 +      @{thm real_of_nat_number_of}, @{thm real_number_of}]
    8.29 +  #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT)
    8.30 +  #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT))
    8.31 +*}
    8.32  
    8.33  
    8.34  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
     9.1 --- a/src/HOL/Tools/int_arith.ML	Mon May 11 11:53:21 2009 +0200
     9.2 +++ b/src/HOL/Tools/int_arith.ML	Mon May 11 15:18:32 2009 +0200
     9.3 @@ -5,8 +5,8 @@
     9.4  
     9.5  signature INT_ARITH =
     9.6  sig
     9.7 -  val fast_int_arith_simproc: simproc
     9.8    val setup: Context.generic -> Context.generic
     9.9 +  val global_setup: theory -> theory
    9.10  end
    9.11  
    9.12  structure Int_Arith : INT_ARITH =
    9.13 @@ -49,17 +49,15 @@
    9.14    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
    9.15    proc = proc1, identifier = []};
    9.16  
    9.17 -val allowed_consts =
    9.18 -  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
    9.19 -   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
    9.20 -   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
    9.21 -   @{const_name "HOL.less_eq"}];
    9.22 -
    9.23 -fun check t = case t of
    9.24 -   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
    9.25 -                else s mem_string allowed_consts
    9.26 - | a$b => check a andalso check b
    9.27 - | _ => false;
    9.28 +fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
    9.29 +  | check (Const (@{const_name "HOL.one"}, _)) = true
    9.30 +  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
    9.31 +      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
    9.32 +      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
    9.33 +      @{const_name "HOL.zero"},
    9.34 +      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
    9.35 +  | check (a $ b) = check a andalso check b
    9.36 +  | check _ = false;
    9.37  
    9.38  val conv =
    9.39    Simplifier.rewrite
    9.40 @@ -80,35 +78,24 @@
    9.41    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    9.42    proc = sproc, identifier = []}
    9.43  
    9.44 -val add_rules =
    9.45 -    simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
    9.46 -    @{thms int_arith_rules}
    9.47 -
    9.48 -val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    9.49 -
    9.50 -val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
    9.51 -  :: Numeral_Simprocs.combine_numerals
    9.52 -  :: Numeral_Simprocs.cancel_numerals;
    9.53 -
    9.54 -val setup =
    9.55 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    9.56 -   {add_mono_thms = add_mono_thms,
    9.57 -    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
    9.58 -    inj_thms = nat_inj_thms @ inj_thms,
    9.59 -    lessD = lessD @ [@{thm zless_imp_add1_zle}],
    9.60 -    neqE = neqE,
    9.61 -    simpset = simpset addsimps add_rules
    9.62 -                      addsimprocs numeral_base_simprocs}) #>
    9.63 -  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
    9.64 -  Lin_Arith.add_discrete_type @{type_name Int.int}
    9.65 -
    9.66  val fast_int_arith_simproc =
    9.67 -  Simplifier.simproc (the_context ())
    9.68 -  "fast_int_arith" 
    9.69 +  Simplifier.simproc @{theory} "fast_int_arith"
    9.70       ["(m::'a::{ordered_idom,number_ring}) < n",
    9.71        "(m::'a::{ordered_idom,number_ring}) <= n",
    9.72        "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
    9.73  
    9.74 -end;
    9.75 +val global_setup = Simplifier.map_simpset
    9.76 +  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
    9.77  
    9.78 -Addsimprocs [Int_Arith.fast_int_arith_simproc];
    9.79 +val setup =
    9.80 +  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    9.81 +  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    9.82 +  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
    9.83 +      @ @{thms arith_special} @ @{thms int_arith_rules})
    9.84 +  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
    9.85 +      :: Numeral_Simprocs.combine_numerals
    9.86 +      :: Numeral_Simprocs.cancel_numerals)
    9.87 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
    9.88 +  #> Lin_Arith.add_discrete_type @{type_name Int.int}
    9.89 +
    9.90 +end;
    10.1 --- a/src/HOL/Tools/lin_arith.ML	Mon May 11 11:53:21 2009 +0200
    10.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon May 11 15:18:32 2009 +0200
    10.3 @@ -6,27 +6,25 @@
    10.4  
    10.5  signature BASIC_LIN_ARITH =
    10.6  sig
    10.7 -  val arith_split_add: attribute
    10.8 -  val lin_arith_pre_tac: Proof.context -> int -> tactic
    10.9 +  val lin_arith_simproc: simpset -> term -> thm option
   10.10 +  val fast_nat_arith_simproc: simproc
   10.11    val fast_arith_tac: Proof.context -> int -> tactic
   10.12    val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
   10.13 -  val lin_arith_simproc: simpset -> term -> thm option
   10.14 -  val fast_nat_arith_simproc: simproc
   10.15    val linear_arith_tac: Proof.context -> int -> tactic
   10.16  end;
   10.17  
   10.18  signature LIN_ARITH =
   10.19  sig
   10.20    include BASIC_LIN_ARITH
   10.21 -  val add_discrete_type: string -> Context.generic -> Context.generic
   10.22 +  val pre_tac: Proof.context -> int -> tactic
   10.23 +  val add_inj_thms: thm list -> Context.generic -> Context.generic
   10.24 +  val add_lessD: thm -> Context.generic -> Context.generic
   10.25 +  val add_simps: thm list -> Context.generic -> Context.generic
   10.26 +  val add_simprocs: simproc list -> Context.generic -> Context.generic
   10.27    val add_inj_const: string * typ -> Context.generic -> Context.generic
   10.28 -  val map_data:
   10.29 -    ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   10.30 -      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} ->
   10.31 -     {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   10.32 -      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ->
   10.33 -    Context.generic -> Context.generic
   10.34 +  val add_discrete_type: string -> Context.generic -> Context.generic
   10.35    val setup: Context.generic -> Context.generic
   10.36 +  val global_setup: theory -> theory
   10.37    val split_limit: int Config.T
   10.38    val neq_limit: int Config.T
   10.39    val warning_count: int ref
   10.40 @@ -47,37 +45,38 @@
   10.41  val sym = sym;
   10.42  val not_lessD = @{thm linorder_not_less} RS iffD1;
   10.43  val not_leD = @{thm linorder_not_le} RS iffD1;
   10.44 -val le0 = thm "le0";
   10.45  
   10.46 -fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   10.47 +fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI;
   10.48  
   10.49  val mk_Trueprop = HOLogic.mk_Trueprop;
   10.50  
   10.51  fun atomize thm = case Thm.prop_of thm of
   10.52 -    Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
   10.53 -    atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
   10.54 +    Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
   10.55 +    atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   10.56    | _ => [thm];
   10.57  
   10.58 -fun neg_prop ((TP as Const("Trueprop",_)) $ (Const("Not",_) $ t)) = TP $ t
   10.59 -  | neg_prop ((TP as Const("Trueprop",_)) $ t) = TP $ (HOLogic.Not $t)
   10.60 +fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
   10.61 +  | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
   10.62    | neg_prop t = raise TERM ("neg_prop", [t]);
   10.63  
   10.64  fun is_False thm =
   10.65    let val _ $ t = Thm.prop_of thm
   10.66 -  in t = Const("False",HOLogic.boolT) end;
   10.67 +  in t = HOLogic.false_const end;
   10.68  
   10.69  fun is_nat t = (fastype_of1 t = HOLogic.natT);
   10.70  
   10.71 -fun mk_nat_thm sg t =
   10.72 -  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   10.73 -  in instantiate ([],[(cn,ct)]) le0 end;
   10.74 +fun mk_nat_thm thy t =
   10.75 +  let
   10.76 +    val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
   10.77 +    and ct = cterm_of thy t
   10.78 +  in instantiate ([], [(cn, ct)]) @{thm le0} end;
   10.79  
   10.80  end;
   10.81  
   10.82  
   10.83  (* arith context data *)
   10.84  
   10.85 -structure ArithContextData = GenericDataFun
   10.86 +structure Lin_Arith_Data = GenericDataFun
   10.87  (
   10.88    type T = {splits: thm list,
   10.89              inj_consts: (string * typ) list,
   10.90 @@ -92,27 +91,25 @@
   10.91      discrete = Library.merge (op =) (discrete1, discrete2)};
   10.92  );
   10.93  
   10.94 -val get_arith_data = ArithContextData.get o Context.Proof;
   10.95 +val get_arith_data = Lin_Arith_Data.get o Context.Proof;
   10.96  
   10.97 -val arith_split_add = Thm.declaration_attribute (fn thm =>
   10.98 -  ArithContextData.map (fn {splits, inj_consts, discrete} =>
   10.99 -    {splits = update Thm.eq_thm_prop thm splits,
  10.100 -     inj_consts = inj_consts, discrete = discrete}));
  10.101 +fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
  10.102 +  {splits = update Thm.eq_thm_prop thm splits,
  10.103 +   inj_consts = inj_consts, discrete = discrete});
  10.104  
  10.105 -fun add_discrete_type d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
  10.106 +fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
  10.107    {splits = splits, inj_consts = inj_consts,
  10.108     discrete = update (op =) d discrete});
  10.109  
  10.110 -fun add_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
  10.111 +fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
  10.112    {splits = splits, inj_consts = update (op =) c inj_consts,
  10.113     discrete = discrete});
  10.114  
  10.115 -val (split_limit, setup1) = Attrib.config_int "linarith_split_limit" 9;
  10.116 -val (neq_limit, setup2) = Attrib.config_int "linarith_neq_limit" 9;
  10.117 -val setup_options = setup1 #> setup2;
  10.118 +val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
  10.119 +val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
  10.120  
  10.121  
  10.122 -structure LA_Data_Ref =
  10.123 +structure LA_Data =
  10.124  struct
  10.125  
  10.126  val fast_arith_neq_limit = neq_limit;
  10.127 @@ -756,15 +753,32 @@
  10.128    )
  10.129  end;
  10.130  
  10.131 -end;  (* LA_Data_Ref *)
  10.132 +end;  (* LA_Data *)
  10.133  
  10.134  
  10.135 -val lin_arith_pre_tac = LA_Data_Ref.pre_tac;
  10.136 +val pre_tac = LA_Data.pre_tac;
  10.137  
  10.138 -structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data_Ref);
  10.139 +structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
  10.140  
  10.141  val map_data = Fast_Arith.map_data;
  10.142  
  10.143 +fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
  10.144 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
  10.145 +    lessD = lessD, neqE = neqE, simpset = simpset};
  10.146 +
  10.147 +fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
  10.148 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
  10.149 +    lessD = f lessD, neqE = neqE, simpset = simpset};
  10.150 +
  10.151 +fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
  10.152 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
  10.153 +    lessD = lessD, neqE = neqE, simpset = f simpset};
  10.154 +
  10.155 +fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
  10.156 +fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
  10.157 +fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
  10.158 +fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
  10.159 +
  10.160  fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
  10.161  val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
  10.162  val trace = Fast_Arith.trace;
  10.163 @@ -774,7 +788,7 @@
  10.164     Most of the work is done by the cancel tactics. *)
  10.165  
  10.166  val init_arith_data =
  10.167 - map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
  10.168 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
  10.169     {add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
  10.170      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
  10.171      inj_thms = inj_thms,
  10.172 @@ -891,17 +905,18 @@
  10.173    init_arith_data #>
  10.174    Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
  10.175      addSolver (mk_solver' "lin_arith"
  10.176 -      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
  10.177 -  Context.mapping
  10.178 -   (setup_options #>
  10.179 -    Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
  10.180 -    Method.setup @{binding linarith}
  10.181 -      (Args.bang_facts >> (fn prems => fn ctxt =>
  10.182 -        METHOD (fn facts =>
  10.183 -          HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
  10.184 -            THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
  10.185 -    Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
  10.186 -      "declaration of split rules for arithmetic procedure") I;
  10.187 +      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
  10.188 +
  10.189 +val global_setup =
  10.190 +  setup_split_limit #> setup_neq_limit #>
  10.191 +  Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
  10.192 +    "declaration of split rules for arithmetic procedure" #>
  10.193 +  Method.setup @{binding linarith}
  10.194 +    (Args.bang_facts >> (fn prems => fn ctxt =>
  10.195 +      METHOD (fn facts =>
  10.196 +        HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
  10.197 +          THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
  10.198 +  Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac;
  10.199  
  10.200  end;
  10.201  
    11.1 --- a/src/HOL/Tools/rat_arith.ML	Mon May 11 11:53:21 2009 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,46 +0,0 @@
    11.4 -(*  Title:      HOL/Real/rat_arith.ML
    11.5 -    Author:     Lawrence C Paulson
    11.6 -    Copyright   2004 University of Cambridge
    11.7 -
    11.8 -Simprocs for common factor cancellation & Rational coefficient handling
    11.9 -
   11.10 -Instantiation of the generic linear arithmetic package for type rat.
   11.11 -*)
   11.12 -
   11.13 -local
   11.14 -
   11.15 -val simps =
   11.16 - [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
   11.17 -  read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
   11.18 -  @{thm divide_1}, @{thm divide_zero_left},
   11.19 -  @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   11.20 -  @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   11.21 -  @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
   11.22 -  @{thm of_int_minus}, @{thm of_int_diff},
   11.23 -  @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
   11.24 -
   11.25 -val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
   11.26 -                    @{thm of_nat_eq_iff} RS iffD2]
   11.27 -(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
   11.28 -                    of_nat_less_iff RS iffD2 *)
   11.29 -
   11.30 -val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
   11.31 -                    @{thm of_int_eq_iff} RS iffD2]
   11.32 -(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
   11.33 -                    of_int_less_iff RS iffD2 *)
   11.34 -
   11.35 -in
   11.36 -
   11.37 -val rat_arith_setup =
   11.38 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   11.39 -   {add_mono_thms = add_mono_thms,
   11.40 -    mult_mono_thms = mult_mono_thms,
   11.41 -    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
   11.42 -    lessD = lessD,  (*Can't change lessD: the rats are dense!*)
   11.43 -    neqE =  neqE,
   11.44 -    simpset = simpset addsimps simps
   11.45 -                      addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
   11.46 -  Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
   11.47 -  Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})
   11.48 -
   11.49 -end;
    12.1 --- a/src/HOL/Tools/real_arith.ML	Mon May 11 11:53:21 2009 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,42 +0,0 @@
    12.4 -(*  Title:      HOL/Real/real_arith.ML
    12.5 -    ID:         $Id$
    12.6 -    Author:     Tobias Nipkow, TU Muenchen
    12.7 -    Copyright   1999 TU Muenchen
    12.8 -
    12.9 -Simprocs for common factor cancellation & Rational coefficient handling
   12.10 -
   12.11 -Instantiation of the generic linear arithmetic package for type real.
   12.12 -*)
   12.13 -
   12.14 -local
   12.15 -
   12.16 -val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
   12.17 -             @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
   12.18 -             @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
   12.19 -             @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
   12.20 -             @{thm real_of_nat_number_of}, @{thm real_number_of}]
   12.21 -
   12.22 -val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
   12.23 -                    @{thm real_of_nat_inject} RS iffD2]
   12.24 -(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
   12.25 -                    real_of_nat_less_iff RS iffD2 *)
   12.26 -
   12.27 -val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
   12.28 -                    @{thm real_of_int_inject} RS iffD2]
   12.29 -(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
   12.30 -                    real_of_int_less_iff RS iffD2 *)
   12.31 -
   12.32 -in
   12.33 -
   12.34 -val real_arith_setup =
   12.35 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   12.36 -   {add_mono_thms = add_mono_thms,
   12.37 -    mult_mono_thms = mult_mono_thms,
   12.38 -    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
   12.39 -    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
   12.40 -    neqE = neqE,
   12.41 -    simpset = simpset addsimps simps}) #>
   12.42 -  Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
   12.43 -  Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
   12.44 -
   12.45 -end;
    13.1 --- a/src/HOL/ex/Arith_Examples.thy	Mon May 11 11:53:21 2009 +0200
    13.2 +++ b/src/HOL/ex/Arith_Examples.thy	Mon May 11 15:18:32 2009 +0200
    13.3 @@ -123,12 +123,12 @@
    13.4    (* FIXME: need to replace 1 by its numeral representation *)
    13.5    apply (subst numeral_1_eq_1 [symmetric])
    13.6    (* FIXME: arith does not know about iszero *)
    13.7 -  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
    13.8 +  apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
    13.9  oops
   13.10  
   13.11  lemma "(i::int) mod 42 <= 41"
   13.12    (* FIXME: arith does not know about iszero *)
   13.13 -  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
   13.14 +  apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
   13.15  oops
   13.16  
   13.17  lemma "-(i::int) * 1 = 0 ==> i = 0"