[isabelle-dev] simplifier and subgoaler not transitive

[Christian Urban]

I am amazed....by you and the simplifier!

Yes, indeed one rule in question was added by mksimps.
You were spot on. I never knew that they have some 
more-than-special meaning. ;o)

The reason why I prefer to keep the freshness constraints
together is that

   atom a # (x1, x2, x3, x4, x5)

would expand to

   atom a # x1 /\ atom a # x2 /\ ...

thus bloating the goal state.

Poring over the trace again and again, and adding "probes", 
like the ones below (in case somebody is interested), actually 
the trace information is quite instructive. It is just a lot of 
pain to piece everything together...but I guess that is what 
one has to love when working with Isabelle. ;o)

In conclusion, I need to implement a special solver for solving the 
type of goals I want to solve...quite a sophisticated piece of code
the simplifier, but good that it lets me do that. 

Thanks again for all replies!
Christian

ML {*
val test_solver = mk_solver "test solver" 
   (fn ss => fn n => print_tac ("TEST SOLVER"))

fun test_subgoaler ss n = 
   print_tac ("SUBGOALER TEST") THEN asm_simp_tac ss n
*}

declaration {* fn _ =>
  Simplifier.map_ss (fn ss => Simplifier.set_subgoaler test_subgoaler (ss addSolver test_solver)) 
*}



On Wednesday, May 23, 2012 at 11:39:53 (+1000), Thomas Sewell wrote:
 > 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-dev at in.tum.de
 > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 > 
 > _______________________________________________
 > isabelle-dev mailing list
 > isabelle-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--