sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
(* Title: HOL/ex/BinEx.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
*)
header {* Binary arithmetic examples *}
theory BinEx = Main:
subsection {* The Integers *}
text {* Addition *}
lemma "(# 13::int) + # 19 = # 32"
by simp
lemma "(# 1234::int) + # 5678 = # 6912"
by simp
lemma "(# 1359::int) + # -2468 = # -1109"
by simp
lemma "(# 93746::int) + # -46375 = # 47371"
by simp
text {* \medskip Negation *}
lemma "- (# 65745::int) = # -65745"
by simp
lemma "- (# -54321::int) = # 54321"
by simp
text {* \medskip Multiplication *}
lemma "(# 13::int) * # 19 = # 247"
by simp
lemma "(# -84::int) * # 51 = # -4284"
by simp
lemma "(# 255::int) * # 255 = # 65025"
by simp
lemma "(# 1359::int) * # -2468 = # -3354012"
by simp
lemma "(# 89::int) * # 10 \<noteq> # 889"
by simp
lemma "(# 13::int) < # 18 - # 4"
by simp
lemma "(# -345::int) < # -242 + # -100"
by simp
lemma "(# 13557456::int) < # 18678654"
by simp
lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2"
by simp
lemma "(# 1234567::int) \<le> # 1234567"
by simp
text {* \medskip Quotient and Remainder *}
lemma "(# 10::int) div # 3 = # 3"
by simp
lemma "(# 10::int) mod # 3 = Numeral1"
by simp
text {* A negative divisor *}
lemma "(# 10::int) div # -3 = # -4"
by simp
lemma "(# 10::int) mod # -3 = # -2"
by simp
text {*
A negative dividend\footnote{The definition agrees with mathematical
convention but not with the hardware of most computers}
*}
lemma "(# -10::int) div # 3 = # -4"
by simp
lemma "(# -10::int) mod # 3 = # 2"
by simp
text {* A negative dividend \emph{and} divisor *}
lemma "(# -10::int) div # -3 = # 3"
by simp
lemma "(# -10::int) mod # -3 = # -1"
by simp
text {* A few bigger examples *}
lemma "(# 8452::int) mod # 3 = Numeral1"
by simp
lemma "(# 59485::int) div # 434 = # 137"
by simp
lemma "(# 1000006::int) mod # 10 = # 6"
by simp
text {* \medskip Division by shifting *}
lemma "# 10000000 div # 2 = (# 5000000::int)"
by simp
lemma "# 10000001 mod # 2 = (Numeral1::int)"
by simp
lemma "# 10000055 div # 32 = (# 312501::int)"
by simp
lemma "# 10000055 mod # 32 = (# 23::int)"
by simp
lemma "# 100094 div # 144 = (# 695::int)"
by simp
lemma "# 100094 mod # 144 = (# 14::int)"
by simp
subsection {* The Natural Numbers *}
text {* Successor *}
lemma "Suc # 99999 = # 100000"
by (simp add: Suc_nat_number_of)
-- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
text {* \medskip Addition *}
lemma "(# 13::nat) + # 19 = # 32"
by simp
lemma "(# 1234::nat) + # 5678 = # 6912"
by simp
lemma "(# 973646::nat) + # 6475 = # 980121"
by simp
text {* \medskip Subtraction *}
lemma "(# 32::nat) - # 14 = # 18"
by simp
lemma "(# 14::nat) - # 15 = Numeral0"
by simp
lemma "(# 14::nat) - # 1576644 = Numeral0"
by simp
lemma "(# 48273776::nat) - # 3873737 = # 44400039"
by simp
text {* \medskip Multiplication *}
lemma "(# 12::nat) * # 11 = # 132"
by simp
lemma "(# 647::nat) * # 3643 = # 2357021"
by simp
text {* \medskip Quotient and Remainder *}
lemma "(# 10::nat) div # 3 = # 3"
by simp
lemma "(# 10::nat) mod # 3 = Numeral1"
by simp
lemma "(# 10000::nat) div # 9 = # 1111"
by simp
lemma "(# 10000::nat) mod # 9 = Numeral1"
by simp
lemma "(# 10000::nat) div # 16 = # 625"
by simp
lemma "(# 10000::nat) mod # 16 = Numeral0"
by simp
text {* \medskip Testing the cancellation of complementary terms *}
lemma "y + (x + -x) = (Numeral0::int) + y"
by simp
lemma "y + (-x + (- y + x)) = (Numeral0::int)"
by simp
lemma "-x + (y + (- y + x)) = (Numeral0::int)"
by simp
lemma "x + (x + (- x + (- x + (- y + - z)))) = (Numeral0::int) - y - z"
by simp
lemma "x + x - x - x - y - z = (Numeral0::int) - y - z"
by simp
lemma "x + y + z - (x + z) = y - (Numeral0::int)"
by simp
lemma "x + (y + (y + (y + (-x + -x)))) = (Numeral0::int) + y - x + y + y"
by simp
lemma "x + (y + (y + (y + (-y + -x)))) = y + (Numeral0::int) + y"
by simp
lemma "x + y - x + z - x - y - z + x < (Numeral1::int)"
by simp
subsection {* Normal form of bit strings *}
text {*
Definition of normal form for proving that binary arithmetic on
normalized operands yields normalized results. Normal means no
leading 0s on positive numbers and no leading 1s on negatives.
*}
consts normal :: "bin set"
inductive normal
intros
Pls [simp]: "Pls: normal"
Min [simp]: "Min: normal"
BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
text {*
\medskip Binary arithmetic on normalized operands yields normalized
results.
*}
lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"
apply (case_tac c)
apply auto
done
lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"
apply (erule normal.cases)
apply auto
done
lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"
apply (induct w)
apply (auto simp add: NCons_Pls NCons_Min)
done
lemma NCons_True: "NCons w True \<noteq> Pls"
apply (induct w)
apply auto
done
lemma NCons_False: "NCons w False \<noteq> Min"
apply (induct w)
apply auto
done
lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal"
apply (erule normal.induct)
apply (case_tac [4] w)
apply (auto simp add: NCons_True bin_succ_BIT)
done
lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal"
apply (erule normal.induct)
apply (case_tac [3] w)
apply (auto simp add: NCons_False bin_pred_BIT)
done
lemma bin_add_normal [rule_format]:
"w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)"
apply (induct w)
apply simp
apply simp
apply (rule impI)
apply (rule allI)
apply (induct_tac z)
apply (simp_all add: bin_add_BIT)
apply (safe dest!: normal_BIT_D)
apply simp_all
done
lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (Numeral0::int))"
apply (erule normal.induct)
apply auto
done
lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
apply (erule normal.induct)
apply (simp_all add: bin_minus_BIT)
apply (rule normal.intros)
apply assumption
apply (simp add: normal_Pls_eq_0)
apply (simp only: number_of_minus iszero_def zminus_equation [of _ "int 0"])
apply (rule not_sym)
apply simp
done
lemma bin_mult_normal [rule_format]:
"w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
apply (erule normal.induct)
apply (simp_all add: bin_minus_normal bin_mult_BIT)
apply (safe dest!: normal_BIT_D)
apply (simp add: bin_add_normal)
done
end