# HG changeset patch
# User kuncar
# Date 1368710472 -7200
# Node ID 1aa2e40df9ff36052c0a686df37e7a71c37e5443
# Parent  dfa06e82a720c858945cfe8b340dfcf26cb7a5d4
reflexivity rules for the function type and equality

diff -r dfa06e82a720 -r 1aa2e40df9ff src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu May 16 15:03:28 2013 +0200
+++ b/src/HOL/Lifting.thy	Thu May 16 15:21:12 2013 +0200
@@ -39,6 +39,29 @@
 definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
 
+lemma left_total_fun:
+  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
+  unfolding left_total_def fun_rel_def
+  apply (rule allI, rename_tac f)
+  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
+  apply clarify
+  apply (subgoal_tac "(THE x. A x y) = x", simp)
+  apply (rule someI_ex)
+  apply (simp)
+  apply (rule the_equality)
+  apply assumption
+  apply (simp add: left_unique_def)
+  done
+
+lemma left_unique_fun:
+  "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
+  unfolding left_total_def left_unique_def fun_rel_def
+  by (clarify, rule ext, fast)
+
+lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
+
+lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
+
 subsection {* Quotient Predicate *}
 
 definition
@@ -578,7 +601,8 @@
 setup Lifting_Info.setup
 
 lemmas [reflexivity_rule] = 
-  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
+  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition 
+  left_total_fun left_unique_fun left_total_eq left_unique_eq
 
 text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
   because we don't want to get reflp' variant of these theorems *}