
diff -r 4191acef9d0e -r 5431e1392b14 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Sep 27 09:15:40 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Fri Sep 27 09:26:31 2013 +0200
@@ -2282,5 +2282,224 @@
     using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
 qed
 
+subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
+
+context begin interpretation lifting_syntax .
+
+definition filter_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
+where "filter_rel R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
+
+lemma filter_rel_eventually:
+  "filter_rel R F G \<longleftrightarrow> 
+  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
+by(simp add: filter_rel_def eventually_def)
+
+lemma filtermap_id [simp, id_simps]: "filtermap id = id"
+by(simp add: fun_eq_iff id_def filtermap_ident)
+
+lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
+using filtermap_id unfolding id_def .
+
+lemma Quotient_filter [quot_map]:
+  assumes Q: "Quotient R Abs Rep T"
+  shows "Quotient (filter_rel R) (filtermap Abs) (filtermap Rep) (filter_rel T)"
+unfolding Quotient_alt_def
+proof(intro conjI strip)
+  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
+    unfolding Quotient_alt_def by blast
+
+  fix F G
+  assume "filter_rel T F G"
+  thus "filtermap Abs F = G" unfolding filter_eq_iff
+    by(auto simp add: eventually_filtermap filter_rel_eventually * fun_relI del: iffI elim!: fun_relD)
+next
+  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
+
+  fix F
+  show "filter_rel T (filtermap Rep F) F" 
+    by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI
+            del: iffI simp add: eventually_filtermap filter_rel_eventually)
+qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff filter_rel_eventually
+         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
+
+lemma eventually_parametric [transfer_rule]:
+  "((A ===> op =) ===> filter_rel A ===> op =) eventually eventually"
+by(simp add: fun_rel_def filter_rel_eventually)
+
+lemma filter_rel_eq [relator_eq]: "filter_rel op = = op ="
+by(auto simp add: filter_rel_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
+
+lemma filter_rel_mono [relator_mono]:
+  "A \<le> B \<Longrightarrow> filter_rel A \<le> filter_rel B"
+unfolding filter_rel_eventually[abs_def]
+by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
+
+lemma reflp_filter_rel [reflexivity_rule]: "reflp R \<Longrightarrow> reflp (filter_rel R)"
+unfolding filter_rel_eventually[abs_def]
+by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD)
+
+lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>"
+by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)
+
+lemma is_filter_parametric_aux:
+  assumes "is_filter F"
+  assumes [transfer_rule]: "bi_total A" "bi_unique A"
+  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
+  shows "is_filter G"
+proof -
+  interpret is_filter F by fact
+  show ?thesis
+  proof
+    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
+    thus "G (\<lambda>x. True)" by(simp add: True)
+  next
+    fix P' Q'
+    assume "G P'" "G Q'"
+    moreover
+    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
+    have "F P = G P'" "F Q = G Q'" by transfer_prover+
+    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
+    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
+    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
+  next
+    fix P' Q'
+    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
+    moreover
+    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
+    have "F P = G P'" by transfer_prover
+    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
+    ultimately have "F Q" by(simp add: mono)
+    moreover have "F Q = G Q'" by transfer_prover
+    ultimately show "G Q'" by simp
+  qed
+qed
+
+lemma is_filter_parametric [transfer_rule]:
+  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
+  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
+apply(rule fun_relI)
+apply(rule iffI)
+ apply(erule (3) is_filter_parametric_aux)
+apply(erule is_filter_parametric_aux[where A="conversep A"])
+apply(auto simp add: fun_rel_def)
+done
+
+lemma left_total_filter_rel [reflexivity_rule]:
+  assumes [transfer_rule]: "bi_total A" "bi_unique A"
+  shows "left_total (filter_rel A)"
+proof(rule left_totalI)
+  fix F :: "'a filter"
+  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
+  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
+    unfolding  bi_total_def by blast
+  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
+  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
+  ultimately have "filter_rel A F (Abs_filter G)"
+    by(simp add: filter_rel_eventually eventually_Abs_filter)
+  thus "\<exists>G. filter_rel A F G" ..
+qed
+
+lemma right_total_filter_rel [transfer_rule]:
+  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (filter_rel A)"
+using left_total_filter_rel[of "A\<inverse>\<inverse>"] by simp
+
+lemma bi_total_filter_rel [transfer_rule]:
+  assumes "bi_total A" "bi_unique A"
+  shows "bi_total (filter_rel A)"
+unfolding bi_total_conv_left_right using assms
+by(simp add: left_total_filter_rel right_total_filter_rel)
+
+lemma left_unique_filter_rel [reflexivity_rule]:
+  assumes "left_unique A"
+  shows "left_unique (filter_rel A)"
+proof(rule left_uniqueI)
+  fix F F' G
+  assume [transfer_rule]: "filter_rel A F G" "filter_rel A F' G"
+  show "F = F'"
+    unfolding filter_eq_iff
+  proof
+    fix P :: "'a \<Rightarrow> bool"
+    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
+      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
+    have "eventually P F = eventually P' G" 
+      and "eventually P F' = eventually P' G" by transfer_prover+
+    thus "eventually P F = eventually P F'" by simp
+  qed
+qed
+
+lemma right_unique_filter_rel [transfer_rule]:
+  "right_unique A \<Longrightarrow> right_unique (filter_rel A)"
+using left_unique_filter_rel[of "A\<inverse>\<inverse>"] by simp
+
+lemma bi_unique_filter_rel [transfer_rule]:
+  "bi_unique A \<Longrightarrow> bi_unique (filter_rel A)"
+by(simp add: bi_unique_conv_left_right left_unique_filter_rel right_unique_filter_rel)
+
+lemma top_filter_parametric [transfer_rule]:
+  "bi_total A \<Longrightarrow> (filter_rel A) top top"
+by(simp add: filter_rel_eventually All_transfer)
+
+lemma bot_filter_parametric [transfer_rule]: "(filter_rel A) bot bot"
+by(simp add: filter_rel_eventually fun_rel_def)
+
+lemma sup_filter_parametric [transfer_rule]:
+  "(filter_rel A ===> filter_rel A ===> filter_rel A) sup sup"
+by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD)
+
+lemma Sup_filter_parametric [transfer_rule]:
+  "(set_rel (filter_rel A) ===> filter_rel A) Sup Sup"
+proof(rule fun_relI)
+  fix S T
+  assume [transfer_rule]: "set_rel (filter_rel A) S T"
+  show "filter_rel A (Sup S) (Sup T)"
+    by(simp add: filter_rel_eventually eventually_Sup) transfer_prover
+qed
+
+lemma principal_parametric [transfer_rule]:
+  "(set_rel A ===> filter_rel A) principal principal"
+proof(rule fun_relI)
+  fix S S'
+  assume [transfer_rule]: "set_rel A S S'"
+  show "filter_rel A (principal S) (principal S')"
+    by(simp add: filter_rel_eventually eventually_principal) transfer_prover
+qed
+
+context
+  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+  assumes [transfer_rule]: "bi_unique A" 
+begin
+
+lemma le_filter_parametric [transfer_rule]:
+  "(filter_rel A ===> filter_rel A ===> op =) op \<le> op \<le>"
+unfolding le_filter_def[abs_def] by transfer_prover
+
+lemma less_filter_parametric [transfer_rule]:
+  "(filter_rel A ===> filter_rel A ===> op =) op < op <"
+unfolding less_filter_def[abs_def] by transfer_prover
+
+context
+  assumes [transfer_rule]: "bi_total A"
+begin
+
+lemma Inf_filter_parametric [transfer_rule]:
+  "(set_rel (filter_rel A) ===> filter_rel A) Inf Inf"
+unfolding Inf_filter_def[abs_def] by transfer_prover
+
+lemma inf_filter_parametric [transfer_rule]:
+  "(filter_rel A ===> filter_rel A ===> filter_rel A) inf inf"
+proof(intro fun_relI)+
+  fix F F' G G'
+  assume [transfer_rule]: "filter_rel A F F'" "filter_rel A G G'"
+  have "filter_rel A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
+  thus "filter_rel A (inf F G) (inf F' G')" by simp
+qed
+
 end
 
+end
+
+end
+
+end




