lifting package produces abs_eq_iff rules for total quotients
authorhuffman
Fri May 04 17:12:37 2012 +0200 (2012-05-04)
changeset 4788929212a4bb866
parent 47888 45bf22d8a81d
child 47890 0cedab5d2eb7
lifting package produces abs_eq_iff rules for total quotients
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Lifting.thy	Fri May 04 11:08:31 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Fri May 04 17:12:37 2012 +0200
     1.3 @@ -310,6 +310,9 @@
     1.4  lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
     1.5    using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
     1.6  
     1.7 +lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
     1.8 +  using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
     1.9 +
    1.10  end
    1.11  
    1.12  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri May 04 11:08:31 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri May 04 17:12:37 2012 +0200
     2.3 @@ -115,6 +115,8 @@
     2.4            [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
     2.5          |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
     2.6            [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
     2.7 +        |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
     2.8 +          [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
     2.9        | NONE => lthy
    2.10          |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
    2.11            [quot_thm RS @{thm Quotient_All_transfer}])