theory IntEx2+ −
imports "../Quotient" "../Quotient_Product" Nat+ −
(*uses+ −
("Tools/numeral.ML")+ −
("Tools/numeral_syntax.ML")+ −
("Tools/int_arith.ML")*)+ −
begin+ −
+ −
fun+ −
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)+ −
where+ −
"intrel (x, y) (u, v) = (x + v = u + y)"+ −
+ −
quotient_type int = "nat \<times> nat" / intrel+ −
unfolding equivp_def+ −
by (auto simp add: mem_def expand_fun_eq)+ −
+ −
instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"+ −
begin+ −
+ −
ML {* @{term "0 \<Colon> int"} *}+ −
+ −
quotient_definition+ −
"0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"+ −
+ −
quotient_definition+ −
"1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"+ −
+ −
fun+ −
plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"+ −
where+ −
"plus_raw (x, y) (u, v) = (x + u, y + v)"+ −
+ −
quotient_definition+ −
"(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw"+ −
+ −
fun+ −
uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"+ −
where+ −
"uminus_raw (x, y) = (y, x)"+ −
+ −
quotient_definition+ −
"(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw"+ −
+ −
definition+ −
minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"+ −
+ −
fun+ −
mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"+ −
where+ −
"mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"+ −
+ −
quotient_definition+ −
mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw"+ −
+ −
fun+ −
le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"+ −
where+ −
"le_raw (x, y) (u, v) = (x+v \<le> u+y)"+ −
+ −
quotient_definition+ −
le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw"+ −
+ −
definition+ −
less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"+ −
+ −
definition+ −
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"+ −
+ −
definition+ −
zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"+ −
+ −
instance ..+ −
+ −
end+ −
+ −
lemma plus_raw_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"+ −
by auto+ −
+ −
lemma uminus_raw_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"+ −
by auto+ −
+ −
lemma mult_raw_fst:+ −
assumes a: "x \<approx> z"+ −
shows "mult_raw x y \<approx> mult_raw z y"+ −
using a+ −
apply(cases x, cases y, cases z)+ −
apply(auto simp add: mult_raw.simps intrel.simps)+ −
apply(rename_tac u v w x y z)+ −
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")+ −
apply(simp add: mult_ac)+ −
apply(simp add: add_mult_distrib [symmetric])+ −
done+ −
+ −
lemma mult_raw_snd:+ −
assumes a: "x \<approx> z"+ −
shows "mult_raw y x \<approx> mult_raw y z"+ −
using a+ −
apply(cases x, cases y, cases z)+ −
apply(auto simp add: mult_raw.simps intrel.simps)+ −
apply(rename_tac u v w x y z)+ −
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")+ −
apply(simp add: mult_ac)+ −
apply(simp add: add_mult_distrib [symmetric])+ −
done+ −
+ −
lemma mult_raw_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"+ −
apply(simp only: fun_rel_def)+ −
apply(rule allI | rule impI)++ −
apply(rule equivp_transp[OF int_equivp])+ −
apply(rule mult_raw_fst)+ −
apply(assumption)+ −
apply(rule mult_raw_snd)+ −
apply(assumption)+ −
done+ −
+ −
lemma le_raw_rsp[quot_respect]:+ −
shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"+ −
by auto+ −
+ −
lemma plus_assoc_raw:+ −
shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"+ −
by (cases i, cases j, cases k) (simp)+ −
+ −
lemma plus_sym_raw:+ −
shows "plus_raw i j \<approx> plus_raw j i"+ −
by (cases i, cases j) (simp)+ −
+ −
lemma plus_zero_raw:+ −
shows "plus_raw (0, 0) i \<approx> i"+ −
by (cases i) (simp)+ −
+ −
lemma plus_minus_zero_raw:+ −
shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"+ −
by (cases i) (simp)+ −
+ −
lemma times_assoc_raw:+ −
shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"+ −
by (cases i, cases j, cases k) + −
(simp add: algebra_simps)+ −
+ −
lemma times_sym_raw:+ −
shows "mult_raw i j \<approx> mult_raw j i"+ −
by (cases i, cases j) (simp add: algebra_simps)+ −
+ −
lemma times_one_raw:+ −
shows "mult_raw (1, 0) i \<approx> i"+ −
by (cases i) (simp)+ −
+ −
lemma times_plus_comm_raw:+ −
shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"+ −
by (cases i, cases j, cases k) + −
(simp add: algebra_simps)+ −
+ −
lemma one_zero_distinct:+ −
shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"+ −
by simp+ −
+ −
text{* The integers form a @{text comm_ring_1}*}+ −
+ −
instance int :: comm_ring_1+ −
proof+ −
fix i j k :: int+ −
show "(i + j) + k = i + (j + k)"+ −
by (lifting plus_assoc_raw)+ −
show "i + j = j + i" + −
by (lifting plus_sym_raw)+ −
show "0 + i = (i::int)"+ −
by (lifting plus_zero_raw)+ −
show "- i + i = 0"+ −
by (lifting plus_minus_zero_raw)+ −
show "i - j = i + - j"+ −
by (simp add: minus_int_def)+ −
show "(i * j) * k = i * (j * k)"+ −
by (lifting times_assoc_raw)+ −
show "i * j = j * i"+ −
by (lifting times_sym_raw)+ −
show "1 * i = i"+ −
by (lifting times_one_raw)+ −
show "(i + j) * k = i * k + j * k"+ −
by (lifting times_plus_comm_raw)+ −
show "0 \<noteq> (1::int)"+ −
by (lifting one_zero_distinct)+ −
qed+ −
+ −
lemma plus_raw_rsp_aux:+ −
assumes a: "a \<approx> b" "c \<approx> d"+ −
shows "plus_raw a c \<approx> plus_raw b d"+ −
using a+ −
by (cases a, cases b, cases c, cases d)+ −
(simp)+ −
+ −
lemma add:+ −
"(abs_int (x,y)) + (abs_int (u,v)) =+ −
(abs_int (x + u, y + v))"+ −
apply(simp add: plus_int_def id_simps)+ −
apply(fold plus_raw.simps)+ −
apply(rule Quotient_rel_abs[OF Quotient_int])+ −
apply(rule plus_raw_rsp_aux)+ −
apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])+ −
done+ −
+ −
definition int_of_nat_raw: + −
"int_of_nat_raw m = (m :: nat, 0 :: nat)"+ −
+ −
quotient_definition+ −
"int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"+ −
+ −
lemma[quot_respect]: + −
shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"+ −
by (simp add: equivp_reflp[OF int_equivp])+ −
+ −
lemma int_of_nat:+ −
shows "of_nat m = int_of_nat m"+ −
by (induct m)+ −
(simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)+ −
+ −
lemma le_antisym_raw:+ −
shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"+ −
by (cases i, cases j) (simp)+ −
+ −
lemma le_refl_raw:+ −
shows "le_raw i i"+ −
by (cases i) (simp)+ −
+ −
lemma le_trans_raw:+ −
shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"+ −
by (cases i, cases j, cases k) (simp)+ −
+ −
lemma le_cases_raw:+ −
shows "le_raw i j \<or> le_raw j i"+ −
by (cases i, cases j)+ −
(simp add: linorder_linear)+ −
+ −
instance int :: linorder+ −
proof+ −
fix i j k :: int+ −
show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"+ −
by (lifting le_antisym_raw)+ −
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"+ −
by (auto simp add: less_int_def dest: antisym) + −
show "i \<le> i"+ −
by (lifting le_refl_raw)+ −
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"+ −
by (lifting le_trans_raw)+ −
show "i \<le> j \<or> j \<le> i"+ −
by (lifting le_cases_raw)+ −
qed+ −
+ −
instantiation int :: distrib_lattice+ −
begin+ −
+ −
definition+ −
"(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"+ −
+ −
definition+ −
"(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"+ −
+ −
instance+ −
by intro_classes+ −
(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)+ −
+ −
end+ −
+ −
lemma le_plus_raw:+ −
shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"+ −
by (cases i, cases j, cases k) (simp)+ −
+ −
instance int :: ordered_cancel_ab_semigroup_add+ −
proof+ −
fix i j k :: int+ −
show "i \<le> j \<Longrightarrow> k + i \<le> k + j"+ −
by (lifting le_plus_raw)+ −
qed+ −
+ −
abbreviation+ −
"less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"+ −
+ −
lemma zmult_zless_mono2_lemma:+ −
fixes i j::int+ −
and k::nat+ −
shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"+ −
apply(induct "k")+ −
apply(simp)+ −
apply(case_tac "k = 0")+ −
apply(simp_all add: left_distrib add_strict_mono)+ −
done+ −
+ −
lemma zero_le_imp_eq_int_raw:+ −
fixes k::"(nat \<times> nat)"+ −
shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"+ −
apply(cases k)+ −
apply(simp add:int_of_nat_raw)+ −
apply(auto)+ −
apply(rule_tac i="b" and j="a" in less_Suc_induct)+ −
apply(auto)+ −
done+ −
+ −
lemma zero_le_imp_eq_int:+ −
fixes k::int+ −
shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"+ −
unfolding less_int_def int_of_nat+ −
by (lifting zero_le_imp_eq_int_raw)+ −
+ −
lemma zmult_zless_mono2: + −
fixes i j k::int+ −
assumes a: "i < j" "0 < k"+ −
shows "k * i < k * j"+ −
using a+ −
by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)+ −
+ −
text{*The integers form an ordered integral domain*}+ −
instance int :: linordered_idom+ −
proof+ −
fix i j k :: int+ −
show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"+ −
by (rule zmult_zless_mono2)+ −
show "\<bar>i\<bar> = (if i < 0 then -i else i)"+ −
by (simp only: zabs_def)+ −
show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"+ −
by (simp only: zsgn_def)+ −
qed+ −
+ −
lemmas int_distrib =+ −
left_distrib [of "z1::int" "z2" "w", standard]+ −
right_distrib [of "w::int" "z1" "z2", standard]+ −
left_diff_distrib [of "z1::int" "z2" "w", standard]+ −
right_diff_distrib [of "w::int" "z1" "z2", standard]+ −
+ −
lemma int_induct_raw:+ −
assumes a: "P (0::nat, 0)"+ −
and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1, 0))"+ −
and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1, 0)))"+ −
shows "P x"+ −
proof (cases x, clarify)+ −
fix a b+ −
show "P (a, b)"+ −
proof (induct a arbitrary: b rule: Nat.induct)+ −
case zero+ −
show "P (0, b)" using assms by (induct b) auto+ −
next+ −
case (Suc n)+ −
then show ?case using assms by auto+ −
qed+ −
qed+ −
+ −
lemma int_induct:+ −
fixes x :: int+ −
assumes a: "P 0"+ −
and b: "\<And>i. P i \<Longrightarrow> P (i + 1)"+ −
and c: "\<And>i. P i \<Longrightarrow> P (i - 1)"+ −
shows "P x"+ −
using a b c unfolding minus_int_def+ −
by (lifting int_induct_raw)+ −
+ −
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}+ −
+ −
(*+ −
context ring_1+ −
begin+ −
+ −
+ −
definition + −
of_int :: "int \<Rightarrow> 'a" + −
where+ −
"of_int + −
*)+ −
+ −
+ −
subsection {* Binary representation *}+ −
+ −
text {*+ −
This formalization defines binary arithmetic in terms of the integers+ −
rather than using a datatype. This avoids multiple representations (leading+ −
zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text+ −
int_of_binary}, for the numerical interpretation.+ −
+ −
The representation expects that @{text "(m mod 2)"} is 0 or 1,+ −
even if m is negative;+ −
For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus+ −
@{text "-5 = (-3)*2 + 1"}.+ −
+ −
This two's complement binary representation derives from the paper + −
"An Efficient Representation of Arithmetic for Term Rewriting" by+ −
Dave Cohen and Phil Watson, Rewriting Techniques and Applications,+ −
Springer LNCS 488 (240-251), 1991.+ −
*}+ −
+ −
subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}+ −
+ −
definition+ −
Pls :: int where+ −
[code del]: "Pls = 0"+ −
+ −
definition+ −
Min :: int where+ −
[code del]: "Min = - 1"+ −
+ −
definition+ −
Bit0 :: "int \<Rightarrow> int" where+ −
[code del]: "Bit0 k = k + k"+ −
+ −
definition+ −
Bit1 :: "int \<Rightarrow> int" where+ −
[code del]: "Bit1 k = 1 + k + k"+ −
+ −
class number = -- {* for numeric types: nat, int, real, \dots *}+ −
fixes number_of :: "int \<Rightarrow> 'a"+ −
+ −
(*use "~~/src/HOL/Tools/numeral.ML"+ −
+ −
syntax+ −
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")+ −
+ −
use "~~/src/HOL/Tools/numeral_syntax.ML"+ −
+ −
setup NumeralSyntax.setup+ −
+ −
abbreviation+ −
"Numeral0 \<equiv> number_of Pls"+ −
+ −
abbreviation+ −
"Numeral1 \<equiv> number_of (Bit1 Pls)"+ −
+ −
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"+ −
-- {* Unfold all @{text let}s involving constants *}+ −
unfolding Let_def ..+ −
+ −
definition+ −
succ :: "int \<Rightarrow> int" where+ −
[code del]: "succ k = k + 1"+ −
+ −
definition+ −
pred :: "int \<Rightarrow> int" where+ −
[code del]: "pred k = k - 1"+ −
+ −
lemmas+ −
max_number_of [simp] = max_def+ −
[of "number_of u" "number_of v", standard, simp]+ −
and+ −
min_number_of [simp] = min_def + −
[of "number_of u" "number_of v", standard, simp]+ −
-- {* unfolding @{text minx} and @{text max} on numerals *}+ −
+ −
lemmas numeral_simps = + −
succ_def pred_def Pls_def Min_def Bit0_def Bit1_def+ −
+ −
text {* Removal of leading zeroes *}+ −
+ −
lemma Bit0_Pls [simp, code_post]:+ −
"Bit0 Pls = Pls"+ −
unfolding numeral_simps by simp+ −
+ −
lemma Bit1_Min [simp, code_post]:+ −
"Bit1 Min = Min"+ −
unfolding numeral_simps by simp+ −
+ −
lemmas normalize_bin_simps =+ −
Bit0_Pls Bit1_Min+ −
*)+ −
+ −
end+ −