227 begin |
227 begin |
228 |
228 |
229 definition uminus_rep :: "eint2 \<Rightarrow> eint2" where |
229 definition uminus_rep :: "eint2 \<Rightarrow> eint2" where |
230 "uminus_rep p = (let (l,h) = p in (-h, -l))" |
230 "uminus_rep p = (let (l,h) = p in (-h, -l))" |
231 |
231 |
232 lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)" |
232 lemma \<gamma>_uminus_rep: "i \<in> \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)" |
233 by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff |
233 by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff |
234 split: prod.split) |
234 split: prod.split) |
235 |
235 |
236 lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep |
236 lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep |
237 by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases) |
237 by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases) |
238 (auto simp: Icc_eq_Icc split: extended.splits) |
238 (auto simp: Icc_eq_Icc split: extended.splits) |
239 |
239 |
240 instance .. |
240 instance .. |
241 end |
241 end |
242 |
242 |
243 lemma \<gamma>_uminus: "i : \<gamma>_ivl iv \<Longrightarrow> -i \<in> \<gamma>_ivl(- iv)" |
243 lemma \<gamma>_uminus: "i \<in> \<gamma>_ivl iv \<Longrightarrow> -i \<in> \<gamma>_ivl(- iv)" |
244 by transfer (rule \<gamma>_uminus_rep) |
244 by transfer (rule \<gamma>_uminus_rep) |
245 |
245 |
246 lemma uminus_nice: "-[l,h] = [-h,-l]" |
246 lemma uminus_nice: "-[l,h] = [-h,-l]" |
247 by transfer (simp add: uminus_rep_def) |
247 by transfer (simp add: uminus_rep_def) |
248 |
248 |
274 lemma \<gamma>_aboveI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> i \<le> j \<Longrightarrow> j \<in> \<gamma>_ivl(above iv)" |
274 lemma \<gamma>_aboveI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> i \<le> j \<Longrightarrow> j \<in> \<gamma>_ivl(above iv)" |
275 by transfer |
275 by transfer |
276 (auto simp add: above_rep_def \<gamma>_rep_cases is_empty_rep_def |
276 (auto simp add: above_rep_def \<gamma>_rep_cases is_empty_rep_def |
277 split: extended.splits) |
277 split: extended.splits) |
278 |
278 |
279 lemma \<gamma>_belowI: "i : \<gamma>_ivl iv \<Longrightarrow> j \<le> i \<Longrightarrow> j : \<gamma>_ivl(below iv)" |
279 lemma \<gamma>_belowI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> j \<le> i \<Longrightarrow> j \<in> \<gamma>_ivl(below iv)" |
280 by transfer |
280 by transfer |
281 (auto simp add: below_rep_def \<gamma>_rep_cases is_empty_rep_def |
281 (auto simp add: below_rep_def \<gamma>_rep_cases is_empty_rep_def |
282 split: extended.splits) |
282 split: extended.splits) |
283 |
283 |
284 definition inv_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where |
284 definition inv_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where |