renamed 'filter_rel' to 'rel_filter'
authorblanchet
Thu Mar 06 15:14:09 2014 +0100 (2014-03-06)
changeset 55942c2d96043de4b
parent 55941 a6a380edbec5
child 55943 5c2df04e97d1
renamed 'filter_rel' to 'rel_filter'
NEWS
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Thu Mar 06 15:12:23 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 15:14:09 2014 +0100
     1.3 @@ -193,10 +193,11 @@
     1.4  * The following map functions and relators have been renamed:
     1.5      sum_map ~> map_sum
     1.6      map_pair ~> map_prod
     1.7 +    set_rel ~> rel_set
     1.8 +    filter_rel ~> rel_filter
     1.9      fset_rel ~> rel_fset (in "Library/FSet.thy")
    1.10      cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
    1.11 -    set_rel ~> rel_set
    1.12 -    rel_vset ~> vset_rel (in "Library/Quotient_Set.thy")
    1.13 +    vset ~> rel_vset (in "Library/Quotient_Set.thy")
    1.14  
    1.15  * New theory:
    1.16      Cardinals/Ordinal_Arithmetic.thy
     2.1 --- a/src/HOL/Topological_Spaces.thy	Thu Mar 06 15:12:23 2014 +0100
     2.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Mar 06 15:14:09 2014 +0100
     2.3 @@ -2338,13 +2338,13 @@
     2.4  
     2.5  context begin interpretation lifting_syntax .
     2.6  
     2.7 -definition filter_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
     2.8 -where "filter_rel R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
     2.9 -
    2.10 -lemma filter_rel_eventually:
    2.11 -  "filter_rel R F G \<longleftrightarrow> 
    2.12 +definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
    2.13 +where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
    2.14 +
    2.15 +lemma rel_filter_eventually:
    2.16 +  "rel_filter R F G \<longleftrightarrow> 
    2.17    ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
    2.18 -by(simp add: filter_rel_def eventually_def)
    2.19 +by(simp add: rel_filter_def eventually_def)
    2.20  
    2.21  lemma filtermap_id [simp, id_simps]: "filtermap id = id"
    2.22  by(simp add: fun_eq_iff id_def filtermap_ident)
    2.23 @@ -2354,40 +2354,40 @@
    2.24  
    2.25  lemma Quotient_filter [quot_map]:
    2.26    assumes Q: "Quotient R Abs Rep T"
    2.27 -  shows "Quotient (filter_rel R) (filtermap Abs) (filtermap Rep) (filter_rel T)"
    2.28 +  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
    2.29  unfolding Quotient_alt_def
    2.30  proof(intro conjI strip)
    2.31    from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
    2.32      unfolding Quotient_alt_def by blast
    2.33  
    2.34    fix F G
    2.35 -  assume "filter_rel T F G"
    2.36 +  assume "rel_filter T F G"
    2.37    thus "filtermap Abs F = G" unfolding filter_eq_iff
    2.38 -    by(auto simp add: eventually_filtermap filter_rel_eventually * fun_relI del: iffI elim!: fun_relD)
    2.39 +    by(auto simp add: eventually_filtermap rel_filter_eventually * fun_relI del: iffI elim!: fun_relD)
    2.40  next
    2.41    from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
    2.42  
    2.43    fix F
    2.44 -  show "filter_rel T (filtermap Rep F) F" 
    2.45 +  show "rel_filter T (filtermap Rep F) F" 
    2.46      by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI
    2.47 -            del: iffI simp add: eventually_filtermap filter_rel_eventually)
    2.48 -qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff filter_rel_eventually
    2.49 +            del: iffI simp add: eventually_filtermap rel_filter_eventually)
    2.50 +qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
    2.51           fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
    2.52  
    2.53  lemma eventually_parametric [transfer_rule]:
    2.54 -  "((A ===> op =) ===> filter_rel A ===> op =) eventually eventually"
    2.55 -by(simp add: fun_rel_def filter_rel_eventually)
    2.56 -
    2.57 -lemma filter_rel_eq [relator_eq]: "filter_rel op = = op ="
    2.58 -by(auto simp add: filter_rel_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
    2.59 -
    2.60 -lemma filter_rel_mono [relator_mono]:
    2.61 -  "A \<le> B \<Longrightarrow> filter_rel A \<le> filter_rel B"
    2.62 -unfolding filter_rel_eventually[abs_def]
    2.63 +  "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
    2.64 +by(simp add: fun_rel_def rel_filter_eventually)
    2.65 +
    2.66 +lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
    2.67 +by(auto simp add: rel_filter_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
    2.68 +
    2.69 +lemma rel_filter_mono [relator_mono]:
    2.70 +  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
    2.71 +unfolding rel_filter_eventually[abs_def]
    2.72  by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
    2.73  
    2.74 -lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>"
    2.75 -by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)
    2.76 +lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
    2.77 +by(auto simp add: rel_filter_eventually fun_eq_iff fun_rel_def)
    2.78  
    2.79  lemma is_filter_parametric_aux:
    2.80    assumes "is_filter F"
    2.81 @@ -2434,9 +2434,9 @@
    2.82  apply(auto simp add: fun_rel_def)
    2.83  done
    2.84  
    2.85 -lemma left_total_filter_rel [reflexivity_rule]:
    2.86 +lemma left_total_rel_filter [reflexivity_rule]:
    2.87    assumes [transfer_rule]: "bi_total A" "bi_unique A"
    2.88 -  shows "left_total (filter_rel A)"
    2.89 +  shows "left_total (rel_filter A)"
    2.90  proof(rule left_totalI)
    2.91    fix F :: "'a filter"
    2.92    from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
    2.93 @@ -2444,27 +2444,27 @@
    2.94      unfolding  bi_total_def by blast
    2.95    moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
    2.96    hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
    2.97 -  ultimately have "filter_rel A F (Abs_filter G)"
    2.98 -    by(simp add: filter_rel_eventually eventually_Abs_filter)
    2.99 -  thus "\<exists>G. filter_rel A F G" ..
   2.100 +  ultimately have "rel_filter A F (Abs_filter G)"
   2.101 +    by(simp add: rel_filter_eventually eventually_Abs_filter)
   2.102 +  thus "\<exists>G. rel_filter A F G" ..
   2.103  qed
   2.104  
   2.105 -lemma right_total_filter_rel [transfer_rule]:
   2.106 -  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (filter_rel A)"
   2.107 -using left_total_filter_rel[of "A\<inverse>\<inverse>"] by simp
   2.108 -
   2.109 -lemma bi_total_filter_rel [transfer_rule]:
   2.110 +lemma right_total_rel_filter [transfer_rule]:
   2.111 +  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
   2.112 +using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
   2.113 +
   2.114 +lemma bi_total_rel_filter [transfer_rule]:
   2.115    assumes "bi_total A" "bi_unique A"
   2.116 -  shows "bi_total (filter_rel A)"
   2.117 +  shows "bi_total (rel_filter A)"
   2.118  unfolding bi_total_conv_left_right using assms
   2.119 -by(simp add: left_total_filter_rel right_total_filter_rel)
   2.120 -
   2.121 -lemma left_unique_filter_rel [reflexivity_rule]:
   2.122 +by(simp add: left_total_rel_filter right_total_rel_filter)
   2.123 +
   2.124 +lemma left_unique_rel_filter [reflexivity_rule]:
   2.125    assumes "left_unique A"
   2.126 -  shows "left_unique (filter_rel A)"
   2.127 +  shows "left_unique (rel_filter A)"
   2.128  proof(rule left_uniqueI)
   2.129    fix F F' G
   2.130 -  assume [transfer_rule]: "filter_rel A F G" "filter_rel A F' G"
   2.131 +  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
   2.132    show "F = F'"
   2.133      unfolding filter_eq_iff
   2.134    proof
   2.135 @@ -2477,41 +2477,41 @@
   2.136    qed
   2.137  qed
   2.138  
   2.139 -lemma right_unique_filter_rel [transfer_rule]:
   2.140 -  "right_unique A \<Longrightarrow> right_unique (filter_rel A)"
   2.141 -using left_unique_filter_rel[of "A\<inverse>\<inverse>"] by simp
   2.142 -
   2.143 -lemma bi_unique_filter_rel [transfer_rule]:
   2.144 -  "bi_unique A \<Longrightarrow> bi_unique (filter_rel A)"
   2.145 -by(simp add: bi_unique_conv_left_right left_unique_filter_rel right_unique_filter_rel)
   2.146 +lemma right_unique_rel_filter [transfer_rule]:
   2.147 +  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
   2.148 +using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
   2.149 +
   2.150 +lemma bi_unique_rel_filter [transfer_rule]:
   2.151 +  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
   2.152 +by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter)
   2.153  
   2.154  lemma top_filter_parametric [transfer_rule]:
   2.155 -  "bi_total A \<Longrightarrow> (filter_rel A) top top"
   2.156 -by(simp add: filter_rel_eventually All_transfer)
   2.157 -
   2.158 -lemma bot_filter_parametric [transfer_rule]: "(filter_rel A) bot bot"
   2.159 -by(simp add: filter_rel_eventually fun_rel_def)
   2.160 +  "bi_total A \<Longrightarrow> (rel_filter A) top top"
   2.161 +by(simp add: rel_filter_eventually All_transfer)
   2.162 +
   2.163 +lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
   2.164 +by(simp add: rel_filter_eventually fun_rel_def)
   2.165  
   2.166  lemma sup_filter_parametric [transfer_rule]:
   2.167 -  "(filter_rel A ===> filter_rel A ===> filter_rel A) sup sup"
   2.168 -by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD)
   2.169 +  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   2.170 +by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: fun_relD)
   2.171  
   2.172  lemma Sup_filter_parametric [transfer_rule]:
   2.173 -  "(rel_set (filter_rel A) ===> filter_rel A) Sup Sup"
   2.174 +  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   2.175  proof(rule fun_relI)
   2.176    fix S T
   2.177 -  assume [transfer_rule]: "rel_set (filter_rel A) S T"
   2.178 -  show "filter_rel A (Sup S) (Sup T)"
   2.179 -    by(simp add: filter_rel_eventually eventually_Sup) transfer_prover
   2.180 +  assume [transfer_rule]: "rel_set (rel_filter A) S T"
   2.181 +  show "rel_filter A (Sup S) (Sup T)"
   2.182 +    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
   2.183  qed
   2.184  
   2.185  lemma principal_parametric [transfer_rule]:
   2.186 -  "(rel_set A ===> filter_rel A) principal principal"
   2.187 +  "(rel_set A ===> rel_filter A) principal principal"
   2.188  proof(rule fun_relI)
   2.189    fix S S'
   2.190    assume [transfer_rule]: "rel_set A S S'"
   2.191 -  show "filter_rel A (principal S) (principal S')"
   2.192 -    by(simp add: filter_rel_eventually eventually_principal) transfer_prover
   2.193 +  show "rel_filter A (principal S) (principal S')"
   2.194 +    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
   2.195  qed
   2.196  
   2.197  context
   2.198 @@ -2520,11 +2520,11 @@
   2.199  begin
   2.200  
   2.201  lemma le_filter_parametric [transfer_rule]:
   2.202 -  "(filter_rel A ===> filter_rel A ===> op =) op \<le> op \<le>"
   2.203 +  "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
   2.204  unfolding le_filter_def[abs_def] by transfer_prover
   2.205  
   2.206  lemma less_filter_parametric [transfer_rule]:
   2.207 -  "(filter_rel A ===> filter_rel A ===> op =) op < op <"
   2.208 +  "(rel_filter A ===> rel_filter A ===> op =) op < op <"
   2.209  unfolding less_filter_def[abs_def] by transfer_prover
   2.210  
   2.211  context
   2.212 @@ -2532,16 +2532,16 @@
   2.213  begin
   2.214  
   2.215  lemma Inf_filter_parametric [transfer_rule]:
   2.216 -  "(rel_set (filter_rel A) ===> filter_rel A) Inf Inf"
   2.217 +  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
   2.218  unfolding Inf_filter_def[abs_def] by transfer_prover
   2.219  
   2.220  lemma inf_filter_parametric [transfer_rule]:
   2.221 -  "(filter_rel A ===> filter_rel A ===> filter_rel A) inf inf"
   2.222 +  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
   2.223  proof(intro fun_relI)+
   2.224    fix F F' G G'
   2.225 -  assume [transfer_rule]: "filter_rel A F F'" "filter_rel A G G'"
   2.226 -  have "filter_rel A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
   2.227 -  thus "filter_rel A (inf F G) (inf F' G')" by simp
   2.228 +  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
   2.229 +  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
   2.230 +  thus "rel_filter A (inf F G) (inf F' G')" by simp
   2.231  qed
   2.232  
   2.233  end