src/ZF/IntArith.thy
author wenzelm
Fri Jun 10 12:51:29 2011 +0200 (2011-06-10)
changeset 43348 3e153e719039
parent 27237 c94eefffc3a5
child 45602 2a858377c3d2
permissions -rw-r--r--
uniform use of flexflex_rule;
wenzelm@23146
     1
wenzelm@23146
     2
theory IntArith imports Bin
wenzelm@27237
     3
uses ("int_arith.ML")
wenzelm@27237
     4
begin
wenzelm@27237
     5
wenzelm@27237
     6
wenzelm@27237
     7
(** To simplify inequalities involving integer negation and literals,
wenzelm@27237
     8
    such as -x = #3
wenzelm@27237
     9
**)
wenzelm@27237
    10
wenzelm@27237
    11
lemmas [simp] =
wenzelm@27237
    12
  zminus_equation [where y = "integ_of(w)", standard]
wenzelm@27237
    13
  equation_zminus [where x = "integ_of(w)", standard]
wenzelm@27237
    14
wenzelm@27237
    15
lemmas [iff] =
wenzelm@27237
    16
  zminus_zless [where y = "integ_of(w)", standard]
wenzelm@27237
    17
  zless_zminus [where x = "integ_of(w)", standard]
wenzelm@27237
    18
wenzelm@27237
    19
lemmas [iff] =
wenzelm@27237
    20
  zminus_zle [where y = "integ_of(w)", standard]
wenzelm@27237
    21
  zle_zminus [where x = "integ_of(w)", standard]
wenzelm@27237
    22
wenzelm@27237
    23
lemmas [simp] =
wenzelm@27237
    24
  Let_def [where s = "integ_of(w)", standard]
wenzelm@27237
    25
wenzelm@27237
    26
wenzelm@27237
    27
(*** Simprocs for numeric literals ***)
wenzelm@27237
    28
wenzelm@27237
    29
(** Combining of literal coefficients in sums of products **)
wenzelm@27237
    30
wenzelm@27237
    31
lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)"
wenzelm@27237
    32
  by (simp add: zcompare_rls)
wenzelm@27237
    33
wenzelm@27237
    34
lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"
wenzelm@27237
    35
  by (simp add: zcompare_rls)
wenzelm@27237
    36
wenzelm@27237
    37
lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)"
wenzelm@27237
    38
  by (simp add: zcompare_rls)
wenzelm@27237
    39
wenzelm@27237
    40
wenzelm@27237
    41
(** For combine_numerals **)
wenzelm@27237
    42
wenzelm@27237
    43
lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
wenzelm@27237
    44
  by (simp add: zadd_zmult_distrib zadd_ac)
wenzelm@27237
    45
wenzelm@27237
    46
wenzelm@27237
    47
(** For cancel_numerals **)
wenzelm@27237
    48
wenzelm@27237
    49
lemmas rel_iff_rel_0_rls =
wenzelm@27237
    50
  zless_iff_zdiff_zless_0 [where y = "u $+ v", standard]
wenzelm@27237
    51
  eq_iff_zdiff_eq_0 [where y = "u $+ v", standard]
wenzelm@27237
    52
  zle_iff_zdiff_zle_0 [where y = "u $+ v", standard]
wenzelm@27237
    53
  zless_iff_zdiff_zless_0 [where y = n]
wenzelm@27237
    54
  eq_iff_zdiff_eq_0 [where y = n]
wenzelm@27237
    55
  zle_iff_zdiff_zle_0 [where y = n]
wenzelm@27237
    56
wenzelm@27237
    57
lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
wenzelm@27237
    58
  apply (simp add: zdiff_def zadd_zmult_distrib)
wenzelm@27237
    59
  apply (simp add: zcompare_rls)
wenzelm@27237
    60
  apply (simp add: zadd_ac)
wenzelm@27237
    61
  done
wenzelm@27237
    62
wenzelm@27237
    63
lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"
wenzelm@27237
    64
  apply (simp add: zdiff_def zadd_zmult_distrib)
wenzelm@27237
    65
  apply (simp add: zcompare_rls)
wenzelm@27237
    66
  apply (simp add: zadd_ac)
wenzelm@27237
    67
  done
wenzelm@27237
    68
wenzelm@27237
    69
lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"
wenzelm@27237
    70
  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
wenzelm@27237
    71
  done
wenzelm@27237
    72
wenzelm@27237
    73
lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"
wenzelm@27237
    74
  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
wenzelm@27237
    75
  done
wenzelm@27237
    76
wenzelm@27237
    77
lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"
wenzelm@27237
    78
  apply (simp add: zdiff_def zadd_zmult_distrib)
wenzelm@27237
    79
  apply (simp add: zcompare_rls)
wenzelm@27237
    80
  apply (simp add: zadd_ac)
wenzelm@27237
    81
  done
wenzelm@27237
    82
wenzelm@27237
    83
lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"
wenzelm@27237
    84
  apply (simp add: zdiff_def zadd_zmult_distrib)
wenzelm@27237
    85
  apply (simp add: zcompare_rls)
wenzelm@27237
    86
  apply (simp add: zadd_ac)
wenzelm@27237
    87
  done
wenzelm@27237
    88
wenzelm@27237
    89
use "int_arith.ML"
wenzelm@23146
    90
wenzelm@23146
    91
end