--- a/src/HOL/Library/Quotient_Option.thy Fri Apr 20 18:29:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Fri Apr 20 22:49:40 2012 +0200
@@ -78,7 +78,7 @@
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
unfolding bi_unique_def split_option_all by simp
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma None_transfer [transfer_rule]: "(option_rel A) None None"
by simp
@@ -92,7 +92,7 @@
lemma option_map_transfer [transfer_rule]:
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
- unfolding Option.map_def by correspondence
+ unfolding Option.map_def by transfer_prover
lemma option_bind_transfer [transfer_rule]:
"(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
--- a/src/HOL/Library/Quotient_Product.thy Fri Apr 20 18:29:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Fri Apr 20 22:49:40 2012 +0200
@@ -53,7 +53,7 @@
shows "bi_unique (prod_rel R1 R2)"
using assms unfolding bi_unique_def prod_rel_def by auto
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
unfolding fun_rel_def prod_rel_def by simp
@@ -70,12 +70,12 @@
lemma curry_transfer [transfer_rule]:
"((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
- unfolding curry_def by correspondence
+ unfolding curry_def by transfer_prover
lemma map_pair_transfer [transfer_rule]:
"((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
map_pair map_pair"
- unfolding map_pair_def [abs_def] by correspondence
+ unfolding map_pair_def [abs_def] by transfer_prover
lemma prod_rel_transfer [transfer_rule]:
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
--- a/src/HOL/Library/Quotient_Sum.thy Fri Apr 20 18:29:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Apr 20 22:49:40 2012 +0200
@@ -78,7 +78,7 @@
"bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
using assms unfolding bi_unique_def split_sum_all by simp
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
unfolding fun_rel_def by simp
--- a/src/HOL/Tools/transfer.ML Fri Apr 20 18:29:21 2012 +0200
+++ b/src/HOL/Tools/transfer.ML Fri Apr 20 22:49:40 2012 +0200
@@ -12,7 +12,7 @@
val transfer_add: attribute
val transfer_del: attribute
val transfer_tac: Proof.context -> int -> tactic
- val correspondence_tac: Proof.context -> int -> tactic
+ val transfer_prover_tac: Proof.context -> int -> tactic
val setup: theory -> theory
val abs_tac: int -> tactic
end
@@ -23,7 +23,7 @@
structure Data = Named_Thms
(
val name = @{binding transfer_raw}
- val description = "raw correspondence rule for transfer method"
+ val description = "raw transfer rule for transfer method"
)
structure Relator_Eq = Named_Thms
@@ -71,7 +71,7 @@
else_conv
Conv.all_conv) ct
-(* Conversion to preprocess a correspondence rule *)
+(* Conversion to preprocess a transfer rule *)
fun prep_conv ct = (
Conv.implies_conv Conv.all_conv prep_conv
else_conv
@@ -79,11 +79,11 @@
else_conv
Conv.all_conv) ct
-(* Conversion to prep a proof goal containing a correspondence rule *)
-fun correspond_conv ctxt ct = (
- Conv.forall_conv (correspond_conv o snd) ctxt
+(* Conversion to prep a proof goal containing a transfer rule *)
+fun transfer_goal_conv ctxt ct = (
+ Conv.forall_conv (transfer_goal_conv o snd) ctxt
else_conv
- Conv.implies_conv Conv.all_conv (correspond_conv ctxt)
+ Conv.implies_conv Conv.all_conv (transfer_goal_conv ctxt)
else_conv
Trueprop_conv
(Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt))
@@ -149,13 +149,13 @@
rtac @{thm _} i]
end)
-fun correspondence_tac ctxt i =
+fun transfer_prover_tac ctxt i =
let
val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt
in
EVERY
- [CONVERSION (correspond_conv ctxt) i,
- rtac @{thm correspondence_start} i,
+ [CONVERSION (transfer_goal_conv ctxt) i,
+ rtac @{thm transfer_prover_start} i,
REPEAT_ALL_NEW
(resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1),
rewrite_goal_tac @{thms App_def Abs_def} i,
@@ -172,10 +172,10 @@
fixing >> (fn vs => fn ctxt =>
SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac ctxt))
-val correspondence_method : (Proof.context -> Method.method) context_parser =
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
+val transfer_prover_method : (Proof.context -> Method.method) context_parser =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
-(* Attribute for correspondence rules *)
+(* Attribute for transfer rules *)
val prep_rule = Conv.fconv_rule prep_conv
@@ -194,10 +194,10 @@
Data.setup
#> Relator_Eq.setup
#> Attrib.setup @{binding transfer_rule} transfer_attribute
- "correspondence rule for transfer method"
+ "transfer rule for transfer method"
#> Method.setup @{binding transfer} transfer_method
"generic theorem transfer method"
- #> Method.setup @{binding correspondence} correspondence_method
- "for proving correspondence rules"
+ #> Method.setup @{binding transfer_prover} transfer_prover_method
+ "for proving transfer rules"
end
--- a/src/HOL/Transfer.thy Fri Apr 20 18:29:21 2012 +0200
+++ b/src/HOL/Transfer.thy Fri Apr 20 22:49:40 2012 +0200
@@ -81,7 +81,7 @@
lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
unfolding Rel_def by simp
-lemma correspondence_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
+lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
by simp
lemma Rel_eq_refl: "Rel (op =) x x"
@@ -217,7 +217,7 @@
by (safe, metis, fast)
-subsection {* Correspondence rules *}
+subsection {* Transfer rules *}
lemma eq_parametric [transfer_rule]:
assumes "bi_unique A"
@@ -250,7 +250,7 @@
lemma fun_upd_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
- unfolding fun_upd_def [abs_def] by correspondence
+ unfolding fun_upd_def [abs_def] by transfer_prover
lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
by auto