# HG changeset patch # User kuncar # Date 1337188545 -7200 # Node ID 756f30eac7926b60426af2e8086a5f043cd8c07b # Parent 631ea563c20a5ac9457f576363a33364d3370e09 infrastructure that makes possible to prove that a relation is reflexive diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_List.thy --- 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) diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Option.thy --- 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: "(\x. P x) \ P None \ (\x. P (Some x))" by (metis option.exhaust) (* TODO: move to Option.thy *) -lemma option_reflp: +lemma option_reflp[reflp_preserve]: "reflp R \ reflp (option_rel R)" unfolding reflp_def split_option_all by simp diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Product.thy --- 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" diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Set.thy --- 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 \ reflp (set_rel R)" +lemma reflp_set_rel[reflp_preserve]: "reflp R \ reflp (set_rel R)" unfolding reflp_def set_rel_def by fast lemma symp_set_rel: "symp R \ symp (set_rel R)" diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_Sum.thy --- 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: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) -lemma sum_reflp: +lemma sum_reflp[reflp_preserve]: "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" unfolding reflp_def split_sum_all sum_rel.simps by fast diff -r 631ea563c20a -r 756f30eac792 src/HOL/Lifting.thy --- 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" diff -r 631ea563c20a -r 756f30eac792 src/HOL/Tools/Lifting/lifting_info.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 *) diff -r 631ea563c20a -r 756f30eac792 src/HOL/Tools/Lifting/lifting_setup.ML --- 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]),