Re: [isabelle] Well-foundedness of Relational Composition



Just for the record: Sorry, I introduced a typo in my (sorry) lemma. (Actually hinted at by quickcheck, since my formulation is not correct.)

The problem was (once again) to adapt the orientation from the rewriting literature (where "smaller" is on the right) to the orientation of "wf" (where "smaller" is on the left).

It should actually be:

lemma qc_wf_relto_iff:
  assumes "R O S â (R â S)â* O R"
  shows "wf (Sâ* O R O Sâ*) â wf R"
...

This still implies Tjark's lemma and I hope it is provable ;) (I'll give it a try).

cheers

chris

On 04/27/2015 03:05 PM, Tobias Nipkow wrote:
I have just added it. You are welcome to send me an improved version later.

Tobias

On 26/04/2015 15:51, Tjark Weber wrote:
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.