8 

     9 fun

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

    11 where

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

    13 

    14 quotient_type int = "nat \<times> nat" / intrel

    15   unfolding equivp_def

    16   by (auto simp add: mem_def expand_fun_eq)

    17 

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

    19 begin

    20 

    21 ML {* @{term "0 \<Colon> int"} *}

    22 

    23 quotient_definition

    24   "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"

    25 

    26 quotient_definition

    27   "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"

    28 

    29 fun

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

    31 where

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

    33 

    34 quotient_definition

    35   "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw"

    36 

    37 fun

    38   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    39 where

    40   "uminus_raw (x, y) = (y, x)"

    41 

    42 quotient_definition

    43   "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw"

    44 

    45 definition

    46   minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"

    47 

    48 fun

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

    50 where

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

    52 

    53 quotient_definition

    54   mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw"

    55 

    56 fun

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

    58 where

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

    60 

    61 quotient_definition

    62   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw"

    63 

    64 definition

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

    66 

    67 definition

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

    69 

    70 definition

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

    72 

    73 instance ..

    74 

    75 end

    76 

    77 lemma plus_raw_rsp[quot_respect]:

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

    79   by auto

    80 

    81 lemma uminus_raw_rsp[quot_respect]:

    82   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"

    83   by auto

    84 

    85 lemma mult_raw_fst:

    86   assumes a: "x \<approx> z"

    87   shows "mult_raw x y \<approx> mult_raw z y"

    88   using a

    89   apply(cases x, cases y, cases z)

    90   apply(auto simp add: mult_raw.simps intrel.simps)

    91   apply(rename_tac u v w x y z)

    92   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")

    93   apply(simp add: mult_ac)

    94   apply(simp add: add_mult_distrib [symmetric])

    95   done

    96 

    97 lemma mult_raw_snd:

    98   assumes a: "x \<approx> z"

    99   shows "mult_raw y x \<approx> mult_raw y z"

   100   using a

   101   apply(cases x, cases y, cases z)

   102   apply(auto simp add: mult_raw.simps intrel.simps)

   103   apply(rename_tac u v w x y z)

   104   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")

   105   apply(simp add: mult_ac)

   106   apply(simp add: add_mult_distrib [symmetric])

   107   done

   108 

   109 lemma mult_raw_rsp[quot_respect]:

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

   111   apply(simp only: fun_rel_def)

   112   apply(rule allI | rule impI)+

   113   apply(rule equivp_transp[OF int_equivp])

   114   apply(rule mult_raw_fst)

   115   apply(assumption)

   116   apply(rule mult_raw_snd)

   117   apply(assumption)

   118   done

   119 

   120 lemma le_raw_rsp[quot_respect]:

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

   122   by auto

   123 

   124 lemma plus_assoc_raw:

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

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

   127 

   128 lemma plus_sym_raw:

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

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

   131 

   132 lemma plus_zero_raw:

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

   134   by (cases i) (simp)

   135 

   136 lemma plus_minus_zero_raw:

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

   138   by (cases i) (simp)

   139 

   140 lemma times_assoc_raw:

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

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

   143      (simp add: algebra_simps)

   144 

   145 lemma times_sym_raw:

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

   147   by (cases i, cases j) (simp add: algebra_simps)

   148 

   149 lemma times_one_raw:

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

   151   by (cases i) (simp)

   152 

   153 lemma times_plus_comm_raw:

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

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

   156    (simp add: algebra_simps)

   157 

   158 lemma one_zero_distinct:

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

   160   by simp

   161 

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

   163 

   164 instance int :: comm_ring_1

   165 proof

   166   fix i j k :: int

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

   168     by (lifting plus_assoc_raw)

   169   show "i + j = j + i" 

   170     by (lifting plus_sym_raw)

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

   172     by (lifting plus_zero_raw)

   173   show "- i + i = 0"

   174     by (lifting plus_minus_zero_raw)

   175   show "i - j = i + - j"

   176     by (simp add: minus_int_def)

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

   178     by (lifting times_assoc_raw)

   179   show "i * j = j * i"

   180     by (lifting times_sym_raw)

   181   show "1 * i = i"

   182     by (lifting times_one_raw)

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

   184     by (lifting times_plus_comm_raw)

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

   186     by (lifting one_zero_distinct)

   187 qed

   188 

   189 lemma plus_raw_rsp_aux:

   190   assumes a: "a \<approx> b" "c \<approx> d"

   191   shows "plus_raw a c \<approx> plus_raw b d"

   192   using a

   193   by (cases a, cases b, cases c, cases d)

   194      (simp)

   195 

   196 lemma add:

   197   "(abs_int (x,y)) + (abs_int (u,v)) =

   198    (abs_int (x + u, y + v))"

   199   apply(simp add: plus_int_def id_simps)

   200   apply(fold plus_raw.simps)

   201   apply(rule Quotient_rel_abs[OF Quotient_int])

   202   apply(rule plus_raw_rsp_aux)

   203   apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])

   204   done

   205 

   206 definition int_of_nat_raw: 

   207   "int_of_nat_raw m = (m :: nat, 0 :: nat)"

   208 

   209 quotient_definition

   210   "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"

   211 

   212 lemma[quot_respect]: 

   213   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"

   214   by (simp add: equivp_reflp[OF int_equivp])

   215 

   216 lemma int_of_nat:

   217   shows "of_nat m = int_of_nat m"

   218   by (induct m)

   219     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)

   220 

   221 lemma le_antisym_raw:

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

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

   224 

   225 lemma le_refl_raw:

   226   shows "le_raw i i"

   227   by (cases i) (simp)

   228 

   229 lemma le_trans_raw:

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

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

   232 

   233 lemma le_cases_raw:

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

   235   by (cases i, cases j)

   236      (simp add: linorder_linear)

   237 

   238 instance int :: linorder

   239 proof

   240   fix i j k :: int

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

   242     by (lifting le_antisym_raw)

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

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

   245   show "i \<le> i"

   246     by (lifting le_refl_raw)

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

   248     by (lifting le_trans_raw)

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

   250     by (lifting le_cases_raw)

   251 qed

   252 

   253 instantiation int :: distrib_lattice

   254 begin

   255 

   256 definition

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

   258 

   259 definition

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

   261 

   262 instance

   263   by intro_classes

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

   265 

   266 end

   267 

   268 lemma le_plus_raw:

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

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

   271 

   272 instance int :: ordered_cancel_ab_semigroup_add

   273 proof

   274   fix i j k :: int

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

   276     by (lifting le_plus_raw)

   277 qed

   278 

   279 abbreviation

   280   "less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"

   281 

   282 lemma zmult_zless_mono2_lemma:

   283   fixes i j::int

   284   and   k::nat

   285   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"

   286   apply(induct "k")

   287   apply(simp)

   288   apply(case_tac "k = 0")

   289   apply(simp_all add: left_distrib add_strict_mono)

   290   done

   291 

   292 lemma zero_le_imp_eq_int_raw:

   293   fixes k::"(nat \<times> nat)"

   294   shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"

   295   apply(cases k)

   296   apply(simp add:int_of_nat_raw)

   297   apply(auto)

   298   apply(rule_tac i="b" and j="a" in less_Suc_induct)

   299   apply(auto)

   300   done

   301 

   302 lemma zero_le_imp_eq_int:

   303   fixes k::int

   304   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"

   305   unfolding less_int_def int_of_nat

   306   by (lifting zero_le_imp_eq_int_raw)

   307 

   308 lemma zmult_zless_mono2: 

   309   fixes i j k::int

   310   assumes a: "i < j" "0 < k"

   311   shows "k * i < k * j"

   312   using a

   313   by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)

   314 

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

   316 instance int :: linordered_idom

   317 proof

   318   fix i j k :: int

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

   320     by (rule zmult_zless_mono2)

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

   322     by (simp only: zabs_def)

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

   324     by (simp only: zsgn_def)

   325 qed

   326 

   327 lemmas int_distrib =

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

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

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

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

   332 

   333 lemma int_induct_raw:

   334   assumes a: "P (0::nat, 0)"

   335   and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1, 0))"

   336   and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1, 0)))"

   337   shows      "P x"

   338 proof (cases x, clarify)

   339   fix a b

   340   show "P (a, b)"

   341   proof (induct a arbitrary: b rule: Nat.induct)

   342     case zero

   343     show "P (0, b)" using assms by (induct b) auto

   344   next

   345     case (Suc n)

   346     then show ?case using assms by auto

   347   qed

   348 qed

   349 

   350 lemma int_induct:

   351   fixes x :: int

   352   assumes a: "P 0"

   353   and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"

   354   and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"

   355   shows      "P x"

   356   using a b c unfolding minus_int_def

   357   by (lifting int_induct_raw)