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