Re: [isabelle] Well-foundedness of Relational Composition



Tobias,

On Sun, 2015-04-26 at 09:24 +0200, Tobias Nipkow wrote:
> I'll be happy to include it in HOL/Wellfounded.thy if you do me the favour of 
> getting rid of metis - it is not available at that theory yet.

Certainly. A proof that uses only simp and blast is attached.

> Maybe somebody can also think of a more telling name suffix than "_compatible".

This was inspired by the existing lemma wf_union_compatible. Of course,
it is a terrible name.

Best,
Tjark

===== 8< =====

lemma wf_relcomp_compatible:
  assumes "wf R" and "R O S \<subseteq> S O R"
  shows "wf (S O R)"
proof (rule wfI_pf)
  fix A assume A: "A \<subseteq> (S O R) `` A"
  {
    fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
    proof (induction n)
      case 0 show ?case
        using A by (simp add: relcomp_Image)
    next
      case (Suc n)
      then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n)
`` A"
        by (simp add: Image_mono)
      also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A"
        using assms(2) by (simp add: Image_mono O_assoc
relcomp_Image[symmetric] relcomp_mono)
      finally show ?case
        by (simp add: relcomp_Image)
    qed
  }
  then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S
^^ n) `` A)"
    by blast
  then have "(\<Union>n. (S ^^ n) `` A) = {}"
    using assms(1) by (simp only: wfE_pf)
  then show "A = {}"
    using relpow.simps(1) by blast
qed






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.