CODEWITHSUNDEEP
isabelle
alagris
alagris

Reputation: 2206

How to have full control over substitution in Isabelle

In Isabelle I find myself often using

apply(subst xx)
apply(rule subst)
apply(subst_tac xx)

and similar command but often it is a hit or miss. Is there any resources on how to guide the term unification and how to precisely specify the terms that should be substituted for? For example if there are multiple ways to perform unification, how can I disambiguate? If I have multiple equalities among the premises, how can I tell Isabelle which one of them to use? I spend way too much time wrestling with such seemingly simple problems.

This book https://www21.in.tum.de/~nipkow/LNCS2283/ has a chapter dedicated to substitution but it's far too short, only covers erule ssubst and doesn't really answer my questions.

To give some examples, this is ssubst

lemma ssubst: "t = s ⟹ P s ⟹ P t"
  by (drule sym) (erule subst)

but what about

lemma arg_cong: "x = y ⟹ f x = f y"
  by (iprover intro: refl elim: subst)

How can I do erule_tac arg_cong and specify exactly the desired f, x and y? Anything I tried resulted in Failed to apply proof method which is not a particularly enlightening error message.

Upvotes: 1

Views: 111

Answers (1)

Lawrence Paulson
Lawrence Paulson

Reputation: 589

As I recall, a more elaborate substitution method is available, in particular for restricting substitution to certain contexts. But to answer your question properly it's essential to know what sort of assertions you are trying to prove. If you are working with short expressions (up to a couple of lines long), then it's much better to guide the series of transformations using equational reasoning, via also and finally. (See Programming and Proving in Isabelle/HOL, 4.2.2 Chains of (In)Equations.) Then at the cost of writing out these expressions, you'll often find that you can prove each step automatically, without detailed substitutions, and you can follow your reasoning.

Also note that if your expressions are long because they contain large, repeated subexpressions, you can introduce abbreviations using define. You will then not only have shorter and clearer proofs, but you will find that automation will perform much better.

The other situation is when you are working with verification conditions dozens of lines long, or even longer. In that case it is worth looking for more advanced substitution packages.

Upvotes: 1

Related Questions