Question: it looks to me like "(atom v # (x, y)) = (atom v # x & atom v
# y)"
It also looks like what you're trying to do is allow the system to
reason with the above equality without actually giving it that equality.
It looks like you've provided the equality in one direction as a rewrite
rule and in the other direction by adjusting mksimps (just guessing
here, but that's what it looks like).
Did I guess right? If so, I know why that won't work :-) The new rewrite
rules created by mksimps aren't themselves candidates for
simplification, so the system won't apply Nominal2_Base.fresh_at_base_2
to them, which was what resulted in further progress on goal #2.
Those are all giant guesses. Am I anywhere near the mark?
More directly, why not just add the rewrite at the top of this email to
the simpset? This will reduce all of these sharp statements to trivial
inequalities. This is the approach that fits with the general design of
the simplifier. Not the structure you want? Too many inequalities? In
that case you really need a guided solver - giving the simplifier
opportunities for wild exploration will just slow everything down.
Yours,
Thomas.
On 23/05/12 02:23, Christian Urban wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
