reflexivity rules for the function type and equality
authorkuncar
Thu May 16 15:21:12 2013 +0200 (2013-05-16)
changeset 520361aa2e40df9ff
parent 52035 dfa06e82a720
child 52037 837211662fb8
reflexivity rules for the function type and equality
src/HOL/Lifting.thy
     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 *}