Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Christian Urban 

I am amazedby 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

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Makarius 

On Tue, 22 May 2012, Christian Urban wrote:


Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question.


From what I've seen on the thread so far, it is all perfectly normal 
Isabelle user-space.  You did not propose to re-implement the simplifier, 
so it could just as well be discussed on the larger audience of 
isabelle-users.  The experts are out there, and they are using Isabelle 
Professional Edition (aka release).



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread 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). 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

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread 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-...@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

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Christian Urban 


On Tuesday, May 22, 2012 at 20:59:28 (+0200), Tobias Nipkow wrote:
  
  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.

Sorry, this was because of my postediting of the trace.
It should be a x2. Not sure whether this improves things.

Christian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Thomas Sewell 
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