author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48891  c0eafbd55de3 
permissions  rwrr 
23146  1 

2 
theory IntArith imports Bin 

27237  3 
begin 
4 

5 

6 
(** To simplify inequalities involving integer negation and literals, 

7 
such as x = #3 

8 
**) 

9 

10 
lemmas [simp] = 

45602  11 
zminus_equation [where y = "integ_of(w)"] 
12 
equation_zminus [where x = "integ_of(w)"] 

13 
for w 

27237  14 

15 
lemmas [iff] = 

45602  16 
zminus_zless [where y = "integ_of(w)"] 
17 
zless_zminus [where x = "integ_of(w)"] 

18 
for w 

27237  19 

20 
lemmas [iff] = 

45602  21 
zminus_zle [where y = "integ_of(w)"] 
22 
zle_zminus [where x = "integ_of(w)"] 

23 
for w 

27237  24 

25 
lemmas [simp] = 

45602  26 
Let_def [where s = "integ_of(w)"] for w 
27237  27 

28 

29 
(*** Simprocs for numeric literals ***) 

30 

31 
(** Combining of literal coefficients in sums of products **) 

32 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

33 
lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$y $< #0)" 
27237  34 
by (simp add: zcompare_rls) 
35 

46953  36 
lemma eq_iff_zdiff_eq_0: "[ x \<in> int; y \<in> int ] ==> (x = y) \<longleftrightarrow> (x$y = #0)" 
27237  37 
by (simp add: zcompare_rls) 
38 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

39 
lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$y $<= #0)" 
27237  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 = 

45602  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"] 

27237  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] 

45602  58 
for u v (* FIXME n (!?) *) 
27237  59 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

60 
lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$j)$*u $+ m = intify(n))" 
27237  61 
apply (simp add: zdiff_def zadd_zmult_distrib) 
62 
apply (simp add: zcompare_rls) 

63 
apply (simp add: zadd_ac) 

64 
done 

65 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

66 
lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$i)$*u $+ n)" 
27237  67 
apply (simp add: zdiff_def zadd_zmult_distrib) 
68 
apply (simp add: zcompare_rls) 

69 
apply (simp add: zadd_ac) 

70 
done 

71 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

72 
lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$j)$*u $+ m $< n)" 
27237  73 
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) 
74 
done 

75 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

76 
lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$i)$*u $+ n)" 
27237  77 
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) 
78 
done 

79 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

80 
lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$j)$*u $+ m $<= n)" 
27237  81 
apply (simp add: zdiff_def zadd_zmult_distrib) 
82 
apply (simp add: zcompare_rls) 

83 
apply (simp add: zadd_ac) 

84 
done 

85 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
45602
diff
changeset

86 
lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$i)$*u $+ n)" 
27237  87 
apply (simp add: zdiff_def zadd_zmult_distrib) 
88 
apply (simp add: zcompare_rls) 

89 
apply (simp add: zadd_ac) 

90 
done 

91 

48891  92 
ML_file "int_arith.ML" 
23146  93 

94 
end 