# HG changeset patch
# User huffman
# Date 1334929785 -7200
# Node ID 2b1d3eda59eb190fd4014ba01739ef92612d6cd0
# Parent  f7b1034cb9cea1df469d768dc541a861f317dcdd
add secondary transfer rule for universal quantifiers on non-bi-total relations

diff -r f7b1034cb9ce -r 2b1d3eda59eb src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Apr 20 15:34:33 2012 +0200
+++ b/src/HOL/Transfer.thy	Fri Apr 20 15:49:45 2012 +0200
@@ -252,7 +252,26 @@
   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
   unfolding fun_upd_def [abs_def] by correspondence
 
-lemmas transfer_forall_parametric [transfer_rule]
-  = All_parametric [folded transfer_forall_def]
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+  by auto
+
+text {* Fallback rule for transferring universal quantifiers over
+  correspondence relations that are not bi-total, and do not have
+  custom transfer rules (e.g. relations between function types). *}
+
+lemma Domainp_forall_transfer [transfer_rule]:
+  assumes "right_total A"
+  shows "((A ===> op =) ===> op =)
+    (transfer_bforall (Domainp A)) transfer_forall"
+  using assms unfolding right_total_def
+  unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
+  by metis
+
+text {* Preferred rule for transferring universal quantifiers over
+  bi-total correspondence relations (later rules are tried first). *}
+
+lemma transfer_forall_parametric [transfer_rule]:
+  "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
+  unfolding transfer_forall_def by (rule All_parametric)
 
 end