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