streamlined setup of linear arithmetic
authorhaftmann
Mon Nov 04 20:10:06 2013 +0100 (2013-11-04)
changeset 54249ce00f2fef556
parent 54248 c7af3d651658
child 54250 7d2544dd3988
streamlined setup of linear arithmetic
src/HOL/Int.thy
src/HOL/Num.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Power.thy
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/semiring_normalizer.ML
     1.1 --- a/src/HOL/Int.thy	Mon Nov 04 18:08:47 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Nov 04 20:10:06 2013 +0100
     1.3 @@ -424,6 +424,11 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma diff_nat_numeral [simp]: 
     1.8 +  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
     1.9 +  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    1.10 +
    1.11 +
    1.12  text {* For termination proofs: *}
    1.13  lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
    1.14  
    1.15 @@ -747,14 +752,11 @@
    1.16  
    1.17  subsection {* Setting up simplification procedures *}
    1.18  
    1.19 +lemmas of_int_simps =
    1.20 +  of_int_0 of_int_1 of_int_add of_int_mult
    1.21 +
    1.22  lemmas int_arith_rules =
    1.23 -  neg_le_iff_le numeral_One
    1.24 -  minus_zero left_minus right_minus
    1.25 -  mult_zero_left mult_zero_right mult_1_left mult_1_right
    1.26 -  mult_minus_left mult_minus_right
    1.27 -  minus_add_distrib minus_minus mult_assoc
    1.28 -  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.29 -  of_int_0 of_int_1 of_int_add of_int_mult
    1.30 +  numeral_One more_arith_simps of_nat_simps of_int_simps
    1.31  
    1.32  ML_file "Tools/int_arith.ML"
    1.33  declaration {* K Int_Arith.setup *}
    1.34 @@ -875,16 +877,10 @@
    1.35                if d < 0 then 0 else nat d)"
    1.36  by (simp add: Let_def nat_diff_distrib [symmetric])
    1.37  
    1.38 -lemma diff_nat_numeral [simp]: 
    1.39 -  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    1.40 -  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    1.41 -
    1.42  lemma nat_numeral_diff_1 [simp]:
    1.43    "numeral v - (1::nat) = nat (numeral v - 1)"
    1.44    using diff_nat_numeral [of v Num.One] by simp
    1.45  
    1.46 -lemmas nat_arith = diff_nat_numeral
    1.47 -
    1.48  
    1.49  subsection "Induction principles for int"
    1.50  
     2.1 --- a/src/HOL/Num.thy	Mon Nov 04 18:08:47 2013 +0100
     2.2 +++ b/src/HOL/Num.thy	Mon Nov 04 20:10:06 2013 +0100
     2.3 @@ -1072,6 +1072,16 @@
     2.4    BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps
     2.5    abs_zero abs_one arith_extra_simps
     2.6  
     2.7 +lemmas more_arith_simps =
     2.8 +  neg_le_iff_le
     2.9 +  minus_zero left_minus right_minus
    2.10 +  mult_1_left mult_1_right
    2.11 +  mult_minus_left mult_minus_right
    2.12 +  minus_add_distrib minus_minus mult_assoc
    2.13 +
    2.14 +lemmas of_nat_simps =
    2.15 +  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    2.16 +
    2.17  text {* Simplification of relational operations *}
    2.18  
    2.19  lemmas eq_numeral_extra =
    2.20 @@ -1083,6 +1093,38 @@
    2.21    less_numeral_simps less_neg_numeral_simps less_numeral_extra
    2.22    eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
    2.23  
    2.24 +lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
    2.25 +  -- {* Unfold all @{text let}s involving constants *}
    2.26 +  unfolding Let_def ..
    2.27 +
    2.28 +lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
    2.29 +  -- {* Unfold all @{text let}s involving constants *}
    2.30 +  unfolding Let_def ..
    2.31 +
    2.32 +declaration {*
    2.33 +let 
    2.34 +  fun number_of thy T n =
    2.35 +    if not (Sign.of_sort thy (T, @{sort numeral}))
    2.36 +    then raise CTERM ("number_of", [])
    2.37 +    else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
    2.38 +in
    2.39 +  K (
    2.40 +    Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}
    2.41 +      @ @{thms rel_simps}
    2.42 +      @ @{thms pred_numeral_simps}
    2.43 +      @ @{thms arith_special numeral_One}
    2.44 +      @ @{thms of_nat_simps})
    2.45 +    #> Lin_Arith.add_simps [@{thm Suc_numeral},
    2.46 +      @{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
    2.47 +      @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
    2.48 +      @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
    2.49 +      @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
    2.50 +      @{thm mult_Suc}, @{thm mult_Suc_right},
    2.51 +      @{thm of_nat_numeral}]
    2.52 +    #> Lin_Arith.set_number_of number_of)
    2.53 +end
    2.54 +*}
    2.55 +
    2.56  
    2.57  subsubsection {* Simplification of arithmetic when nested to the right. *}
    2.58  
    2.59 @@ -1113,4 +1155,3 @@
    2.60  
    2.61  end
    2.62  
    2.63 -
     3.1 --- a/src/HOL/Numeral_Simprocs.thy	Mon Nov 04 18:08:47 2013 +0100
     3.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Nov 04 20:10:06 2013 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  ML_file "~~/src/Provers/Arith/extract_common_term.ML"
     3.5  
     3.6  lemmas semiring_norm =
     3.7 -  Let_def arith_simps nat_arith rel_simps
     3.8 +  Let_def arith_simps diff_nat_numeral rel_simps
     3.9    if_False if_True
    3.10    add_0 add_Suc add_numeral_left
    3.11    add_neg_numeral_left mult_numeral_left
    3.12 @@ -278,27 +278,8 @@
    3.13    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
    3.14    {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
    3.15  
    3.16 -(* FIXME: duplicate rule warnings for:
    3.17 -  ring_distribs
    3.18 -  numeral_plus_numeral numeral_times_numeral
    3.19 -  numeral_eq_iff numeral_less_iff numeral_le_iff
    3.20 -  numeral_neq_zero zero_neq_numeral zero_less_numeral
    3.21 -  if_True if_False *)
    3.22  declaration {* 
    3.23 -  K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}])
    3.24 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
    3.25 -     @{thm nat_0}, @{thm nat_1},
    3.26 -     @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral},
    3.27 -     @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff},
    3.28 -     @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
    3.29 -     @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
    3.30 -     @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
    3.31 -     @{thm mult_Suc}, @{thm mult_Suc_right},
    3.32 -     @{thm add_Suc}, @{thm add_Suc_right},
    3.33 -     @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral},
    3.34 -     @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral},
    3.35 -     @{thm if_True}, @{thm if_False}])
    3.36 -  #> Lin_Arith.add_simprocs
    3.37 +  K (Lin_Arith.add_simprocs
    3.38        [@{simproc semiring_assoc_fold},
    3.39         @{simproc int_combine_numerals},
    3.40         @{simproc inteq_cancel_numerals},
     4.1 --- a/src/HOL/Power.thy	Mon Nov 04 18:08:47 2013 +0100
     4.2 +++ b/src/HOL/Power.thy	Mon Nov 04 20:10:06 2013 +0100
     4.3 @@ -730,8 +730,18 @@
     4.4    fixes m n :: nat
     4.5    assumes "m\<^sup>2 \<le> n"
     4.6    shows "m \<le> n"
     4.7 -  using assms by (cases m) (simp_all add: power2_eq_square)
     4.8 -
     4.9 +proof (cases m)
    4.10 +  case 0 then show ?thesis by simp
    4.11 +next
    4.12 +  case (Suc k)
    4.13 +  show ?thesis
    4.14 +  proof (rule ccontr)
    4.15 +    assume "\<not> m \<le> n"
    4.16 +    then have "n < m" by simp
    4.17 +    with assms Suc show False
    4.18 +      by (auto simp add: algebra_simps) (simp add: power2_eq_square)
    4.19 +  qed
    4.20 +qed
    4.21  
    4.22  
    4.23  subsection {* Code generator tweak *}
     5.1 --- a/src/HOL/Tools/int_arith.ML	Mon Nov 04 18:08:47 2013 +0100
     5.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Nov 04 20:10:06 2013 +0100
     5.3 @@ -87,9 +87,9 @@
     5.4  val setup =
     5.5    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
     5.6    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
     5.7 -  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
     5.8 -      @ @{thms pred_numeral_simps}
     5.9 -      @ @{thms arith_special} @ @{thms int_arith_rules})
    5.10 +  #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
    5.11 +  #> Lin_Arith.add_simps
    5.12 +      [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}]
    5.13    #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    5.14    #> Lin_Arith.set_number_of number_of
    5.15    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
     6.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Nov 04 18:08:47 2013 +0100
     6.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Nov 04 20:10:06 2013 +0100
     6.3 @@ -791,37 +791,16 @@
     6.4     Most of the work is done by the cancel tactics. *)
     6.5  
     6.6  val init_arith_data =
     6.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
     6.8 -   {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @
     6.9 -      @{thms add_mono_thms_linordered_field} @ add_mono_thms,
    6.10 -    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
    6.11 -      @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
    6.12 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, number_of, ...} =>
    6.13 +   {add_mono_thms = @{thms add_mono_thms_linordered_semiring}
    6.14 +      @ @{thms add_mono_thms_linordered_field} @ add_mono_thms,
    6.15 +    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono}
    6.16 +      :: @{lemma "a = b ==> c * a = c * b" by (rule arg_cong)} :: mult_mono_thms,
    6.17      inj_thms = inj_thms,
    6.18 -    lessD = lessD @ [@{thm "Suc_leI"}],
    6.19 -    neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_linordered_idom}],
    6.20 -    simpset =
    6.21 -      put_simpset HOL_basic_ss @{context}
    6.22 -      addsimps @{thms ring_distribs}
    6.23 -      addsimps [@{thm if_True}, @{thm if_False}]
    6.24 -      addsimps
    6.25 -       [@{thm add_0_left}, @{thm add_0_right},
    6.26 -        @{thm add_Suc}, @{thm add_Suc_right},
    6.27 -        @{thm nat.inject}, @{thm Suc_le_mono}, @{thm Suc_less_eq},
    6.28 -        @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
    6.29 -        @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
    6.30 -        @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
    6.31 -        @{thm "not_one_less_zero"}]
    6.32 -      addsimprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
    6.33 -                   @{simproc group_cancel_eq}, @{simproc group_cancel_le},
    6.34 -                   @{simproc group_cancel_less}]
    6.35 -       (*abel_cancel helps it work in abstract algebraic domains*)
    6.36 -      addsimprocs [@{simproc nateq_cancel_sums},
    6.37 -                   @{simproc natless_cancel_sums},
    6.38 -                   @{simproc natle_cancel_sums}]
    6.39 -      |> Simplifier.add_cong @{thm if_weak_cong}
    6.40 -      |> simpset_of,
    6.41 -    number_of = number_of}) #>
    6.42 -  add_discrete_type @{type_name nat};
    6.43 +    lessD = lessD,
    6.44 +    neqE = @{thm linorder_neqE_nat} :: @{thm linorder_neqE_linordered_idom} :: neqE,
    6.45 +    simpset = put_simpset HOL_basic_ss @{context} |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of,
    6.46 +    number_of = number_of});
    6.47  
    6.48  (* FIXME !?? *)
    6.49  fun add_arith_facts ctxt =
    6.50 @@ -909,9 +888,6 @@
    6.51  
    6.52  (* context setup *)
    6.53  
    6.54 -val setup =
    6.55 -  init_arith_data;
    6.56 -
    6.57  val global_setup =
    6.58    map_theory_simpset (fn ctxt => ctxt
    6.59      addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
    6.60 @@ -924,4 +900,22 @@
    6.61            THEN' tac ctxt)))) "linear arithmetic" #>
    6.62    Arith_Data.add_tactic "linear arithmetic" gen_tac;
    6.63  
    6.64 +val setup =
    6.65 +  init_arith_data
    6.66 +  #> add_discrete_type @{type_name nat}
    6.67 +  #> add_lessD @{thm Suc_leI}
    6.68 +  #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
    6.69 +      @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
    6.70 +      @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
    6.71 +      @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
    6.72 +  #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
    6.73 +      @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
    6.74 +      @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}]
    6.75 +  #> add_simprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
    6.76 +      @{simproc group_cancel_eq}, @{simproc group_cancel_le},
    6.77 +      @{simproc group_cancel_less}]
    6.78 +     (*abel_cancel helps it work in abstract algebraic domains*)
    6.79 +  #> add_simprocs [@{simproc nateq_cancel_sums},@{simproc natless_cancel_sums},
    6.80 +      @{simproc natle_cancel_sums}];
    6.81 +
    6.82  end;
     7.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Nov 04 18:08:47 2013 +0100
     7.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Nov 04 20:10:06 2013 +0100
     7.3 @@ -848,7 +848,7 @@
     7.4  val nat_exp_ss =
     7.5    simpset_of
     7.6     (put_simpset HOL_basic_ss @{context}
     7.7 -    addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
     7.8 +    addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
     7.9      addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
    7.10  
    7.11  fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;