prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
authorkuncar
Thu May 24 14:20:23 2012 +0200 (2012-05-24)
changeset 479827aa35601ff65
parent 47977 455a9f89c47d
child 47983 a5e699834f2d
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
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_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Thu May 24 13:56:21 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Thu May 24 14:20:23 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[reflp_preserve]:
     1.8 +lemma list_reflp[reflexivity_rule]:
     1.9    assumes "reflp R"
    1.10    shows "reflp (list_all2 R)"
    1.11  proof (rule reflpI)
    1.12 @@ -47,6 +47,17 @@
    1.13      by (induct xs) (simp_all add: *)
    1.14  qed
    1.15  
    1.16 +lemma list_left_total[reflexivity_rule]:
    1.17 +  assumes "left_total R"
    1.18 +  shows "left_total (list_all2 R)"
    1.19 +proof (rule left_totalI)
    1.20 +  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
    1.21 +  fix xs
    1.22 +  show "\<exists> ys. list_all2 R xs ys"
    1.23 +    by (induct xs) (simp_all add: * list_all2_Cons1)
    1.24 +qed
    1.25 +
    1.26 +
    1.27  lemma list_symp:
    1.28    assumes "symp R"
    1.29    shows "symp (list_all2 R)"
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Thu May 24 13:56:21 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Thu May 24 14:20:23 2012 +0200
     2.3 @@ -46,10 +46,16 @@
     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[reflp_preserve]:
     2.8 +lemma option_reflp[reflexivity_rule]:
     2.9    "reflp R \<Longrightarrow> reflp (option_rel R)"
    2.10    unfolding reflp_def split_option_all by simp
    2.11  
    2.12 +lemma option_left_total[reflexivity_rule]:
    2.13 +  "left_total R \<Longrightarrow> left_total (option_rel R)"
    2.14 +  apply (intro left_totalI)
    2.15 +  unfolding split_option_ex
    2.16 +  by (case_tac x) (auto elim: left_totalE)
    2.17 +
    2.18  lemma option_symp:
    2.19    "symp R \<Longrightarrow> symp (option_rel R)"
    2.20    unfolding symp_def split_option_all option_rel.simps by fast
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu May 24 13:56:21 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu May 24 14:20:23 2012 +0200
     3.3 @@ -27,12 +27,18 @@
     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 +lemma prod_reflp [reflexivity_rule]:
     3.9    assumes "reflp R1"
    3.10    assumes "reflp R2"
    3.11    shows "reflp (prod_rel R1 R2)"
    3.12  using assms by (auto intro!: reflpI elim: reflpE)
    3.13  
    3.14 +lemma prod_left_total [reflexivity_rule]:
    3.15 +  assumes "left_total R1"
    3.16 +  assumes "left_total R2"
    3.17 +  shows "left_total (prod_rel R1 R2)"
    3.18 +using assms by (auto intro!: left_totalI elim!: left_totalE)
    3.19 +
    3.20  lemma prod_equivp [quot_equiv]:
    3.21    assumes "equivp R1"
    3.22    assumes "equivp R2"
     4.1 --- a/src/HOL/Library/Quotient_Set.thy	Thu May 24 13:56:21 2012 +0200
     4.2 +++ b/src/HOL/Library/Quotient_Set.thy	Thu May 24 14:20:23 2012 +0200
     4.3 @@ -34,9 +34,22 @@
     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_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     4.8 +lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     4.9    unfolding reflp_def set_rel_def by fast
    4.10  
    4.11 +lemma left_total_set_rel[reflexivity_rule]:
    4.12 +  assumes lt_R: "left_total R"
    4.13 +  shows "left_total (set_rel R)"
    4.14 +proof -
    4.15 +  {
    4.16 +    fix A
    4.17 +    let ?B = "{y. \<exists>x \<in> A. R x y}"
    4.18 +    have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast
    4.19 +  }
    4.20 +  then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast
    4.21 +  then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
    4.22 +qed
    4.23 +
    4.24  lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
    4.25    unfolding symp_def set_rel_def by fast
    4.26  
     5.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu May 24 13:56:21 2012 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu May 24 14:20:23 2012 +0200
     5.3 @@ -46,10 +46,16 @@
     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[reflp_preserve]:
     5.8 +lemma sum_reflp[reflexivity_rule]:
     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  
    5.12 +lemma sum_left_total[reflexivity_rule]:
    5.13 +  "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    5.14 +  apply (intro left_totalI)
    5.15 +  unfolding split_sum_ex 
    5.16 +  by (case_tac x) (auto elim: left_totalE)
    5.17 +
    5.18  lemma sum_symp:
    5.19    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    5.20    unfolding symp_def split_sum_all sum_rel.simps by fast
     6.1 --- a/src/HOL/Lifting.thy	Thu May 24 13:56:21 2012 +0200
     6.2 +++ b/src/HOL/Lifting.thy	Thu May 24 14:20:23 2012 +0200
     6.3 @@ -121,9 +121,6 @@
     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 @@ -380,6 +377,45 @@
    6.14    shows "T c c'"
    6.15    using assms by (auto dest: Quotient_cr_rel)
    6.16  
    6.17 +text {* Proving reflexivity *}
    6.18 +
    6.19 +definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    6.20 +  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    6.21 +
    6.22 +lemma left_totalI:
    6.23 +  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    6.24 +unfolding left_total_def by blast
    6.25 +
    6.26 +lemma left_totalE:
    6.27 +  assumes "left_total R"
    6.28 +  obtains "(\<And>x. \<exists>y. R x y)"
    6.29 +using assms unfolding left_total_def by blast
    6.30 +
    6.31 +lemma Quotient_to_left_total:
    6.32 +  assumes q: "Quotient R Abs Rep T"
    6.33 +  and r_R: "reflp R"
    6.34 +  shows "left_total T"
    6.35 +using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
    6.36 +
    6.37 +lemma reflp_Quotient_composition:
    6.38 +  assumes lt_R1: "left_total R1"
    6.39 +  and r_R2: "reflp R2"
    6.40 +  shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
    6.41 +using assms
    6.42 +proof -
    6.43 +  {
    6.44 +    fix x
    6.45 +    from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
    6.46 +    moreover then have "R1\<inverse>\<inverse> y x" by simp
    6.47 +    moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
    6.48 +    ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
    6.49 +  }
    6.50 +  then show ?thesis by (auto intro: reflpI)
    6.51 +qed
    6.52 +
    6.53 +lemma reflp_equality: "reflp (op =)"
    6.54 +by (auto intro: reflpI)
    6.55 +
    6.56  subsection {* ML setup *}
    6.57  
    6.58  use "Tools/Lifting/lifting_util.ML"
    6.59 @@ -388,7 +424,7 @@
    6.60  setup Lifting_Info.setup
    6.61  
    6.62  declare fun_quotient[quot_map]
    6.63 -declare reflp_equality[reflp_preserve]
    6.64 +lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
    6.65  
    6.66  use "Tools/Lifting/lifting_term.ML"
    6.67  
     7.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu May 24 13:56:21 2012 +0200
     7.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu May 24 14:20:23 2012 +0200
     7.3 @@ -182,7 +182,7 @@
     7.4          
     7.5          val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
     7.6          val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
     7.7 -        val rules = Lifting_Info.get_reflp_preserve_rules ctxt
     7.8 +        val rules = Lifting_Info.get_reflexivity_rules ctxt
     7.9        in
    7.10          EVERY' [CSUBGOAL intro_reflp_tac, 
    7.11                  CONVERSION conv,
     8.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 13:56:21 2012 +0200
     8.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 14:20:23 2012 +0200
     8.3 @@ -21,9 +21,9 @@
     8.4  
     8.5    val get_invariant_commute_rules: Proof.context -> thm list
     8.6    
     8.7 -  val get_reflp_preserve_rules: Proof.context -> thm list
     8.8 -  val add_reflp_preserve_rule_attribute: attribute
     8.9 -  val add_reflp_preserve_rule_attrib: Attrib.src
    8.10 +  val get_reflexivity_rules: Proof.context -> thm list
    8.11 +  val add_reflexivity_rule_attribute: attribute
    8.12 +  val add_reflexivity_rule_attrib: Attrib.src
    8.13  
    8.14    val setup: theory -> theory
    8.15  end;
    8.16 @@ -183,13 +183,13 @@
    8.17  
    8.18  structure Reflp_Preserve = Named_Thms
    8.19  (
    8.20 -  val name = @{binding reflp_preserve}
    8.21 +  val name = @{binding reflexivity_rule}
    8.22    val description = "theorems that a relator preserves a reflexivity property"
    8.23  )
    8.24  
    8.25 -val get_reflp_preserve_rules = Reflp_Preserve.get
    8.26 -val add_reflp_preserve_rule_attribute = Reflp_Preserve.add
    8.27 -val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute)
    8.28 +val get_reflexivity_rules = Reflp_Preserve.get
    8.29 +val add_reflexivity_rule_attribute = Reflp_Preserve.add
    8.30 +val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
    8.31  
    8.32  (* theory setup *)
    8.33  
     9.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu May 24 13:56:21 2012 +0200
     9.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu May 24 14:20:23 2012 +0200
     9.3 @@ -103,8 +103,10 @@
     9.4      fun quot_info phi = Lifting_Info.transform_quotients phi quotients
     9.5      val lthy' = case maybe_reflp_thm of
     9.6        SOME reflp_thm => lthy
     9.7 -        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
     9.8 +        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
     9.9                [reflp_thm])
    9.10 +        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
    9.11 +              [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
    9.12          |> define_code_constr gen_code quot_thm
    9.13        | NONE => lthy
    9.14          |> define_abs_type gen_code quot_thm