# HG changeset patch # User blanchet # Date 1394115249 -3600 # Node ID c2d96043de4b0d594094f8b6d703f35a5c792cfa # Parent a6a380edbec5d0d63dcc09563345ea52b7c56a4e renamed 'filter_rel' to 'rel_filter' diff -r a6a380edbec5 -r c2d96043de4b NEWS --- a/NEWS Thu Mar 06 15:12:23 2014 +0100 +++ b/NEWS Thu Mar 06 15:14:09 2014 +0100 @@ -193,10 +193,11 @@ * The following map functions and relators have been renamed: sum_map ~> map_sum map_pair ~> map_prod + set_rel ~> rel_set + filter_rel ~> rel_filter fset_rel ~> rel_fset (in "Library/FSet.thy") cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy") - set_rel ~> rel_set - rel_vset ~> vset_rel (in "Library/Quotient_Set.thy") + vset ~> rel_vset (in "Library/Quotient_Set.thy") * New theory: Cardinals/Ordinal_Arithmetic.thy diff -r a6a380edbec5 -r c2d96043de4b src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Thu Mar 06 15:12:23 2014 +0100 +++ b/src/HOL/Topological_Spaces.thy Thu Mar 06 15:14:09 2014 +0100 @@ -2338,13 +2338,13 @@ context begin interpretation lifting_syntax . -definition filter_rel :: "('a \ 'b \ bool) \ 'a filter \ 'b filter \ 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 \ +definition rel_filter :: "('a \ 'b \ bool) \ 'a filter \ 'b filter \ bool" +where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)" + +lemma rel_filter_eventually: + "rel_filter R F G \ ((R ===> op =) ===> op =) (\P. eventually P F) (\P. eventually P G)" -by(simp add: filter_rel_def eventually_def) +by(simp add: rel_filter_def eventually_def) lemma filtermap_id [simp, id_simps]: "filtermap id = id" by(simp add: fun_eq_iff id_def filtermap_ident) @@ -2354,40 +2354,40 @@ lemma Quotient_filter [quot_map]: assumes Q: "Quotient R Abs Rep T" - shows "Quotient (filter_rel R) (filtermap Abs) (filtermap Rep) (filter_rel T)" + shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)" unfolding Quotient_alt_def proof(intro conjI strip) from Q have *: "\x y. T x y \ Abs x = y" unfolding Quotient_alt_def by blast fix F G - assume "filter_rel T F G" + assume "rel_filter 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) + by(auto simp add: eventually_filtermap rel_filter_eventually * fun_relI del: iffI elim!: fun_relD) next from Q have *: "\x. T (Rep x) x" unfolding Quotient_alt_def by blast fix F - show "filter_rel T (filtermap Rep F) F" + show "rel_filter T (filtermap Rep F) F" by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\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 + del: iffI simp add: eventually_filtermap rel_filter_eventually) +qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_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 \ B \ filter_rel A \ filter_rel B" -unfolding filter_rel_eventually[abs_def] + "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually" +by(simp add: fun_rel_def rel_filter_eventually) + +lemma rel_filter_eq [relator_eq]: "rel_filter op = = op =" +by(auto simp add: rel_filter_eventually fun_rel_eq fun_eq_iff filter_eq_iff) + +lemma rel_filter_mono [relator_mono]: + "A \ B \ rel_filter A \ rel_filter B" +unfolding rel_filter_eventually[abs_def] by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl) -lemma filter_rel_conversep [simp]: "filter_rel A\\ = (filter_rel A)\\" -by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def) +lemma rel_filter_conversep [simp]: "rel_filter A\\ = (rel_filter A)\\" +by(auto simp add: rel_filter_eventually fun_eq_iff fun_rel_def) lemma is_filter_parametric_aux: assumes "is_filter F" @@ -2434,9 +2434,9 @@ apply(auto simp add: fun_rel_def) done -lemma left_total_filter_rel [reflexivity_rule]: +lemma left_total_rel_filter [reflexivity_rule]: assumes [transfer_rule]: "bi_total A" "bi_unique A" - shows "left_total (filter_rel A)" + shows "left_total (rel_filter 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] @@ -2444,27 +2444,27 @@ unfolding bi_total_def by blast moreover have "is_filter (\P. eventually P F) \ 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 "\G. filter_rel A F G" .. + ultimately have "rel_filter A F (Abs_filter G)" + by(simp add: rel_filter_eventually eventually_Abs_filter) + thus "\G. rel_filter A F G" .. qed -lemma right_total_filter_rel [transfer_rule]: - "\ bi_total A; bi_unique A \ \ right_total (filter_rel A)" -using left_total_filter_rel[of "A\\"] by simp - -lemma bi_total_filter_rel [transfer_rule]: +lemma right_total_rel_filter [transfer_rule]: + "\ bi_total A; bi_unique A \ \ right_total (rel_filter A)" +using left_total_rel_filter[of "A\\"] by simp + +lemma bi_total_rel_filter [transfer_rule]: assumes "bi_total A" "bi_unique A" - shows "bi_total (filter_rel A)" + shows "bi_total (rel_filter 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]: +by(simp add: left_total_rel_filter right_total_rel_filter) + +lemma left_unique_rel_filter [reflexivity_rule]: assumes "left_unique A" - shows "left_unique (filter_rel A)" + shows "left_unique (rel_filter A)" proof(rule left_uniqueI) fix F F' G - assume [transfer_rule]: "filter_rel A F G" "filter_rel A F' G" + assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G" show "F = F'" unfolding filter_eq_iff proof @@ -2477,41 +2477,41 @@ qed qed -lemma right_unique_filter_rel [transfer_rule]: - "right_unique A \ right_unique (filter_rel A)" -using left_unique_filter_rel[of "A\\"] by simp - -lemma bi_unique_filter_rel [transfer_rule]: - "bi_unique A \ bi_unique (filter_rel A)" -by(simp add: bi_unique_conv_left_right left_unique_filter_rel right_unique_filter_rel) +lemma right_unique_rel_filter [transfer_rule]: + "right_unique A \ right_unique (rel_filter A)" +using left_unique_rel_filter[of "A\\"] by simp + +lemma bi_unique_rel_filter [transfer_rule]: + "bi_unique A \ bi_unique (rel_filter A)" +by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter) lemma top_filter_parametric [transfer_rule]: - "bi_total A \ (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) + "bi_total A \ (rel_filter A) top top" +by(simp add: rel_filter_eventually All_transfer) + +lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot" +by(simp add: rel_filter_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) + "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup" +by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: fun_relD) lemma Sup_filter_parametric [transfer_rule]: - "(rel_set (filter_rel A) ===> filter_rel A) Sup Sup" + "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup" proof(rule fun_relI) fix S T - assume [transfer_rule]: "rel_set (filter_rel A) S T" - show "filter_rel A (Sup S) (Sup T)" - by(simp add: filter_rel_eventually eventually_Sup) transfer_prover + assume [transfer_rule]: "rel_set (rel_filter A) S T" + show "rel_filter A (Sup S) (Sup T)" + by(simp add: rel_filter_eventually eventually_Sup) transfer_prover qed lemma principal_parametric [transfer_rule]: - "(rel_set A ===> filter_rel A) principal principal" + "(rel_set A ===> rel_filter A) principal principal" proof(rule fun_relI) fix S S' assume [transfer_rule]: "rel_set A S S'" - show "filter_rel A (principal S) (principal S')" - by(simp add: filter_rel_eventually eventually_principal) transfer_prover + show "rel_filter A (principal S) (principal S')" + by(simp add: rel_filter_eventually eventually_principal) transfer_prover qed context @@ -2520,11 +2520,11 @@ begin lemma le_filter_parametric [transfer_rule]: - "(filter_rel A ===> filter_rel A ===> op =) op \ op \" + "(rel_filter A ===> rel_filter A ===> op =) op \ op \" unfolding le_filter_def[abs_def] by transfer_prover lemma less_filter_parametric [transfer_rule]: - "(filter_rel A ===> filter_rel A ===> op =) op < op <" + "(rel_filter A ===> rel_filter A ===> op =) op < op <" unfolding less_filter_def[abs_def] by transfer_prover context @@ -2532,16 +2532,16 @@ begin lemma Inf_filter_parametric [transfer_rule]: - "(rel_set (filter_rel A) ===> filter_rel A) Inf Inf" + "(rel_set (rel_filter A) ===> rel_filter 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" + "(rel_filter A ===> rel_filter A ===> rel_filter 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 + assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'" + have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover + thus "rel_filter A (inf F G) (inf F' G')" by simp qed end