merged

--- a/src/HOL/Lifting.thy	Fri Sep 27 09:17:25 2013 +0200
+++ b/src/HOL/Lifting.thy	Fri Sep 27 10:40:02 2013 +0200
@@ -76,6 +76,16 @@
 
 lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
 
+lemma [simp]:
+  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
+  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+by(auto simp add: left_unique_def right_unique_def)
+
+lemma [simp]:
+  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
+  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
+by(simp_all add: left_total_def right_total_def)
+
 subsection {* Quotient Predicate *}
 
 definition

--- a/src/HOL/Lifting_Set.thy	Fri Sep 27 09:17:25 2013 +0200
+++ b/src/HOL/Lifting_Set.thy	Fri Sep 27 10:40:02 2013 +0200
@@ -23,7 +23,7 @@
   and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
 by(simp_all add: set_rel_def)
 
-lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
+lemma set_rel_conversep [simp]: "set_rel A\<inverse>\<inverse> = (set_rel A)\<inverse>\<inverse>"
   unfolding set_rel_def by auto
 
 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
@@ -71,8 +71,7 @@
 
 lemma right_total_set_rel [transfer_rule]:
   "right_total A \<Longrightarrow> right_total (set_rel A)"
-  unfolding right_total_def set_rel_def
-  by (rule allI, rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
+using left_total_set_rel[of "A\<inverse>\<inverse>"] by simp
 
 lemma right_unique_set_rel [transfer_rule]:
   "right_unique A \<Longrightarrow> right_unique (set_rel A)"
@@ -80,11 +79,7 @@
 
 lemma bi_total_set_rel [transfer_rule]:
   "bi_total A \<Longrightarrow> bi_total (set_rel A)"
-  unfolding bi_total_def set_rel_def
-  apply safe
-  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
-  apply (rename_tac Y, rule_tac x="{x. \<exists>y\<in>Y. A x y}" in exI, fast)
-  done
+by(simp add: bi_total_conv_left_right left_total_set_rel right_total_set_rel)
 
 lemma bi_unique_set_rel [transfer_rule]:
   "bi_unique A \<Longrightarrow> bi_unique (set_rel A)"
@@ -100,7 +95,7 @@
   assumes "Quotient R Abs Rep T"
   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
   using assms unfolding Quotient_alt_def4
-  apply (simp add: set_rel_OO[symmetric] set_rel_conversep)
+  apply (simp add: set_rel_OO[symmetric])
   apply (simp add: set_rel_def, fast)
   done
 

--- a/src/HOL/Predicate.thy	Fri Sep 27 09:17:25 2013 +0200
+++ b/src/HOL/Predicate.thy	Fri Sep 27 10:40:02 2013 +0200
@@ -5,7 +5,7 @@
 header {* Predicates as enumerations *}
 
 theory Predicate
-imports List
+imports String
 begin
 
 subsection {* The type of predicate enumerations (a monad) *}
@@ -590,13 +590,8 @@
   "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   by (simp add: the_def)
 
-definition not_unique :: "'a pred \<Rightarrow> 'a" where
-  [code del]: "not_unique A = (THE x. eval A x)"
-
-code_abort not_unique
-
-lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
-  by (rule the_eqI) (simp add: singleton_def not_unique_def)
+lemma the_eq [code]: "the A = singleton (\<lambda>x. Code.abort (STR ''not_unique'') (\<lambda>_. the A)) A"
+  by (rule the_eqI) (simp add: singleton_def the_def)
 
 code_reflect Predicate
   datatypes pred = Seq and seq = Empty | Insert | Join
@@ -722,7 +717,7 @@
 
 hide_type (open) pred seq
 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map the
   iterate_upto
 hide_fact (open) null_def member_def
 

--- a/src/HOL/Topological_Spaces.thy	Fri Sep 27 09:17:25 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy	Fri Sep 27 10:40:02 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

--- a/src/HOL/Transfer.thy	Fri Sep 27 09:17:25 2013 +0200
+++ b/src/HOL/Transfer.thy	Fri Sep 27 10:40:02 2013 +0200
@@ -201,6 +201,12 @@
   "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
   unfolding bi_unique_def fun_rel_def by auto
 
+lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
+by(auto simp add: bi_unique_def)
+
+lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
+by(auto simp add: bi_total_def)
+
 text {* Properties are preserved by relation composition. *}
 
 lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"