Email Gateway (Aug 22 2022 at 13:59): Email Gateway (Aug 22 2022 at 13:59):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
In the example:
lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def
lemma "dummy (0::nat) (1::nat) (2::nat) (3::nat)"
unfolding numeral_nat
I get the state:
which is what I want - but is there a better way?
The following works for 2 only:
lemma "dummy (0::nat) (1::nat) (2::nat) (3::nat)"
unfolding numerals
Is the fact "Num.numerals" useful at all?
It is used once in HOL/ex/Primrec.thy but it seems that it can be omitted.
Thanks,
Jørgen
Email Gateway (Aug 22 2022 at 13:59):From: Lawrence Paulson <lp15@cam.ac.uk>
It is literally this:
lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)"
by (rule numeral_One) (rule numeral_2_eq_2)
I certainly don’t see the point of making a special case of 1 and 2, especially given that it is almost never used. There are a few uses in the AFP, see below. I’m sure they could all be eliminated easily. I’m not sure who would volunteer to do this.
Larry Paulson
./Applicative_Lifting/Combinators.thy: then show ?thesis by (simp add: numerals)
./Card_Number_Partitions/Card_Number_Partitions.thy: from this show ?thesis by (auto simp add: numerals(2))
./Card_Number_Partitions/Card_Number_Partitions.thy: by (simp add: numerals(2) del: Partition.simps)
./Program-Conflict-Analysis/ConstraintSystems.thy: from S_ENTRY_PAT[of "{#q#}+{#q'#}", simplified] REVSPLIT(1) REVSPLIT'(1) have S_ENTRY: "(v, mon_w fg w, {#q#} + {#q'#}) \<in> S_cs fg (2::nat)" by (simp add: numerals)
./Regular_Algebras/Dioid_Power_Sum.thy:lemmas powsum_simps = powsum_def atLeastAtMostSuc_conv numerals
./Tree_Decomposition/TreewidthTree.thy: lessI less_or_eq_imp_le numerals(2))
./Word_Lib/Word_Lemmas.thy: by (metis numerals(1) power_not_zero power_zero_numeral)
Email Gateway (Aug 22 2022 at 14:06):From: Lars Hupel <hupel@in.tum.de>
It is used once in HOL/ex/Primrec.thy but it seems that it can be omitted.
That one yes, but there's also a non-trivial occurence in HOL, namely in
a tactic in "Semiring_Normalization". While a naive cleanup is possible
(inline the lemma in the tactic), I don't think this is a good idea.
Cheers
Lars
Last updated: Apr 25 2024 at 12:23 UTC