src/HOL/Transfer.thy
author blanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 56654 54326fa7afe6
parent 56543 9bd56f2e4c10
child 56677 660ffb526069
permissions -rw-r--r--
qualify name
     1 (*  Title:      HOL/Transfer.thy
     2     Author:     Brian Huffman, TU Muenchen
     3     Author:     Ondrej Kuncar, TU Muenchen
     4 *)
     5 
     6 header {* Generic theorem transfer using relations *}
     7 
     8 theory Transfer
     9 imports Hilbert_Choice BNF_FP_Base Metis Option
    10 begin
    11 
    12 (* We include Option here altough it's not needed here. 
    13    By doing this, we avoid a diamond problem for BNF and 
    14    FP sugar interpretation defined in this file. *)
    15 
    16 subsection {* Relator for function space *}
    17 
    18 locale lifting_syntax
    19 begin
    20   notation rel_fun (infixr "===>" 55)
    21   notation map_fun (infixr "--->" 55)
    22 end
    23 
    24 context
    25 begin
    26 interpretation lifting_syntax .
    27 
    28 lemma rel_funD2:
    29   assumes "rel_fun A B f g" and "A x x"
    30   shows "B (f x) (g x)"
    31   using assms by (rule rel_funD)
    32 
    33 lemma rel_funE:
    34   assumes "rel_fun A B f g" and "A x y"
    35   obtains "B (f x) (g y)"
    36   using assms by (simp add: rel_fun_def)
    37 
    38 lemmas rel_fun_eq = fun.rel_eq
    39 
    40 lemma rel_fun_eq_rel:
    41 shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
    42   by (simp add: rel_fun_def)
    43 
    44 
    45 subsection {* Transfer method *}
    46 
    47 text {* Explicit tag for relation membership allows for
    48   backward proof methods. *}
    49 
    50 definition Rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    51   where "Rel r \<equiv> r"
    52 
    53 text {* Handling of equality relations *}
    54 
    55 definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    56   where "is_equality R \<longleftrightarrow> R = (op =)"
    57 
    58 lemma is_equality_eq: "is_equality (op =)"
    59   unfolding is_equality_def by simp
    60 
    61 text {* Reverse implication for monotonicity rules *}
    62 
    63 definition rev_implies where
    64   "rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)"
    65 
    66 text {* Handling of meta-logic connectives *}
    67 
    68 definition transfer_forall where
    69   "transfer_forall \<equiv> All"
    70 
    71 definition transfer_implies where
    72   "transfer_implies \<equiv> op \<longrightarrow>"
    73 
    74 definition transfer_bforall :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    75   where "transfer_bforall \<equiv> (\<lambda>P Q. \<forall>x. P x \<longrightarrow> Q x)"
    76 
    77 lemma transfer_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (transfer_forall (\<lambda>x. P x))"
    78   unfolding atomize_all transfer_forall_def ..
    79 
    80 lemma transfer_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (transfer_implies A B)"
    81   unfolding atomize_imp transfer_implies_def ..
    82 
    83 lemma transfer_bforall_unfold:
    84   "Trueprop (transfer_bforall P (\<lambda>x. Q x)) \<equiv> (\<And>x. P x \<Longrightarrow> Q x)"
    85   unfolding transfer_bforall_def atomize_imp atomize_all ..
    86 
    87 lemma transfer_start: "\<lbrakk>P; Rel (op =) P Q\<rbrakk> \<Longrightarrow> Q"
    88   unfolding Rel_def by simp
    89 
    90 lemma transfer_start': "\<lbrakk>P; Rel (op \<longrightarrow>) P Q\<rbrakk> \<Longrightarrow> Q"
    91   unfolding Rel_def by simp
    92 
    93 lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
    94   by simp
    95 
    96 lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P"
    97   unfolding Rel_def by simp
    98 
    99 lemma Rel_eq_refl: "Rel (op =) x x"
   100   unfolding Rel_def ..
   101 
   102 lemma Rel_app:
   103   assumes "Rel (A ===> B) f g" and "Rel A x y"
   104   shows "Rel B (f x) (g y)"
   105   using assms unfolding Rel_def rel_fun_def by fast
   106 
   107 lemma Rel_abs:
   108   assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
   109   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   110   using assms unfolding Rel_def rel_fun_def by fast
   111 
   112 subsection {* Predicates on relations, i.e. ``class constraints'' *}
   113 
   114 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   115   where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
   116 
   117 definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   118   where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
   119 
   120 definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   121   where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
   122 
   123 definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   124   where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
   125 
   126 definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   127   where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
   128 
   129 definition bi_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   130   where "bi_unique R \<longleftrightarrow>
   131     (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
   132     (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
   133 
   134 lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
   135 unfolding left_unique_def by blast
   136 
   137 lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
   138 unfolding left_unique_def by blast
   139 
   140 lemma left_totalI:
   141   "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
   142 unfolding left_total_def by blast
   143 
   144 lemma left_totalE:
   145   assumes "left_total R"
   146   obtains "(\<And>x. \<exists>y. R x y)"
   147 using assms unfolding left_total_def by blast
   148 
   149 lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
   150 by(simp add: bi_unique_def)
   151 
   152 lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
   153 by(simp add: bi_unique_def)
   154 
   155 lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
   156 unfolding right_unique_def by fast
   157 
   158 lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
   159 unfolding right_unique_def by fast
   160 
   161 lemma right_total_alt_def2:
   162   "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
   163   unfolding right_total_def rel_fun_def
   164   apply (rule iffI, fast)
   165   apply (rule allI)
   166   apply (drule_tac x="\<lambda>x. True" in spec)
   167   apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
   168   apply fast
   169   done
   170 
   171 lemma right_unique_alt_def2:
   172   "right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
   173   unfolding right_unique_def rel_fun_def by auto
   174 
   175 lemma bi_total_alt_def2:
   176   "bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
   177   unfolding bi_total_def rel_fun_def
   178   apply (rule iffI, fast)
   179   apply safe
   180   apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
   181   apply (drule_tac x="\<lambda>y. True" in spec)
   182   apply fast
   183   apply (drule_tac x="\<lambda>x. True" in spec)
   184   apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
   185   apply fast
   186   done
   187 
   188 lemma bi_unique_alt_def2:
   189   "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
   190   unfolding bi_unique_def rel_fun_def by auto
   191 
   192 lemma [simp]:
   193   shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
   194   and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
   195 by(auto simp add: left_unique_def right_unique_def)
   196 
   197 lemma [simp]:
   198   shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
   199   and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
   200 by(simp_all add: left_total_def right_total_def)
   201 
   202 lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
   203 by(auto simp add: bi_unique_def)
   204 
   205 lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
   206 by(auto simp add: bi_total_def)
   207 
   208 lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> op=)" unfolding right_unique_def by blast
   209 lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> op=)" unfolding left_unique_def by blast
   210 
   211 lemma right_total_alt_def: "right_total R = (conversep R OO R \<ge> op=)" unfolding right_total_def by blast
   212 lemma left_total_alt_def: "left_total R = (R OO conversep R \<ge> op=)" unfolding left_total_def by blast
   213 
   214 lemma bi_total_alt_def: "bi_total A = (left_total A \<and> right_total A)"
   215 unfolding left_total_def right_total_def bi_total_def by blast
   216 
   217 lemma bi_unique_alt_def: "bi_unique A = (left_unique A \<and> right_unique A)"
   218 unfolding left_unique_def right_unique_def bi_unique_def by blast
   219 
   220 lemma bi_totalI: "left_total R \<Longrightarrow> right_total R \<Longrightarrow> bi_total R"
   221 unfolding bi_total_alt_def ..
   222 
   223 lemma bi_uniqueI: "left_unique R \<Longrightarrow> right_unique R \<Longrightarrow> bi_unique R"
   224 unfolding bi_unique_alt_def ..
   225 
   226 end
   227 
   228 subsection {* Equality restricted by a predicate *}
   229 
   230 definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
   231   where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
   232 
   233 lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id" 
   234 unfolding eq_onp_def Grp_def by auto 
   235 
   236 lemma eq_onp_to_eq:
   237   assumes "eq_onp P x y"
   238   shows "x = y"
   239 using assms by (simp add: eq_onp_def)
   240 
   241 lemma eq_onp_same_args:
   242   shows "eq_onp P x x = P x"
   243 using assms by (auto simp add: eq_onp_def)
   244 
   245 lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
   246 by (metis mem_Collect_eq subset_eq)
   247 
   248 ML_file "Tools/Transfer/transfer.ML"
   249 setup Transfer.setup
   250 declare refl [transfer_rule]
   251 
   252 hide_const (open) Rel
   253 
   254 context
   255 begin
   256 interpretation lifting_syntax .
   257 
   258 text {* Handling of domains *}
   259 
   260 lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
   261   by auto
   262 
   263 lemma Domaimp_refl[transfer_domain_rule]:
   264   "Domainp T = Domainp T" ..
   265 
   266 lemma Domainp_prod_fun_eq[relator_domain]:
   267   "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
   268 by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
   269 
   270 text {* Properties are preserved by relation composition. *}
   271 
   272 lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
   273   by auto
   274 
   275 lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
   276   unfolding bi_total_def OO_def by fast
   277 
   278 lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
   279   unfolding bi_unique_def OO_def by blast
   280 
   281 lemma right_total_OO:
   282   "\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
   283   unfolding right_total_def OO_def by fast
   284 
   285 lemma right_unique_OO:
   286   "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
   287   unfolding right_unique_def OO_def by fast
   288 
   289 lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
   290 unfolding left_total_def OO_def by fast
   291 
   292 lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
   293 unfolding left_unique_def OO_def by blast
   294 
   295 
   296 subsection {* Properties of relators *}
   297 
   298 lemma left_total_eq[transfer_rule]: "left_total op=" 
   299   unfolding left_total_def by blast
   300 
   301 lemma left_unique_eq[transfer_rule]: "left_unique op=" 
   302   unfolding left_unique_def by blast
   303 
   304 lemma right_total_eq [transfer_rule]: "right_total op="
   305   unfolding right_total_def by simp
   306 
   307 lemma right_unique_eq [transfer_rule]: "right_unique op="
   308   unfolding right_unique_def by simp
   309 
   310 lemma bi_total_eq[transfer_rule]: "bi_total (op =)"
   311   unfolding bi_total_def by simp
   312 
   313 lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)"
   314   unfolding bi_unique_def by simp
   315 
   316 lemma left_total_fun[transfer_rule]:
   317   "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
   318   unfolding left_total_def rel_fun_def
   319   apply (rule allI, rename_tac f)
   320   apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
   321   apply clarify
   322   apply (subgoal_tac "(THE x. A x y) = x", simp)
   323   apply (rule someI_ex)
   324   apply (simp)
   325   apply (rule the_equality)
   326   apply assumption
   327   apply (simp add: left_unique_def)
   328   done
   329 
   330 lemma left_unique_fun[transfer_rule]:
   331   "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
   332   unfolding left_total_def left_unique_def rel_fun_def
   333   by (clarify, rule ext, fast)
   334 
   335 lemma right_total_fun [transfer_rule]:
   336   "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
   337   unfolding right_total_def rel_fun_def
   338   apply (rule allI, rename_tac g)
   339   apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
   340   apply clarify
   341   apply (subgoal_tac "(THE y. A x y) = y", simp)
   342   apply (rule someI_ex)
   343   apply (simp)
   344   apply (rule the_equality)
   345   apply assumption
   346   apply (simp add: right_unique_def)
   347   done
   348 
   349 lemma right_unique_fun [transfer_rule]:
   350   "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
   351   unfolding right_total_def right_unique_def rel_fun_def
   352   by (clarify, rule ext, fast)
   353 
   354 lemma bi_total_fun[transfer_rule]:
   355   "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
   356   unfolding bi_unique_alt_def bi_total_alt_def
   357   by (blast intro: right_total_fun left_total_fun)
   358 
   359 lemma bi_unique_fun[transfer_rule]:
   360   "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
   361   unfolding bi_unique_alt_def bi_total_alt_def
   362   by (blast intro: right_unique_fun left_unique_fun)
   363 
   364 end
   365 
   366 ML_file "Tools/Transfer/transfer_bnf.ML" 
   367 
   368 declare pred_fun_def [simp]
   369 declare rel_fun_eq [relator_eq]
   370 
   371 subsection {* Transfer rules *}
   372 
   373 context
   374 begin
   375 interpretation lifting_syntax .
   376 
   377 lemma Domainp_forall_transfer [transfer_rule]:
   378   assumes "right_total A"
   379   shows "((A ===> op =) ===> op =)
   380     (transfer_bforall (Domainp A)) transfer_forall"
   381   using assms unfolding right_total_def
   382   unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
   383   by fast
   384 
   385 text {* Transfer rules using implication instead of equality on booleans. *}
   386 
   387 lemma transfer_forall_transfer [transfer_rule]:
   388   "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
   389   "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall"
   390   "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
   391   "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
   392   "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
   393   unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
   394   by fast+
   395 
   396 lemma transfer_implies_transfer [transfer_rule]:
   397   "(op =        ===> op =        ===> op =       ) transfer_implies transfer_implies"
   398   "(rev_implies ===> implies     ===> implies    ) transfer_implies transfer_implies"
   399   "(rev_implies ===> op =        ===> implies    ) transfer_implies transfer_implies"
   400   "(op =        ===> implies     ===> implies    ) transfer_implies transfer_implies"
   401   "(op =        ===> op =        ===> implies    ) transfer_implies transfer_implies"
   402   "(implies     ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
   403   "(implies     ===> op =        ===> rev_implies) transfer_implies transfer_implies"
   404   "(op =        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
   405   "(op =        ===> op =        ===> rev_implies) transfer_implies transfer_implies"
   406   unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
   407 
   408 lemma eq_imp_transfer [transfer_rule]:
   409   "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
   410   unfolding right_unique_alt_def2 .
   411 
   412 text {* Transfer rules using equality. *}
   413 
   414 lemma left_unique_transfer [transfer_rule]:
   415   assumes "right_total A"
   416   assumes "right_total B"
   417   assumes "bi_unique A"
   418   shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
   419 using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
   420 by metis
   421 
   422 lemma eq_transfer [transfer_rule]:
   423   assumes "bi_unique A"
   424   shows "(A ===> A ===> op =) (op =) (op =)"
   425   using assms unfolding bi_unique_def rel_fun_def by auto
   426 
   427 lemma right_total_Ex_transfer[transfer_rule]:
   428   assumes "right_total A"
   429   shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
   430 using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
   431 by fast
   432 
   433 lemma right_total_All_transfer[transfer_rule]:
   434   assumes "right_total A"
   435   shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
   436 using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
   437 by fast
   438 
   439 lemma All_transfer [transfer_rule]:
   440   assumes "bi_total A"
   441   shows "((A ===> op =) ===> op =) All All"
   442   using assms unfolding bi_total_def rel_fun_def by fast
   443 
   444 lemma Ex_transfer [transfer_rule]:
   445   assumes "bi_total A"
   446   shows "((A ===> op =) ===> op =) Ex Ex"
   447   using assms unfolding bi_total_def rel_fun_def by fast
   448 
   449 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
   450   unfolding rel_fun_def by simp
   451 
   452 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
   453   unfolding rel_fun_def by simp
   454 
   455 lemma id_transfer [transfer_rule]: "(A ===> A) id id"
   456   unfolding rel_fun_def by simp
   457 
   458 lemma comp_transfer [transfer_rule]:
   459   "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
   460   unfolding rel_fun_def by simp
   461 
   462 lemma fun_upd_transfer [transfer_rule]:
   463   assumes [transfer_rule]: "bi_unique A"
   464   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
   465   unfolding fun_upd_def [abs_def] by transfer_prover
   466 
   467 lemma case_nat_transfer [transfer_rule]:
   468   "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
   469   unfolding rel_fun_def by (simp split: nat.split)
   470 
   471 lemma rec_nat_transfer [transfer_rule]:
   472   "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
   473   unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
   474 
   475 lemma funpow_transfer [transfer_rule]:
   476   "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
   477   unfolding funpow_def by transfer_prover
   478 
   479 lemma mono_transfer[transfer_rule]:
   480   assumes [transfer_rule]: "bi_total A"
   481   assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>"
   482   assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>"
   483   shows "((A ===> B) ===> op=) mono mono"
   484 unfolding mono_def[abs_def] by transfer_prover
   485 
   486 lemma right_total_relcompp_transfer[transfer_rule]: 
   487   assumes [transfer_rule]: "right_total B"
   488   shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) 
   489     (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
   490 unfolding OO_def[abs_def] by transfer_prover
   491 
   492 lemma relcompp_transfer[transfer_rule]: 
   493   assumes [transfer_rule]: "bi_total B"
   494   shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
   495 unfolding OO_def[abs_def] by transfer_prover
   496 
   497 lemma right_total_Domainp_transfer[transfer_rule]:
   498   assumes [transfer_rule]: "right_total B"
   499   shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp"
   500 apply(subst(2) Domainp_iff[abs_def]) by transfer_prover
   501 
   502 lemma Domainp_transfer[transfer_rule]:
   503   assumes [transfer_rule]: "bi_total B"
   504   shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
   505 unfolding Domainp_iff[abs_def] by transfer_prover
   506 
   507 lemma reflp_transfer[transfer_rule]: 
   508   "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
   509   "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
   510   "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
   511   "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
   512   "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
   513 using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def 
   514 by fast+
   515 
   516 lemma right_unique_transfer [transfer_rule]:
   517   assumes [transfer_rule]: "right_total A"
   518   assumes [transfer_rule]: "right_total B"
   519   assumes [transfer_rule]: "bi_unique B"
   520   shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
   521 using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
   522 by metis
   523 
   524 lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
   525 unfolding eq_onp_def rel_fun_def by auto
   526 
   527 lemma rel_fun_eq_onp_rel:
   528   shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   529 by (auto simp add: eq_onp_def rel_fun_def)
   530 
   531 lemma eq_onp_transfer [transfer_rule]:
   532   assumes [transfer_rule]: "bi_unique A"
   533   shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
   534 unfolding eq_onp_def[abs_def] by transfer_prover
   535 
   536 end
   537 
   538 end