# HG changeset patch
# User kuncar
# Date 1477677281 -7200
# Node ID b17acc1834e3a6414d92686ebd616aa833902352
# Parent  9ee2480d10b7404683aa7f4c3a30d44cbb6a21b9
a more general relator domain rule for the function type

diff -r 9ee2480d10b7 -r b17acc1834e3 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Oct 28 16:59:25 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Oct 28 19:54:41 2016 +0200
@@ -1354,7 +1354,7 @@
   fixes f :: "'a::topological_space \<Rightarrow> ennreal"
   shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))"
 proof (transfer fixing: A)
-  show "pred_fun (\<lambda>_. True)  (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
+  show "pred_fun top  (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f"
     for f :: "'a \<Rightarrow> ereal"
     using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq)
 qed
diff -r 9ee2480d10b7 -r b17acc1834e3 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Oct 28 16:59:25 2016 +0200
+++ b/src/HOL/Transfer.thy	Fri Oct 28 19:54:41 2016 +0200
@@ -246,11 +246,18 @@
 lemma Domainp_refl[transfer_domain_rule]:
   "Domainp T = Domainp T" ..
 
-lemma Domain_eq_top: "Domainp op= = top" by auto
+lemma Domain_eq_top[transfer_domain_rule]: "Domainp op= = top" by auto
 
-lemma Domainp_prod_fun_eq[relator_domain]:
-  "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))"
-by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)
+lemma Domainp_pred_fun_eq[relator_domain]:
+  assumes "left_unique T"
+  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"
+  using assms unfolding rel_fun_def Domainp_iff[abs_def] left_unique_def fun_eq_iff pred_fun_def
+  apply safe
+   apply blast
+  apply (subst all_comm)
+  apply (rule choice)
+  apply blast
+  done
 
 text \<open>Properties are preserved by relation composition.\<close>
 
@@ -361,6 +368,10 @@
 declare pred_fun_def [simp]
 declare rel_fun_eq [relator_eq]
 
+(* Delete the automated generated rule from the bnf command;
+  we have a more general rule (Domainp_pred_fun_eq) that subsumes it. *)
+declare fun.Domainp_rel[relator_domain del]
+
 subsection \<open>Transfer rules\<close>
 
 context includes lifting_syntax