Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] Larry, you are the original author of hypsubst. Does the hypsubst_thin terminology make sense to you? It is used here both for the configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly legacy in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
The name makes sense: thin refers to deleting the assumption. It is ugly of course, which will be an incentive for users to update their proofs. Larry On 15 Jan 2014, at 15:05, Makarius makar...@sketis.net wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] Larry, you are the original author of hypsubst. Does the hypsubst_thin terminology make sense to you? It is used here both for the configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly legacy in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Whoops. It's both a typo and use of the wrong release. The patch happens to work against Isabelle2013-1 or Isabelle2013-2, since there are no relevant differences in the theory sources. I can confirm that isabelle build -a works in either 2013-1 or 2013-2. Short version of the story, I forgot the name of the newest release. Long version: The confusion was caused in part because the newest l4.verified branch is called '2013-1'. It contains Isabelle 2013-2, but the switch was accomplished so straightforwardly that we didn't end up with a new branch name. Apologies about the confusion, Thomas. On 16/01/14 02:00, Makarius wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Hi Thomas, Am 14.01.2014 um 14:43 schrieb Thomas Sewell thomas.sew...@nicta.com.au: To address Jasmin and Larry's concern, it is possible to switch back to the compatibility mode by setting a config variable in the context, or by calling the ML version with an extra parameter. Any legacy proof script can be repaired by adding the line using [[ hypsubst_thin = true ]] before any apply/by line. That's perfect. I understand why Tjark and Larry would prefer a minimal change, using contextual information to decide when to deviate from the old behaviour. It would certainly create less maintenance work. Let me elaborate why this approach is my first preference: [...] 2) Having the behaviour of tactics change because of largely invisible background concerns seems a recipe for confusion. This particularly applies to building-block tactics such as safe and clarify. I would prefer they be predictable and reliable. Yes. While I agree with Tjark in principle, it appears to me that the syntactic conditions you described are weird enough (even though they make sense upon reflection) that they would confuse users, possibly even those who have been following this thread. Regards, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
This sounds great! You seem to have done everything right. Having the compatibility mode will make it easy to get everything working again quickly, with the conversion to the new setup becoming a background task (possibly to be combined with refactoring horrible old proofs). Larry On 14 Jan 2014, at 13:43, Thomas Sewell thomas.sew...@nicta.com.au wrote: For those reasons I'd prefer to plough ahead as long as the impact is manageable. I'll test the AFP and ISABELLE_FULL_TEST soon. I'm running out of energy for this side project, however. If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] globally in them, but I hope to avoid that for the same reason as (2) above: having invisible adjustments to standard tactics seems like something we should avoid. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Mon, 2014-01-13 at 12:38 +, Thomas Sewell wrote: Given a hypothesis of the form x = Suc a or Suc a = x, where x is a free (blue) variable, hypsubst will substitute Suc a for x throughout the goal, and then discard the hypothesis. The substitution is almost always wanted. Discarding the hypothesis may, however, be unsafe, since there may be facts about x at the proof or locale level that now cannot be used. It may also be unsafe in the subtle case where a schematic variable in the goal can be instantiated to functions of x but not of Suc a. This unsafeness is undesirable because hypsubst is called from tactics that are meant to be safe. I will freely admit my ignorance of the issues involved, but perhaps it would be desirable to identify these unsafe situations in the code and discard the hypothesis if (and only if) doing so is safe? Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Hi Thomas, Am 13.01.2014 um 13:38 schrieb Thomas Sewell thomas.sew...@nicta.com.au: The change requires, for instance, about a dozen lines of changes to the files in HOL/Library, which contain about 50K lines of proof, or 3 lines of changes to HOL/Bali, with 30K. The change to the Nominal examples (30K), however, is a bit longer (100 changes) and a bit more unpleasant. I've also checked the change against one chunk of L4.verified, with 70K lines in it, and have around 60 lines of changes to make. From my perspective, this level of impact seems to be annoying but not too annoying. I'm interested in what others think. Your suggested change looks very reasonable to me. However, if possible, it would be nice if the old behavior could be kept via a flag -- unless it's easy to simulate reliably (e.g. using thin_rl). One reason for my concern is that the new (co)datatype package's tactics rely extensively on hyp_subst_tac and we currently don't have enough tests in the repository to catch all failures. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
If there's interest in getting this change installed, I'll slog through these, and then figure out what's broken and what's expected to be broken in the latest tip of Isabelle and in the AFP. I'd call for volunteers to help with that bit though. I would very much appreciate such a change to hypsubst! (Having thought of doing this patch myself several times, not knowing about the older discussion on this list ;) ) -- Peter All comments welcome, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
I think the problem is that the unsafe situations cannot be detected locally, i.e., there is no way for the tactic to know that a particular free variable is actually a locale constant. I could be wrong: the current treatment of contexts may make this information available after all. That would be the best solution. But if this contextual information is not available, then I think that some sort of compatibility mode will unfortunately be necessary, given the number of instances where introducing the safe behaviour causes proofs to fail. I have to say, in most cases these are tricky proofs that refer to specific assumptions, but lots of these still exist. Larry On 13 Jan 2014, at 12:50, Tjark Weber webe...@in.tum.de wrote: I will freely admit my ignorance of the issues involved, but perhaps it would be desirable to identify these unsafe situations in the code and discard the hypothesis if (and only if) doing so is safe? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
I’m impressed with your determination to slog through so many changes, but I am not sure that we have the right to impose this on our users, which is why I would prefer one of the other solutions, namely (1) contextual information if available (2) some sort of compatibility mode. Thank you very much indeed for taking up this matter again, because I do believe it is important. Larry On 13 Jan 2014, at 12:38, Thomas Sewell thomas.sew...@nicta.com.au wrote: If there's interest in getting this change installed, I'll slog through these, and then figure out what's broken and what's expected to be broken in the latest tip of Isabelle and in the AFP. I'd call for volunteers to help with that bit though. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Mon, 13 Jan 2014, Lawrence Paulson wrote: I think the problem is that the unsafe situations cannot be detected locally, i.e., there is no way for the tactic to know that a particular free variable is actually a locale constant. Indeed. The proposed change is basically some form of localization of hypsubst, in the sense that it does not make implicit assumptions how free variables got introduced, their scope etc. In ancient times, a Free was fixed in the immediate scape of the goal state, but that is long past. the current treatment of contexts may make this information available after all. That is a very old topic, and there are various ideas in some drawer that have accumulated a lot of dust. It could easily take a few more years to revisit that. It somehow belongs to the national debts problem from 2006. Since December 2013, I am again improving the situation concerning the formal proof context within proof tools, notably the Simplifier and its add-ons. It is always surprising how long really tiny steps take, e.g. see current Isabelle/f26a7f06266d. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Note that this change would affect auto, force, fast, etc. Possibly a “legacy” version of auto would help with compatibility, or otherwise some sort of option setting to (locally) restore the old behaviour in all affected methods. Larry On 13 Jan 2014, at 15:47, Makarius makar...@sketis.net wrote: With an easy escape, i.e. the alternate name of the proof method and a confifuration option to recover the old behaviour, users should manage to convert their old stuff reasonably well. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
This sounds logical. But what about auto? Like the other three, it is used to perform obvious steps in a proof, and it is not terminal. Larry On 1 Sep 2010, at 14:17, Thomas Sewell wrote: Let me try to explain the difference from the perspective of a user. There are three classical tools that will behave differently: safe, clarify and clarsimp. Each of these will, when it would have substituted and removed equalities in the past, now substitute those equalities, possibly reorient them, and leave them as hypotheses. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
I always intended auto to be initial rather than terminal. I'm not aware of the unsafe mode you refer to, but it may have been introduced later. Larry On 1 Sep 2010, at 14:40, Thomas Sewell wrote: Good point - I think of auto as terminal. My understanding was that auto had both a safe and unsafe mode internally, where safe exploration is clarsimp-like and seen by the user, and unsafe exploration is fastsimp-like and kept only if it solves the goal. For tactics which continue after auto, this would put it in the clarsimp/safe group. This fits with my experience in writing the supplied patch, where some subgoal_tacs which came after autos had to be adjusted slightly. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Thanks for looking into this problem, which has been around in one way or another from the very beginning. Lost in all the technical discussions is the question of what the user will see. We have the option of leaving blast and force as they are now to minimise danger of incompatibility, though it would be disappointing if existing calls to these stopped working after what should be an improvement. I would expect them, on the contrary, to solve more problems than before. Anyway, the main methods to be affected are presumably safe and auto. I have made a small table showing the number of times the classical proof methods are used in the HOL distribution: safe956 auto23389 clarify 1403 force 1692 fastsimp 560 blast 7609 fast1079 best43 If the only method that behaves differently is safe, I wonder whether there's any point to doing this. It would be better to improve all the methods. If the new version is identical to the old one except that occasionally some equalities persist, then it ought to work as a drop-in replacement in nearly every instance. Is this what you see? Larry On 23 Aug 2010, at 08:52, Thomas Sewell wrote: As previously discussed in the thread Safe for boolean equality, the current strategy for using equality hypotheses 'x = expr', in which substitution for x is done and then the hypothesis is discarded, is unsafe. The conclusion of that discussion was that the problem was annoying but fairly rare, that there is some concern it may become more common as local are used more extensively, and that fixing it would probably require a painful change to the behaviour of auto. The problem is that by forgetting what x equates to in our goal, we lose the connection from the goal to the context outside our goal. There may be other facts available that name x. There may also be schematic variables which could be instantiated to hd x but not the bound variable replacing it. The simple solution in my mind is to keep the equality in the goal, and since noone else seemed interested I thought I'd attempt to do this myself and see how difficult it was. I attach the resulting patch. After several rounds of bugfixes and compatibility improvements, it requires 23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word. The code change in Provers/hypsubst.ML adds code for counting the free and bound variables in a goal, and checking whether either side of an equality hypothesis is a unique variable, occuring nowhere else. The main substitution algorithms avoid using such equalities and also preserve rather than delete the hypothesis they select. There is a new tactic for discarding these equalities, which is added as an unsafe wrapper in Context_Rules, allowing all unsafe tactics to behave roughly as before. The version of hypsubst called by blast is left unchanged, as blast proofs seem to be highly sensitive to changes. There is plenty of room for optimisation, I tried to keep the diff readable. Three kinds of proofs seem to need fixing: 1. proofs where subgoal_tac or similar now needs to refer to xa rather than x. 2. proofs where erule ssubst, drule sym/arg_cong/fun_cong etc need to be further specialised. 3. proofs where variables are eliminated and then induction is performed, i.e. the word library. Explicitly adding apply hypsubst_thin seems the best solution. At this stage I'm not sure how to proceed. I would be very happy to see safe get safer, but I'm not sure how acceptable this level of incompatibility is in an Isabelle change. There's an alternative approach I thought of recently but haven't tried yet - replacing used equalities with meta-equalities - which might reduce the incompatibilities of type 2. I haven't checked whether there are any performance implications. I'd be keen to hear what other Isabelle developers think. Yours, Thomas. hypsubst-diff.txt___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Hi Thomas, Thomas Sewell wrote: It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines. There is still hope if we move the unrelated discussions to another thread... I have another small comment on the issue with algebra: You were saying that the goals were solved in the presimplification phase together with clarify. Are you sure about this? I played a little with the theory, and it seemed to me that it is only solved using the fact dvd_mult2, which is not used in the presimplification rules. Thus, clarify leaves behind an assumption which somehow confuses the following code. I am not sure what assumptions are made by the following code, but maybe it should be able to ignore additional assumptions...? Maybe Amine Chaieb can comment on this further, but it may take a while to get an answer... As you say, terminal methods that break with the patch are problematic, so we should try to understand this, even if we decide in the end that it is a problem of the algebra method. One more small thing: @@ -115,27 +116,55 @@ | (_, Bound i) = if loose(i,t) orelse novars andalso has_vars t then raise Match else false (*eliminates u*) - | (Free _, _) = if bnd orelse Logic.occs(t,u) orelse + | (Free f, _) = if bnd orelse Logic.occs(Free f,u) orelse novars andalso has_vars u then raise Match else true(*eliminates t*) - | (_, Free _) = if bnd orelse Logic.occs(u,t) orelse + | (_, Free f) = if bnd orelse Logic.occs(Free f,t) orelse novars andalso has_vars t then raise Match else false (*eliminates u*) | _ = raise Match; How is this change related to the rest? It seems to me that the only difference between (Free f) and t/u is only the possible eta contraction... So my question should rather be: Why was this correct before? Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Let's try to answer everyone again: Alex: I think I was wrong about the cases involving algebra. There may be something interesting going on. The prenormalisation phase calls clarify_tac, then full_atomize_tac, then some other stuff. With a Free variable x assumed to be even, the resulting goals with the old and new versions of hypsubst are of the form ALL k. P (2 * k) and ALL k. x = 2 * k -- P (2 * k). It's possible that the quantifier elimination process that follows doesn't know what to do with the additional implication, or maybe just its left hand side. If the same problem occurs for more interesting examples, it could be fixed by following clarify_tac with Hypsubst.thin_triv_tac in groebner.ML. Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Makarius: Indeed bounds, frees and consts can all be seen as the same kind of thing. At the moment the only real benefits of hyp_subst over asm_full_simp are robustness in the case of Vars and the capacity to reorient equations in order to rewrite bounds - frees - expressions. Adjusting this to rewrite bounds - frees - consts - expressions would be easy - is this what you are asking for? I don't see this as widely useful, but perhaps you have an application in mind. Finally, the full run of isabelle make test is indeed quite broken, including apparently going into a loop while defining a record in Hoare_Parallel. I'll look into it. Yours, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On Wed, 25 Aug 2010, Thomas Sewell wrote: Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Often it is hard to tell what is a bug or an obscure feature required like that by some other tool. Anyway, I recommend to try that tiny bit of the change on all existing Isabelle + AFP theories. Then we can apply it independently, with a more informative log message that fixed bug, though. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
I'm pretty sure this one is a bug. Try typing this into your favourite Isabelle session: lemma foo: fwrap f = (%v. f v) == P f apply clarify And note the system hangs. I think this is a pretty good argument to support the case that it doesn't occur in any existing Isabelle scripts. Just to be safe, though, I can test this change in isolation against all the HOL libraries and the AFP thisevening when my machine has spare CPU time. I guess I should test against Isabelle 2009-2 rather than a development snapshot since the AFP will be known to build? Yours, Thomas. On 26/08/10 02:49, Makarius wrote: On Wed, 25 Aug 2010, Thomas Sewell wrote: Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Often it is hard to tell what is a bug or an obscure feature required like that by some other tool. Anyway, I recommend to try that tiny bit of the change on all existing Isabelle + AFP theories. Then we can apply it independently, with a more informative log message that fixed bug, though. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/23/2010 12:30 PM, Thomas Sewell wrote: Hello again isabelle-dev. I should clear up some confusion that may have been caused by my mail. I was trying to avoid repeating all that had been said on this issue, and it seems I left out some that hadn't been said as well. This approach avoids ever deleting an equality on a Free variable during a 'safe' reasoning step. It will substitute with that equality but keep it in place. This is a significant change to the intermediate state of some tactic scripts, thus the incompatibilities, especially on induction. It is somewhat surprising there aren't more such incompatibilities. There's no truly safe way to delete an equality on a Free variable without inspecting the whole context. Naive questions: * why is inspecting the whole context infeasible? * why can't we just collect (and cache?) the Frees occuring in assumptions managed by assumption.ML and never delete equalities involving them? Since equalities are not deleted, care must be taken to avoid an infinite loop in which a substitution is repeatedly attempted. This is the reason for the uniqueness check - if x appears only in 'x = expr' then there is no more substitution to be done. Some subtleties were discovered experimentally: - 'x = y' should not be substituted if either x or y is unique, or else we enter a loop substituting x - y - x - 'expr = x' needs to be reoriented when it is substituted, or else hypsubst and simp will loop doing opposite substitutions. - 'x = y' is OK to substitute if y is a unique free and x is a non-unique Bound. This is what is meant by a 'useful' substitution in the comment. Other equalities, which would cause a no-effect or cyclic substitution, are referred to as trivial (abbreviated triv) in this code. The language should probably be cleanup up to use a consistent set of names. Sounds complicated, but cool. You adapted blast_hyp_subst_tac in that way too, right? The subtlety here is that blast tries to approximate the effect of that tactic in the search and has accuracy problems even now. The more complicated the substitution criterion, the more weirdness is induced here. With the current situation before the patch, the accuracy problems can be fully repaired it seems; what works best for blast is a simple criterion of substitutability which is decidable from the hyp (and possibly information that stays constant in the whole search) only. Let me address Alex's detailed comments: 1. In the HOL sources the algebra method is used to solve two problems about parity essentially by accident. No Groebner bases were involved, but the surrouding logic, which appeals to clarify_tac and a custom simpset, happened to solve the goal. With this change the simplified goal had an extra quantifier in it. Note that with this change terminal tactics operating in 'unsafe' mode - fast, best, etc - will call thin_triv_tac via Context_Rules and behave similarly to before. It is terminal tactics which take safe steps - like algebra - that are most likely to break. 2. Yes, count vars is a bit strange, as it will consider (%f. f) (%x. x) to contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp, which it gets right. Yours, Thomas. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On Tue, 24 Aug 2010, Andreas Schropp wrote: Naive questions: * why is inspecting the whole context infeasible? * why can't we just collect (and cache?) the Frees occuring in assumptions managed by assumption.ML and never delete equalities involving them? Assumptions belong to the foundation layer, i.e. they are conceptionally somehow accidental, even hidden. This is also the reason why using the old prems abbreviation is a bad thing: you can never be sure what it will contain, because Isar language elements are entitled to extend the hypothetical context as required internally, e.g. as done by 'obtain', but not by 'have'. Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. Anyway, I would prefer if the non-local behaviour of hyp_subst could be repaired without too many additional complications, i.e. by using the visible goal that it is offered in a sensible way. There are some further problems of hyp_subst that maybe Stefan Berghofer still recalls. We have been standing there many times before, but never managed to improve it without too much effort, or breaking too many existing proof scripts. The real trouble only starts when trying the main portion of existing applications, and also doing some performance measurements ... Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/24/2010 06:35 PM, Makarius wrote: On Tue, 24 Aug 2010, Andreas Schropp wrote: Naive questions: * why is inspecting the whole context infeasible? * why can't we just collect (and cache?) the Frees occuring in assumptions managed by assumption.ML and never delete equalities involving them? Assumptions belong to the foundation layer, i.e. they are conceptionally somehow accidental, even hidden. Why is the safeness of this equality-elimination not a property only dependent on the foundation layer? Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. I don't get this response: if a Free x is not mentioned in any assumes, the elimination of a hyp x=t can not affect provability of the goal, because any deductions involving x can be done with an arbitrary term of the same type (esp. t) instead, right? Anyway, I would prefer if the non-local behaviour of hyp_subst could be repaired without too many additional complications, i.e. by using the visible goal that it is offered in a sensible way. There are some further problems of hyp_subst that maybe Stefan Berghofer still recalls. We have been standing there many times before, but never managed to improve it without too much effort, or breaking too many existing proof scripts. The real trouble only starts when trying the main portion of existing applications, and also doing some performance measurements ... Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Hi Thomas, Thomas Sewell wrote: I should clear up some confusion that may have been caused by my mail. I was trying to avoid repeating all that had been said on this issue, and it seems I left out some that hadn't been said as well. This approach avoids ever deleting an equality on a Free variable during a 'safe' reasoning step. It will substitute with that equality but keep it in place. Thanks for the clarification. I think I understand better now. Note that with this change terminal tactics operating in 'unsafe' mode - fast, best, etc - will call thin_triv_tac via Context_Rules and behave similarly to before. similarly? :-))) What different behaviour could occur? 2. Yes, count vars is a bit strange, as it will consider (%f. f) (%x. x) to contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp, which it gets right. So it's probably just the name that confused me... Best, Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Andreas Schropp wrote: On 08/24/2010 06:35 PM, Makarius wrote: Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. I don't get this response: if a Free x is not mentioned in any assumes, the elimination of a hyp x=t can not affect provability of the goal, because any deductions involving x can be done with an arbitrary term of the same type (esp. t) instead, right? The safety concerns discussed here are not the only relevant design principle. If a method would peek at the assumtions in a context, you would get a different behaviour of lemma fixes x shows A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method Safe or not, this is obviously undesirable. Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/24/2010 07:51 PM, Alexander Krauss wrote: Andreas Schropp wrote: On 08/24/2010 06:35 PM, Makarius wrote: Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. I don't get this response: if a Free x is not mentioned in any assumes, the elimination of a hyp x=t can not affect provability of the goal, because any deductions involving x can be done with an arbitrary term of the same type (esp. t) instead, right? The safety concerns discussed here are not the only relevant design principle. If a method would peek at the assumtions in a context, you would get a different behaviour of I am just talking about tracking Frees occuring in any assumptions, no general peeking at assumptions. But I get your point. And actually any tactic can peek at the assumptions, via examination of the hyps of the goal-state, so this is at best an unenforcable design consideration and nothing really changes by making this functionality available from assumption.ML. The more practical justification (opposed to the theoretical justification, which I alluded to above) of doing this in the context of equality-elimination might be that most of our tools are based on unification. So they should be closed under substitutions, meaning that if they can prove P, they can prove any well-typed substitutions of Frees and Vars in P? lemma fixes x shows A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method Safe or not, this is obviously undesirable. Well yes, but users have to be aware of the difference between an assume (extending the context) and an explicit goal assumption (not extending the context) anyway. Otherwise things like lemma x=t == t=x x=x proof - assume x=t thus t=x by (rule sym) show x=x by (rule refl) qed should work too without bracing or reording. Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/24/2010 09:13 PM, Andreas Schropp wrote: On 08/24/2010 07:51 PM, Alexander Krauss wrote: lemma fixes x shows A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method Safe or not, this is obviously undesirable. BTW: if you want to be even more conservative you take both fixes and assumes into account (are the Frees in assumes always guaranteed to be fixed?) when approximating safeness of equality-elimination. Then you would have to compare e.g. lemma shows !! x. A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method to observe the difference. Is that better or worse? ^^ ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/24/2010 10:51 PM, Makarius wrote: On Tue, 24 Aug 2010, Andreas Schropp wrote: And actually any tactic can peek at the assumptions, via examination of the hyps of the goal-state A tactic must never peek at the hyps field of the goal state, and it must never peek at the main goal being proved. See also section 3.2 in the Isabelle/Isar implementation manual for some further well-formedness conditions that cannot be enforced by the ML type discipline. Section 3.2 only lists the following The main well-formedness conditions for proper tactics are summarized as follows. · General tactic failure is indicated by an empty result, only serious faults may produce an exception. · The main conclusion must not be changed, apart from instantiating schematic variables. · A tactic operates either uniformly on all subgoals, or specifically on a selected subgoal (without bumping into unrelated subgoals). · Range errors in subgoal addressing produce an empty result. Can someone provide a full list? Is everybody respecting all of them? I don't even know them ... BTW: this email asks a lot of questions about conformity to seemingly undocumented design principles. Please don't mistake that for aggressiveness or something. ^^ The LCF type discipline of the kernel prevents proving wrong results, but it does not prevent breaking tools, or violating higher structuring principles. What are those higher structuring principles? What does violation of them imply? One very important one is independence on logical details of the derivation of previous results. This forbids any tools using proof terms, e.g. Extraction, AWE, unoverloading, HOL-ZF. What is the motivation behind our proof terms if it is considered a well-formedness violation to use them? E.g. tools need to work uniformly for assumptions or derived facts, fixed parameters or locally defined entities. This means I should not do a case distinction based on if something is an assumption etc? That sounds reasonable, but why is it important? Logically an assumption is quite different from a derived fact: introducing an assumption weakens your results, whereas introducing a derived fact never does. Why do we try to blur the line here? What does this say about our equality-elimination criterion, which wants to check if there are any assumptions involving a Free? For historical reasons one can also have Frees that are not fixed in the context, or hyps that are not assumed. So is that a higher structuring principle? Can you list some more with motivations behind them? A good sanity check of some idea that involves the proof context is to see how it interacts either with 'have' or 'obtain' in Isar. I.e. the following should be conservative additions to the proof situation: have P x sorry This doesn't change the assumptions, so no interaction with that equality-elimination safeness approximation idea? or obtain P x sorry This adds the assumption P x, so hyps x=t are not eliminated, which may be more conservative than we need it to be, if there is no further assumption on x (but how realistic is that?). What is obtain without a where clause good for? It looks like a complicated way to write a have P x. The behaviour wrt obtain x where P x is right: this adds fix x assume P x, so hyps x=t are not eliminated, which is correct because we don't know P t so the elimination would loose information. These are just necessariy conditions on structural integrity wrt. the context, not sufficient ones. And are there sufficient ones? Is structural integrity of contexts important for that equality-elimination safeness approximation idea? Where is structural integrity of contexts used and established? You mentioned above that For historical reasons one can also have Frees that are not fixed in the context, or hyps that are not assumed., so this is not part of structural integrity for contexts? ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines. I'm trying to steer clear of contexts - it would seem more elegant to me if there was a purely tactical solution to this problem. To answer Andreas' question about blast_hyp_subst_tac: I made some attempts, but it seemed that making blast_hyp_subst_tac share behaviour or even code with the other versions led to incompatibilities I didn't really understand. The patch I sent keeps blast_hyp_subst_tac strictly in compatibility mode with previous behaviour. I think you've outlined why there was a problem - blast is guessing incorrectly what the tactic will do. Perhaps in the future the Hypsubst ML structure could export its eq_var and triv_asm term inspection functions so blast would have a better idea what it would do (assuming blast can construct accurately what the subgoal passed would be). To respond to Makarius' comment that the real trouble only starts when trying the main portion of existing applications, and also doing some performance measurements ...: I've run the simplest performance measurement I can: rebuilding HOL and HOL-ex. On my desktop machine at home: Pre-patch: Finished HOL (0:11:32 elapsed time, 0:11:30 cpu time, factor 0.99) With patch: Finished HOL (0:11:37 elapsed time, 0:11:33 cpu time, factor 0.99) On my desktop machine at work: Pre-patch: Finished HOL (0:07:24 elapsed time, 0:07:22 cpu time, factor 0.99) Finished HOL-ex (0:15:25 elapsed time, 0:15:21 cpu time, factor 0.99) With patch: Finished HOL (0:07:41 elapsed time, 0:07:41 cpu time, factor 1.00) Finished HOL-ex (0:15:30 elapsed time, 0:15:23 cpu time, factor 0.99) In both cases parallel features are off (ISABELLE_USEDIR_OPTIONS=-q 0 -M 1). Obviously this is only the beginning of the story. As I mentioned before there are some obvious performance improvements that can be made to the tactic itself, which I avoided for the sake of clarity. Whether the additional assumptions are slowing down other tactics is hard to tell. With regard to running a broader set of existing applications: I was hoping to get some agreement as to whether this is a desirable approach or not before investing much more time in repairing proof scripts. I've set the standard isabelle make -k test test running, which may produce interesting results but will more likely tell us that many proofs are broken in trivial ways. Yours, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Safe approach to hypothesis substitution
As previously discussed in the thread Safe for boolean equality, the
current strategy for using equality hypotheses 'x = expr', in which
substitution for x is done and then the hypothesis is discarded, is
unsafe. The conclusion of that discussion was that the problem was
annoying but fairly rare, that there is some concern it may become more
common as local are used more extensively, and that fixing it would
probably require a painful change to the behaviour of auto.
The problem is that by forgetting what x equates to in our goal, we lose
the connection from the goal to the context outside our goal. There may
be other facts available that name x. There may also be schematic
variables which could be instantiated to hd x but not the bound
variable replacing it.
The simple solution in my mind is to keep the equality in the goal, and
since noone else seemed interested I thought I'd attempt to do this
myself and see how difficult it was. I attach the resulting patch. After
several rounds of bugfixes and compatibility improvements, it requires
23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word.
The code change in Provers/hypsubst.ML adds code for counting the free
and bound variables in a goal, and checking whether either side of an
equality hypothesis is a unique variable, occuring nowhere else. The
main substitution algorithms avoid using such equalities and also
preserve rather than delete the hypothesis they select. There is a new
tactic for discarding these equalities, which is added as an unsafe
wrapper in Context_Rules, allowing all unsafe tactics to behave roughly
as before. The version of hypsubst called by blast is left unchanged, as
blast proofs seem to be highly sensitive to changes. There is plenty of
room for optimisation, I tried to keep the diff readable.
Three kinds of proofs seem to need fixing:
1. proofs where subgoal_tac or similar now needs to refer to xa
rather than x.
2. proofs where erule ssubst, drule sym/arg_cong/fun_cong etc need to
be further specialised.
3. proofs where variables are eliminated and then induction is
performed, i.e. the word library. Explicitly adding apply
hypsubst_thin seems the best solution.
At this stage I'm not sure how to proceed. I would be very happy to see
safe get safer, but I'm not sure how acceptable this level of
incompatibility is in an Isabelle change. There's an alternative
approach I thought of recently but haven't tried yet - replacing used
equalities with meta-equalities - which might reduce the
incompatibilities of type 2.
I haven't checked whether there are any performance implications.
I'd be keen to hear what other Isabelle developers think.
Yours,
Thomas.
diff -r 2e1b6a8a0fdd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Divides.thy Mon Aug 23 17:33:59 2010 +1000
@@ -429,7 +429,7 @@
apply (case_tac y = 0) apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac -(y * k) = y * - k)
- apply (erule ssubst)
+ apply (simp only:)
apply (erule div_mult_self1_is_id)
apply simp
done
@@ -438,8 +438,7 @@
apply (case_tac y = 0) apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac y * k = -y * -k)
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
apply simp
apply simp
done
diff -r 2e1b6a8a0fdd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/HOL.thy Mon Aug 23 17:33:59 2010 +1000
@@ -871,6 +871,7 @@
Hypsubst.hypsubst_setup
(*prevent substitution on bool*)
# Context_Rules.addSWrapper (fn tac = hyp_subst_tac' ORELSE' tac)
+ # Context_Rules.addWrapper (fn tac = Hypsubst.thin_triv_tac false ORELSE'
tac)
end
*}
diff -r 2e1b6a8a0fdd src/HOL/Int.thy
--- a/src/HOL/Int.thy Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Int.thy Mon Aug 23 17:33:59 2010 +1000
@@ -542,7 +542,7 @@
lemma negD: (x \Colon int) 0 \Longrightarrow \existsn. x = - (of_nat
(Suc n))
apply (cases x)
apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x=y - Suc x in exI, arith)
+apply (rule_tac x=y - Suc xa in exI, arith)
done
diff -r 2e1b6a8a0fdd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Library/Multiset.thy Mon Aug 23 17:33:59 2010 +1000
@@ -1116,7 +1116,7 @@
apply (simp (no_asm))
apply (rule_tac x = (K - {#a#}) + Ka in exI)
apply (simp (no_asm_simp) add: add_assoc [symmetric])
- apply (drule_tac f = \lambdaM. M - {#a#} in arg_cong)
+ apply (drule_tac f = \lambdaM. M - {#a#} and x=?S + ?T in arg_cong)
apply (simp add: diff_union_single_conv)
apply (simp (no_asm_use) add: trans_def)
apply blast
@@ -1127,7 +1127,7 @@
apply (rule conjI)
apply (simp add: multiset_ext_iff split: nat_diff_split)
apply (rule conjI)
- apply (drule_tac f = \lambdaM. M - {#a#} in arg_cong, simp)
+ apply (drule_tac f
Re: [isabelle-dev] Safe approach to hypothesis substitution
Hi Thomas, Thanks for digging into this. The concrete patch is exactly what was needed to advance this discussion. Here are a few comments. I am sure others will have more... I attach the resulting patch. After several rounds of bugfixes and compatibility improvements, it requires 23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word. So it is painful (as there are a much more theories out there), but it may work, and it may be worth the trouble in the long run. The code change in Provers/hypsubst.ML adds code for counting the free and bound variables in a goal, and checking whether either side of an equality hypothesis is a unique variable, occuring nowhere else. The main substitution algorithms avoid using such equalities and also preserve rather than delete the hypothesis they select. Do I understand correctly that substituting the hypothesis is safe, but discarding them afterwards is unsafe? Then, why should they not be used? More importantly, why is it safe to use and discard an equality when the variable occurs elsewhere in the goal? The equality itself could interact with a fact from the context? Consider the contrived example locale l = fixes x :: nat assumes neq: x ~= 0 begin lemma x = 0 == x = x + 1 == False apply safe After safe, the lemma becomes unprovable, since the hypothesis that contradicts the context is removed. It seems that your patch does not fix this... (I haven't tried... just guessing from reading the code) [...] A few concrete remarks concerning the patch (which seems to be relative to Isabelle2009-2): diff -r 2e1b6a8a0fdd src/HOL/Parity.thy --- a/src/HOL/Parity.thyWed Jul 28 06:38:17 2010 +1000 +++ b/src/HOL/Parity.thyMon Aug 23 17:33:59 2010 +1000 @@ -66,9 +66,10 @@ by presburger lemma even_times_anything: even (x::int) == even (x * y) - by algebra + by (simp add: int_even_iff_2_dvd) -lemma anything_times_even: even (y::int) == even (x * y) by algebra +lemma anything_times_even: even (y::int) == even (x * y) + by (simp add: int_even_iff_2_dvd) lemma odd_times_odd: odd (x::int) == odd y == odd (x * y) by (simp add: even_def zmod_zmult1_eq) ?!? Why is the behaviour of the algebra method changed? diff -r 2e1b6a8a0fdd src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Wed Jul 28 06:38:17 2010 +1000 +++ b/src/Provers/hypsubst.ML Mon Aug 23 17:33:59 2010 +1000 +(* Counts the occurences of Free and Bound variables in a term. *) +fun count_vars' _ (Free f) = Termtab.map_default (Free f, 0) (fn x = x + 1) + | count_vars' _ (Var _) = I + | count_vars' _ (Const _) = I + | count_vars' n (Bound m) = Termtab.map_default (Bound (m - n), 0) + (fn x = x + 1) + | count_vars' n (Abs (_, _, t)) = count_vars' (n + 1) t + | count_vars' n (f $ x) = count_vars' n f o count_vars' n x + +fun count_vars ts = fold (count_vars' 0) ts Termtab.empty This is very strange, since it counts the bound variables in (%f. f) (%x. x) as the same variable. It doesn't seem to produce a problem now, since the variables in a hypothesis are goal parameters, which are nested linearly, but it is confusing nevertheless. + +(* An equality hypothesis 'x = y' is trivial if substituting with it would have + no useful effect. The principal test for this is if x or y is a unique + variable, occuring nowhere else in the goal. The exception to the rule is + if x is bound and y is unique but free. *) What is a useful effect? This is not a rhetorical question -- I really don't understand. Is the second sentence the actual definition? A more general remark: Larry's comments in hypsubst.ML: (*If novars then we forbid Vars in the equality. If bnd then we only look for Bound variables to eliminate. When can we safely delete the equality? Not if it equates two constants; consider 0=1. Not if it resembles x=t[x], since substitution does not eliminate x. Not if it resembles ?x=0; consider ?x=0 == ?x=1 or even ?x=0 == P Not if it involves a variable free in the premises, but we can't check for this -- hence bnd and bound_hyp_subst_tac The last point really indicates the main problem: the premises are actually facts in the surrounding context. In other words, it is almost never safe to eliminate Frees, unless we know for some reason that all relevant facts have already been inserted in the goal... So it seems the only really conservative step is to eliminate bound variables only??? How many proofs would have to be fixed if safe methods were restricted to this? I gues it's a lot more, but it may still be better than trading one heuristic for a more complex one, which is still unsafe... Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Hello again isabelle-dev. I should clear up some confusion that may have been caused by my mail. I was trying to avoid repeating all that had been said on this issue, and it seems I left out some that hadn't been said as well. This approach avoids ever deleting an equality on a Free variable during a 'safe' reasoning step. It will substitute with that equality but keep it in place. This is a significant change to the intermediate state of some tactic scripts, thus the incompatibilities, especially on induction. It is somewhat surprising there aren't more such incompatibilities. There's no truly safe way to delete an equality on a Free variable without inspecting the whole context. Since equalities are not deleted, care must be taken to avoid an infinite loop in which a substitution is repeatedly attempted. This is the reason for the uniqueness check - if x appears only in 'x = expr' then there is no more substitution to be done. Some subtleties were discovered experimentally: - 'x = y' should not be substituted if either x or y is unique, or else we enter a loop substituting x - y - x - 'expr = x' needs to be reoriented when it is substituted, or else hypsubst and simp will loop doing opposite substitutions. - 'x = y' is OK to substitute if y is a unique free and x is a non-unique Bound. This is what is meant by a 'useful' substitution in the comment. Other equalities, which would cause a no-effect or cyclic substitution, are referred to as trivial (abbreviated triv) in this code. The language should probably be cleanup up to use a consistent set of names. Let me address Alex's detailed comments: 1. In the HOL sources the algebra method is used to solve two problems about parity essentially by accident. No Groebner bases were involved, but the surrouding logic, which appeals to clarify_tac and a custom simpset, happened to solve the goal. With this change the simplified goal had an extra quantifier in it. Note that with this change terminal tactics operating in 'unsafe' mode - fast, best, etc - will call thin_triv_tac via Context_Rules and behave similarly to before. It is terminal tactics which take safe steps - like algebra - that are most likely to break. 2. Yes, count vars is a bit strange, as it will consider (%f. f) (%x. x) to contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp, which it gets right. Yours, Thomas. From: Alexander Krauss [kra...@in.tum.de] Sent: Monday, August 23, 2010 7:35 PM To: Thomas Sewell Cc: Isabelle Developers Mailing List Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution Hi Thomas, Thanks for digging into this. The concrete patch is exactly what was needed to advance this discussion. Here are a few comments. I am sure others will have more... I attach the resulting patch. After several rounds of bugfixes and compatibility improvements, it requires 23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word. So it is painful (as there are a much more theories out there), but it may work, and it may be worth the trouble in the long run. The code change in Provers/hypsubst.ML adds code for counting the free and bound variables in a goal, and checking whether either side of an equality hypothesis is a unique variable, occuring nowhere else. The main substitution algorithms avoid using such equalities and also preserve rather than delete the hypothesis they select. Do I understand correctly that substituting the hypothesis is safe, but discarding them afterwards is unsafe? Then, why should they not be used? More importantly, why is it safe to use and discard an equality when the variable occurs elsewhere in the goal? The equality itself could interact with a fact from the context? Consider the contrived example locale l = fixes x :: nat assumes neq: x ~= 0 begin lemma x = 0 == x = x + 1 == False apply safe After safe, the lemma becomes unprovable, since the hypothesis that contradicts the context is removed. It seems that your patch does not fix this... (I haven't tried... just guessing from reading the code) [...] A few concrete remarks concerning the patch (which seems to be relative to Isabelle2009-2): diff -r 2e1b6a8a0fdd src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Jul 28 06:38:17 2010 +1000 +++ b/src/HOL/Parity.thy Mon Aug 23 17:33:59 2010 +1000 @@ -66,9 +66,10 @@ by presburger lemma even_times_anything: even (x::int) == even (x * y) - by algebra + by (simp add: int_even_iff_2_dvd) -lemma anything_times_even: even (y::int) == even (x * y) by algebra +lemma anything_times_even: even (y::int) == even (x * y) + by (simp add: int_even_iff_2_dvd) lemma odd_times_odd: odd (x::int) == odd y == odd (x * y) by (simp add: even_def zmod_zmult1_eq) ?!? Why is the behaviour of the algebra method changed? diff -r 2e1b6a8a0fdd src/Provers
