Email Gateway (Aug 23 2022 at 08:56): Email Gateway (Aug 23 2022 at 08:56):From: Peter Lammich <lammich@in.tum.de>
Hi,
the theory Word_Lemmas in AFP/Word_Lib depends on Complex_Main.
However, the only actually dependencies in this theory are three points
where an coercion nat=>int is added implicitly.
Thus, the dependency on Complex_Main, that imports a lot of (possibly
unwanted) machinery can easily be dropped.
Is there any reason for this dependency, or should it actually be
dropped?
Best,
Peter
Find attached a diff/patch:
11,13c11,13
< Complex_Main
< Word_EqI
< Word_Enum
Main
Word_Lib.Word_EqI
Word_Lib.Word_Enum
5753c5753
< "LENGTH('a) \<ge> 3 \<Longrightarrow> sint (of_nat (word_clz (w ::
'a :: len word)) :: 'a sword) \<le> LENGTH('a)"
"LENGTH('a) \<ge> 3 \<Longrightarrow> sint (of_nat (word_clz (w ::
'a :: len word)) :: 'a sword) \<le> int (LENGTH('a))"
5761c5761
< \<Longrightarrow> - sint (of_nat (word_clz (w :: 'a :: len word))
:: 'a signed word) \<le> LENGTH('a)"
\<Longrightarrow> - sint (of_nat (word_clz (w :: 'a :: len word))
:: 'a signed word) \<le> int (LENGTH('a))"
6111c6111
< \<and> sint (of_nat (word_ctz x) :: 'a signed word) \<le>
LENGTH('a)"
\<and> sint (of_nat (word_ctz x) :: 'a signed word) \<le> int
(LENGTH('a))"
Email Gateway (Aug 23 2022 at 08:56):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Yes I’d be very happy to drop it and I don’t remember introducing it either. It seems it was added in a merge commit at some point.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:56):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
ps: I’ll have a look. If it doesn’t influence anything else, I’ll pull it into the 2020 release.
Cheers,
Gerwin
Last updated: Apr 26 2024 at 01:06 UTC