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