Re: [isabelle] Automatic derivation of specialised theorems



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

On 18/02/14 15:41, Manuel Eberl wrote:
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:

1. replace every occurrence of “x div foo x” in the theorem with “?x”
(i.e. just replace lhs of equation with rhs everywhere)
2. perform some simplification, possibly with a restricted simpset
3. register the new theorem under the name of the old one, plus the
suffix “_nat”


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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.