Stream: Isabelle/ML

Topic: Discharge a goal using simplifier in ML

Jason Hu (Sep 10 2022 at 03:29):

Hi, I am trying to write a tactic that does the following:

1. find an expression of some commutative monoid in a proof goal, call it original
2. compute a rearranged expression, call it new
3. replace original with new; since original = new, I suppose the simplifier can just prove it
4. remove the premise original = new from the premises.

so my question is, how do I achieve step 3 and 4? I asked previously so people say that the simplifier is complete in solving commutative monoid. A few pointers leading me to the right direction would be appreciated.

Jan van Brügge (Sep 10 2022 at 10:13):

Do you know either where in the goal original will appear or what original will be? Otherwise this will be really hard

Jason Hu (Sep 10 2022 at 14:57):

yes I know its type and it's in a fixed position (more or less). In general, finding original shouldn't be difficult and deriving new is dead easy

Jason Hu (Sep 10 2022 at 14:58):

or in a big picture, I want to replace the goal P original with P new without adding anything to the context

Jan van Brügge (Sep 10 2022 at 15:27):

You will have to create the term original = new and prove that separately. Then you can use unfold_thms_tac to replace all occurrences of original by new.

Last updated: Apr 26 2024 at 12:28 UTC