setup code generation for filters as suggested by Florian
authorhoelzl
Mon Jan 11 11:56:35 2016 +0100 (2016-01-11)
changeset 62123df65f5c27c15
parent 62122 eed7ca453573
child 62124 d0dff7a80c26
setup code generation for filters as suggested by Florian
src/HOL/Filter.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Filter.thy	Mon Jan 11 07:44:20 2016 +0100
     1.2 +++ b/src/HOL/Filter.thy	Mon Jan 11 11:56:35 2016 +0100
     1.3 @@ -26,11 +26,6 @@
     1.4    show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
     1.5  qed
     1.6  
     1.7 -text \<open>Kill code generation for filters\<close>
     1.8 -
     1.9 -code_datatype Abs_filter
    1.10 -declare [[code abort: Rep_filter]]
    1.11 -
    1.12  lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
    1.13    using Rep_filter [of F] by simp
    1.14  
    1.15 @@ -1222,4 +1217,52 @@
    1.16  
    1.17  end
    1.18  
    1.19 +text \<open>Code generation for filters\<close>
    1.20 +
    1.21 +definition abstract_filter :: "(unit \<Rightarrow> 'a filter) \<Rightarrow> 'a filter"
    1.22 +  where [simp]: "abstract_filter f = f ()"
    1.23 +
    1.24 +code_datatype principal abstract_filter
    1.25 +
    1.26 +hide_const (open) abstract_filter
    1.27 +
    1.28 +declare [[code drop: filterlim prod_filter filtermap eventually
    1.29 +  "inf :: _ filter \<Rightarrow> _" "sup :: _ filter \<Rightarrow> _" "less_eq :: _ filter \<Rightarrow> _"
    1.30 +  Abs_filter]]
    1.31 +
    1.32 +declare filterlim_principal [code]
    1.33 +declare principal_prod_principal [code]
    1.34 +declare filtermap_principal [code]
    1.35 +declare eventually_principal [code]
    1.36 +declare inf_principal [code]
    1.37 +declare sup_principal [code]
    1.38 +declare principal_le_iff [code]
    1.39 +
    1.40 +lemma Rep_filter_iff_eventually [simp, code]:
    1.41 +  "Rep_filter F P \<longleftrightarrow> eventually P F"
    1.42 +  by (simp add: eventually_def)
    1.43 +
    1.44 +lemma bot_eq_principal_empty [code]:
    1.45 +  "bot = principal {}"
    1.46 +  by simp
    1.47 +
    1.48 +lemma top_eq_principal_UNIV [code]:
    1.49 +  "top = principal UNIV"
    1.50 +  by simp
    1.51 +
    1.52 +instantiation filter :: (equal) equal
    1.53 +begin
    1.54 +
    1.55 +definition equal_filter :: "'a filter \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.56 +  where "equal_filter F F' \<longleftrightarrow> F = F'"
    1.57 +
    1.58 +lemma equal_filter [code]:
    1.59 +  "HOL.equal (principal A) (principal B) \<longleftrightarrow> A = B"
    1.60 +  by (simp add: equal_filter_def)
    1.61 +
    1.62 +instance
    1.63 +  by standard (simp add: equal_filter_def)
    1.64 +
    1.65  end
    1.66 +
    1.67 +end
     2.1 --- a/src/HOL/Topological_Spaces.thy	Mon Jan 11 07:44:20 2016 +0100
     2.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Jan 11 11:56:35 2016 +0100
     2.3 @@ -2444,8 +2444,9 @@
     2.4  end
     2.5  
     2.6  lemma uniformity_Abort:
     2.7 -  "uniformity = Abs_filter (\<lambda>P. Code.abort (STR ''uniformity is not executable'') (\<lambda>x. Rep_filter uniformity P))"
     2.8 -  unfolding Code.abort_def Rep_filter_inverse ..
     2.9 +  "uniformity =
    2.10 +    Filter.abstract_filter (\<lambda>u. Code.abort (STR ''uniformity is not executable'') (\<lambda>u. uniformity))"
    2.11 +  by simp
    2.12  
    2.13  class open_uniformity = "open" + uniformity +
    2.14    assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"