Email Gateway (Aug 22 2022 at 14:24): Email Gateway (Aug 22 2022 at 14:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I think I made some changes to the imports during my overhaul of rings.
It had something to do with pending sort hypotheses. In retrospect, a
more ad-hoc solution may have been the better choice considering these
complaints now.
the restoration of the previous situation is trivial:
diff -r 0da35bf3e6cf src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy Thu Nov 17 16:32:53 2016 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Fri Nov 18 20:56:02 2016 +0100
@@ -9,7 +9,7 @@
section "Bool lists and integers"theory Bool_List_Representation
-imports Complex_Main Bits_Int
+imports Main Bits_Int
begindefinition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -1106,7 +1106,7 @@
apply (case_tac m)
apply simp
apply (case_tac "m <= n")
- apply auto
+ apply (auto simp add: div_add_self2)
donelemma bin_rsplit_len:
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 14:24):From: Peter Lammich <lammich@in.tum.de>
Thanks Florian.
Can you push this please?
@Makarius: Will this make it into Isabelle2016-1?
Email Gateway (Aug 22 2022 at 14:24):From: Makarius <makarius@sketis.net>
A push on isabelle-dev would mean it is for the next release after
Isabelle2016-1. It needs to go to the isabelle-release instead: all
changes need to be sent to me via email. See now
https://bitbucket.org/isabelle_project/isabelle-release/commits/eace715f4988
Here is also the point in history where the slightly odd const name "ii"
was originally introduced, oddly together with the same "ii" as notation:
http://isabelle.in.tum.de/repos/isabelle/rev/10dbf16be15f#l8.17
Here the notation was changed to the current \<i>, without changing the
const name: http://isabelle.in.tum.de/repos/isabelle/rev/67a628beb981#l3.25
Facts are usually just called i_foo_bar instead of ii_foo_bar. So an
obvious reform after the Isabelle2016-1 release is this:
* rename const "ii" to "imaginary_unit" (with existing syntax \<i>);
the const name hardly ever shows up in applications
* standardize all corresponding fact names towards i_foo_bar
In principle, the const could be also called \<i> and the syntax
removed. Morally it would probably mean to rename facts using that
symbolic identifier instead of ASCII.
Moreover, HOL/Nonstandard_Analysis/NSComplex.thy provides another odd
const "iii" for "star_of \<i>". Maybe this could be improved after the
release as well. Much of the "star" notation looks very old and could
benefit from present-day notational facilities.
Makarius
Email Gateway (Aug 22 2022 at 14:24):From: Lawrence Paulson <lp15@cam.ac.uk>
Remark: it is also called ii in HOL Light. A lot of legacy material here.
Larry
Email Gateway (Aug 22 2022 at 14:39):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I realized that by importing Complex_Main, some very short-named
constants like "ii" pop up in the global namespace, and thus are not
available for variable names any more without explicit fixing. This is
very inconvenient. Can't these constants be hidden by default, and only
made visible on demand, eg, as we do for Lattice_Syntax?
Email Gateway (Aug 22 2022 at 14:39):From: Peter Lammich <lammich@in.tum.de>
Hi Johannes,
you are right, having ii as imaginary number is not that strange in
Complex_Main. However, what puzzled me is how it creeped into the
Collections framework, making it omnipresent in many developments
depending on Collections framework directly or indirectly (actually,
many AFP entries). The short answer is:
HOL/Word/Bool_List_Representation now imports Complex_Main: I would
argue that one cannot expect having ii and pi and ... in the namespace
after importing HOL/Word, which is about machine word representation!
So what is the policy to avoid such namespace pollutions? A quick fix
would be adding some hide_const to Bool_List_Representation, but that
would not be very robust ...
Email Gateway (Aug 22 2022 at 14:39):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Hm, "ii" (and \<i>) represent the imaginary number, something one can
expect from a theory called Complex_Main.
But as \<i> is also available I think it is okay to hide "ii".
But is this a problem occurring the first time with Isabelle2016-1-
RC2?
It should be already available in Isabelle2016 (and before).
- Johannes
Email Gateway (Aug 22 2022 at 14:39):From: Manuel Eberl <eberlm@in.tum.de>
I think I made some changes to the imports during my overhaul of rings.
It had something to do with pending sort hypotheses. In retrospect, a
more ad-hoc solution may have been the better choice considering these
complaints now.
I also think that hiding ii is a reasonable solution (as long as it is
still accessible as Complex.ii or similar) but then the question is what
to do about pi or similarly short names like sin, cos, exp, cis.
Manuel
Last updated: Apr 16 2024 at 16:19 UTC