# HG changeset patch # User krauss # Date 1333311299 -7200 # Node ID 3b9eeb4a2967982b91b5e48aeec6d34ec5425b15 # Parent 2d4ea84278da5e28432ce2be8e57df9c7cd8e811# Parent aabdd7765b647ffc6c845c1a116d33a91567f596 merged diff -r 2d4ea84278da -r 3b9eeb4a2967 Admin/mira.py --- a/Admin/mira.py Sun Apr 01 22:03:45 2012 +0200 +++ b/Admin/mira.py Sun Apr 01 22:14:59 2012 +0200 @@ -59,7 +59,7 @@ ISABELLE_USEDIR_OPTIONS="%s" -[[ -z "$ISABELLE_JDK_HOME" ]] && ISABELLE_JDK_HOME="$ISABELLE_HOME/contrib/jdk" +ISABELLE_JDK_HOME="$JAVA_HOME" Z3_NON_COMMERCIAL="yes" %s diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Code_Numeral.thy Sun Apr 01 22:14:59 2012 +0200 @@ -3,7 +3,7 @@ header {* Type of target language numerals *} theory Code_Numeral -imports Nat_Numeral Nat_Transfer Divides +imports Nat_Transfer Divides begin text {* diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Divides.thy Sun Apr 01 22:14:59 2012 +0200 @@ -6,7 +6,7 @@ header {* The division operators div and mod *} theory Divides -imports Nat_Numeral Nat_Transfer +imports Nat_Transfer uses "~~/src/Provers/Arith/cancel_div_mod.ML" begin diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Int.thy Sun Apr 01 22:14:59 2012 +0200 @@ -990,6 +990,8 @@ "numeral v - (1::nat) = nat (numeral v - 1)" using diff_nat_numeral [of v Num.One] by simp +lemmas nat_arith = diff_nat_numeral + subsection "Induction principles for int" @@ -1756,6 +1758,8 @@ lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int] lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric] +lemmas zpower_numeral_even = power_numeral_even [where 'a=int] +lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int] lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)" diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/IsaMakefile Sun Apr 01 22:14:59 2012 +0200 @@ -284,7 +284,6 @@ List.thy \ Main.thy \ Map.thy \ - Nat_Numeral.thy \ Nat_Transfer.thy \ New_DSequence.thy \ New_Random_Sequence.thy \ diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Nat.thy Sun Apr 01 22:14:59 2012 +0200 @@ -1112,6 +1112,24 @@ -- {* elimination of @{text -} on @{text nat} in assumptions *} by (auto split: nat_diff_split) +lemma Suc_pred': "0 < n ==> n = Suc(n - 1)" + by simp + +lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))" + unfolding One_nat_def by (cases m) simp_all + +lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))" + unfolding One_nat_def by (cases m) simp_all + +lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - 1)" + unfolding One_nat_def by (cases n) simp_all + +lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" + unfolding One_nat_def by (cases m) simp_all + +lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" + by (fact Let_def) + subsubsection {* Monotonicity of Multiplication *} diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Sun Apr 01 22:03:45 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ -(* Title: HOL/Nat_Numeral.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge -*) - -header {* Binary numerals for the natural numbers *} - -theory Nat_Numeral -imports Int -begin - -subsection{*Comparisons*} - -text{*Simprules for comparisons where common factors can be cancelled.*} -lemmas zero_compare_simps = - add_strict_increasing add_strict_increasing2 add_increasing - zero_le_mult_iff zero_le_divide_iff - zero_less_mult_iff zero_less_divide_iff - mult_le_0_iff divide_le_0_iff - mult_less_0_iff divide_less_0_iff - zero_le_power2 power2_less_0 - -subsubsection{*Nat *} - -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)" -by simp - -(*Expresses a natural number constant as the Suc of another one. - NOT suitable for rewriting because n recurs on the right-hand side.*) -lemmas expand_Suc = Suc_pred' [of "numeral v", OF zero_less_numeral] for v - -subsubsection{*Arith *} - -(* These two can be useful when m = numeral... *) - -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))" - unfolding One_nat_def by (cases m) simp_all - -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))" - unfolding One_nat_def by (cases m) simp_all - -lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))" - unfolding One_nat_def by (cases m) simp_all - - -subsection{*Literal arithmetic involving powers*} - -text{*For arbitrary rings*} - -lemma power_numeral_even: - fixes z :: "'a::monoid_mult" - shows "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" - unfolding numeral_Bit0 power_add Let_def .. - -lemma power_numeral_odd: - fixes z :: "'a::monoid_mult" - shows "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" - unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right - unfolding power_Suc power_add Let_def mult_assoc .. - -lemmas zpower_numeral_even = power_numeral_even [where 'a=int] -lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int] - -lemmas nat_arith = - diff_nat_numeral - -lemmas semiring_norm = - Let_def arith_simps nat_arith rel_simps - if_False if_True - add_0 add_Suc add_numeral_left - add_neg_numeral_left mult_numeral_left - numeral_1_eq_1 [symmetric] Suc_eq_plus1 - eq_numeral_iff_iszero not_iszero_Numeral1 - -lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" - by (fact Let_def) - - -subsection{*Literal arithmetic and @{term of_nat}*} - -lemma of_nat_double: - "0 \ x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)" -by (simp only: mult_2 nat_add_distrib of_nat_add) - - -subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} - -text{*Where K above is a literal*} - -lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)" -by (simp split: nat_diff_split) - -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" -by (simp split: nat_diff_split) - - -subsubsection{*Various Other Lemmas*} - -text {*Evens and Odds, for Mutilated Chess Board*} - -text{*Case analysis on @{term "n<2"}*} -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" -by (auto simp add: numeral_2_eq_2) - -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} - -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" -by simp - -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" -by simp - -text{*Can be used to eliminate long strings of Sucs, but not by default*} -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" -by simp - -text{*Legacy theorems*} - -lemmas nat_1_add_1 = one_add_one [where 'a=nat] - -end diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Nat_Transfer.thy --- a/src/HOL/Nat_Transfer.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Nat_Transfer.thy Sun Apr 01 22:14:59 2012 +0200 @@ -4,7 +4,7 @@ header {* Generic transfer machinery; specific transfer from nats to ints and back. *} theory Nat_Transfer -imports Nat_Numeral +imports Int uses ("Tools/transfer.ML") begin diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Num.thy --- a/src/HOL/Num.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Num.thy Sun Apr 01 22:14:59 2012 +0200 @@ -965,6 +965,27 @@ (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))" by (simp add: numeral_eq_Suc Let_def) +text {* Case analysis on @{term "n < 2"} *} + +lemma less_2_cases: "n < 2 \ n = 0 \ n = Suc 0" + by (auto simp add: numeral_2_eq_2) + +text {* Removal of Small Numerals: 0, 1 and (in additive positions) 2 *} +text {* bh: Are these rules really a good idea? *} + +lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" + by simp + +lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" + by simp + +text {* Can be used to eliminate long strings of Sucs, but not by default. *} + +lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" + by simp + +lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) + subsection {* Numeral equations as default simplification rules *} diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Sun Apr 01 22:14:59 2012 +0200 @@ -14,6 +14,14 @@ ("Tools/nat_numeral_simprocs.ML") begin +lemmas semiring_norm = + Let_def arith_simps nat_arith rel_simps + if_False if_True + add_0 add_Suc add_numeral_left + add_neg_numeral_left mult_numeral_left + numeral_1_eq_1 [symmetric] Suc_eq_plus1 + eq_numeral_iff_iszero not_iszero_Numeral1 + declare split_div [of _ _ "numeral k", arith_split] for k declare split_mod [of _ _ "numeral k", arith_split] for k diff -r 2d4ea84278da -r 3b9eeb4a2967 src/HOL/Power.thy --- a/src/HOL/Power.thy Sun Apr 01 22:03:45 2012 +0200 +++ b/src/HOL/Power.thy Sun Apr 01 22:14:59 2012 +0200 @@ -81,6 +81,15 @@ "a ^ Suc (2*n) = a * (a ^ n) ^ 2" by (simp add: power_even_eq) +lemma power_numeral_even: + "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" + unfolding numeral_Bit0 power_add Let_def .. + +lemma power_numeral_odd: + "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" + unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right + unfolding power_Suc power_add Let_def mult_assoc .. + end context comm_monoid_mult @@ -596,6 +605,9 @@ subsection {* Miscellaneous rules *} +lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" + unfolding One_nat_def by (cases m) simp_all + lemma power2_sum: fixes x y :: "'a::comm_semiring_1" shows "(x + y)\ = x\ + y\ + 2 * x * y" @@ -647,6 +659,16 @@ apply assumption done +text {* Simprules for comparisons where common factors can be cancelled. *} + +lemmas zero_compare_simps = + add_strict_increasing add_strict_increasing2 add_increasing + zero_le_mult_iff zero_le_divide_iff + zero_less_mult_iff zero_less_divide_iff + mult_le_0_iff divide_le_0_iff + mult_less_0_iff divide_less_0_iff + zero_le_power2 power2_less_0 + subsection {* Exponentiation for the Natural Numbers *}