164 if res |
164 if res |
165 then (I l1 (min_option True h1 (h2 - Some 1)), |
165 then (I l1 (min_option True h1 (h2 - Some 1)), |
166 I (max_option False (l1 + Some 1) l2) h2) |
166 I (max_option False (l1 + Some 1) l2) h2) |
167 else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" |
167 else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" |
168 |
168 |
169 interpretation Rep rep_ivl |
169 permanent_interpretation Rep rep_ivl |
170 proof |
170 proof |
171 case goal1 thus ?case |
171 case goal1 thus ?case |
172 by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) |
172 by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) |
173 qed |
173 qed |
174 |
174 |
175 interpretation Val_abs rep_ivl num_ivl plus_ivl |
175 permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl |
176 proof |
176 proof |
177 case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def) |
177 case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def) |
178 next |
178 next |
179 case goal2 thus ?case |
179 case goal2 thus ?case |
180 by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits) |
180 by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits) |
181 qed |
181 qed |
182 |
182 |
183 interpretation Rep1 rep_ivl |
183 permanent_interpretation Rep1 rep_ivl |
184 proof |
184 proof |
185 case goal1 thus ?case |
185 case goal1 thus ?case |
186 by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) |
186 by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) |
187 next |
187 next |
188 case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def) |
188 case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def) |
189 qed |
189 qed |
190 |
190 |
191 interpretation |
191 permanent_interpretation |
192 Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl |
192 Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl |
193 proof |
193 proof |
194 case goal1 thus ?case |
194 case goal1 thus ?case |
195 by(auto simp add: filter_plus_ivl_def) |
195 by(auto simp add: filter_plus_ivl_def) |
196 (metis rep_minus_ivl add_diff_cancel add_commute)+ |
196 (metis rep_minus_ivl add_diff_cancel add_commute)+ |
198 case goal2 thus ?case |
198 case goal2 thus ?case |
199 by(cases a1, cases a2, |
199 by(cases a1, cases a2, |
200 auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) |
200 auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) |
201 qed |
201 qed |
202 |
202 |
203 interpretation |
203 permanent_interpretation |
204 Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)" |
204 Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)" |
205 defines afilter_ivl is afilter |
205 defines afilter_ivl is afilter |
206 and bfilter_ivl is bfilter |
206 and bfilter_ivl is bfilter |
207 and AI_ivl is AI |
207 and AI_ivl is AI |
208 and aval_ivl is aval' |
208 and aval_ivl is aval' |