Roland Coghetto (Jun 04 2025 at 12:15): Roland Coghetto (Jun 04 2025 at 12:15):When I define a data type and an associated function I get an unexpected error: Equation is redundant (covered by preceding clauses)
Isabelle does not accept my index_val function.
Equation is redundant (covered by preceding clauses):
index_val ni_112_62 = 11262 / 10⇧2
I really can't find the reason for this error: I have many different cases in the definition of my index_val function.
I rewrote the code with a simpler (naming) example, and this code is accepted.
I've indicated it in the datatype my_data and func my_conversion below, for the example.
Help is welcome because I would like to keep the ai_102_00 notation as much as possible.
The complete code:
theory Scratch
imports HOL.Rat
begindatatype coefficient_index =
ai_102_00 | ai_104_04 | ai_160_84 | ai_164_06 | ai_167_34 |
ai_170_69 | ai_174_10 | ai_177_58 | ai_181_14 | ai_184_76 |
ai_188_45 | ai_192_22 | ai_196_07 | ai_199_99 | ai_203_99 |
ai_208_07 | ai_212_23 | ni_100_00 | ni_102_00 | ni_104_04 |
ni_106_12 | ni_108_24 | ni_110_41 | ni_112_62 | ni_114_87 |
ni_117_17 | ni_119_51 | ni_121_90 | ni_124_34fun index_val :: "coefficient_index⇒rat" where
"index_val ai_102_00 = 102.00"
|"index_val ai_104_04 = 104.04"
|"index_val ai_160_84 = 160.84"
|"index_val ai_164_06 = 164.06"
|"index_val ai_167_34 = 167.34"
|"index_val ai_170_69 = 170.69"
|"index_val ai_174_10 = 174.10"
|"index_val ai_177_58 = 177.58"
|"index_val ai_181_14 = 181.14"
|"index_val ai_184_76 = 184.76"
|"index_val ai_188_45 = 188.45"
|"index_val ai_192_22 = 192.22"
|"index_val ai_196_07 = 196.07"
|"index_val ai_199_99 = 199.99"
|"index_val ai_203_99 = 203.99"
|"index_val ai_208_07 = 208.07"
|"index_val ai_212_23 = 212.23"
|"index_val ni_100_00 = 100.00"
|"index_val ni_102_00 = 102.00"
|"index_val ni_104_04 = 104.04"
|"index_val ni_106_12 = 106.12"
|"index_val ni_108_24 = 108.24"
|"index_val ni_110_42 = 110.42"
|"index_val ni_112_62 = 112.62"
|"index_val ni_114_87 = 114.87"
|"index_val ni_117_17 = 117.17"
|"index_val ni_119_51 = 119.51"
|"index_val ni_121_90 = 121.90"
|"index_val ni_124_34 = 124.34"value "index_val ai_212_23"
value "index_val ni_112_62"
ML ‹
real(5521) / real(50);
›datatype my_data =
d1|d2|d3|d4|d5|d6|d7|d8|d9|d10|
d11|d12|d13|d14|d15|d16|d17|d18|d19|d20|
d21|d22|d23|d24|d25|d26|d27|d28|d29|d30fun my_conversion :: "my_data ⇒ nat" where
"my_conversion d1 = 1"
|"my_conversion d2 = 2"
|"my_conversion d3 = 3"
|"my_conversion d4 = 4"
|"my_conversion d5 = 5"
|"my_conversion d6 = 6"
|"my_conversion d7 = 7"
|"my_conversion d8 = 8"
|"my_conversion d9 = 9"
|"my_conversion d10 = 10"
|"my_conversion d11 = 1"
|"my_conversion d12 = 2"
|"my_conversion d13 = 3"
|"my_conversion d14 = 4"
|"my_conversion d15 = 5"
|"my_conversion d16 = 6"
|"my_conversion d17 = 7"
|"my_conversion d18 = 8"
|"my_conversion d19 = 9"
|"my_conversion d20 = 10"
|"my_conversion d21 = 2"
|"my_conversion d22 = 2"
|"my_conversion d23 = 3"
|"my_conversion d24 = 4"
|"my_conversion d25 = 5"
|"my_conversion d26 = 6"
|"my_conversion d27 = 7"
|"my_conversion d28 = 8"
|"my_conversion d29 = 9"
|"my_conversion d30 = 10"value "my_conversion d25"
fun my_conversion2 :: "my_data ⇒ rat" where
"my_conversion2 d1 = 1.0"
|"my_conversion2 d2 = 2.0"
|"my_conversion2 d3 = 3.0"
|"my_conversion2 d4 = 4.0"
|"my_conversion2 d5 = 5.0"
|"my_conversion2 d6 = 6.0"
|"my_conversion2 d7 = 7.0"
|"my_conversion2 d8 = 8.0"
|"my_conversion2 d9 = 9.0"
|"my_conversion2 d10 = 10.0"
|"my_conversion2 d11 = 1.0"
|"my_conversion2 d12 = 2.0"
|"my_conversion2 d13 = 3.0"
|"my_conversion2 d14 = 4.0"
|"my_conversion2 d15 = 5.0"
|"my_conversion2 d16 = 6.0"
|"my_conversion2 d17 = 7.0"
|"my_conversion2 d18 = 8.0"
|"my_conversion2 d19 = 9.0"
|"my_conversion2 d20 = 10.0"
|"my_conversion2 d21 = 2.0"
|"my_conversion2 d22 = 2.0"
|"my_conversion2 d23 = 3.0"
|"my_conversion2 d24 = 4.0"
|"my_conversion2 d25 = 5.0"
|"my_conversion2 d26 = 6.0"
|"my_conversion2 d27 = 7.0"
|"my_conversion2 d28 = 8.0"
|"my_conversion2 d29 = 9.0"
|"my_conversion2 d30 = 10.0"value "my_conversion2 d25"
end
terru (Jun 04 2025 at 12:21):you have an equation "index_val ni_110_42 = 110.42" but there's no constructor ni_110_42 (probably this is a typo for ni_110_41?)
Since it's not a constant, it's regarded as a variable binding (this is indicated by having the name be a different colour in jedit), so this equation covers all cases & everything subsequent is regarded as redundant.
Roland Coghetto (Jun 04 2025 at 12:41):Thank you! That's exactly it.
Last updated: Jun 21 2025 at 01:46 UTC