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, 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
