--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/Examples/IntEx2.thy Thu Feb 25 07:57:17 2010 +0100
@@ -0,0 +1,445 @@
+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"
+apply (induct m)
+apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
+done
+
+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
+using a
+apply(drule_tac zero_le_imp_eq_int)
+apply(auto simp add: zmult_zless_mono2_lemma)
+done
+
+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]
+
+
+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