# HG changeset patch
# User Andreas Lochbihler
# Date 1423659076 -3600
# Node ID 509caf5edfa6795378da9b855a2847d5843a91eb
# Parent  6949c8837e90426ec451cfd7d9d12390d6052d6d
add intro and elim rules for right_total

diff -r 6949c8837e90 -r 509caf5edfa6 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Feb 11 13:50:11 2015 +0100
+++ b/src/HOL/Transfer.thy	Wed Feb 11 13:51:16 2015 +0100
@@ -154,6 +154,14 @@
 lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
 unfolding right_unique_def by fast
 
+lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
+by(simp add: right_total_def)
+
+lemma right_totalE:
+  assumes "right_total A"
+  obtains x where "A x y"
+using assms by(auto simp add: right_total_def)
+
 lemma right_total_alt_def2:
   "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
   unfolding right_total_def rel_fun_def