[isabelle-dev] simplifier and subgoaler not transitive

[Tobias Nipkow]

Am 22/05/2012 18:23, schrieb 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).

Indeed, there is no guarantee. Hence it is unclear of it is cost effective to
figure out why exactly it did not work in your example. I took a look ...

> 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
> ======

but am at least as confused as you are:

>  [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

Where does this rewrite rule come from? Its name suggests it was created during
the simp process, but there is no indication of that.

>  [1]Trying to rewrite:
> atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True

This should be an instance of the above rule, but it is not, there is a funny t.
I have no idea where that comes from. I'm confused.

With ATPs, and the simplifier is one, it is best not to spend much time on
figuring out why they failed but to accept it when they fail. [A typical problem
for the simplifier are rules of the form P x y ==> Q x, which can be applied if
a premise P a b is present but not if it needs another conidtional rule R x y
==> P x y first.]

Tobias


>  [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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev