# HG changeset patch
# User hoelzl
# Date 1452509795 -3600
# Node ID df65f5c27c1513ca89a42a62671e5e7ae487dfae
# Parent  eed7ca453573b773e83997e59e62d987952623bc
setup code generation for filters as suggested by Florian

diff -r eed7ca453573 -r df65f5c27c15 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/HOL/Filter.thy	Mon Jan 11 11:56:35 2016 +0100
@@ -26,11 +26,6 @@
   show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
 qed
 
-text \<open>Kill code generation for filters\<close>
-
-code_datatype Abs_filter
-declare [[code abort: Rep_filter]]
-
 lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
   using Rep_filter [of F] by simp
 
@@ -1222,4 +1217,52 @@
 
 end
 
+text \<open>Code generation for filters\<close>
+
+definition abstract_filter :: "(unit \<Rightarrow> 'a filter) \<Rightarrow> 'a filter"
+  where [simp]: "abstract_filter f = f ()"
+
+code_datatype principal abstract_filter
+
+hide_const (open) abstract_filter
+
+declare [[code drop: filterlim prod_filter filtermap eventually
+  "inf :: _ filter \<Rightarrow> _" "sup :: _ filter \<Rightarrow> _" "less_eq :: _ filter \<Rightarrow> _"
+  Abs_filter]]
+
+declare filterlim_principal [code]
+declare principal_prod_principal [code]
+declare filtermap_principal [code]
+declare eventually_principal [code]
+declare inf_principal [code]
+declare sup_principal [code]
+declare principal_le_iff [code]
+
+lemma Rep_filter_iff_eventually [simp, code]:
+  "Rep_filter F P \<longleftrightarrow> eventually P F"
+  by (simp add: eventually_def)
+
+lemma bot_eq_principal_empty [code]:
+  "bot = principal {}"
+  by simp
+
+lemma top_eq_principal_UNIV [code]:
+  "top = principal UNIV"
+  by simp
+
+instantiation filter :: (equal) equal
+begin
+
+definition equal_filter :: "'a filter \<Rightarrow> 'a filter \<Rightarrow> bool"
+  where "equal_filter F F' \<longleftrightarrow> F = F'"
+
+lemma equal_filter [code]:
+  "HOL.equal (principal A) (principal B) \<longleftrightarrow> A = B"
+  by (simp add: equal_filter_def)
+
+instance
+  by standard (simp add: equal_filter_def)
+
 end
+
+end
diff -r eed7ca453573 -r df65f5c27c15 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Jan 11 11:56:35 2016 +0100
@@ -2444,8 +2444,9 @@
 end
 
 lemma uniformity_Abort:
-  "uniformity = Abs_filter (\<lambda>P. Code.abort (STR ''uniformity is not executable'') (\<lambda>x. Rep_filter uniformity P))"
-  unfolding Code.abort_def Rep_filter_inverse ..
+  "uniformity =
+    Filter.abstract_filter (\<lambda>u. Code.abort (STR ''uniformity is not executable'') (\<lambda>u. uniformity))"
+  by simp
 
 class open_uniformity = "open" + uniformity +
   assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"