src/HOL/Quotient_Examples/Quotient_Int.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 54863 82acc20ded73
child 57492 74bf65a1910a
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     1 (*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
     2     Author:     Cezary Kaliszyk
     3     Author:     Christian Urban
     4 
     5 Integers based on Quotients, based on an older version by Larry
     6 Paulson.
     7 *)
     8 
     9 theory Quotient_Int
    10 imports "~~/src/HOL/Library/Quotient_Product" Nat
    11 begin
    12 
    13 fun
    14   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
    15 where
    16   "intrel (x, y) (u, v) = (x + v = u + y)"
    17 
    18 quotient_type int = "nat \<times> nat" / intrel
    19   by (auto simp add: equivp_def fun_eq_iff)
    20 
    21 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
    22 begin
    23 
    24 quotient_definition
    25   "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" done
    26 
    27 quotient_definition
    28   "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" done
    29 
    30 fun
    31   plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    32 where
    33   "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
    34 
    35 quotient_definition
    36   "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
    37 
    38 fun
    39   uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    40 where
    41   "uminus_int_raw (x, y) = (y, x)"
    42 
    43 quotient_definition
    44   "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw" by auto
    45 
    46 definition
    47   minus_int_def:  "z - w = z + (-w\<Colon>int)"
    48 
    49 fun
    50   times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    51 where
    52   "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
    53 
    54 lemma times_int_raw_fst:
    55   assumes a: "x \<approx> z"
    56   shows "times_int_raw x y \<approx> times_int_raw z y"
    57   using a
    58   apply(cases x, cases y, cases z)
    59   apply(auto simp add: times_int_raw.simps intrel.simps)
    60   apply(rename_tac u v w x y z)
    61   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
    62   apply(simp add: mult_ac)
    63   apply(simp add: add_mult_distrib [symmetric])
    64 done
    65 
    66 lemma times_int_raw_snd:
    67   assumes a: "x \<approx> z"
    68   shows "times_int_raw y x \<approx> times_int_raw y z"
    69   using a
    70   apply(cases x, cases y, cases z)
    71   apply(auto simp add: times_int_raw.simps intrel.simps)
    72   apply(rename_tac u v w x y z)
    73   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
    74   apply(simp add: mult_ac)
    75   apply(simp add: add_mult_distrib [symmetric])
    76 done
    77 
    78 quotient_definition
    79   "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
    80   apply(rule equivp_transp[OF int_equivp])
    81   apply(rule times_int_raw_fst)
    82   apply(assumption)
    83   apply(rule times_int_raw_snd)
    84   apply(assumption)
    85 done
    86 
    87 fun
    88   le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
    89 where
    90   "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
    91 
    92 quotient_definition
    93   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
    94 
    95 definition
    96   less_int_def: "(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 
   109 text{* The integers form a @{text comm_ring_1}*}
   110 
   111 instance int :: comm_ring_1
   112 proof
   113   fix i j k :: int
   114   show "(i + j) + k = i + (j + k)"
   115     by (descending) (auto)
   116   show "i + j = j + i"
   117     by (descending) (auto)
   118   show "0 + i = (i::int)"
   119     by (descending) (auto)
   120   show "- i + i = 0"
   121     by (descending) (auto)
   122   show "i - j = i + - j"
   123     by (simp add: minus_int_def)
   124   show "(i * j) * k = i * (j * k)"
   125     by (descending) (auto simp add: algebra_simps)
   126   show "i * j = j * i"
   127     by (descending) (auto)
   128   show "1 * i = i"
   129     by (descending) (auto)
   130   show "(i + j) * k = i * k + j * k"
   131     by (descending) (auto simp add: algebra_simps)
   132   show "0 \<noteq> (1::int)"
   133     by (descending) (auto)
   134 qed
   135 
   136 lemma plus_int_raw_rsp_aux:
   137   assumes a: "a \<approx> b" "c \<approx> d"
   138   shows "plus_int_raw a c \<approx> plus_int_raw b d"
   139   using a
   140   by (cases a, cases b, cases c, cases d)
   141      (simp)
   142 
   143 lemma add_abs_int:
   144   "(abs_int (x,y)) + (abs_int (u,v)) =
   145    (abs_int (x + u, y + v))"
   146   apply(simp add: plus_int_def id_simps)
   147   apply(fold plus_int_raw.simps)
   148   apply(rule Quotient3_rel_abs[OF Quotient3_int])
   149   apply(rule plus_int_raw_rsp_aux)
   150   apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int])
   151   done
   152 
   153 definition int_of_nat_raw:
   154   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
   155 
   156 quotient_definition
   157   "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" done
   158 
   159 lemma int_of_nat:
   160   shows "of_nat m = int_of_nat m"
   161   by (induct m)
   162      (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
   163 
   164 instance int :: linorder
   165 proof
   166   fix i j k :: int
   167   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
   168     by (descending) (auto)
   169   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
   170     by (auto simp add: less_int_def dest: antisym)
   171   show "i \<le> i"
   172     by (descending) (auto)
   173   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   174     by (descending) (auto)
   175   show "i \<le> j \<or> j \<le> i"
   176     by (descending) (auto)
   177 qed
   178 
   179 instantiation int :: distrib_lattice
   180 begin
   181 
   182 definition
   183   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
   184 
   185 definition
   186   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
   187 
   188 instance
   189   by default
   190      (auto simp add: inf_int_def sup_int_def max_min_distrib2)
   191 
   192 end
   193 
   194 instance int :: ordered_cancel_ab_semigroup_add
   195 proof
   196   fix i j k :: int
   197   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   198     by (descending) (auto)
   199 qed
   200 
   201 abbreviation
   202   "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
   203 
   204 lemma zmult_zless_mono2_lemma:
   205   fixes i j::int
   206   and   k::nat
   207   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
   208   apply(induct "k")
   209   apply(simp)
   210   apply(case_tac "k = 0")
   211   apply(simp_all add: distrib_right add_strict_mono)
   212   done
   213 
   214 lemma zero_le_imp_eq_int_raw:
   215   fixes k::"(nat \<times> nat)"
   216   shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
   217   apply(cases k)
   218   apply(simp add:int_of_nat_raw)
   219   apply(auto)
   220   apply(rule_tac i="b" and j="a" in less_Suc_induct)
   221   apply(auto)
   222   done
   223 
   224 lemma zero_le_imp_eq_int:
   225   fixes k::int
   226   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
   227   unfolding less_int_def int_of_nat
   228   by (descending) (rule zero_le_imp_eq_int_raw)
   229 
   230 lemma zmult_zless_mono2:
   231   fixes i j k::int
   232   assumes a: "i < j" "0 < k"
   233   shows "k * i < k * j"
   234   using a
   235   by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
   236 
   237 text{*The integers form an ordered integral domain*}
   238 
   239 instance int :: linordered_idom
   240 proof
   241   fix i j k :: int
   242   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   243     by (rule zmult_zless_mono2)
   244   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   245     by (simp only: zabs_def)
   246   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   247     by (simp only: zsgn_def)
   248 qed
   249 
   250 lemmas int_distrib =
   251   distrib_right [of z1 z2 w]
   252   distrib_left [of w z1 z2]
   253   left_diff_distrib [of z1 z2 w]
   254   right_diff_distrib [of w z1 z2]
   255   minus_add_distrib[of z1 z2]
   256   for z1 z2 w :: int
   257 
   258 lemma int_induct2:
   259   assumes "P 0 0"
   260   and     "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
   261   and     "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
   262   shows   "P n m"
   263 using assms
   264 by (induction_schema) (pat_completeness, lexicographic_order)
   265 
   266 
   267 lemma int_induct:
   268   fixes j :: int
   269   assumes a: "P 0"
   270   and     b: "\<And>i::int. P i \<Longrightarrow> P (i + 1)"
   271   and     c: "\<And>i::int. P i \<Longrightarrow> P (i - 1)"
   272   shows      "P j"
   273 using a b c 
   274 unfolding minus_int_def
   275 by (descending) (auto intro: int_induct2)
   276   
   277 
   278 text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
   279 
   280 definition
   281   "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
   282 
   283 quotient_definition
   284   "int_to_nat::int \<Rightarrow> nat"
   285 is
   286   "int_to_nat_raw" 
   287 unfolding int_to_nat_raw_def by auto 
   288 
   289 lemma nat_le_eq_zle:
   290   fixes w z::"int"
   291   shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
   292   unfolding less_int_def
   293   by (descending) (auto simp add: int_to_nat_raw_def)
   294 
   295 end