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
