author wenzelm 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```