118 

   119 lemma le_raw_rsp[quotient_rsp]:

   120   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"

   121 by auto

   238 term of_nat

   239 thm of_nat_def

   240 

   241 lemma int_def: "of_nat m = ABS_int (m, 0)"

   242 apply(induct m) 

   243 apply(simp add: Zero_int_def zero_qnt_def)

   244 apply(simp)

   245 apply(simp add: add_int_def One_int_def)

   246 apply(simp add: plus_qnt_def one_qnt_def)

   247 oops

   248 

   249 lemma le_antisym_raw:

   250   shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"

   251 by (cases i, cases j) (simp)

   252 

   253 lemma le_refl_raw:

   254   shows "le_raw i i"

   255 by (cases i) (simp)

   256 

   257 lemma le_trans_raw:

   258   shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"

   259 by (cases i, cases j, cases k) (simp)

   260 

   261 lemma le_cases_raw:

   262   shows "le_raw i j \<or> le_raw j i"

   263 by (cases i, cases j) 

   264    (simp add: linorder_linear)

   265 

   266 instance int :: linorder

   267 proof

   268   fix i j k :: int

   269   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"

   270     unfolding le_int_def

   271     apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})

   272     done

   273   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"

   274     by (auto simp add: less_int_def dest: antisym) 

   275   show "i \<le> i"

   276     unfolding le_int_def

   277     apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})

   278     done

   279   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"

   280     unfolding le_int_def

   281     apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})

   282     done

   283   show "i \<le> j \<or> j \<le> i"

   284     unfolding le_int_def

   285     apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})

   286     done

   287 qed

   288 

   289 instantiation int :: distrib_lattice

   290 begin

   291 

   292 definition

   293   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"

   294 

   295 definition

   296   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"

   297 

   298 instance

   299   by intro_classes

   300     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)

   301 

   302 end

   303 

   304 lemma le_plus_raw:

   305   shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"

   306 by (cases i, cases j, cases k) (simp)

   307 

   308 

   309 instance int :: pordered_cancel_ab_semigroup_add

   310 proof

   311   fix i j k :: int

   312   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"

   313     unfolding le_int_def add_int_def

   314     apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})

   315     done

   316 qed

   317 

   318 lemma test:

   319   "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>

   320     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"

   321 apply(cases i, cases j, cases k)

   322 apply(auto simp add: mult algebra_simps)

   323 sorry

   324 

   325 

   326 text{*The integers form an ordered integral domain*}

   327 instance int :: ordered_idom

   328 proof

   329   fix i j k :: int

   330   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"

   331     unfolding mult_int_def le_int_def less_int_def Zero_int_def

   332     apply(tactic {* procedure_tac @{context} @{thm test} 1 *})

   333     defer

   334     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   335     defer

   336     apply(tactic {* clean_tac @{context} 1*})

   337     sorry

   338   show "\<bar>i\<bar> = (if i < 0 then -i else i)"

   339     by (simp only: zabs_def)

   340   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"

   341     by (simp only: zsgn_def)

   342 qed

   343 

   344 instance int :: lordered_ring

   345 proof  

   346   fix k :: int

   347   show "abs k = sup k (- k)"

   348     by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])

   349 qed

   350 

   351 lemmas int_distrib =

   352   left_distrib [of "z1::int" "z2" "w", standard]

   353   right_distrib [of "w::int" "z1" "z2", standard]

   354   left_diff_distrib [of "z1::int" "z2" "w", standard]

   355   right_diff_distrib [of "w::int" "z1" "z2", standard]

   356 

   357 

   358 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}

   359 

   360 (*

   361 context ring_1

   362 begin

   363 

   364  

   365 definition 

   366   of_int :: "int \<Rightarrow> 'a" 

   367 where

   368   "of_int 

   369 *)

   370 

   371 

   372 subsection {* Binary representation *}

   373 

   374 text {*

   375   This formalization defines binary arithmetic in terms of the integers

   376   rather than using a datatype. This avoids multiple representations (leading

   377   zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text

   378   int_of_binary}, for the numerical interpretation.

   379 

   380   The representation expects that @{text "(m mod 2)"} is 0 or 1,

   381   even if m is negative;

   382   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus

   383   @{text "-5 = (-3)*2 + 1"}.

   384   

   385   This two's complement binary representation derives from the paper 

   386   "An Efficient Representation of Arithmetic for Term Rewriting" by

   387   Dave Cohen and Phil Watson, Rewriting Techniques and Applications,

   388   Springer LNCS 488 (240-251), 1991.

   389 *}

   390 

   391 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}

   392 

   393 definition

   394   Pls :: int where

   395   [code del]: "Pls = 0"

   396 

   397 definition

   398   Min :: int where

   399   [code del]: "Min = - 1"

   400 

   401 definition

   402   Bit0 :: "int \<Rightarrow> int" where

   403   [code del]: "Bit0 k = k + k"

   404 

   405 definition

   406   Bit1 :: "int \<Rightarrow> int" where

   407   [code del]: "Bit1 k = 1 + k + k"

   408 

   409 class number = -- {* for numeric types: nat, int, real, \dots *}

   410   fixes number_of :: "int \<Rightarrow> 'a"

   411 

   412 use "~~/src/HOL/Tools/numeral.ML"

   413 

   414 syntax

   415   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")

   416 

   417 use "~~/src/HOL/Tools/numeral_syntax.ML"

   418 setup NumeralSyntax.setup

   419 

   420 abbreviation

   421   "Numeral0 \<equiv> number_of Pls"

   422 

   423 abbreviation

   424   "Numeral1 \<equiv> number_of (Bit1 Pls)"

   425 

   426 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"

   427   -- {* Unfold all @{text let}s involving constants *}

   428   unfolding Let_def ..

   429 

   430 definition

   431   succ :: "int \<Rightarrow> int" where

   432   [code del]: "succ k = k + 1"

   433 

   434 definition

   435   pred :: "int \<Rightarrow> int" where

   436   [code del]: "pred k = k - 1"

   437 

   438 lemmas

   439   max_number_of [simp] = max_def

   440     [of "number_of u" "number_of v", standard, simp]

   441 and

   442   min_number_of [simp] = min_def 

   443     [of "number_of u" "number_of v", standard, simp]

   444   -- {* unfolding @{text minx} and @{text max} on numerals *}

   445 

   446 lemmas numeral_simps = 

   447   succ_def pred_def Pls_def Min_def Bit0_def Bit1_def

   448 

   449 text {* Removal of leading zeroes *}

   450 

   451 lemma Bit0_Pls [simp, code_post]:

   452   "Bit0 Pls = Pls"

   453   unfolding numeral_simps by simp

   454 

   455 lemma Bit1_Min [simp, code_post]:

   456   "Bit1 Min = Min"

   457   unfolding numeral_simps by simp

   458 

   459 lemmas normalize_bin_simps =

   460   Bit0_Pls Bit1_Min