A conclusion of what I have understood so far:
* A new »of_float :: float = 'a::field« is provided (btw. »float« could
be also constructed from the rationals rather than the reals).
* »real« is restricted to »real :: nat = real« (which corresponds
nicely to »int :: nat = int«).
* The special case
Currently we have
definition
of_real :: real ⇒ 'a::real_algebra_1 where
of_real r = scaleR r 1
Maybe of_real could be done another way.
And floats could be injected into the rationals.
Larry
On 29 Jul 2015, at 16:34, Johannes Hölzl hoe...@in.tum.de wrote:
Ah, I forgot about real of
Ah, I forgot about real of float.
I assume you meant:
of_float :: float = 'a::field
- Johannes
Am Mittwoch, den 29.07.2015, 16:07 +0100 schrieb Larry Paulson:
This is an unusual case, because this function is not even injective. I would
prefer to reserve of_XXX for generic functions,
This is an unusual case, because this function is not even injective. I would
prefer to reserve of_XXX for generic functions, like the existing ones.
I now see that there is another case:
real :: float = real
This one is injective, and a properly generic function
of_float ::
In recent work, I’ve seen again how tricky things are with coercions. We need
“real” because it is already used in thousands of places and in many basic
lemmas, but it can only do nat=real and int=real. If we are working more
abstractly, only of_nat and of_int are general enough. It isn’t
The first question is, do we need a prefix syntax for type constraints? My
point was that the ability to write
[:real:]of_nat k
might be better than having to introduce and abbreviations such as real_of_nat,
but this is not clear. The latter has the advantage that it is automatically
On 24/06/15 15:55, Larry Paulson wrote:
A more appropriate point is that it can be tricky in Isabelle/jEdit to
determine the type of an expression such as “of_nat k”, as there is nothing to
click on.
When I type ‘term sqrt (of_nat 2)’ and hover over the ‘of_nat’, it
says ‘constant
I guess what Larry means is there is no way to see a type of a constant
that is not there in the source.
Consider e.g.
declare [[coercion of_nat :: nat ⇒ real]]
term sqrt (2 :: nat)
Today the output says sqrt (real_of_nat 2). But if there would be no
abbreviation for of_nat :: nat ⇒ real,
You can hover in the output panel, but you won't see types of constants
there.
Dmitriy
On 24.06.2015 16:09, Manuel Eberl wrote:
Ah, I see the problem. In that case, one could still hover over the
of_nat in the output window, but it is perhaps not ideal.
On 24/06/15 16:08, Dmitriy Traytel
Ah, I see the problem. In that case, one could still hover over the
of_nat in the output window, but it is perhaps not ideal.
On 24/06/15 16:08, Dmitriy Traytel wrote:
I guess what Larry means is there is no way to see a type of a
constant that is not there in the source.
Consider e.g.
On 24.06.2015 16:29, Larry Paulson wrote:
This may be the problem. I don’t remember exactly what I was trying to do,
only that it was very difficult. Of course nobody uses show_types any more.
At least this was the problem for me. A notorious instance of the same
problem are the functions in
On Sat, 6 Jun 2015, Florian Haftmann wrote:
Conceivably we could introduce a prefix syntax for type constraints, e.g.
[:real:]of_nat k
I’d find such a thing useful from time to time.
My personal favourite would be System-F-style type instantiation
of_nat [real] k
instead
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:
Conceivably we could introduce a prefix syntax for type constraints, e.g.
[:real:]of_nat k
I’d find such a thing useful from time to time.
My personal favourite would be System-F-style type instantiation
of_nat [real] k
instead of type annotations but there are hardly any
My proposal of [: :] is suggestive of typing and should be good enough,
considering that such “type casts” would seldom be necessary.
Larry
On 6 Jun 2015, at 16:06, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Conceivably we could introduce a prefix syntax for type
Why do we need abbreviations such as these?
abbreviation real_of_nat :: nat \Rightarrow real”
where real_of_nat \equiv of_nat
abbreviation real_of_int :: int \Rightarrow real”
where real_of_int \equiv of_int
abbreviation real_of_rat :: rat \Rightarrow real”
where real_of_rat
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
Maybe we should resurrect the idea of using adhoc overloading for the
real abbreviation.
The idea in itself is not bad, but I am reluctant to pull ad-hoc
overloading into the HOL theories itself. There are still too many
dragons sitting in the dark.
Florian, does your rework of the generic
On 5 Jun 2015, at 22:22, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Why do we need abbreviations such as these?
abbreviation real_of_nat :: nat \Rightarrow real”
where real_of_nat \equiv of_nat
abbreviation real_of_int :: int \Rightarrow real”
where
Maybe we should resurrect the idea of using adhoc overloading for the
real abbreviation.
Florian, does your rework of the generic machinery for syntactic
abbreviations include moving more of the adhoc overloading into HOL?
Then we could setup real as an adhoc overloaded constant and the proof
The situation regarding coercions has become extremely untidy, and I think it
should be cleared up. We have four generic functions:
of_nat :: nat \Rightarrow ‘a::semiring_1
of_int :: int \Rightarrow ‘a::ring_1
of_rat :: rat \Rightarrow ‘a:: field_char_0
of_real ::
I think I could live without real: coercions save a lot of the writing.
Moreover, the real_of_foo abbreviations help to avoid type annotations:
I suppose that all of the current occurrences of real could be replaced with
one particular real_of_foo.
For reading (subgoals etc), one could perhaps
For me the main point of real is the ease of writing. If we get rid of some
lemma duplications but trade that in for many type annotations, I am not in favour.
Tobias
On 02/06/2015 20:18, Florian Haftmann wrote:
Dear all,
recently, I stumbled (once again) over the matter of the »real«
Thank you for reminding me of the reading part. My ability to read formulas
decreases quadratically with their length. Trading in real_of_int for real
makes things definitely worse.
I would want to see a concrete figures how much duplication is avoided in the
current theories and how much
Agree. And now real (fact k)” must never be used, now that “fact” is also
generic.
This reminds me of a current IDE limitation: there’s currently no way (as far
as I know) to get the type of a nonvariable expression, such as fact k” above.
Larry Paulson
On 2 Jun 2015, at 19:18, Florian
25 matches
Mail list logo
