src/HOL/Transfer.thy
changeset 56524 f4ba736040fa
parent 56520 3373f5d1e074
child 56543 9bd56f2e4c10
     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