Email Gateway (Aug 19 2022 at 13:35): Email Gateway (Aug 19 2022 at 13:35):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I currently have the following situation: I have a number of theorems in
some typeclass that contain terms such as “x div foo x” (where foo is a
function constant and x is a free variable)
For particular instantiations of this typeclass, “x div foo x” often has
a much easier form. Say, for instance, I have a theorem “(?x::nat) div
foo ?x = ?x” I would therefore like to do the following for any theorem
that contains “?x div foo ?x” as a subterm:
replace every occurrence of “x div foo x” in the theorem with “?x”
(i.e. just replace lhs of equation with rhs everywhere)
perform some simplification, possibly with a restricted simpset
Are there any existing mechanisms for something like this? If not, how
should I proceed? For instance, how do I get a list of all theorems
containing such a pattern? (All of this will be done only in the theory
where the type class instance was first derived, so this is a very
“local” operation, the number of theorems affected is not very large)
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:35):From: Peter Lammich <lammich@in.tum.de>
- replace every occurrence of “x div foo x” in the theorem with “?x”
(i.e. just replace lhs of equation with rhs everywhere)- perform some simplification, possibly with a restricted simpset
- register the new theorem under the name of the old one, plus the
suffix “_nat”
1 + 2 sounds like the "unfolded" and "simplified" attributes.
For 3, I do not know any "clean" solution ;)
-- Peter
Are there any existing mechanisms for something like this? If not, how
should I proceed? For instance, how do I get a list of all theorems
containing such a pattern? (All of this will be done only in the theory
where the type class instance was first derived, so this is a very
“local” operation, the number of theorems affected is not very large)Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:35):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
From your name "_nat", I guess that you just need this transformation for natural
numbers, so you can exploit the rewriting morphism of interpretation. If you state more
equations there, you get more simplification. This also allows you to register the facts
under the same name with a prefix such as "nat.". Suffixes are not supported. Here's a
silly example.
class foo = div + fixes foo :: "'a => 'a" begin
lemma foo: "x div foo x = y" sorry
end
interpretation nat!: foo "op *" "op div" "op mod" "id :: nat => nat"
where "!!x :: nat. x div id x == x" sorry
thm nat.foo
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:36):From: Manuel Eberl <eberlm@in.tum.de>
Not quite. I also need it for int. I thought about using locales, but
that would require me to also put the original theorems into a locale of
their own; I'm not sure whether I want that.
Also, in regard to what Peter said: I'm not really looking for a
solution within the high level stuff of Isabelle, I was thinking of a
solution in Isabelle/ML. My main problem is finding all the theorems
that contain an occurrence of some pattern; if I knew how to do that, I
could probably manage the rest myself with what little knowledge I have
of Isabelle/ML.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:42):From: Makarius <makarius@sketis.net>
I've found this approach by Andreas quite nice. What is wrong about
putting your original theorems into a locale?
Without any further context of the actual application, it is hard to tell
what you actually need, in contrast to what you think you want.
Makarius
Email Gateway (Aug 19 2022 at 13:42):From: Manuel Eberl <eberlm@in.tum.de>
Point taken.
The context is the following, modified GCD theory, in particular the
lemmas in euclidean_semiring_gcd: http://shodan.linuxd.org/paste/Fl46bj4E
The problem is that the general theorems in euclidean_semiring_gcd
contain statements such as "is_unit x", "associated x y",
"normalisation_factor x", "euclidean_size x". However:
For int, they simplify to "abs x = 1", "abs x = abs y", "sgn x", and
"abs x", respectively
for 'a poly, they simplify to "x ? 0 ? degree x = 0", "associated x
y", "coeff (degree x) x", and "degree x", respectively
Also, expressions such as "x div normalisation_factor x" simplify
accordingly to "x" for nat and "abs x" for int.
Of course, one would like to have a general theorem stating that "gcd
(x::'a::euclidean_semiring) 0 = x div normalisation_factor x", but also
specialised ones saying "gcd (x::nat) 0 = x" and "gcd (x::int) 0 = abs x".
I think locales can do most of those (although I'm not quite sure how to
set it up exactly), but some things, but some things, such as
automatically discarding trivial assumptions like "normalisation_factor
x = 1" for x :: nat are, to my knowledge, not possible with locales.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:57):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
Since you did not specify which theorems you need to transfer, I had a go at gcd_0_left,
lcmI, and lcm_unique and inserted the following after the instantiation nat ::
euclidean_semiring_gcd.
interpretation nat!: euclidean_semiring_gcd
gcd lcm Gcd Lcm "op *" "op div" "op mod" "op +" "0 :: nat" 1 id "normalisation_factor"
where "!!x :: nat. x div normalisation_factor x == x"
and "!!x :: nat. normalisation_factor x = (if x = 0 then 0 else 1) == True"
and "(PROP Q ==> True ==> PROP P) == (PROP Q ==> PROP P)"
-- "get rid of assumption True in lcmI"
and "True ∧ x == x" -- "get rid of True in conjunction in lcm_unique"
sorry
thm nat.gcd_0_left nat.lcmI nat.lcm_unique
The set of rules seem sufficient for the three theorems, but you probably need more for
other theorems.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 14:01):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
thank you, as far as I can tell, that is more or less what I wanted.
However, I'm struggling to prove the obligations that this command gives
me, in particular:
⋀a. a ≠ 0 ⟹ semiring_div.is_unit op * 1 (normalisation_factor a)
This should be reasonably simple to prove if I could unfold the
definition of is_unit, but I cannot, because for that I would require
“class.semiring_div (op *) (op div) (op mod) (op +) 0 (Suc 0)” and I
don't know where to get it from. Besides, working with classes/locales
in such an indirect way seems a bit pedestrian to me – is there a better
way?
In other words: what is the least ugly way to get rid of those proof
obligations?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 14:02):From: Manuel Eberl <eberlm@in.tum.de>
Apologies for writing another mail, but I just noticed another problem:
your solution generates the following theorem for lcmI:
dvd.dvd op * (?x∷nat) (?k∷nat) ⟹ dvd.dvd op * (?y∷nat) ?k ⟹ (⋀l∷nat.
dvd.dvd op * ?x l ⟹
dvd.dvd op * ?y l ⟹ dvd.dvd op * ?k l) ⟹ ?k = lcm ?x ?y
I would, of course, very much like to have “dvd.dvd op * (?x::nat)
(?k::nat)” as “(?x::nat) dvd (?k::nat)"
What do I have to change to achieve that?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 14:02):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
You have already shown in the instantiation of euclidean_semiring_gcd with nat that all
the proof obligations hold for naturals. The proof obligation that you mention is
generated by trying to prove manually once more that the operations on nat satisfy
euclidean_semiring_gcd. Normally, unfold_locales should solve this completely, but in the
example below, I have replaced euclidean_size with id. Therefore, the easiest way to prove
the class predicate is to make sure that the parameters exactly fit an existing
interpretation and then call unfold_locales. You can inspect the existing interpretations
with print_interps <locale name>.
The reason for using id instead of euclidean_size is that interpretation generates the
theorems only if the set of parameters are not already subsumed by a previous
interpretation. If I had used euclidean_size instead of id, interpretation would not do
anything at all.
The following works for me:
interpretation nat!: euclidean_semiring_gcd gcd lcm Gcd Lcm "op *" "op div" "op mod"
"op +" "0 :: nat" 1 id normalisation_factor
where "!!x :: nat. x div normalisation_factor x == x"
and "!!x :: nat. normalisation_factor x = (if x = 0 then 0 else 1) == True"
and "(PROP Q ==> True ==> PROP P) == (PROP Q ==> PROP P)"
and "True ∧ x == x"
apply(subst euclidean_size_nat_def[symmetric]) -- "replace id with euclidean_size"
apply unfold_locales -- "get rid of the class predicate"
apply(simp_all add: atomize_eq split: split_if) -- "solve all the rewrite equations"
done
Best,
Andreas
Email Gateway (Aug 19 2022 at 14:02):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
You just have to add another rewrite rule to the where clauses of the interpretation:
"dvd.dvd op * == (op dvd :: nat => _)"
You can show this by expanding the definitions as follows.
by(simp add: fun_eq_iff dvd.dvd_def dvd_def)
Best,
Andreas
Last updated: Apr 19 2024 at 08:19 UTC