merged
authorwenzelm
Fri, 28 Oct 2016 20:01:38 +0200
changeset 64427 195242d16c03
parent 64425 b17acc1834e3 (diff)
parent 64426 cec5427b5c5f (current diff)
child 64428 de00179d2147
merged
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Oct 28 19:08:35 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Oct 28 20:01:38 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
--- a/src/HOL/Transfer.thy	Fri Oct 28 19:08:35 2016 +0200
+++ b/src/HOL/Transfer.thy	Fri Oct 28 20:01:38 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