Email Gateway (Aug 18 2022 at 10:16): Email Gateway (Aug 18 2022 at 10:16):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
I'm tying to convert an ML file of proofs to Isar,
and I come across the following:
thm zmod_uminus ;
thm zmod_zsub_left_eq ;
thm zmod_zsub_right_eq ;
thm zmod_zadd_left_eq ;
thm zmod_zadd_right_eq ;
thm zmod_zmult1_eq ;
thm zmod_zmult1_eq_rev ;
- (?a mod ?b) mod ?b = - ?a mod ?b
(?a - ?b) mod ?c = (?a mod ?c - ?b) mod ?c
(?a - ?b) mod ?c = (?a - ?b mod ?c) mod ?c
(?a + ?b) mod ?c = (?a mod ?c + ?b) mod ?c
(?a + ?b) mod ?c = (?a + ?b mod ?c) mod ?c
?a * ?b mod ?c = ?a * (?b mod ?c) mod ?c
?b * ?a mod ?c = ?b mod ?c * ?a mod ?c(and other uses of these theorems in Isar seem to work OK)
Now,
ML {*
val zmod_uminus = thm "zmod_uminus" ;
val zmod_zsub_left_eq = thm "zmod_zsub_left_eq" ;
val zmod_zsub_right_eq = thm "zmod_zsub_right_eq" ;
val zmod_zadd_left_eq = thm "zmod_zadd_left_eq" ;
val zmod_zadd_right_eq = thm "zmod_zadd_right_eq " ;
val zmod_zmult1_eq = thm "zmod_zmult1_eq" ;
val zmod_zmult1_eq_rev = thm "zmod_zmult1_eq_rev" ;
*}
*** Error in ML
*** val zmod_uminus = "- (?a mod ?b) mod ?b = - ?a mod ?b" : Thm.thm
*** val zmod_zsub_left_eq = "(?a - ?b) mod ?c = (?a mod ?c - ?b) mod ?c"
*** : Thm.thm
*** val zmod_zsub_right_eq = "(?a - ?b) mod ?c = (?a - ?b mod ?c) mod ?c"
*** : Thm.thm
*** val zmod_zadd_left_eq = "(?a + ?b) mod ?c = (?a mod ?c + ?b) mod ?c"
*** : Thm.thm
*** Exception- ERROR "Unknown theorem(s) \"zmod_zadd_right_eq \"" raised
*** Unknown theorem(s) "zmod_zadd_right_eq "
*** Error.
*** At command "ML" (line 754 of stdin).
ie for some reason one of the theorems is unknown to the ML command thm
Does anyone have any ideas on why this could be?
Jeremy
Email Gateway (Aug 18 2022 at 10:16):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Don't anyone bother looking at the previous query, it was a simple typo
(in fact, a space, which was why it wasn't immediately obvious)
Jeremy
Last updated: May 03 2024 at 04:19 UTC