src/HOL/Transfer.thy
author Andreas Lochbihler
Mon Jul 21 17:51:29 2014 +0200 (2014-07-21)
changeset 57599 7ef939f89776
parent 57398 882091eb1e9a
child 58128 43a1ba26a8cb
permissions -rw-r--r--
add parametricity lemmas
     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 although 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_Def.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_top_eq_eq: "eq_onp top = op=" 
   242 by (simp add: eq_onp_def)
   243 
   244 lemma eq_onp_same_args:
   245   shows "eq_onp P x x = P x"
   246 using assms by (auto simp add: eq_onp_def)
   247 
   248 lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
   249 by auto
   250 
   251 ML_file "Tools/Transfer/transfer.ML"
   252 setup Transfer.setup
   253 declare refl [transfer_rule]
   254 
   255 hide_const (open) Rel
   256 
   257 context
   258 begin
   259 interpretation lifting_syntax .
   260 
   261 text {* Handling of domains *}
   262 
   263 lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
   264   by auto
   265 
   266 lemma Domaimp_refl[transfer_domain_rule]:
   267   "Domainp T = Domainp T" ..
   268 
   269 lemma Domainp_prod_fun_eq[relator_domain]:
   270   "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
   271 by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
   272 
   273 text {* Properties are preserved by relation composition. *}
   274 
   275 lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
   276   by auto
   277 
   278 lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
   279   unfolding bi_total_def OO_def by fast
   280 
   281 lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
   282   unfolding bi_unique_def OO_def by blast
   283 
   284 lemma right_total_OO:
   285   "\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
   286   unfolding right_total_def OO_def by fast
   287 
   288 lemma right_unique_OO:
   289   "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
   290   unfolding right_unique_def OO_def by fast
   291 
   292 lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
   293 unfolding left_total_def OO_def by fast
   294 
   295 lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
   296 unfolding left_unique_def OO_def by blast
   297 
   298 
   299 subsection {* Properties of relators *}
   300 
   301 lemma left_total_eq[transfer_rule]: "left_total op=" 
   302   unfolding left_total_def by blast
   303 
   304 lemma left_unique_eq[transfer_rule]: "left_unique op=" 
   305   unfolding left_unique_def by blast
   306 
   307 lemma right_total_eq [transfer_rule]: "right_total op="
   308   unfolding right_total_def by simp
   309 
   310 lemma right_unique_eq [transfer_rule]: "right_unique op="
   311   unfolding right_unique_def by simp
   312 
   313 lemma bi_total_eq[transfer_rule]: "bi_total (op =)"
   314   unfolding bi_total_def by simp
   315 
   316 lemma bi_unique_eq[transfer_rule]: "bi_unique (op =)"
   317   unfolding bi_unique_def by simp
   318 
   319 lemma left_total_fun[transfer_rule]:
   320   "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
   321   unfolding left_total_def rel_fun_def
   322   apply (rule allI, rename_tac f)
   323   apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
   324   apply clarify
   325   apply (subgoal_tac "(THE x. A x y) = x", simp)
   326   apply (rule someI_ex)
   327   apply (simp)
   328   apply (rule the_equality)
   329   apply assumption
   330   apply (simp add: left_unique_def)
   331   done
   332 
   333 lemma left_unique_fun[transfer_rule]:
   334   "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
   335   unfolding left_total_def left_unique_def rel_fun_def
   336   by (clarify, rule ext, fast)
   337 
   338 lemma right_total_fun [transfer_rule]:
   339   "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
   340   unfolding right_total_def rel_fun_def
   341   apply (rule allI, rename_tac g)
   342   apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
   343   apply clarify
   344   apply (subgoal_tac "(THE y. A x y) = y", simp)
   345   apply (rule someI_ex)
   346   apply (simp)
   347   apply (rule the_equality)
   348   apply assumption
   349   apply (simp add: right_unique_def)
   350   done
   351 
   352 lemma right_unique_fun [transfer_rule]:
   353   "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
   354   unfolding right_total_def right_unique_def rel_fun_def
   355   by (clarify, rule ext, fast)
   356 
   357 lemma bi_total_fun[transfer_rule]:
   358   "\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
   359   unfolding bi_unique_alt_def bi_total_alt_def
   360   by (blast intro: right_total_fun left_total_fun)
   361 
   362 lemma bi_unique_fun[transfer_rule]:
   363   "\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
   364   unfolding bi_unique_alt_def bi_total_alt_def
   365   by (blast intro: right_unique_fun left_unique_fun)
   366 
   367 end
   368 
   369 ML_file "Tools/Transfer/transfer_bnf.ML" 
   370 
   371 declare pred_fun_def [simp]
   372 declare rel_fun_eq [relator_eq]
   373 
   374 subsection {* Transfer rules *}
   375 
   376 context
   377 begin
   378 interpretation lifting_syntax .
   379 
   380 lemma Domainp_forall_transfer [transfer_rule]:
   381   assumes "right_total A"
   382   shows "((A ===> op =) ===> op =)
   383     (transfer_bforall (Domainp A)) transfer_forall"
   384   using assms unfolding right_total_def
   385   unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
   386   by fast
   387 
   388 text {* Transfer rules using implication instead of equality on booleans. *}
   389 
   390 lemma transfer_forall_transfer [transfer_rule]:
   391   "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
   392   "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall"
   393   "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
   394   "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
   395   "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
   396   unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
   397   by fast+
   398 
   399 lemma transfer_implies_transfer [transfer_rule]:
   400   "(op =        ===> op =        ===> op =       ) transfer_implies transfer_implies"
   401   "(rev_implies ===> implies     ===> implies    ) transfer_implies transfer_implies"
   402   "(rev_implies ===> op =        ===> implies    ) transfer_implies transfer_implies"
   403   "(op =        ===> implies     ===> implies    ) transfer_implies transfer_implies"
   404   "(op =        ===> op =        ===> implies    ) transfer_implies transfer_implies"
   405   "(implies     ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
   406   "(implies     ===> op =        ===> rev_implies) transfer_implies transfer_implies"
   407   "(op =        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
   408   "(op =        ===> op =        ===> rev_implies) transfer_implies transfer_implies"
   409   unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
   410 
   411 lemma eq_imp_transfer [transfer_rule]:
   412   "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
   413   unfolding right_unique_alt_def2 .
   414 
   415 text {* Transfer rules using equality. *}
   416 
   417 lemma left_unique_transfer [transfer_rule]:
   418   assumes "right_total A"
   419   assumes "right_total B"
   420   assumes "bi_unique A"
   421   shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
   422 using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
   423 by metis
   424 
   425 lemma eq_transfer [transfer_rule]:
   426   assumes "bi_unique A"
   427   shows "(A ===> A ===> op =) (op =) (op =)"
   428   using assms unfolding bi_unique_def rel_fun_def by auto
   429 
   430 lemma right_total_Ex_transfer[transfer_rule]:
   431   assumes "right_total A"
   432   shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
   433 using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
   434 by fast
   435 
   436 lemma right_total_All_transfer[transfer_rule]:
   437   assumes "right_total A"
   438   shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
   439 using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
   440 by fast
   441 
   442 lemma All_transfer [transfer_rule]:
   443   assumes "bi_total A"
   444   shows "((A ===> op =) ===> op =) All All"
   445   using assms unfolding bi_total_def rel_fun_def by fast
   446 
   447 lemma Ex_transfer [transfer_rule]:
   448   assumes "bi_total A"
   449   shows "((A ===> op =) ===> op =) Ex Ex"
   450   using assms unfolding bi_total_def rel_fun_def by fast
   451 
   452 lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
   453   unfolding rel_fun_def by simp
   454 
   455 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
   456   unfolding rel_fun_def by simp
   457 
   458 lemma id_transfer [transfer_rule]: "(A ===> A) id id"
   459   unfolding rel_fun_def by simp
   460 
   461 lemma comp_transfer [transfer_rule]:
   462   "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
   463   unfolding rel_fun_def by simp
   464 
   465 lemma fun_upd_transfer [transfer_rule]:
   466   assumes [transfer_rule]: "bi_unique A"
   467   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
   468   unfolding fun_upd_def [abs_def] by transfer_prover
   469 
   470 lemma case_nat_transfer [transfer_rule]:
   471   "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
   472   unfolding rel_fun_def by (simp split: nat.split)
   473 
   474 lemma rec_nat_transfer [transfer_rule]:
   475   "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
   476   unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
   477 
   478 lemma funpow_transfer [transfer_rule]:
   479   "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
   480   unfolding funpow_def by transfer_prover
   481 
   482 lemma mono_transfer[transfer_rule]:
   483   assumes [transfer_rule]: "bi_total A"
   484   assumes [transfer_rule]: "(A ===> A ===> op=) op\<le> op\<le>"
   485   assumes [transfer_rule]: "(B ===> B ===> op=) op\<le> op\<le>"
   486   shows "((A ===> B) ===> op=) mono mono"
   487 unfolding mono_def[abs_def] by transfer_prover
   488 
   489 lemma right_total_relcompp_transfer[transfer_rule]: 
   490   assumes [transfer_rule]: "right_total B"
   491   shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) 
   492     (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
   493 unfolding OO_def[abs_def] by transfer_prover
   494 
   495 lemma relcompp_transfer[transfer_rule]: 
   496   assumes [transfer_rule]: "bi_total B"
   497   shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
   498 unfolding OO_def[abs_def] by transfer_prover
   499 
   500 lemma right_total_Domainp_transfer[transfer_rule]:
   501   assumes [transfer_rule]: "right_total B"
   502   shows "((A ===> B ===> op=) ===> A ===> op=) (\<lambda>T x. \<exists>y\<in>Collect(Domainp B). T x y) Domainp"
   503 apply(subst(2) Domainp_iff[abs_def]) by transfer_prover
   504 
   505 lemma Domainp_transfer[transfer_rule]:
   506   assumes [transfer_rule]: "bi_total B"
   507   shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
   508 unfolding Domainp_iff[abs_def] by transfer_prover
   509 
   510 lemma reflp_transfer[transfer_rule]: 
   511   "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
   512   "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
   513   "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
   514   "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
   515   "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
   516 using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def 
   517 by fast+
   518 
   519 lemma right_unique_transfer [transfer_rule]:
   520   assumes [transfer_rule]: "right_total A"
   521   assumes [transfer_rule]: "right_total B"
   522   assumes [transfer_rule]: "bi_unique B"
   523   shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
   524 using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
   525 by metis
   526 
   527 lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
   528 unfolding eq_onp_def rel_fun_def by auto
   529 
   530 lemma rel_fun_eq_onp_rel:
   531   shows "((eq_onp R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   532 by (auto simp add: eq_onp_def rel_fun_def)
   533 
   534 lemma eq_onp_transfer [transfer_rule]:
   535   assumes [transfer_rule]: "bi_unique A"
   536   shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
   537 unfolding eq_onp_def[abs_def] by transfer_prover
   538 
   539 lemma rtranclp_parametric [transfer_rule]:
   540   assumes "bi_unique A" "bi_total A"
   541   shows "((A ===> A ===> op =) ===> A ===> A ===> op =) rtranclp rtranclp"
   542 proof(rule rel_funI iffI)+
   543   fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and R' x y x' y'
   544   assume R: "(A ===> A ===> op =) R R'" and "A x x'"
   545   {
   546     assume "R\<^sup>*\<^sup>* x y" "A y y'"
   547     thus "R'\<^sup>*\<^sup>* x' y'"
   548     proof(induction arbitrary: y')
   549       case base
   550       with `bi_unique A` `A x x'` have "x' = y'" by(rule bi_uniqueDr)
   551       thus ?case by simp
   552     next
   553       case (step y z z')
   554       from `bi_total A` obtain y' where "A y y'" unfolding bi_total_def by blast
   555       hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH)
   556       moreover from R `A y y'` `A z z'` `R y z`
   557       have "R' y' z'" by(auto dest: rel_funD)
   558       ultimately show ?case ..
   559     qed
   560   next
   561     assume "R'\<^sup>*\<^sup>* x' y'" "A y y'"
   562     thus "R\<^sup>*\<^sup>* x y"
   563     proof(induction arbitrary: y)
   564       case base
   565       with `bi_unique A` `A x x'` have "x = y" by(rule bi_uniqueDl)
   566       thus ?case by simp
   567     next
   568       case (step y' z' z)
   569       from `bi_total A` obtain y where "A y y'" unfolding bi_total_def by blast
   570       hence "R\<^sup>*\<^sup>* x y" by(rule step.IH)
   571       moreover from R `A y y'` `A z z'` `R' y' z'`
   572       have "R y z" by(auto dest: rel_funD)
   573       ultimately show ?case ..
   574     qed
   575   }
   576 qed
   577 
   578 end
   579 
   580 end