CODEWITHSUNDEEP
isabelleml
Michael
Michael

Reputation: 216

Access functions from an imported theory in Isabelle/ML

I have an Isabelle theory here:

theory Even imports Main begin

notation Suc ("S")

fun even:: "nat ⇒ bool" where
  "even 0 = True" |
  "even (S n) = (¬even n)"

fun odd:: "nat ⇒ bool" where
 "odd 0 = False" |
 "odd (S n) = (¬odd n)"

theorem "even (S (S n)) = even n"
  by (induction n, simp_all)

theorem "even n ≠ odd n"
  by (induction n, simp_all)
  
end

And a ML file attempting to use functions defined in the theory mode:

use_thy "Even";

fun isEven x =
  if Even.even x then "even" else "odd";

val _ = writeln(isEven 5)

However, when I execute the ML file in Isabelle batch mode, I get the following output (and error):

$ isabelle process -f "EvenCall.ML"
Loading theory "Draft.Even"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
### theory "Draft.Even"
### 0.109s elapsed time, 0.109s cpu time, 0.000s GC time
val it = (): unit
EvenCall.ML:4: error: Structure (Even) has not been declared
Found near if Even.even x then "even" else "odd"
Error trying to use the file: 'EvenCall.ML'

How should I correct this error so the ML file recognizes functions from the theory it uses? Or is there a different way to access the function through the command line?

Upvotes: 0

Views: 45

Answers (0)

Related Questions