src/HOL/Lifting.thy
 changeset 52036 1aa2e40df9ff parent 51994 82cc2aeb7d13 child 52307 32c433c38ddd
```     1.1 --- a/src/HOL/Lifting.thy	Thu May 16 15:03:28 2013 +0200
1.2 +++ b/src/HOL/Lifting.thy	Thu May 16 15:21:12 2013 +0200
1.3 @@ -39,6 +39,29 @@
1.4  definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
1.5    where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
1.6
1.7 +lemma left_total_fun:
1.8 +  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
1.9 +  unfolding left_total_def fun_rel_def
1.10 +  apply (rule allI, rename_tac f)
1.11 +  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
1.12 +  apply clarify
1.13 +  apply (subgoal_tac "(THE x. A x y) = x", simp)
1.14 +  apply (rule someI_ex)
1.15 +  apply (simp)
1.16 +  apply (rule the_equality)
1.17 +  apply assumption
1.18 +  apply (simp add: left_unique_def)
1.19 +  done
1.20 +
1.21 +lemma left_unique_fun:
1.22 +  "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
1.23 +  unfolding left_total_def left_unique_def fun_rel_def
1.24 +  by (clarify, rule ext, fast)
1.25 +
1.26 +lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
1.27 +
1.28 +lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
1.29 +
1.30  subsection {* Quotient Predicate *}
1.31
1.32  definition
1.33 @@ -578,7 +601,8 @@
1.34  setup Lifting_Info.setup
1.35
1.36  lemmas [reflexivity_rule] =
1.37 -  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
1.38 +  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
1.39 +  left_total_fun left_unique_fun left_total_eq left_unique_eq
1.40
1.41  text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
1.42    because we don't want to get reflp' variant of these theorems *}
```