add relator for 'a filter and parametricity theorems
authorAndreas Lochbihler
Fri Sep 27 09:26:31 2013 +0200 (2013-09-27)
changeset 539465431e1392b14
parent 53945 4191acef9d0e
child 53947 54b08afc03c7
add relator for 'a filter and parametricity theorems
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Topological_Spaces.thy	Fri Sep 27 09:15:40 2013 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Sep 27 09:26:31 2013 +0200
     1.3 @@ -2282,5 +2282,224 @@
     1.4      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)
     1.5  qed
     1.6  
     1.7 +subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
     1.8 +
     1.9 +context begin interpretation lifting_syntax .
    1.10 +
    1.11 +definition filter_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
    1.12 +where "filter_rel R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
    1.13 +
    1.14 +lemma filter_rel_eventually:
    1.15 +  "filter_rel R F G \<longleftrightarrow> 
    1.16 +  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
    1.17 +by(simp add: filter_rel_def eventually_def)
    1.18 +
    1.19 +lemma filtermap_id [simp, id_simps]: "filtermap id = id"
    1.20 +by(simp add: fun_eq_iff id_def filtermap_ident)
    1.21 +
    1.22 +lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
    1.23 +using filtermap_id unfolding id_def .
    1.24 +
    1.25 +lemma Quotient_filter [quot_map]:
    1.26 +  assumes Q: "Quotient R Abs Rep T"
    1.27 +  shows "Quotient (filter_rel R) (filtermap Abs) (filtermap Rep) (filter_rel T)"
    1.28 +unfolding Quotient_alt_def
    1.29 +proof(intro conjI strip)
    1.30 +  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
    1.31 +    unfolding Quotient_alt_def by blast
    1.32 +
    1.33 +  fix F G
    1.34 +  assume "filter_rel T F G"
    1.35 +  thus "filtermap Abs F = G" unfolding filter_eq_iff
    1.36 +    by(auto simp add: eventually_filtermap filter_rel_eventually * fun_relI del: iffI elim!: fun_relD)
    1.37 +next
    1.38 +  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
    1.39 +
    1.40 +  fix F
    1.41 +  show "filter_rel T (filtermap Rep F) F" 
    1.42 +    by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI
    1.43 +            del: iffI simp add: eventually_filtermap filter_rel_eventually)
    1.44 +qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff filter_rel_eventually
    1.45 +         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
    1.46 +
    1.47 +lemma eventually_parametric [transfer_rule]:
    1.48 +  "((A ===> op =) ===> filter_rel A ===> op =) eventually eventually"
    1.49 +by(simp add: fun_rel_def filter_rel_eventually)
    1.50 +
    1.51 +lemma filter_rel_eq [relator_eq]: "filter_rel op = = op ="
    1.52 +by(auto simp add: filter_rel_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
    1.53 +
    1.54 +lemma filter_rel_mono [relator_mono]:
    1.55 +  "A \<le> B \<Longrightarrow> filter_rel A \<le> filter_rel B"
    1.56 +unfolding filter_rel_eventually[abs_def]
    1.57 +by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
    1.58 +
    1.59 +lemma reflp_filter_rel [reflexivity_rule]: "reflp R \<Longrightarrow> reflp (filter_rel R)"
    1.60 +unfolding filter_rel_eventually[abs_def]
    1.61 +by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD)
    1.62 +
    1.63 +lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>"
    1.64 +by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)
    1.65 +
    1.66 +lemma is_filter_parametric_aux:
    1.67 +  assumes "is_filter F"
    1.68 +  assumes [transfer_rule]: "bi_total A" "bi_unique A"
    1.69 +  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
    1.70 +  shows "is_filter G"
    1.71 +proof -
    1.72 +  interpret is_filter F by fact
    1.73 +  show ?thesis
    1.74 +  proof
    1.75 +    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
    1.76 +    thus "G (\<lambda>x. True)" by(simp add: True)
    1.77 +  next
    1.78 +    fix P' Q'
    1.79 +    assume "G P'" "G Q'"
    1.80 +    moreover
    1.81 +    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
    1.82 +    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
    1.83 +    have "F P = G P'" "F Q = G Q'" by transfer_prover+
    1.84 +    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
    1.85 +    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
    1.86 +    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
    1.87 +  next
    1.88 +    fix P' Q'
    1.89 +    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
    1.90 +    moreover
    1.91 +    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
    1.92 +    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
    1.93 +    have "F P = G P'" by transfer_prover
    1.94 +    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
    1.95 +    ultimately have "F Q" by(simp add: mono)
    1.96 +    moreover have "F Q = G Q'" by transfer_prover
    1.97 +    ultimately show "G Q'" by simp
    1.98 +  qed
    1.99 +qed
   1.100 +
   1.101 +lemma is_filter_parametric [transfer_rule]:
   1.102 +  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
   1.103 +  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
   1.104 +apply(rule fun_relI)
   1.105 +apply(rule iffI)
   1.106 + apply(erule (3) is_filter_parametric_aux)
   1.107 +apply(erule is_filter_parametric_aux[where A="conversep A"])
   1.108 +apply(auto simp add: fun_rel_def)
   1.109 +done
   1.110 +
   1.111 +lemma left_total_filter_rel [reflexivity_rule]:
   1.112 +  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   1.113 +  shows "left_total (filter_rel A)"
   1.114 +proof(rule left_totalI)
   1.115 +  fix F :: "'a filter"
   1.116 +  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
   1.117 +  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
   1.118 +    unfolding  bi_total_def by blast
   1.119 +  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   1.120 +  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
   1.121 +  ultimately have "filter_rel A F (Abs_filter G)"
   1.122 +    by(simp add: filter_rel_eventually eventually_Abs_filter)
   1.123 +  thus "\<exists>G. filter_rel A F G" ..
   1.124 +qed
   1.125 +
   1.126 +lemma right_total_filter_rel [transfer_rule]:
   1.127 +  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (filter_rel A)"
   1.128 +using left_total_filter_rel[of "A\<inverse>\<inverse>"] by simp
   1.129 +
   1.130 +lemma bi_total_filter_rel [transfer_rule]:
   1.131 +  assumes "bi_total A" "bi_unique A"
   1.132 +  shows "bi_total (filter_rel A)"
   1.133 +unfolding bi_total_conv_left_right using assms
   1.134 +by(simp add: left_total_filter_rel right_total_filter_rel)
   1.135 +
   1.136 +lemma left_unique_filter_rel [reflexivity_rule]:
   1.137 +  assumes "left_unique A"
   1.138 +  shows "left_unique (filter_rel A)"
   1.139 +proof(rule left_uniqueI)
   1.140 +  fix F F' G
   1.141 +  assume [transfer_rule]: "filter_rel A F G" "filter_rel A F' G"
   1.142 +  show "F = F'"
   1.143 +    unfolding filter_eq_iff
   1.144 +  proof
   1.145 +    fix P :: "'a \<Rightarrow> bool"
   1.146 +    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
   1.147 +      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
   1.148 +    have "eventually P F = eventually P' G" 
   1.149 +      and "eventually P F' = eventually P' G" by transfer_prover+
   1.150 +    thus "eventually P F = eventually P F'" by simp
   1.151 +  qed
   1.152 +qed
   1.153 +
   1.154 +lemma right_unique_filter_rel [transfer_rule]:
   1.155 +  "right_unique A \<Longrightarrow> right_unique (filter_rel A)"
   1.156 +using left_unique_filter_rel[of "A\<inverse>\<inverse>"] by simp
   1.157 +
   1.158 +lemma bi_unique_filter_rel [transfer_rule]:
   1.159 +  "bi_unique A \<Longrightarrow> bi_unique (filter_rel A)"
   1.160 +by(simp add: bi_unique_conv_left_right left_unique_filter_rel right_unique_filter_rel)
   1.161 +
   1.162 +lemma top_filter_parametric [transfer_rule]:
   1.163 +  "bi_total A \<Longrightarrow> (filter_rel A) top top"
   1.164 +by(simp add: filter_rel_eventually All_transfer)
   1.165 +
   1.166 +lemma bot_filter_parametric [transfer_rule]: "(filter_rel A) bot bot"
   1.167 +by(simp add: filter_rel_eventually fun_rel_def)
   1.168 +
   1.169 +lemma sup_filter_parametric [transfer_rule]:
   1.170 +  "(filter_rel A ===> filter_rel A ===> filter_rel A) sup sup"
   1.171 +by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD)
   1.172 +
   1.173 +lemma Sup_filter_parametric [transfer_rule]:
   1.174 +  "(set_rel (filter_rel A) ===> filter_rel A) Sup Sup"
   1.175 +proof(rule fun_relI)
   1.176 +  fix S T
   1.177 +  assume [transfer_rule]: "set_rel (filter_rel A) S T"
   1.178 +  show "filter_rel A (Sup S) (Sup T)"
   1.179 +    by(simp add: filter_rel_eventually eventually_Sup) transfer_prover
   1.180 +qed
   1.181 +
   1.182 +lemma principal_parametric [transfer_rule]:
   1.183 +  "(set_rel A ===> filter_rel A) principal principal"
   1.184 +proof(rule fun_relI)
   1.185 +  fix S S'
   1.186 +  assume [transfer_rule]: "set_rel A S S'"
   1.187 +  show "filter_rel A (principal S) (principal S')"
   1.188 +    by(simp add: filter_rel_eventually eventually_principal) transfer_prover
   1.189 +qed
   1.190 +
   1.191 +context
   1.192 +  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.193 +  assumes [transfer_rule]: "bi_unique A" 
   1.194 +begin
   1.195 +
   1.196 +lemma le_filter_parametric [transfer_rule]:
   1.197 +  "(filter_rel A ===> filter_rel A ===> op =) op \<le> op \<le>"
   1.198 +unfolding le_filter_def[abs_def] by transfer_prover
   1.199 +
   1.200 +lemma less_filter_parametric [transfer_rule]:
   1.201 +  "(filter_rel A ===> filter_rel A ===> op =) op < op <"
   1.202 +unfolding less_filter_def[abs_def] by transfer_prover
   1.203 +
   1.204 +context
   1.205 +  assumes [transfer_rule]: "bi_total A"
   1.206 +begin
   1.207 +
   1.208 +lemma Inf_filter_parametric [transfer_rule]:
   1.209 +  "(set_rel (filter_rel A) ===> filter_rel A) Inf Inf"
   1.210 +unfolding Inf_filter_def[abs_def] by transfer_prover
   1.211 +
   1.212 +lemma inf_filter_parametric [transfer_rule]:
   1.213 +  "(filter_rel A ===> filter_rel A ===> filter_rel A) inf inf"
   1.214 +proof(intro fun_relI)+
   1.215 +  fix F F' G G'
   1.216 +  assume [transfer_rule]: "filter_rel A F F'" "filter_rel A G G'"
   1.217 +  have "filter_rel A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
   1.218 +  thus "filter_rel A (inf F G) (inf F' G')" by simp
   1.219 +qed
   1.220 +
   1.221  end
   1.222  
   1.223 +end
   1.224 +
   1.225 +end
   1.226 +
   1.227 +end