diff -r e121ac0028f8 -r 6a031829319a IntEx2.thy
--- a/IntEx2.thy	Sun Dec 06 00:19:45 2009 +0100
+++ b/IntEx2.thy	Sun Dec 06 01:43:46 2009 +0100
@@ -89,10 +89,10 @@
 
 definition
   le_int_def [code del]:
-   "z \<le> w \<longleftrightarrow> le_qnt z w"
+   "z \<le> w = le_qnt z w"
 
 definition
-  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+  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)"
@@ -116,6 +116,10 @@
 apply(simp add: mult algebra_simps)
 sorry
 
+lemma le_raw_rsp[quotient_rsp]:
+  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)
@@ -231,3 +235,226 @@
     sorry
 qed
 
+term of_nat
+thm of_nat_def
+
+lemma int_def: "of_nat m = ABS_int (m, 0)"
+apply(induct m) 
+apply(simp add: Zero_int_def zero_qnt_def)
+apply(simp)
+apply(simp add: add_int_def One_int_def)
+apply(simp add: plus_qnt_def one_qnt_def)
+oops
+
+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"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+    by (auto simp add: less_int_def dest: antisym) 
+  show "i \<le> i"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "i \<le> j \<or> j \<le> i"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
+    done
+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 :: pordered_cancel_ab_semigroup_add
+proof
+  fix i j k :: int
+  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+    unfolding le_int_def add_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
+    done
+qed
+
+lemma test:
+  "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
+    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
+apply(cases i, cases j, cases k)
+apply(auto simp add: mult algebra_simps)
+sorry
+
+
+text{*The integers form an ordered integral domain*}
+instance int :: ordered_idom
+proof
+  fix i j k :: int
+  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+    unfolding mult_int_def le_int_def less_int_def Zero_int_def
+    apply(tactic {* procedure_tac @{context} @{thm test} 1 *})
+    defer
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  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
+
+instance int :: lordered_ring
+proof  
+  fix k :: int
+  show "abs k = sup k (- k)"
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+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