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