equal
deleted
inserted
replaced
53 (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})" |
53 (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})" |
54 by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits) |
54 by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits) |
55 |
55 |
56 lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep |
56 lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep |
57 apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def) |
57 apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def) |
58 apply(auto simp: not_less less_eq_extended_cases split: extended.splits) |
58 apply(auto simp: not_less less_eq_extended_case split: extended.splits) |
59 done |
59 done |
60 |
60 |
61 lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)" |
61 lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)" |
62 by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits) |
62 by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits) |
63 |
63 |