[isabelle-dev] simplifier and subgoaler not transitive

[Christian Urban]

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
diverge. Is there a place where one can read up about
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 
 [1]Adding rewrite rule "??.unknown":
atom v ♯ x1 ≡ True 
 [1]Adding rewrite rule "??.unknown":
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 
 [1]Adding rewrite rule "??.unknown":
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 
 [1]Adding rewrite rule "??.unknown":
atom v ♯ x1 ≡ True 
 [1]Adding rewrite rule "??.unknown":
atom v ♯ t ≡ True 
 empty result sequence -- proof command failed