Re: [isabelle-dev] Remaining uses of defer_recdef?
I've had a quick scan over the NICTA repositories. It doesn't look like there are any live original uses of recdef. There are recdefs in a copy of Simpl-AFP, and in some backups of historical papers. Short summary, NICTA doesn't have any stakes in recdef. Cheers, Thomas. On 08/06/15 06:13, Makarius wrote: On Sat, 6 Jun 2015, Gerwin Klein wrote: On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote: (2) 'defer_recdef' which is unused in the directly visible Isabelle universe. So it could be deleted today. This mailing list thread is an opportunity to point out dark matter in the Isabelle universe, where 'defer_recdef' still occurs. Otherwise I will remove it soon, lets say within 1-2 weeks. Unused in our part of the dark matter universe as well. The thread has shifted over to actual 'recdef'. Are there remaining uses of 'recdef' in the NICTA dark matter? So far I always thought the remaining uses in HOL-Decision_Procs are only a reminder that there are other important applications. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 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
Re: [isabelle-dev] Remaining uses of defer_recdef?
On 06/06/15 17:11, Florian Haftmann wrote: So are there any experience reports that the combinatorial explosion in pattern matching in fun/function had to be worked around somehow? Or do we have to conclude that the pattern complexity of the applications in src/HOL/Decision_Procs is indeed domain-specific? I regularly have to work around this explosion problem. One example is in JinjaThreads/Common/BinOp.thy where I was not able to define the function binop as a whole, but I had to split it up into several definitions - fortunately, there was no recursion involved, so this was possible. There must also be a mailing list thread between Alexander Krauss and me on this topic, but I was not able to unearth it. I have run into the same problem (with similar workarounds) a number of times. In case of a recursive function, I nowadays write f x y z = (case x of ... = (case y of ... = | _ = ...) | _ = ...) and let simps_of_case split the equations by the pattern. In big cases, simps_of_case runs for a minute or two, but there is no hope to get these definitions through with the function. Of course, this does not work with overlapping patterns, but I rarely use them anyway. The main drawback here is that I do not get a suitable cases rule for the function definitions and the proofs accordingly look ugly (especially if I have nested patterns, i.e., nested case distinctions and lots of rename_tac+case_tac). Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
A frequent use case is this: you have 5-10 interesting patterns where stuff happens and an otherwise pattern with a simple rhs. In that case you do want to write those 5-10 patterns explicitly and let the definition facility take care of the hundreds of patterns that the default case expands to. You don't really care that the induction has hundreds of cases because they are trivial. In contrast, rewriting such a definition to avoid the blowup is a pain in the backside and is not guaranteed to make proofs simpler. Tobias On 07/06/2015 21:46, Larry Paulson wrote: I suggest looking for ways for users to avoid exponential blowup. Presumably this means avoiding deeply nested patterns in favour of conditional expressions in some cases. Such a formalisation might be easier to reason with too, who wants an induction rule with hundreds of cases? But coming up with simple guidelines for users might be tricky. Larry On 7 Jun 2015, at 20:33, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: As far as I know, this is due to layered architecture of the function package. »recdef« does everything in one bunch and can hence optimize for sequential pattern matching. Each layer of »function« must feed its result to its successor in a standardized form, and since there is no overall concept of sequential pattern matching, it has to be compiled away once and for all from the very beginning. (roughly spoken) An optimization would require a modified architecture. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
The syntax is nice, but I would interpret _⇩ℕ not as of_nat but as into nat, or more specifically I would read: _⇩ℝ == real _. - Johannes Am Freitag, den 05.06.2015, 23:58 +0200 schrieb Florian Haftmann: Hi again, after I first iteration of discussion I see a list of three requirements: 1. Conversions can be written succinctly. 2. Conversions are printed succinctly. 3. Conversions are unique, there are no accidental equivalences which require explicit conversions. Concerning (1), my guess indeed is the implicit conversions should do the job. There is the borderline case with required explicit type annotations (»of_nat n :: rat«) which is currently handled by distinct abbreviations, but these could be dropped. (2) is not so trivial if you want to make sure that the printed terms are compact but still complete in the sense that they are invariant under copy-and-paste. I think of_nat/of_int/of_rat is fine, but real_of_int etc. is definitely not. Anyway, like in (1) these abbreviations might be entirely superfluous. The disadvantage of the algebraic conversions is that the do not tell what the result type is -- which is usually the more important information, since the argument type's is usually easily inferred. Maybe suitable symbol syntax can help here. Below I made some experiments how fancy symbol syntax could look like, but I am still lacking a conclusive idea. (3) Everything has been said about this already. So, I would suggest we spend thoughts how *printing* of of_foo-Conversions can be improved with reasonable means (2). We are still at the beginngin… Cheers, Florian notation of_nat (_⇩ℕ [999]) notation of_int (_⇩ℤ [999]) notation of_rat (_⇩ℚ [999]) term rep_real (of_nat (Suc n) + of_int (k div l)) thm of_nat_diff notation real_of_nat (of'_nat⇩ℝ) notation real_of_int (of'_int⇩ℝ) notation real_of_rat (of'_int⇩ℚ) term rep_real (of_nat (Suc n) + of_int (k div l)) thm of_nat_diff notation of_nat (of'_ℕ) notation of_int (of'_ℤ) notation of_rat (of'_ℚ) term rep_real (of_nat (Suc n) + of_int (k div l)) thm of_nat_diff notation real_of_nat (ℝ'_of'_ℕ) notation real_of_int (ℝ'_of'_ℤ) notation real_of_rat (ℝ'_of'_ℚ) ___ 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
