[isabelle] thm commands




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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.