# [isabelle-dev] simplifier and subgoaler not transitive

Christian Urban christian.urban at kcl.ac.uk
Tue May 22 18:23:32 CEST 2012

```Dear All,

Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question.

The simplifier has a subgoaler, which helps with rewriting
conditional lemmas. This simplifiying/subgoaling process seems
to be not transitive (probably is not meant to be). The problem
that arises for me is the following: I have set up the simplifier
to automatically solve the first two lemmas:

lemma "atom v # (x1, x2) ==> atom v # x1"
apply(simp)
done

lemma "atom v # x1 ==> v \<noteq> x1"
apply(simp)
done

but it chokes, if I am trying to string both lemmas
together

lemma "atom v # (x1, x2) ==> v \<noteq> x1"
apply(simp) --"fails"

Is there some magic that I can make the simplifier to
deal also with the latter goal?

The cool thing about jEdit is that I have the simplifier
traces of all three goals next to each other (the trick
is to disable the auto update). Unfortunately, I am
not very good at reading these traces. The only thing I
can say is that the simplifier starts off with goal 1
and 3 in the same direction, but then things start to
the tracing information of the simplifier? The traces
are attached for reference.

Best wishes and thanks for any help,
Christian

GOAL 1
======

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ (x1, x2) ⟹ atom v ♯ x1
[1]Applying instance of rewrite rule "??.unknown":
?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯ (?x1.1, ?x2.1) ≡ True
[1]Trying to rewrite:
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ x1
[1]FAILED
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
atom v ♯ x1 ≡ True
atom v ♯ t ≡ True
[1]Applying instance of rewrite rule "??.unknown":
atom v ♯ x1 ≡ True
[1]Rewriting:
atom v ♯ x1 ≡ True
proof (prove): step 1

goal:
No subgoals!

GOAL 2
======

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ x1 ⟹ v ≠ x1
[1]Applying instance of rewrite rule "Nominal2_Base.fresh_at_base_2":
?a1 ♯ ?b1 ≡ ?a1 ≠ atom ?b1
[1]Rewriting:
atom v ♯ x1 ≡ atom v ≠ atom x1
[1]Applying instance of rewrite rule "Nominal2_Base.at_base_class.atom_eq_iff":
atom ?a1 = atom ?b1 ≡ ?a1 = ?b1
[1]Rewriting:
atom v = atom x1 ≡ v = x1
v = x1 ≡ False
[1]Applying instance of rewrite rule "??.unknown":
v = x1 ≡ False
[1]Rewriting:
v = x1 ≡ False
[1]Applying instance of rewrite rule "HOL.simp_thms_8":
¬ False ≡ True
[1]Rewriting:
¬ False ≡ True
proof (prove): step 1

goal:
No subgoals!

Goal 3
======

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ (x1, x2) ⟹ v ≠ x1
[1]Applying instance of rewrite rule "??.unknown":
?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯ (?x1.1, ?x2.1) ≡ True
[1]Trying to rewrite:
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ x1
[2]Applying instance of rewrite rule "Nominal2_Base.fresh_at_base_2":
?a1 ♯ ?b1 ≡ ?a1 ≠ atom ?b1
[2]Rewriting:
atom v ♯ x1 ≡ atom v ≠ atom x1
[2]Applying instance of rewrite rule "Nominal2_Base.at_base_class.atom_eq_iff":
atom ?a1 = atom ?b1 ≡ ?a1 = ?b1
[2]Rewriting:
atom v = atom x1 ≡ v = x1
[1]FAILED
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True