[isabelle] Something strange with simplifier and (op \<ci... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Something strange with simplifier and (op \<ci...

Email Gateway (Aug 18 2022 at 11:06):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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":