Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)



On Di, 2017-08-15 at 12:14 +0200, Tobias Nipkow wrote:
> I learned about
> 
> lemma [measure_function]: "is_measure f â is_measure g â is_measure
> (size_prod f g)"
> by (rule is_measure.intros)
> 
> from Peter Lammich who probably uses it more often. He may have some
> insight asÂ
> to the dangers of using this by default.

I have not used this very often, too. Only for small isolated examples,
but not in the basis of some big developments.

Nevertheless, I would be curious what would happen if one adds this
lemma by default (e.g. to Main)


--Â
 Peter


> 
> Not that the recursive function need not be tupled for this to help
> becauseÂ
> internally the arguments are tupled anyway.
> 
> It would indeed be nice if this were mention in the "function
> manual". In caseÂ
> somebody feel sufficiently au fait with this feature ...
> 
> Tobias
> 
> On 14/08/2017 18:05, Lars Hupel wrote:
> > 
> > > 
> > > Another question for you and Andreas: what is the substantive
> > > difference in intent between Finite_Map and FinFun? I used
> > > Finite_Map as I needed the BNF setup, but I reached for FinFun
> > > first as I knew it was there. In the fullness of time, could they
> > > perhaps be merged?
> > Here's a mailing list thread on that issue:
> > <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September
> > /msg00015.html>.
> > 
> > > 
> > > And another, but perhaps more directly for the BNF people: Iâve
> > > been tripped up on products uniformly having a constant size a
> > > few times now. Hereâs a quick theorem search:
> > > 
> > > ÂÂÂBasic_BNF_LFPs.prod.size(2): size (?x1.0, ?x2.0) = Suc 0
> > > 
> > > Could it too be made more useful by returning the sum of the
> > > sizes of its arguments?
> > There is such a function: "size_prod". However, you have to tell
> > the
> > function package about it.
> > 
> > > 
> > > (These arose in termination arguments, and the fun package seems
> > > to avoid using size on products. I wonder if such a change would
> > > impact it.)
> > Here's a contrived example:
> > 
> > fun contrived :: "('a list à 'a list) â ('a list à 'a list)" where
> > "contrived (xs, y1 # y2 # ys) = contrived (y1 # xs, ys)" |
> > "contrived (x1 # x2 # xs, ys) = contrived (xs, x1 # ys)" |
> > "contrived _ = ([], [])"
> > 
> > By default, the function package won't be able to derive a
> > termination
> > measure for this. But you can add the following before the
> > definition:
> > 
> > lemma [measure_function]: "is_measure (size_prod size size)"
> > by (rule is_measure.intros)
> > 
> > There's probably a good reason why this doesn't happen by default.
> > (Possibly time complexity of the termination prover.) If this thing
> > keeps happening to you (or you need nesting), try this:
> > 
> > lemma [measure_function]: "is_measure f â is_measure g â is_measure
> > (size_prod f g)"
> > by (rule is_measure.intros)
> > 
> > This might mess up things elsewhere though, so try it at your own
> > risk.
> > 
> > Cheers
> > Lars
> > 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.