equal
deleted
inserted
replaced
31 by transfer (simp add: \<gamma>_rep_def) |
31 by transfer (simp add: \<gamma>_rep_def) |
32 |
32 |
33 lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" |
33 lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" |
34 by(auto simp: eq_ivl_def) |
34 by(auto simp: eq_ivl_def) |
35 |
35 |
36 fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where |
36 lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" |
37 "in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h" |
37 is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h" |
38 |
|
39 lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep |
|
40 by(auto simp: eq_ivl_def \<gamma>_rep_def) |
38 by(auto simp: eq_ivl_def \<gamma>_rep_def) |
|
39 |
|
40 lemma in_ivl_nice: "in_ivl i [l\<dots>h] = (l \<le> Fin i \<and> Fin i \<le> h)" |
|
41 by transfer simp |
41 |
42 |
42 definition is_empty_rep :: "eint2 \<Rightarrow> bool" where |
43 definition is_empty_rep :: "eint2 \<Rightarrow> bool" where |
43 "is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)" |
44 "is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)" |
44 |
45 |
45 lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} | |
46 lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} | |