src/HOL/Lifting.thy
changeset 47982 7aa35601ff65
parent 47937 70375fa2679d
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Lifting.thy	Thu May 24 13:56:21 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu May 24 14:20:23 2012 +0200
     1.3 @@ -121,9 +121,6 @@
     1.4  lemma identity_quotient: "Quotient (op =) id id (op =)"
     1.5  unfolding Quotient_def by simp 
     1.6  
     1.7 -lemma reflp_equality: "reflp (op =)"
     1.8 -by (auto intro: reflpI)
     1.9 -
    1.10  text {* TODO: Use one of these alternatives as the real definition. *}
    1.11  
    1.12  lemma Quotient_alt_def:
    1.13 @@ -380,6 +377,45 @@
    1.14    shows "T c c'"
    1.15    using assms by (auto dest: Quotient_cr_rel)
    1.16  
    1.17 +text {* Proving reflexivity *}
    1.18 +
    1.19 +definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.20 +  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    1.21 +
    1.22 +lemma left_totalI:
    1.23 +  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    1.24 +unfolding left_total_def by blast
    1.25 +
    1.26 +lemma left_totalE:
    1.27 +  assumes "left_total R"
    1.28 +  obtains "(\<And>x. \<exists>y. R x y)"
    1.29 +using assms unfolding left_total_def by blast
    1.30 +
    1.31 +lemma Quotient_to_left_total:
    1.32 +  assumes q: "Quotient R Abs Rep T"
    1.33 +  and r_R: "reflp R"
    1.34 +  shows "left_total T"
    1.35 +using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
    1.36 +
    1.37 +lemma reflp_Quotient_composition:
    1.38 +  assumes lt_R1: "left_total R1"
    1.39 +  and r_R2: "reflp R2"
    1.40 +  shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
    1.41 +using assms
    1.42 +proof -
    1.43 +  {
    1.44 +    fix x
    1.45 +    from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
    1.46 +    moreover then have "R1\<inverse>\<inverse> y x" by simp
    1.47 +    moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
    1.48 +    ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
    1.49 +  }
    1.50 +  then show ?thesis by (auto intro: reflpI)
    1.51 +qed
    1.52 +
    1.53 +lemma reflp_equality: "reflp (op =)"
    1.54 +by (auto intro: reflpI)
    1.55 +
    1.56  subsection {* ML setup *}
    1.57  
    1.58  use "Tools/Lifting/lifting_util.ML"
    1.59 @@ -388,7 +424,7 @@
    1.60  setup Lifting_Info.setup
    1.61  
    1.62  declare fun_quotient[quot_map]
    1.63 -declare reflp_equality[reflp_preserve]
    1.64 +lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
    1.65  
    1.66  use "Tools/Lifting/lifting_term.ML"
    1.67