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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
