infrastructure that makes possible to prove that a relation is reflexive
authorkuncar
Wed May 16 19:15:45 2012 +0200 (2012-05-16)
changeset 47936756f30eac792
parent 47935 631ea563c20a
child 47937 70375fa2679d
infrastructure that makes possible to prove that a relation is reflexive
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Wed May 16 19:15:45 2012 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4      by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
     1.5  qed
     1.6  
     1.7 -lemma list_reflp:
     1.8 +lemma list_reflp[reflp_preserve]:
     1.9    assumes "reflp R"
    1.10    shows "reflp (list_all2 R)"
    1.11  proof (rule reflpI)
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Wed May 16 18:16:51 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Wed May 16 19:15:45 2012 +0200
     2.3 @@ -46,7 +46,7 @@
     2.4  lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
     2.5    by (metis option.exhaust) (* TODO: move to Option.thy *)
     2.6  
     2.7 -lemma option_reflp:
     2.8 +lemma option_reflp[reflp_preserve]:
     2.9    "reflp R \<Longrightarrow> reflp (option_rel R)"
    2.10    unfolding reflp_def split_option_all by simp
    2.11  
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Wed May 16 18:16:51 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Wed May 16 19:15:45 2012 +0200
     3.3 @@ -27,6 +27,12 @@
     3.4    shows "prod_rel (op =) (op =) = (op =)"
     3.5    by (simp add: fun_eq_iff)
     3.6  
     3.7 +lemma prod_reflp [reflp_preserve]:
     3.8 +  assumes "reflp R1"
     3.9 +  assumes "reflp R2"
    3.10 +  shows "reflp (prod_rel R1 R2)"
    3.11 +using assms by (auto intro!: reflpI elim: reflpE)
    3.12 +
    3.13  lemma prod_equivp [quot_equiv]:
    3.14    assumes "equivp R1"
    3.15    assumes "equivp R2"
     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Wed May 16 18:16:51 2012 +0200
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Wed May 16 19:15:45 2012 +0200
     4.3 @@ -34,7 +34,7 @@
     4.4  lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)"
     4.5    unfolding set_rel_def fun_eq_iff by auto
     4.6  
     4.7 -lemma reflp_set_rel: "reflp R \<Longrightarrow> reflp (set_rel R)"
     4.8 +lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     4.9    unfolding reflp_def set_rel_def by fast
    4.10  
    4.11  lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Wed May 16 18:16:51 2012 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Wed May 16 19:15:45 2012 +0200
     5.3 @@ -46,7 +46,7 @@
     5.4  lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
     5.5    by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
     5.6  
     5.7 -lemma sum_reflp:
     5.8 +lemma sum_reflp[reflp_preserve]:
     5.9    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    5.10    unfolding reflp_def split_sum_all sum_rel.simps by fast
    5.11  
     6.1 --- a/src/HOL/Lifting.thy	Wed May 16 18:16:51 2012 +0200
     6.2 +++ b/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
     6.3 @@ -100,6 +100,9 @@
     6.4  lemma identity_quotient: "Quotient (op =) id id (op =)"
     6.5  unfolding Quotient_def by simp 
     6.6  
     6.7 +lemma reflp_equality: "reflp (op =)"
     6.8 +by (auto intro: reflpI)
     6.9 +
    6.10  text {* TODO: Use one of these alternatives as the real definition. *}
    6.11  
    6.12  lemma Quotient_alt_def:
    6.13 @@ -364,6 +367,7 @@
    6.14  setup Lifting_Info.setup
    6.15  
    6.16  declare fun_quotient[quot_map]
    6.17 +declare reflp_equality[reflp_preserve]
    6.18  
    6.19  use "Tools/Lifting/lifting_term.ML"
    6.20  
     7.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Wed May 16 18:16:51 2012 +0200
     7.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed May 16 19:15:45 2012 +0200
     7.3 @@ -20,6 +20,10 @@
     7.4    val print_quotients: Proof.context -> unit
     7.5  
     7.6    val get_invariant_commute_rules: Proof.context -> thm list
     7.7 +  
     7.8 +  val get_reflp_preserve_rules: Proof.context -> thm list
     7.9 +  val add_reflp_preserve_rule_attribute: attribute
    7.10 +  val add_reflp_preserve_rule_attrib: Attrib.src
    7.11  
    7.12    val setup: theory -> theory
    7.13  end;
    7.14 @@ -157,11 +161,22 @@
    7.15  
    7.16  fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
    7.17  
    7.18 +structure Reflp_Preserve = Named_Thms
    7.19 +(
    7.20 +  val name = @{binding reflp_preserve}
    7.21 +  val description = "theorems that a relator preserves a reflexivity property"
    7.22 +)
    7.23 +
    7.24 +val get_reflp_preserve_rules = Reflp_Preserve.get
    7.25 +val add_reflp_preserve_rule_attribute = Reflp_Preserve.add
    7.26 +val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute)
    7.27 +
    7.28  (* theory setup *)
    7.29  
    7.30  val setup =
    7.31    quotmaps_attribute_setup
    7.32    #> Invariant_Commute.setup
    7.33 +  #> Reflp_Preserve.setup
    7.34  
    7.35  (* outer syntax commands *)
    7.36  
     8.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 18:16:51 2012 +0200
     8.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 19:15:45 2012 +0200
     8.3 @@ -117,6 +117,8 @@
     8.4            [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
     8.5          |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
     8.6            [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
     8.7 +        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
     8.8 +          [reflp_thm])
     8.9        | NONE => lthy
    8.10          |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
    8.11            [quot_thm RS @{thm Quotient_All_transfer}])
    8.12 @@ -175,6 +177,8 @@
    8.13                [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
    8.14              |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
    8.15                [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
    8.16 +            |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
    8.17 +              [reflp_thm])
    8.18          end
    8.19        | _ => lthy'
    8.20          |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),