Re: [isabelle-dev] NEWS: cases from goals
On Tue, 30 Jun 2015, Lars Noschinski wrote: Moreover note, that the above example provides a solution to the occasional problem of ?thesis1, ?thesis2, etc. -- which are not provided by the system. It just becomes ?case in each case. I'd say this is a partial solution: When I have a situation where I need ?thesis1, ?thesis2, etc. then the goals are often very similar to solve and my proof concludes with ... show ?thesis1 ?thesis These are just implicit auto bindings. In specific situations it is always possible to use explicit is patterns. I wonder though, why the goals method is better then the implicit goal1, goal2, ... cases? Doesn't it lead to more instances of proof (initial_method, goals) -- which I thought is a style you discouraged? The whole use of goal cases is not really best-style Isar. The new proof method is just a way to re-integrate things that have accumulated over the years, such they fit formally better into the framework. The main advantages I see at the moment: * Explicit is better than implicit, i.e. the goals method says that goal cases should be produced (maybe it should be actually called goal_cases!?). The default case names are shorter: 1, 2, 3 instead of goal1, goal2, goal3. It is also possible to specify case names in the method invocation. * Cases don't expose hidden goal parameters by default, according to the way how cases methods work. This means the case invocation needs to provide parameter names as desired. There are presently two main applications where goal cases are really needed in regular Isar proofs: intro_classes and intro_locales. Since these proof methods are a bit too complex to provide properly named cases (although it is possible in theory), post-hoc addition of goals is the way to do it. For example: instance proof (standard, goals) case 1 then show ?case sorry next case 2 then show ?case sorry next case 3 then show ?case sorry qed Now we are also back to the motivating situation to rename default into standard. Note that the default method was originally not meant to be written explicitly in the text at all. If there are significantly better ideas for the above, I am intersted to hear them. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: cases from goals
Here is an updated NEWS entry from Isabelle/0eb41780449b -- no changes, just more explanations: * Proof method goals turns the current subgoals into cases within the context; the conclusion is bound to variable ?case in each case. For example: lemma ⋀x. A x ⟹ B x ⟹ C x and ⋀y z. U y ⟹ V u ⟹ W y z proof goals case prems: 1 then show ?case using prems sorry next case prems: 2 then show ?case using prems sorry qed * The undocumented feature of implicit cases goal1, goal2, goal3, etc. is marked as legacy, and will be removed eventually. The proof method goals achieves a similar effect within regular Isar; often it can be done more adequately by other means (e.g. 'consider'). Above I am using a new idiom, to name prems uniformly in each case. This helps to avoid specific names like 1, 2 etc. intrude the proof body. Thus cases may be re-arranged later, without changing all the proof cases. Moreover note, that the above example provides a solution to the occasional problem of ?thesis1, ?thesis2, etc. -- which are not provided by the system. It just becomes ?case in each case. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: cases from goals
On Fri, 26 Jun 2015, Larry Paulson wrote: Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a while. AFP probably has a few thousand. I did not even check before sorting out this old problem from more than 10 years ago. It could have been addressed earlier, then there would have been less work to eliminate it now. Generally, there are more things that can be improved on Isar proofs, using the new facilities like 'consider' and 'have' / 'show' with eigen-context. Quite often, the elimination of awkward goal42(17) proofs actually uses that instead of falling back on the new goals method. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: cases from goals
Multivariate_Analysis/Integration.thy uses goal1 206 times, so this will take a while. Larry On 26 Jun 2015, at 23:46, Makarius makar...@sketis.net wrote: * Proof method goals turns the current subgoals into cases within the context; the conclusion is bound to variable ?case in each case. * The undocumented feature of implicit cases goal1, goal2, goal3, etc. is marked as legacy, and will be removed eventually. Note that proof method goals achieves a similar effect within regular Isar. This refers to c708dafe2220 and d2fbc021a44d. Example updates of oldd proofs are can be seen in changeset 7e741e22d7fc. Makarius ___ 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
