--- 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
--- 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 {*
--- 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
--- 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)"
--- 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 \
--- 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 *}
--- 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 \<le> 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
--- 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
--- 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 \<Longrightarrow> n = 0 \<or> 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 *}
--- 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
--- 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)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 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 *}