Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Tactic to force simplification?

Email Gateway (Aug 19 2022 at 15:43):

From: Holden Lee <hl422@cam.ac.uk>
Often, I have something I want to prove, say

f x = h x

and there is a simplification I want to use, say

P x => f x = g x

I would like Isabelle to replace the goal

1. f x = h x

by

1. P x
2. g x = h x.

Is there a simple way to do this (without a structured proof)? (Also note
that the x might be inside a !! quantifier, in which case I would want

1. !!x. Q x => f x = h x

would be replaced by

1. !!x. Q x => P x
2. !!x. Q x => g x = h x.)

Thanks,
Holden

Email Gateway (Aug 19 2022 at 15:43):

From: Lars Noschinski <noschinl@in.tum.de>
apply (subst <rule>)

-- Lars

Email Gateway (Aug 19 2022 at 15:43):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Holden,

you might use trans[OF ...] as follows.

context
fixes P :: "'a => bool" and f g h :: "'a => 'a"
begin
lemma simp_me: "P x ==> f x = g x" sorry

lemma to_prove: "f x = h x"
apply (rule trans[OF simp_me])
sorry
end

Cheers,
René

Email Gateway (Aug 19 2022 at 15:43):

From: Holden Lee <hl422@cam.ac.uk>
Thanks. One more wrinkle: In general I would like this to work if there
were other terms present. For example, to replace

1. f x + f1 x = h x + h1 x

with

1. P x
2. g x + f1 x = h x + h1 x. [in full generality, it would be some function
   F x (f x) on the LHS, to be replaced by F x (g x).]

Would this be possible?

Last updated: Apr 19 2024 at 01:05 UTC