author | chaieb |
Wed, 06 Oct 2004 13:58:56 +0200 | |
changeset 15232 | 388a6f431d83 |
child 15239 | fb73c8154b19 |
permissions | -rwxr-xr-x |
15232
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
1 |
theory Barith = Presburger |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
2 |
files ("barith.ML") : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
3 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
4 |
lemma imp_commute: "(PROP P ==> PROP Q |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
5 |
==> PROP R) == (PROP Q ==> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
6 |
PROP P ==> PROP R)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
7 |
proof |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
8 |
assume h1: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
9 |
PROP R" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
10 |
assume h2: "PROP Q" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
11 |
assume h3: "PROP P" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
12 |
from h3 h2 show "PROP R" by (rule h1) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
13 |
next |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
14 |
assume h1: "PROP Q \<Longrightarrow> PROP P \<Longrightarrow> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
15 |
PROP R" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
16 |
assume h2: "PROP P" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
17 |
assume h3: "PROP Q" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
18 |
from h3 h2 show "PROP R" by (rule h1) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
19 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
20 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
21 |
lemma imp_simplify: "(PROP P \<Longrightarrow> PROP P |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
22 |
\<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
23 |
PROP Q)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
24 |
proof |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
25 |
assume h1: "PROP P \<Longrightarrow> PROP P \<Longrightarrow> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
26 |
PROP Q" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
27 |
assume h2: "PROP P" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
28 |
from h2 h2 show "PROP Q" by (rule h1) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
29 |
next |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
30 |
assume h: "PROP P \<Longrightarrow> PROP Q" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
31 |
assume "PROP P" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
32 |
then show "PROP Q" by (rule h) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
33 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
34 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
35 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
36 |
(* Abstraction of constants *) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
37 |
lemma abs_const: "(x::int) <= x \<and> x <= x" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
38 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
39 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
40 |
(* Abstraction of Variables *) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
41 |
lemma abs_var: "l <= (x::int) \<and> x <= u \<Longrightarrow> l <= (x::int) \<and> x <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
42 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
43 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
44 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
45 |
(* Unary operators *) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
46 |
lemma abs_neg: "l <= (x::int) \<and> x <= u \<Longrightarrow> -u <= -x \<and> -x <= -l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
47 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
48 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
49 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
50 |
(* Binary operations *) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
51 |
(* Addition*) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
52 |
lemma abs_add: "\<lbrakk> l1 <= (x1::int) \<and> x1 <= u1 ; l2 <= (x2::int) \<and> x2 <= u2\<rbrakk> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
53 |
\<Longrightarrow> l1 + l2 <= x1 + x2 \<and> x1 + x2 <= u1 + u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
54 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
55 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
56 |
lemma abs_sub: "\<lbrakk> l1 <= (x1::int) \<and> x1 <= u1 ; l2 <= (x2::int) \<and> x2 <= u2\<rbrakk> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
57 |
\<Longrightarrow> l1 - u2 <= x1 - x2 \<and> x1 - x2 <= u1 - l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
58 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
59 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
60 |
lemma abs_sub_x: "l <= (x::int) \<and> x <= u \<Longrightarrow> 0 <= x - x \<and> x - x <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
61 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
62 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
63 |
(* For resolving the last step*) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
64 |
lemma subinterval: "\<lbrakk>l <= (e::int) \<and> e <= u ; l' <= l ; u <= u' \<rbrakk> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
65 |
\<Longrightarrow> l' <= e \<and> e <= u'" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
66 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
67 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
68 |
lemma min_max_minus : "min (-a ::int) (-b) = - max a b" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
69 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
70 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
71 |
lemma max_min_minus : " max (-a ::int) (-b) = - min a b" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
72 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
73 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
74 |
lemma max_max_commute : "max (max (a::int) b) (max c d) = max (max a c) (max b d)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
75 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
76 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
77 |
lemma min_min_commute : "min (min (a::int) b) (min c d) = min (min a c) (min b d)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
78 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
79 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
80 |
lemma zintervals_min: "\<lbrakk> l1 <= (x1::int) \<and> x1<= u1 ; l2 <= x2 \<and> x2 <= u2 \<rbrakk> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
81 |
\<Longrightarrow> min l1 l2 <= x1 \<and> x1 <= max u1 u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
82 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
83 |
lemma zmult_zle_mono: "(i::int) \<le> j \<Longrightarrow> 0 \<le> k \<Longrightarrow> k * i \<le> k * j" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
84 |
apply (erule order_le_less [THEN iffD1, THEN disjE, of "0::int"]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
85 |
apply (erule order_le_less [THEN iffD1, THEN disjE]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
86 |
apply (rule order_less_imp_le) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
87 |
apply (rule zmult_zless_mono2) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
88 |
apply simp_all |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
89 |
done |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
90 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
91 |
lemma zmult_mono: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
92 |
assumes l1_pos : "0 <= l1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
93 |
and l2_pos : "0 <= l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
94 |
and l1_le : "l1 <= (x1::int)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
95 |
and l2_le : "l2 <= (x2::int)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
96 |
shows "l1*l2 <= x1*x2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
97 |
proof - |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
98 |
from l1_pos and l1_le have x1_pos: "0 \<le> x1" by (rule order_trans) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
99 |
from l1_le and l2_pos |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
100 |
have "l2 * l1 \<le> l2 * x1" by (rule zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
101 |
then have "l1 * l2 \<le> x1 * l2" by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
102 |
also from l2_le and x1_pos |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
103 |
have "x1 * l2 \<le> x1 * x2" by (rule zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
104 |
finally show ?thesis . |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
105 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
106 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
107 |
lemma zinterval_lposlpos: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
108 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
109 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
110 |
and l1_pos : "0 <= l1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
111 |
and l2_pos : "0 <= l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
112 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
113 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
114 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
115 |
from x1_lu have l1_le : "l1 <= x1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
116 |
from x1_lu have x1_le : "x1 <= u1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
117 |
from x2_lu have l2_le : "l2 <= x2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
118 |
from x2_lu have x2_le : "x2 <= u2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
119 |
from x1_lu have l1_leu : "l1 <= u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
120 |
from x2_lu have l2_leu : "l2 <= u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
121 |
from l1_pos l2_pos l1_le l2_le |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
122 |
have l1l2_le : "l1*l2 <= x1*x2" by (simp add: zmult_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
123 |
from l1_pos x1_lu have x1_pos : "0 <= x1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
124 |
from l2_pos x2_lu have x2_pos : "0 <= x2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
125 |
from l1_pos x1_lu have u1_pos : "0 <= u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
126 |
from l2_pos x2_lu have u2_pos : "0 <= u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
127 |
from x1_pos x2_pos x1_le x2_le |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
128 |
have x1x2_le : "x1*x2 <= u1*u2" by (simp add: zmult_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
129 |
from l2_leu l1_pos have l1l2_leu2 : "l1*l2 <= l1*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
130 |
by (simp add: zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
131 |
from l1l2_leu2 have min1 : "l1*l2 = min (l1*l2) (l1*u2)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
132 |
from l2_leu u1_pos have u1l2_le : "u1*l2 <=u1*u2" by (simp add: zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
133 |
from u1l2_le have min2 : "u1*l2 = min (u1*l2) (u1*u2)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
134 |
from l1_leu l2_pos have "l2*l1 <= l2*u1" by (simp add:zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
135 |
then have l1l2_le_u1l2 : "l1*l2 <= u1*l2" by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
136 |
from min1 min2 l1l2_le_u1l2 have min_th : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
137 |
"min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) = (l1*l2)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
138 |
from l1l2_leu2 have max1 : "l1*u2 = max (l1*l2) (l1*u2)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
139 |
from u1l2_le have max2 : "u1*u2 = max (u1*l2) (u1*u2)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
140 |
from l1_leu u2_pos have "u2*l1 <= u2*u1" by (simp add:zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
141 |
then have l1u2_le_u1u2 : "l1*u2 <= u1*u2" by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
142 |
from max1 max2 l1u2_le_u1u2 have max_th : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
143 |
"max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2)) = (u1*u2)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
144 |
from min_th have min_th' : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= l1*l2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
145 |
from max_th have max_th' : "u1*u2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
146 |
from min_th' max_th' l1l2_le x1x2_le |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
147 |
show ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
148 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
149 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
150 |
lemma min_le_I1 : "min (a::int) b <= a" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
151 |
lemma min_le_I2 : "min (a::int) b <= b" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
152 |
lemma zinterval_lneglpos : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
153 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
154 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
155 |
and l1_neg : "l1 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
156 |
and x1_pos : "0 <= x1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
157 |
and l2_pos : "0 <= l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
158 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
159 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
160 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
161 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
162 |
from x1_lu x1_pos have x1_0_u1 : "0 <= x1 \<and> x1 <= u1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
163 |
from l1_neg have ml1_pos : "0 <= -l1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
164 |
from x1_lu x1_pos have u1_pos : "0 <= u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
165 |
from x2_lu l2_pos have u2_pos : "0 <= u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
166 |
from x2_lu have l2_le_u2 : "l2 <= u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
167 |
from l2_le_u2 u1_pos |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
168 |
have u1l2_le_u1u2 : "u1*l2 <= u1*u2" by (simp add: zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
169 |
have trv_0 : "(0::int) <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
170 |
have "0*0 <= u1*l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
171 |
by (simp only: zmult_mono[OF trv_0 trv_0 u1_pos l2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
172 |
then have u1l2_pos : "0 <= u1*l2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
173 |
from l1_neg have ml1_pos : "0 <= -l1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
174 |
from ml1_pos l2_pos have "0*0 <= (-l1)*l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
175 |
by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos l2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
176 |
then have "0 <= -(l1*l2)" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
177 |
then have "0 - (-(l1*l2)) <= 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
178 |
then |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
179 |
have l1l2_neg : "l1*l2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
180 |
from ml1_pos u2_pos have "0*0 <= (-l1)*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
181 |
by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos u2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
182 |
then have "0 <= -(l1*u2)" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
183 |
then have "0 - (-(l1*u2)) <= 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
184 |
then |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
185 |
have l1u2_neg : "l1*u2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
186 |
from l1l2_neg u1l2_pos have l1l2_le_u1l2: "l1*l2 <= u1*l2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
187 |
from l1u2_neg u1l2_pos have l1u2_le_u1l2 : "l1*u2 <= u1*l2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
188 |
from ml1_pos l2_le_u2 have "(-l1)*l2 <= (-l1)*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
189 |
by (simp only: zmult_zle_mono) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
190 |
then have l1u2_le_l1l2 : "l1*u2 <= l1*l2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
191 |
from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
192 |
have min1 : "l1*u2 = min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
193 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
194 |
from u1l2_pos u1l2_le_u1u2 have "0 = min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
195 |
with l1u2_neg min1 have minth : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2))" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
196 |
from l1u2_le_l1l2 l1l2_le_u1l2 u1l2_le_u1u2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
197 |
have max1 : "u1*u2 = max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
198 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
199 |
from u1l2_pos u1l2_le_u1u2 have "u1*u2 = max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
200 |
with max1 have "max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2)) = max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
201 |
then have maxth : " max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2)) <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
202 |
have x1x2_0_u : "min (min (0 * l2) (0 * u2)) (min (u1 * l2) (u1 * u2)) <= x1 * x2 & |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
203 |
x1 * x2 <= max (max (0 * l2) (0 * u2)) (max (u1 * l2) (u1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
204 |
by (simp only: zinterval_lposlpos[OF x1_0_u1 x2_lu trv_0 l2_pos],simp) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
205 |
from minth maxth x1x2_0_u show ?thesis by (simp add: subinterval[OF _ minth maxth]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
206 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
207 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
208 |
lemma zinterval_lneglneg : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
209 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
210 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
211 |
and l1_neg : "l1 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
212 |
and x1_pos : "0 <= x1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
213 |
and l2_neg : "l2 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
214 |
and x2_pos : "0 <= x2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
215 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
216 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
217 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
218 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
219 |
from x1_lu x1_pos have x1_0_u1 : "0 <= x1 \<and> x1 <= u1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
220 |
from l1_neg have ml1_pos : "0 <= -l1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
221 |
from l1_neg have l1_le0 : "l1 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
222 |
from x1_lu x1_pos have u1_pos : "0 <= u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
223 |
from x2_lu x2_pos have x2_0_u2 : "0 <= x2 \<and> x2 <= u2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
224 |
from l2_neg have ml2_pos : "0 <= -l2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
225 |
from l2_neg have l2_le0 : "l2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
226 |
from x2_lu x2_pos have u2_pos : "0 <= u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
227 |
have trv_0 : "(0::int) <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
228 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
229 |
have x1x2_th1 : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
230 |
"min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2)) \<le> x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
231 |
x1 * x2 \<le> max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
232 |
by (rule_tac zinterval_lneglpos[OF x1_lu x2_0_u2 l1_le0 x1_pos trv_0]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
233 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
234 |
have x1x2_eq_x2x1 : "x1*x2 = x2*x1" by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
235 |
have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
236 |
"min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x2 * x1 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
237 |
x2 * x1 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
238 |
by (rule_tac zinterval_lneglpos[OF x2_lu x1_0_u1 l2_le0 x2_pos trv_0]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
239 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
240 |
then have x1x2_th2 : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
241 |
"min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)) \<le> x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
242 |
x1 * x2 \<le> max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
243 |
by (simp add: x1x2_eq_x2x1) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
244 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
245 |
from x1x2_th1 x1x2_th2 have x1x2_th3: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
246 |
"min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2))) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
247 |
(min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1))) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
248 |
\<le> x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
249 |
x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
250 |
\<le> max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2))) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
251 |
(max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1)))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
252 |
by (rule_tac zintervals_min[OF x1x2_th1 x1x2_th2]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
253 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
254 |
from ml1_pos u2_pos |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
255 |
have "0*0 <= -l1*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
256 |
by (simp only: zmult_mono[OF trv_0 trv_0 ml1_pos u2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
257 |
then have l1u2_neg : "l1*u2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
258 |
from l1u2_neg have min_l1u2_0 : "min (0) (l1*u2) = l1*u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
259 |
from l1u2_neg have max_l1u2_0 : "max (0) (l1*u2) = 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
260 |
from u1_pos u2_pos |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
261 |
have "0*0 <= u1*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
262 |
by (simp only: zmult_mono[OF trv_0 trv_0 u1_pos u2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
263 |
then have u1u2_pos :"0 <= u1*u2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
264 |
from u1u2_pos have min_0_u1u2 : "min 0 (u1*u2) = 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
265 |
from u1u2_pos have max_0_u1u2 : "max 0 (u1*u2) = u1*u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
266 |
from ml2_pos u1_pos have "0*0 <= -l2*u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
267 |
by (simp only: zmult_mono[OF trv_0 trv_0 ml2_pos u1_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
268 |
then have l2u1_neg : "l2*u1 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
269 |
from l2u1_neg have min_l2u1_0 : "min 0 (l2*u1) = l2*u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
270 |
from l2u1_neg have max_l2u1_0 : "max 0 (l2*u1) = 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
271 |
from min_l1u2_0 min_0_u1u2 min_l2u1_0 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
272 |
have min_th1: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
273 |
" min (l2*u1) (l1*u2) <= min (min (min (l1 * 0) (l1 * u2)) (min (u1 * 0) (u1 * u2))) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
274 |
(min (min (l2 * 0) (l2 * u1)) (min (u2 * 0) (u2 * u1)))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
275 |
by (simp add: min_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
276 |
from max_l1u2_0 max_0_u1u2 max_l2u1_0 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
277 |
have max_th1: "max (max (max (l1 * 0) (l1 * u2)) (max (u1 * 0) (u1 * u2))) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
278 |
(max (max (l2 * 0) (l2 * u1)) (max (u2 * 0) (u2 * u1))) <= u1*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
279 |
by (simp add: max_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
280 |
have x1x2_th4: "min (l2*u1) (l1*u2) <= x1*x2 \<and> x1*x2 <= u1*u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
281 |
by (rule_tac subinterval[OF x1x2_th3 min_th1 max_th1]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
282 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
283 |
have " min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) = min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1))" by (simp add: min_min_commute min_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
284 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
285 |
have " min (min (l1*l2) (u1*u2)) (min (l1*u2) (l2*u1)) <= min (l1*u2) (l2*u1)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
286 |
by |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
287 |
(rule_tac min_le_I2 [of "(min (l1*l2) (u1*u2))" "(min (l1*u2) (l2*u1))"]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
288 |
ultimately have "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= min (l1*u2) (l2*u1)" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
289 |
then |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
290 |
have min_le1: "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <=min (l2*u1) (l1*u2)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
291 |
by (simp add: min_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
292 |
have "u1*u2 <= max (u1*l2) (u1*u2)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
293 |
by (rule_tac le_maxI2[of "u1*u2" "u1*l2"]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
294 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
295 |
moreover have "max (u1*l2) (u1*u2) <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
296 |
by(rule_tac le_maxI2[of "(max (u1*l2) (u1*u2))" "(max (l1*l2) (l1*u2))"]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
297 |
then |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
298 |
have max_le1:"u1*u2 <= max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
299 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
300 |
show ?thesis by (simp add: subinterval[OF x1x2_th4 min_le1 max_le1]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
301 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
302 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
303 |
lemma zinterval_lpos: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
304 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
305 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
306 |
and l1_pos: "0 <= l1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
307 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
308 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
309 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
310 |
from x1_lu have l1_le : "l1 <= x1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
311 |
from x1_lu have x1_le : "x1 <= u1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
312 |
from x2_lu have l2_le : "l2 <= x2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
313 |
from x2_lu have x2_le : "x2 <= u2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
314 |
from x1_lu have l1_leu : "l1 <= u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
315 |
from x2_lu have l2_leu : "l2 <= u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
316 |
have "(0 <= l2) \<or> (l2 < 0 \<and> 0<= x2) \<or> (x2 <0 \<and> 0 <= u2) \<or> (u2 <0)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
317 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
318 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
319 |
assume l2_pos: "0 <= l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
320 |
have ?thesis by (simp add: zinterval_lposlpos[OF x1_lu x2_lu l1_pos l2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
321 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
322 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
323 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
324 |
assume l2_neg : "l2 < 0" and x2_pos: "0<= x2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
325 |
from l2_neg have l2_le_0 : "l2 <= 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
326 |
thm zinterval_lneglpos[OF x2_lu x1_lu l2_le_0 x2_pos l1_pos] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
327 |
have th1 : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
328 |
"min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
329 |
x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
330 |
by (simp add : zinterval_lneglpos[OF x2_lu x1_lu l2_le_0 x2_pos l1_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
331 |
have mth1 : "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) = min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
332 |
by (simp add: min_min_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
333 |
have mth2: "max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1)) = max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
334 |
by (simp add: max_max_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
335 |
have x1x2_th : "x2*x1 = x1*x2" by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
336 |
from th1 mth1 mth2 x1x2_th have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
337 |
"min (min (l1 * l2) (l1 * u2)) (min (u1 * l2) (u1 * u2)) \<le> x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
338 |
x1 * x2 \<le> max (max (l1 * l2) (l1 * u2)) (max (u1 * l2) (u1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
339 |
by auto |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
340 |
then have ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
341 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
342 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
343 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
344 |
assume x2_neg : "x2 <0" and u2_pos : "0 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
345 |
from x2_lu x2_neg have mx2_mu2_ml2 : "-u2 <= -x2 \<and> -x2 <= -l2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
346 |
from u2_pos have mu2_neg : "-u2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
347 |
from x2_neg have mx2_pos : "0 <= -x2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
348 |
thm zinterval_lneglpos[OF mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
349 |
have mx1x2_lu : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
350 |
"min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
351 |
\<le> - x2 * x1 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
352 |
- x2 * x1 \<le> max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
353 |
by (simp only: zinterval_lneglpos [OF mx2_mu2_ml2 x1_lu mu2_neg mx2_pos l1_pos],simp) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
354 |
have min_eq_mmax : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
355 |
"min (min (- u2 * l1) (- u2 * u1)) (min (- l2 * l1) (- l2 * u1)) = |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
356 |
- max (max (u2 * l1) (u2 * u1)) (max (l2 * l1) (l2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
357 |
by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
358 |
have max_eq_mmin : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
359 |
" max (max (- u2 * l1) (- u2 * u1)) (max (- l2 * l1) (- l2 * u1)) = |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
360 |
-min (min (u2 * l1) (u2 * u1)) (min (l2 * l1) (l2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
361 |
by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
362 |
from mx1x2_lu min_eq_mmax max_eq_mmin |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
363 |
have "- max (max (u2 * l1) (u2 * u1)) (max (l2 * l1) (l2 * u1))<= - x1 * x2 & |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
364 |
- x1*x2 <= -min (min (u2 * l1) (u2 * u1)) (min (l2 * l1) (l2 * u1))" by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
365 |
then have ?thesis by (simp add: min_min_commute min_commute max_commute max_max_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
366 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
367 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
368 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
369 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
370 |
assume u2_neg : "u2 < 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
371 |
from x2_lu have mx2_lu : "-u2 <= -x2 \<and> -x2 <= -l2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
372 |
from u2_neg have mu2_pos : "0 <= -u2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
373 |
thm zinterval_lposlpos [OF x1_lu mx2_lu l1_pos mu2_pos] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
374 |
have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
375 |
\<le> x1 * - x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
376 |
x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
377 |
" by (rule_tac zinterval_lposlpos [OF x1_lu mx2_lu l1_pos mu2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
378 |
then have mx1x2_lu: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
379 |
"min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) \<le> - x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
380 |
- x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
381 |
" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
382 |
moreover have "min (min (-l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) =- max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2)) " |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
383 |
by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
384 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
385 |
have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
386 |
"max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) = - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
387 |
by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
388 |
thm subinterval[OF mx1x2_lu] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
389 |
ultimately have "- max (max (l1 * u2) ( l1 * l2)) (max ( u1 * u2) ( u1 * l2))\<le> - x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
390 |
- x1 * x2 \<le> - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2)) " by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
391 |
then have ?thesis by (simp add: max_commute min_commute) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
392 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
393 |
ultimately show ?thesis by blast |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
394 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
395 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
396 |
lemma zinterval_uneg : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
397 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
398 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
399 |
and u1_neg: "u1 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
400 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
401 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
402 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
403 |
from x1_lu have mx1_lu : "-u1 <= -x1 \<and> -x1 <= -l1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
404 |
from u1_neg have mu1_pos : "0 <= -u1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
405 |
thm zinterval_lpos [OF mx1_lu x2_lu mu1_pos] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
406 |
have mx1x2_lu : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
407 |
"min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
408 |
\<le> - x1 * x2 \<and> - x1 * x2 \<le> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
409 |
max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
410 |
by (rule_tac zinterval_lpos [OF mx1_lu x2_lu mu1_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
411 |
moreover have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
412 |
"min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) = - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))" by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
413 |
moreover have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
414 |
"max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) = - min (min (u1 * l2) ( u1 * u2)) (min (l1 * l2) (l1 * u2))" by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
415 |
ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))\<le> - x1 * x2 \<and> - x1 * x2 \<le> - min (min (u1 * l2) ( u1 * u2)) (min (l1 * l2) (l1 * u2))" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
416 |
then show ?thesis by (simp add: min_commute max_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
417 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
418 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
419 |
lemma zinterval_lnegxpos: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
420 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
421 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
422 |
and l1_neg: "l1 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
423 |
and x1_pos: "0<= x1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
424 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
425 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
426 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
427 |
have "(0 <= l2) \<or> (l2 < 0 \<and> 0<= x2) \<or> (x2 <0 \<and> 0 <= u2) \<or> (u2 <= 0)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
428 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
429 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
430 |
assume l2_pos: "0 <= l2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
431 |
thm zinterval_lpos [OF x2_lu x1_lu l2_pos] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
432 |
have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
433 |
"min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
434 |
x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
435 |
by (rule_tac zinterval_lpos [OF x2_lu x1_lu l2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
436 |
moreover have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) = min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2))" by (simp add: mult_ac min_commute min_min_commute) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
437 |
moreover have "max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1)) = max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
438 |
by (simp add: mult_ac max_commute max_max_commute) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
439 |
ultimately have ?thesis by (simp add: mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
440 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
441 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
442 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
443 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
444 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
445 |
assume l2_neg: "l2 < 0" and x2_pos: " 0<= x2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
446 |
from l1_neg have l1_le0 : "l1 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
447 |
from l2_neg have l2_le0 : "l2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
448 |
have ?thesis by (simp add: zinterval_lneglneg [OF x1_lu x2_lu l1_le0 x1_pos l2_le0 x2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
449 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
450 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
451 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
452 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
453 |
assume x2_neg: "x2 <0" and u2_pos: "0 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
454 |
from x2_lu have mx2_lu: "-u2 <= -x2 \<and> -x2 <= -l2" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
455 |
from x2_neg have mx2_pos: "0 <= -x2" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
456 |
from u2_pos have mu2_neg: "-u2 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
457 |
from l1_neg have l1_le0 : "l1 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
458 |
thm zinterval_lneglneg [OF x1_lu mx2_lu l1_le0 x1_pos mu2_neg mx2_pos] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
459 |
have "min (min (l1 * - u2) (l1 * - l2)) (min (u1 * - u2) (u1 * - l2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
460 |
\<le> x1 * - x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
461 |
x1 * - x2 \<le> max (max (l1 * - u2) (l1 * - l2)) (max (u1 * - u2) (u1 * - l2))" by (rule_tac zinterval_lneglneg [OF x1_lu mx2_lu l1_le0 x1_pos mu2_neg mx2_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
462 |
then have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
463 |
\<le> - x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
464 |
- x1 * x2 \<le> max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2))" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
465 |
moreover have "min (min (- l1 * u2) (- l1 * l2)) (min (- u1 * u2) (- u1 * l2)) = - max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2))" by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
466 |
moreover have "max (max (- l1 * u2) (- l1 * l2)) (max (- u1 * u2) (- u1 * l2)) = - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))" by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
467 |
ultimately have "- max (max (l1 * u2) (l1 * l2)) (max (u1 * u2) (u1 * l2))\<le> - x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
468 |
- x1 * x2 \<le> - min (min (l1 * u2) (l1 * l2)) (min (u1 * u2) (u1 * l2))" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
469 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
470 |
then have ?thesis by (simp add: min_commute max_commute mult_ac) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
471 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
472 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
473 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
474 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
475 |
assume u2_neg: "u2 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
476 |
thm zinterval_uneg[OF x2_lu x1_lu u2_neg] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
477 |
have "min (min (l2 * l1) (l2 * u1)) (min (u2 * l1) (u2 * u1)) \<le> x2 * x1 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
478 |
x2 * x1 \<le> max (max (l2 * l1) (l2 * u1)) (max (u2 * l1) (u2 * u1))" by (rule_tac zinterval_uneg[OF x2_lu x1_lu u2_neg]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
479 |
then have ?thesis by (simp add: mult_ac min_commute max_commute min_min_commute max_max_commute) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
480 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
481 |
ultimately show ?thesis by blast |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
482 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
483 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
484 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
485 |
lemma zinterval_xnegupos: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
486 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
487 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
488 |
and x1_neg: "x1 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
489 |
and u1_pos: "0<= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
490 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
491 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
492 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
493 |
from x1_lu have mx1_lu : "-u1 <= -x1 \<and> -x1 <= -l1" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
494 |
from u1_pos have mu1_neg : "-u1 <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
495 |
from x1_neg have mx1_pos : "0 <= -x1" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
496 |
thm zinterval_lnegxpos[OF mx1_lu x2_lu mu1_neg mx1_pos ] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
497 |
have "min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
498 |
\<le> - x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
499 |
- x1 * x2 \<le> max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
500 |
by (rule_tac zinterval_lnegxpos[OF mx1_lu x2_lu mu1_neg mx1_pos ]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
501 |
moreover have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
502 |
"min (min (- u1 * l2) (- u1 * u2)) (min (- l1 * l2) (- l1 * u2)) = - max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
503 |
by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
504 |
moreover have |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
505 |
"max (max (- u1 * l2) (- u1 * u2)) (max (- l1 * l2) (- l1 * u2)) = - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
506 |
by (simp add: min_max_minus max_min_minus) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
507 |
ultimately have "- max (max (u1 * l2) (u1 * u2)) (max (l1 * l2) (l1 * u2))\<le> - x1 * x2 \<and> |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
508 |
- x1 * x2 \<le> - min (min (u1 * l2) (u1 * u2)) (min (l1 * l2) (l1 * u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
509 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
510 |
then show ?thesis by (simp add: mult_ac min_commute max_commute) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
511 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
512 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
513 |
lemma abs_mul: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
514 |
assumes x1_lu : "l1 <= (x1::int) \<and> x1 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
515 |
and x2_lu : "l2 <= (x2::int) \<and> x2 <= u2" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
516 |
shows conc : "min (min (l1*l2) (l1*u2)) (min (u1*l2) (u1*u2)) <= x1 * x2 |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
517 |
\<and> x1 * x2 <= max (max (l1*l2) (l1*u2)) (max (u1*l2) (u1*u2))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
518 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
519 |
have "(0 <= l1) \<or> (l1 <= 0 \<and> 0<= x1) \<or> (x1 <=0 \<and> 0 <= u1) \<or> (u1 <= 0)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
520 |
by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
521 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
522 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
523 |
assume l1_pos: "0 <= l1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
524 |
have ?thesis by (rule_tac zinterval_lpos [OF x1_lu x2_lu l1_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
525 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
526 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
527 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
528 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
529 |
assume l1_neg :"l1 <= 0" and x1_pos: "0<= x1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
530 |
have ?thesis by (rule_tac zinterval_lnegxpos[OF x1_lu x2_lu l1_neg x1_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
531 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
532 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
533 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
534 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
535 |
assume x1_neg : "x1 <= 0" and u1_pos: "0 <= u1" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
536 |
have ?thesis by (rule_tac zinterval_xnegupos [OF x1_lu x2_lu x1_neg u1_pos]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
537 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
538 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
539 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
540 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
541 |
assume u1_neg: "u1 <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
542 |
have ?thesis by (rule_tac zinterval_uneg [OF x1_lu x2_lu u1_neg]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
543 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
544 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
545 |
ultimately show ?thesis by blast |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
546 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
547 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
548 |
lemma mult_x_mono_lpos : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
549 |
assumes l_pos : "0 <= (l::int)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
550 |
and x_lu : "l <= (x::int) \<and> x <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
551 |
shows "l*l <= x*x \<and> x*x <= u*u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
552 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
553 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
554 |
from x_lu have x_l : "l <= x" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
555 |
thm zmult_mono[OF l_pos l_pos x_l x_l] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
556 |
then have xx_l : "l*l <= x*x" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
557 |
by (simp add: zmult_mono[OF l_pos l_pos x_l x_l]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
558 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
559 |
from x_lu have x_u : "x <= u" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
560 |
from l_pos x_l have x_pos : "0 <= x" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
561 |
thm zmult_mono[OF x_pos x_pos x_u x_u] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
562 |
then have xx_u : "x*x <= u*u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
563 |
by (simp add: zmult_mono[OF x_pos x_pos x_u x_u]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
564 |
ultimately show ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
565 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
566 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
567 |
lemma mult_x_mono_luneg : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
568 |
assumes l_neg : "(l::int) <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
569 |
and u_neg : "u <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
570 |
and x_lu : "l <= (x::int) \<and> x <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
571 |
shows "u*u <= x*x \<and> x*x <= l*l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
572 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
573 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
574 |
from x_lu have mx_lu : "-u <= -x \<and> -x <= -l" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
575 |
from u_neg have mu_pos : "0<= -u" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
576 |
thm mult_x_mono_lpos[OF mu_pos mx_lu] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
577 |
have "- u * - u \<le> - x * - x \<and> - x * - x \<le> - l * - l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
578 |
by (rule_tac mult_x_mono_lpos[OF mu_pos mx_lu]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
579 |
then show ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
580 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
581 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
582 |
lemma mult_x_mono_lxnegupos : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
583 |
assumes l_neg : "(l::int) <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
584 |
and u_pos : "0 <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
585 |
and x_neg : "x <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
586 |
and x_lu : "l <= (x::int) \<and> x <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
587 |
shows "0 <= x*x \<and> x*x <= max (l*l) (u*u)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
588 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
589 |
from x_lu x_neg have mx_0l : "0 <= - x \<and> - x <= - l" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
590 |
have trv_0 : "(0::int) <= 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
591 |
thm mult_x_mono_lpos[OF trv_0 mx_0l] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
592 |
have "0 * 0 \<le> - x * - x \<and> - x * - x \<le> - l * - l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
593 |
by (rule_tac mult_x_mono_lpos[OF trv_0 mx_0l]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
594 |
then have xx_0ll : "0 <= x*x \<and> x*x <= l*l" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
595 |
have "l*l <= max (l*l) (u*u)" by (simp add: le_maxI1) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
596 |
with xx_0ll show ?thesis by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
597 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
598 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
599 |
lemma mult_x_mono_lnegupos : |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
600 |
assumes l_neg : "(l::int) <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
601 |
and u_pos : "0 <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
602 |
and x_lu : "l <= (x::int) \<and> x <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
603 |
shows "0 <= x*x \<and> x*x <= max (l*l) (u*u)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
604 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
605 |
have "0<= x \<or> x <= 0" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
606 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
607 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
608 |
assume x_neg : "x <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
609 |
thm mult_x_mono_lxnegupos[OF l_neg u_pos x_neg x_lu] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
610 |
have ?thesis by (rule_tac mult_x_mono_lxnegupos[OF l_neg u_pos x_neg x_lu]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
611 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
612 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
613 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
614 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
615 |
assume x_pos : "0 <= x" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
616 |
from x_lu have mx_lu : "-u <= -x \<and> -x <= -l" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
617 |
from x_pos have mx_neg : "-x <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
618 |
from u_pos have mu_neg : "-u <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
619 |
from x_lu x_pos have ml_pos : "0 <= -l" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
620 |
thm mult_x_mono_lxnegupos[OF mu_neg ml_pos mx_neg mx_lu] |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
621 |
have "0 \<le> - x * - x \<and> - x * - x \<le> max (- u * - u) (- l * - l)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
622 |
by (rule_tac mult_x_mono_lxnegupos[OF mu_neg ml_pos mx_neg mx_lu]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
623 |
then have ?thesis by (simp add: max_commute) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
624 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
625 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
626 |
ultimately show ?thesis by blast |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
627 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
628 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
629 |
lemma abs_mul_x: |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
630 |
assumes x_lu : "l <= (x::int) \<and> x <= u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
631 |
shows |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
632 |
"(if 0 <= l then l*l else if u <= 0 then u*u else 0) <= x*x |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
633 |
\<and> x*x <= (if 0 <= l then u*u else if u <= 0 then l*l else (max (l*l) (u*u)))" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
634 |
proof- |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
635 |
have "(0 <= l) \<or> (l < 0 \<and> u <= 0) \<or> (l < 0 \<and> 0 < u)" by arith |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
636 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
637 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
638 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
639 |
assume l_pos : "0 <= l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
640 |
from l_pos have "(if 0 <= l then l*l else if u <= 0 then u*u else 0) = l*l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
641 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
642 |
moreover from l_pos have "(if 0 <= l then u*u else if u <= 0 then l*l else (max (l*l) (u*u))) = u*u" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
643 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
644 |
moreover have "l * l \<le> x * x \<and> x * x \<le> u * u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
645 |
by (rule_tac mult_x_mono_lpos[OF l_pos x_lu]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
646 |
ultimately have ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
647 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
648 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
649 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
650 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
651 |
assume l_neg : "l < 0" and u_neg : "u <= 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
652 |
from l_neg have l_le0 : "l <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
653 |
from l_neg u_neg have "(if 0 <= l then l*l else if u <= 0 then u*u else 0) = u*u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
654 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
655 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
656 |
from l_neg u_neg have "(if 0 <= l then u*u else if u <= 0 then l*l else (max (l*l) (u*u))) = l*l" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
657 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
658 |
have "u * u \<le> x * x \<and> x * x \<le> l * l" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
659 |
by (rule_tac mult_x_mono_luneg[OF l_le0 u_neg x_lu]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
660 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
661 |
ultimately have ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
662 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
663 |
moreover |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
664 |
{ |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
665 |
assume l_neg : "l < 0" and u_pos: "0 < u" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
666 |
from l_neg have l_le0 : "l <= 0" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
667 |
from u_pos have u_ge0 : "0 <= u" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
668 |
from l_neg u_pos have "(if 0 <= l then l*l else if u <= 0 then u*u else 0) = 0" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
669 |
by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
670 |
moreover from l_neg u_pos have "(if 0 <= l then u*u else if u <= 0 then l*l else (max (l*l) (u*u))) = max (l*l) (u*u)" by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
671 |
moreover have "0 \<le> x * x \<and> x * x \<le> max (l * l) (u * u)" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
672 |
by (rule_tac mult_x_mono_lnegupos[OF l_le0 u_ge0 x_lu]) |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
673 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
674 |
ultimately have ?thesis by simp |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
675 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
676 |
} |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
677 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
678 |
ultimately show ?thesis by blast |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
679 |
qed |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
680 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
681 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
682 |
use"barith.ML" |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
683 |
setup Barith.setup |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
684 |
|
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
685 |
end |
388a6f431d83
a very simple decision procedure for a fragment of bounded arithmetic
chaieb
parents:
diff
changeset
|
686 |