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 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] »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
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 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
