Email Gateway (Aug 23 2022 at 08:48): Email Gateway (Aug 23 2022 at 08:48):From: Martin Desharnais <martin.desharnais@gmail.com>
Dear Isabelle users,
I am in a situation where I want to use function extensionality for
multiple simplification equalities in a forward proof. Following is a
simplification of my current theory.
I have a function "foo" that has multiple (long) pattern matching cases.
Some of the cases have unique definitions (such as the "foo True" case)
but many cases simply forward some of the parameters to a generic
function "f" with some more fixed arguments.
Thus many simplification lemmas have the form "foo False xs = f 0 False
xs". I want some simpler lemmas with no schematic variables like "xs"
for those cases. I want to use these simpler lemmas in proofs but, more
importantly, in a PDF presentation of the theory.
I can write a backward proof for each of them (cf. foo_False_backward),
but I then need to restate all those cases. I want to avoid such
repetition. My question is thus: how can I state these lemmas using a
forward proof?
context fixes f :: "nat => bool => 'a list => 'a list" begin
fun foo :: "bool => 'a list => 'a list" where
"foo True (x # xs) = xs" |
"foo False xs = f 0 False xs" |
"foo _ _ = []"
lemma foo_False_backward: "foo False = f 0 False"
by auto
(* how to do this ? *)
lemmas foo_False_forward = foo.simps(2) (* something with @{thm ext}? *)
end
This question seems to be an instance of a more general question on
schematic variables. I found an e-mail from October 2015 from Lars
Noschinski [1] where he stated the following.
Isabelle normalizes all rules by (a) moving universal
quantifiers as far outside as possible and (b) replacing outermost
universal quantifiers by schematic variables.
If I could invert operation (b), I could use the theorem HOL.ext and
achieve my goal. Anecdotally, I have encounter other cases where I would
need to replace schematic variables by universal quantifiers. My second
question is thus: how can one replace schematic variable by universal
quantifiers?
Regards,
Martin Desharnais
[1]:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-October/msg00024.html
signature.asc
Email Gateway (Aug 23 2022 at 08:48):From: Peter Lammich <lammich@in.tum.de>
Hi
One (slightly imperfect, see below) solution is:
(* how to do this ? *)
lemmas foo_False_forward = foo.simps(2)[abs_def]
The abs_def attribute is originally made to reduce all schematic
extensions of a theorem of the form "c ?x1 ... ?xN = ...".
It will convert them to lambdas. I.e., my above solution actually
produces
local.foo False ≡ λxs. f 0 False xs
which Isabelle displays eta-contracted, unless you tell it to not do
so:
declare [[eta_contract = false]]
Moreover, abs_def does not work with conditional equations:
definition "x>0 ⟹ bar x y ≡ x+y"
thm bar_def[abs_def] ( fail )
although the y could safely be removed.
Last updated: Apr 25 2024 at 12:23 UTC