1 theory IntEx2

     2 imports "../QuotMain"

     3 uses

     4   ("Tools/numeral.ML")

     5   ("Tools/numeral_syntax.ML")

     6   ("Tools/int_arith.ML")

     7 begin

     8 

     9 

    10 fun

    11   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)

    12 where

    13   "intrel (x, y) (u, v) = (x + v = u + y)"

    14 

    15 quotient int = "nat \<times> nat" / intrel

    16   apply(unfold equivp_def)

    17   apply(auto simp add: mem_def expand_fun_eq)

    18   done

    19 

    20 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"

    21 begin

    22 

    23 quotient_def 

    24   zero_qnt::"int"

    25 where

    26   "zero_qnt \<equiv> (0::nat, 0::nat)"

    27 

    28 definition  Zero_int_def[code del]: 

    29   "0 = zero_qnt"

    30 

    31 quotient_def 

    32   one_qnt::"int"

    33 where

    34   "one_qnt \<equiv> (1::nat, 0::nat)"

    35 

    36 definition One_int_def[code del]:

    37   "1 = one_qnt"

    38 

    39 fun

    40   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    41 where

    42   "plus_raw (x, y) (u, v) = (x + u, y + v)"

    43 

    44 quotient_def 

    45   plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"

    46 where

    47   "plus_qnt \<equiv> plus_raw"

    48 

    49 definition add_int_def[code del]:

    50   "z + w = plus_qnt z w"

    51 

    52 fun

    53   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    54 where

    55   "minus_raw (x, y) = (y, x)"

    56 

    57 quotient_def

    58   minus_qnt::"int \<Rightarrow> int"

    59 where

    60   "minus_qnt \<equiv> minus_raw"

    61 

    62 definition minus_int_def [code del]:

    63     "- z = minus_qnt z"

    64 

    65 definition

    66   diff_int_def [code del]:  "z - w = z + (-w::int)"

    67 

    68 fun

    69   mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    70 where

    71   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

    72 

    73 quotient_def 

    74   mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"

    75 where

    76   "mult_qnt \<equiv> mult_raw"

    77 

    78 definition

    79   mult_int_def [code del]: "z * w = mult_qnt z w"

    80 

    81 fun

    82   le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

    83 where

    84   "le_raw (x, y) (u, v) = (x+v \<le> u+y)"

    85 

    86 quotient_def 

    87   le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"

    88 where

    89   "le_qnt \<equiv> le_raw"

    90 

    91 definition

    92   le_int_def [code del]:

    93    "z \<le> w = le_qnt z w"

    94 

    95 definition

    96   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"

    97 

    98 definition

    99   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"

   100 

   101 definition

   102   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"

   103 

   104 instance ..

   105 

   106 end

   107 

   108 thm add_assoc

   109 

   110 lemma plus_raw_rsp[quotient_rsp]:

   111   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"

   112 by auto

   113 

   114 lemma minus_raw_rsp[quotient_rsp]:

   115   shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"

   116   by auto

   117 

   118 lemma mult_raw_rsp[quotient_rsp]:

   119   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"

   120 apply(auto)

   121 apply(simp add: mult algebra_simps)

   122 sorry

   123 

   124 lemma le_raw_rsp[quotient_rsp]:

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

   126 by auto

   127 

   128 lemma plus_assoc_raw:

   129   shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"

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

   131 

   132 lemma plus_sym_raw:

   133   shows "plus_raw i j \<approx> plus_raw j i"

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

   135 

   136 lemma plus_zero_raw:

   137   shows "plus_raw  (0, 0) i \<approx> i"

   138 by (cases i) (simp)

   139 

   140 lemma plus_minus_zero_raw:

   141   shows "plus_raw (minus_raw i) i \<approx> (0, 0)"

   142 by (cases i) (simp)

   143 

   144 lemma mult_assoc_raw:

   145   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"

   146 by (cases i, cases j, cases k) 

   147    (simp add: mult algebra_simps)

   148 

   149 lemma mult_sym_raw:

   150   shows "mult_raw i j \<approx> mult_raw j i"

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

   152 

   153 lemma mult_one_raw:

   154   shows "mult_raw  (1, 0) i \<approx> i"

   155 by (cases i) (simp)

   156 

   157 lemma mult_plus_comm_raw:

   158   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"

   159 by (cases i, cases j, cases k) 

   160    (simp add: mult algebra_simps)

   161 

   162 lemma one_zero_distinct:

   163   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"

   164   by simp

   165 

   166 text{*The integers form a @{text comm_ring_1}*}

   167 

   168 

   169 ML {* val qty = @{typ "int"} *}

   170 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}

   171 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}

   172 

   173 instance int :: comm_ring_1

   174 proof

   175   fix i j k :: int

   176   show "(i + j) + k = i + (j + k)"

   177     unfolding add_int_def

   178     apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})

   179     done

   180   show "i + j = j + i" 

   181     unfolding add_int_def

   182     apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})

   183     done

   184   show "0 + i = (i::int)"

   185     unfolding add_int_def Zero_int_def 

   186     apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *})

   187     done

   188   show "- i + i = 0"

   189     unfolding add_int_def minus_int_def Zero_int_def 

   190     apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *})

   191     done

   192   show "i - j = i + - j"

   193     by (simp add: diff_int_def)

   194   show "(i * j) * k = i * (j * k)"

   195     unfolding mult_int_def 

   196     apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *})

   197     done

   198   show "i * j = j * i"

   199     unfolding mult_int_def 

   200     apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *})

   201     done

   202   show "1 * i = i"

   203     unfolding mult_int_def One_int_def

   204     apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *})

   205     done

   206   show "(i + j) * k = i * k + j * k"

   207     unfolding mult_int_def add_int_def

   208     apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *})

   209     done

   210   show "0 \<noteq> (1::int)"

   211     unfolding Zero_int_def One_int_def

   212     apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *})

   213     done

   214 qed

   215 

   216 term of_nat

   217 thm of_nat_def

   218 

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

   220 apply(induct m) 

   221 apply(simp add: Zero_int_def zero_qnt_def)

   222 apply(simp)

   223 apply(simp add: add_int_def One_int_def)

   224 apply(simp add: plus_qnt_def one_qnt_def)

   225 oops

   226 

   227 lemma le_antisym_raw:

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

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

   230 

   231 lemma le_refl_raw:

   232   shows "le_raw i i"

   233 by (cases i) (simp)

   234 

   235 lemma le_trans_raw:

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

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

   238 

   239 lemma le_cases_raw:

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

   241 by (cases i, cases j) 

   242    (simp add: linorder_linear)

   243 

   244 instance int :: linorder

   245 proof

   246   fix i j k :: int

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

   248     unfolding le_int_def

   249     apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})

   250     done

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

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

   253   show "i \<le> i"

   254     unfolding le_int_def

   255     apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})

   256     done

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

   258     unfolding le_int_def

   259     apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})

   260     done

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

   262     unfolding le_int_def

   263     apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})

   264     done

   265 qed

   266 

   267 instantiation int :: distrib_lattice

   268 begin

   269 

   270 definition

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

   272 

   273 definition

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

   275 

   276 instance

   277   by intro_classes

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

   279 

   280 end

   281 

   282 lemma le_plus_raw:

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

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

   285 

   286 

   287 instance int :: pordered_cancel_ab_semigroup_add

   288 proof

   289   fix i j k :: int

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

   291     unfolding le_int_def add_int_def

   292     apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})

   293     done

   294 qed

   295 

   296 lemma test:

   297   "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>

   298     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"

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

   300 apply(auto simp add: mult algebra_simps)

   301 sorry

   302 

   303 

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

   305 instance int :: ordered_idom

   306 proof

   307   fix i j k :: int

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

   309     unfolding mult_int_def le_int_def less_int_def Zero_int_def

   310     apply(tactic {* lift_tac @{context} @{thm test} 1 *})

   311     done

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

   313     by (simp only: zabs_def)

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

   315     by (simp only: zsgn_def)

   316 qed

   317 

   318 instance int :: lordered_ring

   319 proof  

   320   fix k :: int

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

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

   323 qed

   324 

   325 lemmas int_distrib =

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

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

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

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

   330 

   331 

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

   333 

   334 (*

   335 context ring_1

   336 begin

   337 

   338  

   339 definition 

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

   341 where

   342   "of_int 

   343 *)

   344 

   345 

   346 subsection {* Binary representation *}

   347 

   348 text {*

   349   This formalization defines binary arithmetic in terms of the integers

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

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

   352   int_of_binary}, for the numerical interpretation.

   353 

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

   355   even if m is negative;

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

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

   358   

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

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

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

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

   363 *}

   364 

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

   366 

   367 definition

   368   Pls :: int where

   369   [code del]: "Pls = 0"

   370 

   371 definition

   372   Min :: int where

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

   374 

   375 definition

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

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

   378 

   379 definition

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

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

   382 

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

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

   385 

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

   387 

   388 syntax

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

   390 

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

   392 (*

   393 setup NumeralSyntax.setup

   394 

   395 abbreviation

   396   "Numeral0 \<equiv> number_of Pls"

   397 

   398 abbreviation

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

   400 

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

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

   403   unfolding Let_def ..

   404 

   405 definition

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

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

   408 

   409 definition

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

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

   412 

   413 lemmas

   414   max_number_of [simp] = max_def

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

   416 and

   417   min_number_of [simp] = min_def 

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

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

   420 

   421 lemmas numeral_simps = 

   422   succ_def pred_def Pls_def Min_def Bit0_def Bit1_def

   423 

   424 text {* Removal of leading zeroes *}

   425 

   426 lemma Bit0_Pls [simp, code_post]:

   427   "Bit0 Pls = Pls"

   428   unfolding numeral_simps by simp

   429 

   430 lemma Bit1_Min [simp, code_post]:

   431   "Bit1 Min = Min"

   432   unfolding numeral_simps by simp

   433 

   434 lemmas normalize_bin_simps =

   435   Bit0_Pls Bit1_Min

   436 *)