equal
deleted
inserted
replaced
23 |
23 |
24 typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}" |
24 typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}" |
25 proof |
25 proof |
26 show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro) |
26 show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro) |
27 qed |
27 qed |
|
28 |
|
29 text \<open>Kill code generation for filters\<close> |
|
30 |
|
31 code_datatype Abs_filter |
|
32 declare [[code abort: Rep_filter]] |
28 |
33 |
29 lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" |
34 lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" |
30 using Rep_filter [of F] by simp |
35 using Rep_filter [of F] by simp |
31 |
36 |
32 lemma Abs_filter_inverse': |
37 lemma Abs_filter_inverse': |