1.1 --- a/src/HOL/Transfer.thy Thu Apr 10 17:48:17 2014 +0200
1.2 +++ b/src/HOL/Transfer.thy Thu Apr 10 17:48:18 2014 +0200
1.3 @@ -6,9 +6,13 @@
1.4 header {* Generic theorem transfer using relations *}
1.5
1.6 theory Transfer
1.7 -imports Hilbert_Choice Basic_BNFs Metis
1.8 +imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
1.9 begin
1.10
1.11 +(* We include Option here altough it's not needed here.
1.12 + By doing this, we avoid a diamond problem for BNF and
1.13 + FP sugar interpretation defined in this file. *)
1.14 +
1.15 subsection {* Relator for function space *}
1.16
1.17 locale lifting_syntax
1.18 @@ -105,33 +109,6 @@
1.19 shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
1.20 using assms unfolding Rel_def rel_fun_def by fast
1.21
1.22 -end
1.23 -
1.24 -ML_file "Tools/transfer.ML"
1.25 -setup Transfer.setup
1.26 -
1.27 -declare refl [transfer_rule]
1.28 -
1.29 -declare rel_fun_eq [relator_eq]
1.30 -
1.31 -hide_const (open) Rel
1.32 -
1.33 -context
1.34 -begin
1.35 -interpretation lifting_syntax .
1.36 -
1.37 -text {* Handling of domains *}
1.38 -
1.39 -lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
1.40 - by auto
1.41 -
1.42 -lemma Domaimp_refl[transfer_domain_rule]:
1.43 - "Domainp T = Domainp T" ..
1.44 -
1.45 -lemma Domainp_prod_fun_eq[relator_domain]:
1.46 - "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
1.47 -by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
1.48 -
1.49 subsection {* Predicates on relations, i.e. ``class constraints'' *}
1.50
1.51 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
1.52 @@ -181,7 +158,7 @@
1.53 lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
1.54 unfolding right_unique_def by fast
1.55
1.56 -lemma right_total_alt_def:
1.57 +lemma right_total_alt_def2:
1.58 "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
1.59 unfolding right_total_def rel_fun_def
1.60 apply (rule iffI, fast)
1.61 @@ -191,11 +168,11 @@
1.62 apply fast
1.63 done
1.64
1.65 -lemma right_unique_alt_def:
1.66 +lemma right_unique_alt_def2:
1.67 "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
1.68 unfolding right_unique_def rel_fun_def by auto
1.69
1.70 -lemma bi_total_alt_def:
1.71 +lemma bi_total_alt_def2:
1.72 "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
1.73 unfolding bi_total_def rel_fun_def
1.74 apply (rule iffI, fast)
1.75 @@ -208,7 +185,7 @@
1.76 apply fast
1.77 done
1.78
1.79 -lemma bi_unique_alt_def:
1.80 +lemma bi_unique_alt_def2:
1.81 "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
1.82 unfolding bi_unique_def rel_fun_def by auto
1.83
1.84 @@ -228,24 +205,72 @@
1.85 lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
1.86 by(auto simp add: bi_total_def)
1.87
1.88 -lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
1.89 +lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> op=)" unfolding right_unique_def by blast
1.90 +lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> op=)" unfolding left_unique_def by blast
1.91 +
1.92 +lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> op=)" unfolding right_total_def by blast
1.93 +lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> op=)" unfolding left_total_def by blast
1.94 +
1.95 +lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)"
1.96 unfolding left_total_def right_total_def bi_total_def by blast
1.97
1.98 -lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
1.99 -by(simp add: left_total_def right_total_def bi_total_def)
1.100 -
1.101 -lemma bi_unique_iff: "bi_unique A \<longleftrightarrow> right_unique A \<and> left_unique A"
1.102 +lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)"
1.103 unfolding left_unique_def right_unique_def bi_unique_def by blast
1.104
1.105 -lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
1.106 -by(auto simp add: left_unique_def right_unique_def bi_unique_def)
1.107 -
1.108 lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
1.109 -unfolding bi_total_iff ..
1.110 +unfolding bi_total_alt_def ..
1.111
1.112 lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
1.113 -unfolding bi_unique_iff ..
1.114 +unfolding bi_unique_alt_def ..
1.115
1.116 +end
1.117 +
1.118 +subsection {* Equality restricted by a predicate *}
1.119 +
1.120 +definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.121 + where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
1.122 +
1.123 +lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id"
1.124 +unfolding eq_onp_def Grp_def by auto
1.125 +
1.126 +lemma eq_onp_to_eq:
1.127 + assumes "eq_onp P x y"
1.128 + shows "x = y"
1.129 +using assms by (simp add: eq_onp_def)
1.130 +
1.131 +lemma eq_onp_same_args:
1.132 + shows "eq_onp P x x = P x"
1.133 +using assms by (auto simp add: eq_onp_def)
1.134 +
1.135 +lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
1.136 +by (metis mem_Collect_eq subset_eq)
1.137 +
1.138 +ML_file "Tools/Transfer/transfer.ML"
1.139 +setup Transfer.setup
1.140 +declare refl [transfer_rule]
1.141 +
1.142 +ML_file "Tools/Transfer/transfer_bnf.ML"
1.143 +
1.144 +declare pred_fun_def [simp]
1.145 +declare rel_fun_eq [relator_eq]
1.146 +
1.147 +hide_const (open) Rel
1.148 +
1.149 +context
1.150 +begin
1.151 +interpretation lifting_syntax .
1.152 +
1.153 +text {* Handling of domains *}
1.154 +
1.155 +lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
1.156 + by auto
1.157 +
1.158 +lemma Domaimp_refl[transfer_domain_rule]:
1.159 + "Domainp T = Domainp T" ..
1.160 +
1.161 +lemma Domainp_prod_fun_eq[relator_domain]:
1.162 + "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
1.163 +by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
1.164
1.165 text {* Properties are preserved by relation composition. *}
1.166
1.167 @@ -333,12 +358,12 @@
1.168
1.169 lemma bi_total_fun[transfer_rule]:
1.170 "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
1.171 - unfolding bi_unique_iff bi_total_iff
1.172 + unfolding bi_unique_alt_def bi_total_alt_def
1.173 by (blast intro: right_total_fun left_total_fun)
1.174
1.175 lemma bi_unique_fun[transfer_rule]:
1.176 "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
1.177 - unfolding bi_unique_iff bi_total_iff
1.178 + unfolding bi_unique_alt_def bi_total_alt_def
1.179 by (blast intro: right_unique_fun left_unique_fun)
1.180
1.181 subsection {* Transfer rules *}
1.182 @@ -376,7 +401,7 @@
1.183
1.184 lemma eq_imp_transfer [transfer_rule]:
1.185 "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
1.186 - unfolding right_unique_alt_def .
1.187 + unfolding right_unique_alt_def2 .
1.188
1.189 text {* Transfer rules using equality. *}
1.190
1.191 @@ -490,6 +515,18 @@
1.192 using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
1.193 by metis
1.194
1.195 +lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
1.196 +unfolding eq_onp_def rel_fun_def by auto
1.197 +
1.198 +lemma rel_fun_eq_onp_rel:
1.199 + shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
1.200 +by (auto simp add: eq_onp_def rel_fun_def)
1.201 +
1.202 +lemma eq_onp_transfer [transfer_rule]:
1.203 + assumes [transfer_rule]: "bi_unique A"
1.204 + shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
1.205 +unfolding eq_onp_def[abs_def] by transfer_prover
1.206 +
1.207 end
1.208
1.209 end