1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Abs_Int2_ivl |
3 theory Abs_Int2_ivl |
4 imports Abs_Int2 |
4 imports "~~/src/HOL/Library/Quotient_List" |
|
5 "~~/src/HOL/Library/Extended" |
|
6 Abs_Int2 |
5 begin |
7 begin |
6 |
8 |
7 subsection "Interval Analysis" |
9 subsection "Interval Analysis" |
8 |
10 |
9 datatype lb = Minf | Lb int |
11 type_synonym eint = "int extended" |
10 datatype ub = Pinf | Ub int |
12 type_synonym eint2 = "eint * eint" |
11 |
13 |
12 datatype ivl = Ivl lb ub |
14 definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where |
13 |
15 "\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})" |
14 definition "\<gamma>_ivl i = (case i of |
16 |
15 Ivl (Lb l) (Ub h) \<Rightarrow> {l..h} | |
17 definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where |
16 Ivl (Lb l) Pinf \<Rightarrow> {l..} | |
18 "eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)" |
17 Ivl Minf (Ub h) \<Rightarrow> {..h} | |
19 |
18 Ivl Minf Pinf \<Rightarrow> UNIV)" |
20 lemma refl_eq_ivl[simp]: "eq_ivl p p" |
19 |
21 by(auto simp: eq_ivl_def) |
20 abbreviation Ivl_Lb_Ub :: "int \<Rightarrow> int \<Rightarrow> ivl" ("{_\<dots>_}") where |
22 |
21 "{lo\<dots>hi} == Ivl (Lb lo) (Ub hi)" |
23 quotient_type ivl = eint2 / eq_ivl |
22 abbreviation Ivl_Lb_Pinf :: "int \<Rightarrow> ivl" ("{_\<dots>}") where |
24 by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def) |
23 "{lo\<dots>} == Ivl (Lb lo) Pinf" |
25 |
24 abbreviation Ivl_Minf_Ub :: "int \<Rightarrow> ivl" ("{\<dots>_}") where |
26 lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep |
25 "{\<dots>hi} == Ivl Minf (Ub hi)" |
27 by(simp add: eq_ivl_def) |
26 abbreviation Ivl_Minf_Pinf :: "ivl" ("{\<dots>}") where |
28 |
27 "{\<dots>} == Ivl Minf Pinf" |
29 abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where |
28 |
30 "[l\<dots>h] == abs_ivl(l,h)" |
29 lemmas lub_splits = lb.splits ub.splits |
31 |
30 |
32 lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" |
31 definition "num_ivl n = {n\<dots>n}" |
33 by(auto simp: eq_ivl_def) |
32 |
34 |
33 fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where |
35 fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where |
34 "in_ivl k (Ivl (Lb l) (Ub h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" | |
36 "in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h" |
35 "in_ivl k (Ivl (Lb l) Pinf) \<longleftrightarrow> l \<le> k" | |
37 |
36 "in_ivl k (Ivl Minf (Ub h)) \<longleftrightarrow> k \<le> h" | |
38 lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep |
37 "in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True" |
39 by(auto simp: eq_ivl_def \<gamma>_rep_def) |
38 |
40 |
39 |
41 definition is_empty_rep :: "eint2 \<Rightarrow> bool" where |
40 instantiation lb :: linorder |
42 "is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)" |
41 begin |
43 |
42 |
44 lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} | |
43 definition less_eq_lb where |
45 (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})" |
44 "l1 \<le> l2 = (case l1 of Minf \<Rightarrow> True | Lb i1 \<Rightarrow> (case l2 of Minf \<Rightarrow> False | Lb i2 \<Rightarrow> i1 \<le> i2))" |
46 by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits) |
45 |
47 |
46 definition less_lb :: "lb \<Rightarrow> lb \<Rightarrow> bool" where |
48 lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep |
47 "((l1::lb) < l2) = (l1 \<le> l2 & ~ l1 \<ge> l2)" |
49 apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def) |
|
50 apply(auto simp: not_less less_eq_extended_cases split: extended.splits) |
|
51 done |
|
52 |
|
53 lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)" |
|
54 by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits) |
|
55 |
|
56 definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)" |
|
57 |
|
58 lift_definition empty_ivl :: ivl is empty_rep |
|
59 by simp |
|
60 |
|
61 lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep" |
|
62 by(auto simp add: is_empty_rep_def empty_rep_def) |
|
63 |
|
64 lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})" |
|
65 by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits) |
|
66 |
|
67 declare is_empty_rep_iff[THEN iffD1, simp] |
|
68 |
|
69 |
|
70 instantiation ivl :: semilattice |
|
71 begin |
|
72 |
|
73 definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where |
|
74 "le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in |
|
75 if is_empty_rep(l1,h1) then True else |
|
76 if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)" |
|
77 |
|
78 lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2" |
|
79 apply rule |
|
80 apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1] |
|
81 apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def) |
|
82 apply(auto simp: not_less split: extended.splits) |
|
83 done |
|
84 |
|
85 lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep |
|
86 by(auto simp: eq_ivl_def le_iff_subset) |
|
87 |
|
88 definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))" |
|
89 |
|
90 definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where |
|
91 "join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 |
|
92 else let (l1,h1) = p1; (l2,h2) = p2 in (min l1 l2, max h1 h2))" |
|
93 |
|
94 lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep |
|
95 by(auto simp: eq_ivl_iff join_rep_def) |
|
96 |
|
97 lift_definition top_ivl :: ivl is "(Minf,Pinf)" |
|
98 by(auto simp: eq_ivl_def) |
|
99 |
|
100 lemma is_empty_min_max: |
|
101 "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)" |
|
102 by(auto simp add: is_empty_rep_def max_def min_def split: if_splits) |
48 |
103 |
49 instance |
104 instance |
50 proof |
105 proof |
51 case goal1 show ?case by(rule less_lb_def) |
106 case goal1 show ?case by (rule less_ivl_def) |
52 next |
107 next |
53 case goal2 show ?case by(auto simp: less_eq_lb_def split:lub_splits) |
108 case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits) |
54 next |
109 next |
55 case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits) |
110 case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits) |
56 next |
111 next |
57 case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits) |
112 case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits) |
58 next |
113 next |
59 case goal5 thus ?case by(auto simp: less_eq_lb_def split:lub_splits) |
114 case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max) |
60 qed |
115 next |
61 |
116 case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max) |
62 end |
117 next |
63 |
118 case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def) |
64 instantiation ub :: linorder |
119 next |
65 begin |
120 case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def) |
66 |
121 qed |
67 definition less_eq_ub where |
122 |
68 "u1 \<le> u2 = (case u2 of Pinf \<Rightarrow> True | Ub i2 \<Rightarrow> (case u1 of Pinf \<Rightarrow> False | Ub i1 \<Rightarrow> i1 \<le> i2))" |
123 end |
69 |
124 |
70 definition less_ub :: "ub \<Rightarrow> ub \<Rightarrow> bool" where |
125 text{* Implement (naive) executable equality: *} |
71 "((u1::ub) < u2) = (u1 \<le> u2 & ~ u1 \<ge> u2)" |
126 instantiation ivl :: equal |
|
127 begin |
|
128 |
|
129 definition equal_ivl where |
|
130 "equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)" |
72 |
131 |
73 instance |
132 instance |
74 proof |
133 proof |
75 case goal1 show ?case by(rule less_ub_def) |
134 case goal1 show ?case by(simp add: equal_ivl_def eq_iff) |
76 next |
135 qed |
77 case goal2 show ?case by(auto simp: less_eq_ub_def split:lub_splits) |
136 |
78 next |
137 end |
79 case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits) |
138 |
80 next |
139 lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)" |
81 case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits) |
140 by(simp add: not_less) |
82 next |
141 lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)" |
83 case goal5 thus ?case by(auto simp: less_eq_ub_def split:lub_splits) |
142 by(simp add: not_less) |
84 qed |
143 |
85 |
144 instantiation ivl :: lattice |
86 end |
145 begin |
87 |
146 |
88 lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def |
147 definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where |
89 |
148 "meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))" |
90 lemma le_lub_simps[simp]: |
149 |
91 "Minf \<le> l" "Lb i \<le> Lb j = (i \<le> j)" "~ Lb i \<le> Minf" |
150 lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2" |
92 "h \<le> Pinf" "Ub i \<le> Ub j = (i \<le> j)" "~ Pinf \<le> Ub j" |
151 by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits) |
93 by(auto simp: le_lub_defs split: lub_splits) |
152 |
94 |
153 lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep |
95 definition empty where "empty = {1\<dots>0}" |
154 by(auto simp: \<gamma>_meet_rep eq_ivl_def) |
96 |
155 |
97 fun is_empty where |
156 definition "\<bottom> = empty_ivl" |
98 "is_empty {l\<dots>h} = (h<l)" | |
|
99 "is_empty _ = False" |
|
100 |
|
101 lemma [simp]: "is_empty(Ivl l h) = |
|
102 (case l of Lb l \<Rightarrow> (case h of Ub h \<Rightarrow> h<l | Pinf \<Rightarrow> False) | Minf \<Rightarrow> False)" |
|
103 by(auto split: lub_splits) |
|
104 |
|
105 lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}" |
|
106 by(auto simp add: \<gamma>_ivl_def split: ivl.split lub_splits) |
|
107 |
|
108 |
|
109 instantiation ivl :: semilattice |
|
110 begin |
|
111 |
|
112 fun le_aux where |
|
113 "le_aux (Ivl l1 h1) (Ivl l2 h2) = (l2 \<le> l1 & h1 \<le> h2)" |
|
114 |
|
115 definition le_ivl where |
|
116 "i1 \<sqsubseteq> i2 = |
|
117 (if is_empty i1 then True else |
|
118 if is_empty i2 then False else le_aux i1 i2)" |
|
119 |
|
120 definition "i1 \<squnion> i2 = |
|
121 (if is_empty i1 then i2 else if is_empty i2 then i1 |
|
122 else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (min l1 l2) (max h1 h2))" |
|
123 |
|
124 definition "\<top> = {\<dots>}" |
|
125 |
157 |
126 instance |
158 instance |
127 proof |
159 proof |
128 case goal1 thus ?case |
|
129 by(cases x, simp add: le_ivl_def) |
|
130 next |
|
131 case goal2 thus ?case |
160 case goal2 thus ?case |
132 by(cases x, cases y, cases z, auto simp: le_ivl_def split: if_splits) |
161 unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep) |
133 next |
162 next |
134 case goal3 thus ?case |
163 case goal3 thus ?case |
135 by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits) |
164 unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep) |
136 next |
165 next |
137 case goal4 thus ?case |
166 case goal4 thus ?case |
138 by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits) |
167 unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep) |
139 next |
168 next |
140 case goal5 thus ?case |
169 case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset) |
141 by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits if_splits) |
170 qed |
142 next |
171 |
143 case goal6 thus ?case |
172 end |
144 by(cases x, simp add: Top_ivl_def le_ivl_def le_lub_defs split: lub_splits) |
173 |
145 qed |
174 |
146 |
175 lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p" |
147 end |
176 by (metis eq_ivl_iff is_empty_empty_rep) |
148 |
177 |
149 |
178 lemma le_ivl_nice: "[l1\<dots>h1] \<le> [l2\<dots>h2] \<longleftrightarrow> |
150 instantiation ivl :: lattice |
179 (if [l1\<dots>h1] = \<bottom> then True else |
151 begin |
180 if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)" |
152 |
181 unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty) |
153 definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else |
182 |
154 case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (max l1 l2) (min h1 h2))" |
183 lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] = |
155 |
184 (if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else |
156 definition "\<bottom> = empty" |
185 if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])" |
157 |
186 unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty) |
158 instance |
187 |
159 proof |
188 lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]" |
160 case goal2 thus ?case |
189 by transfer (simp add: meet_rep_def) |
161 by (simp add:meet_ivl_def empty_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits) |
190 |
162 next |
191 |
163 case goal3 thus ?case |
192 instantiation ivl :: plus |
164 by (simp add: empty_def meet_ivl_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits) |
193 begin |
165 next |
194 |
166 case goal4 thus ?case |
195 definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where |
167 by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_lub_defs max_def min_def split: lub_splits if_splits) |
196 "plus_rep p1 p2 = |
168 next |
197 (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else |
169 case goal1 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def) |
198 let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))" |
170 qed |
199 |
171 |
200 lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep |
172 end |
201 by(auto simp: plus_rep_def eq_ivl_iff) |
173 |
|
174 |
|
175 instantiation lb :: plus |
|
176 begin |
|
177 |
|
178 fun plus_lb where |
|
179 "Lb x + Lb y = Lb(x+y)" | |
|
180 "_ + _ = Minf" |
|
181 |
202 |
182 instance .. |
203 instance .. |
183 end |
204 end |
184 |
205 |
185 instantiation ub :: plus |
206 lemma plus_ivl_nice: "[l1\<dots>h1] + [l2\<dots>h2] = |
186 begin |
207 (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then \<bottom> else [l1+l2 \<dots> h1+h2])" |
187 |
208 unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty) |
188 fun plus_ub where |
209 |
189 "Ub x + Ub y = Ub(x+y)" | |
210 lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf" |
190 "_ + _ = Pinf" |
211 by(cases x) auto |
|
212 lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf" |
|
213 by(cases x) auto |
|
214 |
|
215 lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)" |
|
216 by(cases x) auto |
|
217 lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)" |
|
218 by(cases x) auto |
|
219 |
|
220 instantiation ivl :: uminus |
|
221 begin |
|
222 |
|
223 definition uminus_rep :: "eint2 \<Rightarrow> eint2" where |
|
224 "uminus_rep p = (let (l,h) = p in (-h, -l))" |
|
225 |
|
226 lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)" |
|
227 by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff |
|
228 split: prod.split) |
|
229 |
|
230 lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep |
|
231 by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases) |
|
232 (auto simp: Icc_eq_Icc split: extended.splits) |
191 |
233 |
192 instance .. |
234 instance .. |
193 end |
235 end |
194 |
236 |
195 instantiation ivl :: plus |
237 lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]" |
196 begin |
238 by transfer (simp add: uminus_rep_def) |
197 |
239 |
198 definition "i1+i2 = (if is_empty i1 | is_empty i2 then empty else |
240 instantiation ivl :: minus |
199 case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))" |
241 begin |
200 |
242 definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl) - iv2 = iv1 + -iv2" |
201 instance .. |
243 instance .. |
202 end |
244 end |
203 |
245 |
204 fun uminus_ub :: "ub \<Rightarrow> lb" where |
246 |
205 "uminus_ub(Ub( x)) = Lb(-x)" | |
247 definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where |
206 "uminus_ub Pinf = Minf" |
248 "filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))" |
207 |
249 |
208 fun uminus_lb :: "lb \<Rightarrow> ub" where |
250 definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where |
209 "uminus_lb(Lb( x)) = Ub(-x)" | |
251 "filter_less_rep res p1 p2 = |
210 "uminus_lb Minf = Pinf" |
252 (if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else |
211 |
253 let (l1,h1) = p1; (l2,h2) = p2 in |
212 instantiation ivl :: uminus |
|
213 begin |
|
214 |
|
215 fun uminus_ivl where |
|
216 "-(Ivl l h) = Ivl (uminus_ub h) (uminus_lb l)" |
|
217 |
|
218 instance .. |
|
219 end |
|
220 |
|
221 instantiation ivl :: minus |
|
222 begin |
|
223 |
|
224 definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where |
|
225 "(i1::ivl) - i2 = i1 + -i2" |
|
226 |
|
227 instance .. |
|
228 end |
|
229 |
|
230 lemma minus_ivl_cases: "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else |
|
231 case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))" |
|
232 by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits) |
|
233 |
|
234 lemma gamma_minus_ivl: |
|
235 "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)" |
|
236 by(auto simp add: minus_ivl_def plus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits) |
|
237 |
|
238 definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*) |
|
239 i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))" |
|
240 |
|
241 fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where |
|
242 "filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) = |
|
243 (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else |
|
244 if res |
254 if res |
245 then (Ivl l1 (min h1 (h2 + Ub -1)), Ivl (max (l1 + Lb 1) l2) h2) |
255 then ((l1, min h1 (h2 + Fin -1)), (max (l1 + Fin 1) l2, h2)) |
246 else (Ivl (max l1 l2) h1, Ivl l2 (min h1 h2)))" |
256 else ((max l1 l2, h1), (l2, min h1 h2)))" |
|
257 |
|
258 lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep |
|
259 by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff) |
|
260 declare filter_less_ivl.abs_eq[code] (* bug in lifting *) |
|
261 |
|
262 lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] = |
|
263 (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else |
|
264 if b |
|
265 then ([l1 \<dots> min h1 (h2 + Fin -1)], [max (l1 + Fin 1) l2 \<dots> h2]) |
|
266 else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))" |
|
267 unfolding prod_rel_eq[symmetric] bot_ivl_def |
|
268 by transfer (auto simp: filter_less_rep_def eq_ivl_empty) |
|
269 |
|
270 lemma add_mono_le_Fin: |
|
271 "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))" |
|
272 by(drule (1) add_mono) simp |
|
273 |
|
274 lemma add_mono_Fin_le: |
|
275 "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2" |
|
276 by(drule (1) add_mono) simp |
|
277 |
|
278 lemma plus_rep_plus: |
|
279 "\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)" |
|
280 by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin) |
247 |
281 |
248 interpretation Val_abs |
282 interpretation Val_abs |
249 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
283 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
250 proof |
284 proof |
251 case goal1 thus ?case |
285 case goal1 thus ?case by transfer (simp add: le_iff_subset) |
252 by(auto simp: \<gamma>_ivl_def le_ivl_def le_lub_defs split: ivl.split lub_splits if_splits) |
286 next |
253 next |
287 case goal2 show ?case by transfer (simp add: \<gamma>_rep_def) |
254 case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def) |
288 next |
255 next |
289 case goal3 show ?case by transfer (simp add: \<gamma>_rep_def) |
256 case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def) |
|
257 next |
290 next |
258 case goal4 thus ?case |
291 case goal4 thus ?case |
259 by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split lub_splits) |
292 apply transfer |
260 qed |
293 apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le) |
|
294 by(auto simp: empty_rep_def is_empty_rep_def) |
|
295 qed |
|
296 |
261 |
297 |
262 interpretation Val_abs1_gamma |
298 interpretation Val_abs1_gamma |
263 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
299 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
264 defines aval_ivl is aval' |
300 defines aval_ivl is aval' |
265 proof |
301 proof |
266 case goal1 thus ?case |
302 case goal1 show ?case |
267 by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_def max_def split: ivl.split lub_splits) |
303 by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split) |
268 next |
304 next |
269 case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def) |
305 case goal2 show ?case unfolding bot_ivl_def by transfer simp |
270 qed |
306 qed |
271 |
307 |
272 lemma mono_minus_ivl: fixes i1 :: ivl |
308 lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)" |
273 shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'" |
309 by(auto simp: plus_rep_def plus_rep_plus split: prod.splits) |
274 apply(auto simp add: minus_ivl_cases empty_def le_ivl_def le_lub_defs split: ivl.splits) |
310 |
275 apply(simp split: lub_splits) |
311 lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow> |
276 apply(simp split: lub_splits) |
312 \<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))" |
277 apply(simp split: lub_splits) |
313 by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv) |
278 done |
314 (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus) |
279 |
315 |
|
316 lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and> |
|
317 eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2; |
|
318 n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk> |
|
319 \<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2" |
|
320 by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac) |
|
321 (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+ |
280 |
322 |
281 interpretation Val_abs1 |
323 interpretation Val_abs1 |
282 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
324 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
283 and test_num' = in_ivl |
325 and test_num' = in_ivl |
284 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
326 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
285 proof |
327 proof |
286 case goal1 thus ?case |
328 case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def) |
287 by (simp add: \<gamma>_ivl_def split: ivl.split lub_splits) |
329 next |
288 next |
330 case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric] |
289 case goal2 thus ?case |
331 by transfer (simp add: filter_plus) |
290 by(auto simp add: filter_plus_ivl_def) |
|
291 (metis gamma_minus_ivl add_diff_cancel add_commute)+ |
|
292 next |
332 next |
293 case goal3 thus ?case |
333 case goal3 thus ?case |
294 by(cases a1, cases a2, auto simp: \<gamma>_ivl_def min_def max_def split: if_splits lub_splits) |
334 unfolding prod_rel_eq[symmetric] |
|
335 apply transfer |
|
336 apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits) |
|
337 apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits) |
|
338 done |
295 qed |
339 qed |
296 |
340 |
297 interpretation Abs_Int1 |
341 interpretation Abs_Int1 |
298 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
342 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
299 and test_num' = in_ivl |
343 and test_num' = in_ivl |