[isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]



The mailing list seems not to accept html mails ... I'll try again and
hope that the mail is still readable, else sorry for the spam:


Hi all,

is there something special to the function composition (op \<circ>)
operator built in Isabelle?

I have some problems understanding the behaviour of the simplifier in
conjunction with the lemma o_apply.
A (simp (no_asm_use) only: o_apply) - command gives different results
depending on the proof context I use it in. For example,
it may but need not happen that a "(f\<circ>g)" is rewritten to
"\<lambda>u. f (g u)" by (simp (no_asm_use) only: o_apply) in the same
subgoal, depending on where it occurs in a proof.
It also happens that only some occurences of "(f\<circ>g)" are rewritten
and others not.

So is there something going on behind the scenes that I do not see ?.
Also the simplifier traces are not very useful there (see below).

Here is a (rather complex, sorry for that) example:

Doing the following:

lemma " \<And>e w' w1' w2 x. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2; x \<in> fst (\<alpha> (f e)); x \<in> mon_pl (map (\<alpha> \<circ> f) w2)\<rbrakk> \<Longrightarrow> False"

  apply (simp (no_asm_use) only: o_apply)


I get (as expected).

    (* 1. \<And>e w' w1' w2 x. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst (\<alpha> (f e)) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2; x \<in> fst (\<alpha> (f e)); x \<in> mon_pl (map (\<alpha> \<circ> f) w2)\<rbrakk> \<Longrightarrow> False *)


That is, only the "fst ((\<alpha> \<circ> f) e) " was rewritten to "fst
(\<alpha> (f e))"

Now the same subgoal occurs in some (larger) proof:

lemma cil_inner_map: "w\<in>w1 \<otimes>\<^bsub>(\<alpha>\<circ>f)\<^esub> w2 \<Longrightarrow> map f w \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2" 

  apply (induct rule: cil_set_induct_fix\<alpha>)

  apply (simp)

  apply (simp_all del: o_apply)

  apply (rule cil_cons1)

  apply (auto simp add: map_compose[symmetric] simp del: o_apply)

    At this point, I have the same subgoal as above:

    (* 1. \<And>e w' w1' w2 x. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2; x \<in> fst (\<alpha> (f e)); x \<in> mon_pl (map (\<alpha> \<circ> f) w2)\<rbrakk> \<Longrightarrow> False *)

Then I do:

  apply (simp (no_asm_use) only: o_apply)


    But I get:

    (* 1. \<And>e w' w1' w2 x. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<lambda>u. \<alpha> (f u))\<^esub> w2; fst (\<alpha> (f e)) \<inter> mon_pl (map (\<lambda>u. \<alpha> (f u)) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2; x \<in> fst (\<alpha> (f e)); x \<in> mon_pl (map (\<alpha> \<circ> f) w2)\<rbrakk> \<Longrightarrow> False *)


note that now also "\<alpha> \<circ> f" was rewritten to "\<lambda>u.
\<alpha> (f u)" two times (both marked red) and one time it was not
rewritten (marked green).
(The a\<otimes>\<^bsub>b\<^esub>c is some syntax for cil(b,a,c), where
cil is a function defined with recdef).

I have no idea what's going on here, I thought a (simp (no_asm_use)
only: X) would only apply the rewriting rule X and nothing else.

The simplifier trace of the first run is as expected:

[0]Adding rewrite rule "Fun.o_apply":

(?f1 \<circ> ?g1) ?x1 \<equiv> ?f1 (?g1 ?x1)

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:

\<And>e w' w1' w2 x. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2; x \<in> fst (\<alpha> (f e)); x \<in> mon_pl (map (\<alpha> \<circ> f) w2)\<rbrakk> \<Longrightarrow> False

[1]Applying instance of rewrite rule "Fun.o_apply":

(?f1 \<circ> ?g1) ?x1 \<equiv> ?f1 (?g1 ?x1)

[1]Rewriting:

(\<alpha> \<circ> f) e \<equiv> \<alpha> (f e)


-------------------
The trace of the second run is somewhat strange. The simplifier rule is
applied 3 times, but I cannot see where it gets the term "(\<alpha>
\<circ> f) u" from, this term simply does not occur in the original
formula !

[0]Adding rewrite rule "Fun.o_apply":

(?f1 \<circ> ?g1) ?x1 \<equiv> ?f1 (?g1 ?x1)

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:

\<And>e w' w1' w2 x. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2; x \<in> fst (\<alpha> (f e)); x \<in> mon_pl (map (\<alpha> \<circ> f) w2)\<rbrakk> \<Longrightarrow> False

[1]Applying instance of rewrite rule "Fun.o_apply":

(?f1 \<circ> ?g1) ?x1 \<equiv> ?f1 (?g1 ?x1)

*[1]Rewriting:*

*(\<alpha> \<circ> f) u \<equiv> \<alpha> (f u)*

[1]Applying instance of rewrite rule "Fun.o_apply":

(?f1 \<circ> ?g1) ?x1 \<equiv> ?f1 (?g1 ?x1)

[1]Rewriting:

(\<alpha> \<circ> f) e \<equiv> \<alpha> (f e)

[1]Applying instance of rewrite rule "Fun.o_apply":

(?f1 \<circ> ?g1) ?x1 \<equiv> ?f1 (?g1 ?x1)

*[1]Rewriting:*

*(\<alpha> \<circ> f) u \<equiv> \<alpha> (f u)*



Sorry for the complex example, if someone wants I will try to compose a
runnable theory and send it to him. But my question for short is:

What's going on behind the scenes that is not reported in the simplifier
trace ?


Thanks in advance and regards
  Peter


-- 
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380



-- 
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380






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