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 :: "real ⇒ 'a::real_algebra_1”
looks easy to define.
Larry
> On 29 Jul 2015, at 15:24, Johannes Hölzl <hoe...@in.tum.de> wrote:
>
> I'm fine with it. The only problem maight be that
> real :: "ereal => real"
> is overloaded in Extended_Real, which is quite often used in Probability
> theory. I can rename it to "of_ereal".
>
> - Johannes
>
> Am Mittwoch, den 29.07.2015, 15:02 +0100 schrieb Larry Paulson:
>> 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 unusual to find both types of coercions in a single
>> formula, and to make matters worse, their behaviour under
>> simplification isn’t identical. But how can we fix this without
>> breaking thousands of proofs?
>>
>> I have a suggestion based on the assumption that real :: int=>real is
>> almost never used. (I have previously removed overloading from other
>> functions, and found essentially no uses of the integer version.) If
>> this assumption is correct, we should be able to define real ::
>> nat=>real as an abbreviation for of_nat, so that the two functions are
>> synonymous. Then we could eliminate the existing abbreviation
>> real_of_nat. This should win all around: we keep the name “real”,
>> which is more readable than “of_nat”, and get rid of the overloading.
>> The effect on existing proofs should be modest, especially if we
>> change things to ensure that of_nat is simplified exactly as real is
>> now.
>>
>> Obviously, the biggest obstacle is likely to be occurrences of real ::
>> int=>real. Any explicit occurrences will immediately be flagged, and
>> can be replaced by of_int.
>>
>> Views?
>>
>> Larry
>>
>>> On 3 Jun 2015, at 12:23, Larry Paulson <l...@cam.ac.uk> wrote:
>>>
>>> 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 :: real \<Rightarrow> 'a::real_algebra_1
>>>
>>> With these functions, we can express practically all numeric conversions,
>>> and they are based on algebraic principles. There is no need to introduce
>>> quadratically many other functions for each possible combination of source
>>> and target type. And yet we seem to done that. 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 \<equiv> of_rat"
>>>
>>> abbreviation complex_of_real :: "real \<Rightarrow> complex"
>>> where "complex_of_real \<equiv> of_real"
>>>
>>> And then why use overloading so that “real” redirects to one of those,
>>> which in turn abbreviates one of the original four functions? Note that
>>> "real x = of_nat x” is not an instance of reflexivity, but must be proved
>>> using the definition real_of_nat_def. This definition is used 88 times in
>>> our HOL development, and it’s also my direct experience of having two
>>> different but equivalent coercions complicates proofs.
>>>
>>> We currently set up automatic coercions in Real.thy as follows:
>>>
>>> declare [[coercion "of_nat :: nat \<Rightarrow> int"]]
>>> declare [[coercion "real :: nat \<Rightarrow> real"]]
>>> declare [[coercion "real :: int \<Rightarrow> real”]
>>>
>>> And then in Complex.thy as follows:
>>>
>>> declare [[coercion "of_real :: real \<Rightarrow> complex"]]
>>> declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
>>> declare [[coercion "of_int :: int \<Rightarrow> complex"]]
>>> declare [[coercion "of_nat :: nat \<Rightarrow> complex”]]
>>>
>>> This latter version is the correct one, using just the primitive coercions.
>>>
>>> I think that we should phase out all the derivative coercions in favour of
>>> the primitive ones. I know that our complicated system arose by accident,
>>> but it would not be that difficult to fix things.
>>>
>>> Larry
>>>
>>>> On 3 Jun 2015, at 09:55, Fabian Immler <imm...@in.tum.de> wrote:
>>>>
>>>> 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 think about less obstructive
>>>> abbreviations like e.g., "real_N" and "real_Z", or "real⇩N" and "real⇩Z".
>>>> But I see that "real_of_foo" is much more uniform and you can immediately
>>>> read off the type "foo".
>>>>
>>>> Fabian
>>>
>>
>> _______________________________________________
>> 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
