--- a/src/HOL/Library/Quotient_List.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy Wed May 16 19:15:45 2012 +0200
@@ -37,7 +37,7 @@
by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
qed
-lemma list_reflp:
+lemma list_reflp[reflp_preserve]:
assumes "reflp R"
shows "reflp (list_all2 R)"
proof (rule reflpI)
--- a/src/HOL/Library/Quotient_Option.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Wed May 16 19:15:45 2012 +0200
@@ -46,7 +46,7 @@
lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
by (metis option.exhaust) (* TODO: move to Option.thy *)
-lemma option_reflp:
+lemma option_reflp[reflp_preserve]:
"reflp R \<Longrightarrow> reflp (option_rel R)"
unfolding reflp_def split_option_all by simp
--- a/src/HOL/Library/Quotient_Product.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Wed May 16 19:15:45 2012 +0200
@@ -27,6 +27,12 @@
shows "prod_rel (op =) (op =) = (op =)"
by (simp add: fun_eq_iff)
+lemma prod_reflp [reflp_preserve]:
+ assumes "reflp R1"
+ assumes "reflp R2"
+ shows "reflp (prod_rel R1 R2)"
+using assms by (auto intro!: reflpI elim: reflpE)
+
lemma prod_equivp [quot_equiv]:
assumes "equivp R1"
assumes "equivp R2"
--- a/src/HOL/Library/Quotient_Set.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Wed May 16 19:15:45 2012 +0200
@@ -34,7 +34,7 @@
lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
unfolding set_rel_def fun_eq_iff by auto
-lemma reflp_set_rel: "reflp R \<Longrightarrow> reflp (set_rel R)"
+lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
unfolding reflp_def set_rel_def by fast
lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
--- a/src/HOL/Library/Quotient_Sum.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Wed May 16 19:15:45 2012 +0200
@@ -46,7 +46,7 @@
lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
-lemma sum_reflp:
+lemma sum_reflp[reflp_preserve]:
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
unfolding reflp_def split_sum_all sum_rel.simps by fast
--- a/src/HOL/Lifting.thy Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Lifting.thy Wed May 16 19:15:45 2012 +0200
@@ -100,6 +100,9 @@
lemma identity_quotient: "Quotient (op =) id id (op =)"
unfolding Quotient_def by simp
+lemma reflp_equality: "reflp (op =)"
+by (auto intro: reflpI)
+
text {* TODO: Use one of these alternatives as the real definition. *}
lemma Quotient_alt_def:
@@ -364,6 +367,7 @@
setup Lifting_Info.setup
declare fun_quotient[quot_map]
+declare reflp_equality[reflp_preserve]
use "Tools/Lifting/lifting_term.ML"
--- a/src/HOL/Tools/Lifting/lifting_info.ML Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed May 16 19:15:45 2012 +0200
@@ -20,6 +20,10 @@
val print_quotients: Proof.context -> unit
val get_invariant_commute_rules: Proof.context -> thm list
+
+ val get_reflp_preserve_rules: Proof.context -> thm list
+ val add_reflp_preserve_rule_attribute: attribute
+ val add_reflp_preserve_rule_attrib: Attrib.src
val setup: theory -> theory
end;
@@ -157,11 +161,22 @@
fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
+structure Reflp_Preserve = Named_Thms
+(
+ val name = @{binding reflp_preserve}
+ val description = "theorems that a relator preserves a reflexivity property"
+)
+
+val get_reflp_preserve_rules = Reflp_Preserve.get
+val add_reflp_preserve_rule_attribute = Reflp_Preserve.add
+val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute)
+
(* theory setup *)
val setup =
quotmaps_attribute_setup
#> Invariant_Commute.setup
+ #> Reflp_Preserve.setup
(* outer syntax commands *)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed May 16 19:15:45 2012 +0200
@@ -117,6 +117,8 @@
[[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
|> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
+ |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+ [reflp_thm])
| NONE => lthy
|> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
[quot_thm RS @{thm Quotient_All_transfer}])
@@ -175,6 +177,8 @@
[[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
|> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
+ |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+ [reflp_thm])
end
| _ => lthy'
|> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),