[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
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
More information about the isabelle-dev
mailing list