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