Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] simp matching depends on lexicographic variabl...

view this post on Zulip Email Gateway (Aug 19 2022 at 10:08):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,

I'm trying to add a simp rule, but it doesn't do any matching unless,
for subsequent theorems, I name my variables in a certain, lexicographic
order.

I set up the syntax and theorem as next shown, where I've converted
\<lbrace> and \<rbrace> to "{" and "}", except in the syntax command.

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
translations
"\<lbrace>r,s\<rbrace>" == "CONST paS r s"

theorem lrbrace_notation [simp]:
"{{r,s},{p,p}} = {{p,p},{r,s}}"
sorry

The simp rule works for the following:

theorem "{{f,d},{e,e}} = z"
apply simp
--"Output: {{e,e},{f,d}} = z"
oops

However, if I replace "f" with anything lexicographically less than "f",
it doesn't match, and doesn't simplify the goal, such as for the following:

theorem "{{a,d},{e,e}} = z"
apply simp
oops

In the theory, I replace "f" with variables named from "a" to "e", and
it doesn't match, but when I get to "f", it matches.

I attach theory, and I include it below.

Thanks,
GB

theory simp_pair_singleton_switch_alphabet_dependent

imports Complex_Main
begin
typedecl sT
consts paS :: "sT => sT => sT"

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
translations
"\<lbrace>r,s\<rbrace>" == "CONST paS r s"

theorem lrbrace_notation [simp]:
"\<lbrace>\<lbrace>r,s\<rbrace>,\<lbrace>p,p\<rbrace>\<rbrace> =
\<lbrace>\<lbrace>p,p\<rbrace>,\<lbrace>r,s\<rbrace>\<rbrace>"
sorry

theorem "\<lbrace>\<lbrace>f,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
--"Output:
\<lbrace>\<lbrace>e,e\<rbrace>,\<lbrace>f,d\<rbrace>\<rbrace> = z"
oops

theorem "\<lbrace>\<lbrace>a,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>b,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>c,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>d,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>e,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops

theorem regular_braces [simp]:
"{{r,s},{p}} = {{p},{r,s}}"
sorry
theorem "{{a,d},{e,e}} = z"
apply simp
--"Output: {{e}, {a, d}} = z"
oops
end
simp_pair_singleton_switch_alphabet_dependent.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 10:09):

From: Tobias Nipkow <nipkow@in.tum.de>
Yes. You have discovered a feature called "ordered rewriting". It is described
in the Tutorial "Isabelle/HOL - A Proof Assistant for Higher-Order Logic" in
9.1.1 under Permutative Rewrite Rules.

Regards
Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 10:09):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 2/12/2013 1:26 PM, Tobias Nipkow wrote:

Yes. You have discovered a feature called "ordered rewriting". It is described
in the Tutorial "Isabelle/HOL - A Proof Assistant for Higher-Order Logic" in
9.1.1 under Permutative Rewrite Rules.

Tobias,

Thanks for the help. That opened up lots more possibilities that hadn't
even occurred to me, and that I was neglecting.

I implemented about two forms each of the associativity and
left-commutativity rules, like it said to do in the book, and then some
other rules. I wouldn't even have thought about the left-commutative rule.

The rewriting seems to put priority on the associativity and
commutativity rules; I put a rule before them that simplified things,
but then it wasn't used for a simple test case, and the other rules
expanded something I tried to eliminate.

It all works out though, for now. I got finite sets with no repetitions
and equality in about 8 hours instead of two months or never. I thought
I would have to dig through Sets.thy to figure all that out.

When I do a command "apply simp", is there a command to tell me what
rules it applied for that command? All I know about is "print_simpset".
A great debugger tool would be able to single step through the simp
rules for an "apply simp".

I attach a screenshot at 22Kbytes of a big, gnarly, nested set equality
with repetitions that's proved by simp.

Thanks again,
GB

Regards
Tobias

Am 12/02/2013 19:48, schrieb Gottfried Barrow:

Hi,

I'm trying to add a simp rule, but it doesn't do any matching unless, for
subsequent theorems, I name my variables in a certain, lexicographic order.

I set up the syntax and theorem as next shown, where I've converted \<lbrace>
and \<rbrace> to "{" and "}", except in the syntax command.

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
translations
"\<lbrace>r,s\<rbrace>" == "CONST paS r s"

theorem lrbrace_notation [simp]:
"{{r,s},{p,p}} = {{p,p},{r,s}}"
sorry

The simp rule works for the following:

theorem "{{f,d},{e,e}} = z"
apply simp
--"Output: {{e,e},{f,d}} = z"
oops

However, if I replace "f" with anything lexicographically less than "f", it
doesn't match, and doesn't simplify the goal, such as for the following:

theorem "{{a,d},{e,e}} = z"
apply simp
oops

In the theory, I replace "f" with variables named from "a" to "e", and it
doesn't match, but when I get to "f", it matches.

I attach theory, and I include it below.

Thanks,
GB

theory simp_pair_singleton_switch_alphabet_dependent

imports Complex_Main
begin
typedecl sT
consts paS :: "sT => sT => sT"

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
translations
"\<lbrace>r,s\<rbrace>" == "CONST paS r s"

theorem lrbrace_notation [simp]:
"\<lbrace>\<lbrace>r,s\<rbrace>,\<lbrace>p,p\<rbrace>\<rbrace> =
\<lbrace>\<lbrace>p,p\<rbrace>,\<lbrace>r,s\<rbrace>\<rbrace>"
sorry

theorem "\<lbrace>\<lbrace>f,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
--"Output: \<lbrace>\<lbrace>e,e\<rbrace>,\<lbrace>f,d\<rbrace>\<rbrace> = z"
oops

theorem "\<lbrace>\<lbrace>a,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>b,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>c,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>d,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops
theorem "\<lbrace>\<lbrace>e,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
apply simp
oops

theorem regular_braces [simp]:
"{{r,s},{p}} = {{p},{r,s}}"
sorry
theorem "{{a,d},{e,e}} = z"
apply simp
--"Output: {{e}, {a, d}} = z"
oops
end

Gnarly_nested_set_ordered.png

view this post on Zulip Email Gateway (Aug 19 2022 at 10:09):

From: Tobias Nipkow <nipkow@in.tum.de>
Such a tool is in the making. For the time being you can prefix your "apply
simp" by "using [[simp_trace]]". This gives you a very detailed trace, probably
much more than what you want.

Tobias

view this post on Zulip Email Gateway (Aug 19 2022 at 10:11):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
No, "using [[simp_trace]]" works perfect for simple test cases. Using a
fancy debugger wouldn't be any easier. Figuring out where to set the
break points for a debugger can be no easy task, not I've used a
debugger much, or any, because it's easier to just print to screen, and
then prompt the user, than learn how to use a debugger.

So reducing a formula down more and more can serve the purpose of single
stepping or setting break points.

But, I was wanting to confirm whether this sentence, page 178,

"Permutative rewrite rules can be turned into simpli
cation rules in
the usual manner via the simp attribute; the simplifer recognizes
their special status automatically."

means it does the permutative rewrite rules first, and it does mean
that. The commutative and left-commutative rules end up doing together
what I had as one rule.

Regards,
GB

Last updated: Nov 21 2024 at 12:39 UTC