29 |
29 |
30 (*** Simprocs for numeric literals ***) |
30 (*** Simprocs for numeric literals ***) |
31 |
31 |
32 (** Combining of literal coefficients in sums of products **) |
32 (** Combining of literal coefficients in sums of products **) |
33 |
33 |
34 lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)" |
34 lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)" |
35 by (simp add: zcompare_rls) |
35 by (simp add: zcompare_rls) |
36 |
36 |
37 lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)" |
37 lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)" |
38 by (simp add: zcompare_rls) |
38 by (simp add: zcompare_rls) |
39 |
39 |
40 lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)" |
40 lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)" |
41 by (simp add: zcompare_rls) |
41 by (simp add: zcompare_rls) |
42 |
42 |
43 |
43 |
44 (** For combine_numerals **) |
44 (** For combine_numerals **) |
45 |
45 |
56 zless_iff_zdiff_zless_0 [where y = n] |
56 zless_iff_zdiff_zless_0 [where y = n] |
57 eq_iff_zdiff_eq_0 [where y = n] |
57 eq_iff_zdiff_eq_0 [where y = n] |
58 zle_iff_zdiff_zle_0 [where y = n] |
58 zle_iff_zdiff_zle_0 [where y = n] |
59 for u v (* FIXME n (!?) *) |
59 for u v (* FIXME n (!?) *) |
60 |
60 |
61 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))" |
61 lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))" |
62 apply (simp add: zdiff_def zadd_zmult_distrib) |
62 apply (simp add: zdiff_def zadd_zmult_distrib) |
63 apply (simp add: zcompare_rls) |
63 apply (simp add: zcompare_rls) |
64 apply (simp add: zadd_ac) |
64 apply (simp add: zadd_ac) |
65 done |
65 done |
66 |
66 |
67 lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)" |
67 lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)" |
68 apply (simp add: zdiff_def zadd_zmult_distrib) |
68 apply (simp add: zdiff_def zadd_zmult_distrib) |
69 apply (simp add: zcompare_rls) |
69 apply (simp add: zcompare_rls) |
70 apply (simp add: zadd_ac) |
70 apply (simp add: zadd_ac) |
71 done |
71 done |
72 |
72 |
73 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)" |
73 lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)" |
74 apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) |
74 apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) |
75 done |
75 done |
76 |
76 |
77 lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)" |
77 lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)" |
78 apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) |
78 apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) |
79 done |
79 done |
80 |
80 |
81 lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)" |
81 lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $<= n)" |
82 apply (simp add: zdiff_def zadd_zmult_distrib) |
82 apply (simp add: zdiff_def zadd_zmult_distrib) |
83 apply (simp add: zcompare_rls) |
83 apply (simp add: zcompare_rls) |
84 apply (simp add: zadd_ac) |
84 apply (simp add: zadd_ac) |
85 done |
85 done |
86 |
86 |
87 lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)" |
87 lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)" |
88 apply (simp add: zdiff_def zadd_zmult_distrib) |
88 apply (simp add: zdiff_def zadd_zmult_distrib) |
89 apply (simp add: zcompare_rls) |
89 apply (simp add: zcompare_rls) |
90 apply (simp add: zadd_ac) |
90 apply (simp add: zadd_ac) |
91 done |
91 done |
92 |
92 |