--- a/src/HOL/Transfer.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Transfer.thy Fri Nov 07 11:28:37 2014 +0100
@@ -6,13 +6,9 @@
section {* Generic theorem transfer using relations *}
theory Transfer
-imports Hilbert_Choice Metis Option
+imports Hilbert_Choice Metis Basic_BNF_Least_Fixpoints
begin
-(* We import Option here although it's not needed here.
- By doing this, we avoid a diamond problem for BNF and
- FP sugar interpretation defined in this file. *)
-
subsection {* Relator for function space *}
locale lifting_syntax
@@ -453,11 +449,14 @@
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
unfolding rel_fun_def by simp
-lemma id_transfer [transfer_rule]: "(A ===> A) id id"
- unfolding rel_fun_def by simp
+declare id_transfer [transfer_rule]
declare comp_transfer [transfer_rule]
+lemma curry_transfer [transfer_rule]:
+ "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
+ unfolding curry_def by transfer_prover
+
lemma fun_upd_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"