[isabelle] [BUG?] value not working on an expression resulting in "True"



Hi all, I'm a software developer and a new Isabelle user, practicing with the 
tutorial. I'm using Isabelle 2007.

Note these two lines in the below theory (derived from § 2.5.6 of the 
tutorial, 
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf):

normal_form "val (Const True)"

gives: 

 "True"
  :: "bool"

While
value "val (Const True)"  (* this fails *)
fails (and there are no variables, so there's no reason for this).

Here's the theory:

theory ExBoolexBugReport imports Main begin
datatype boolex = Const bool | Neg boolex | And boolex boolex

consts
  "val" :: "boolex \<Rightarrow> bool"
primrec
"val (Const b) = b"
"val (Neg boolex) = (\<not> (val boolex))"
"val (And b c) = ((val b) \<and> (val c))"

value "True"

normal_form "val (Const True)"
value "val (Const True)" (* this fails *)
value "val (Const (True::bool))"

end

Here's the error I get in the *responses* Emacs buffer.

*** Error: in 'ML', line 11.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
***    $( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))
*** 
*** Error: in 'ML', line 11.
*** Can't unify Term.term with EvalTerm.Generated.boolex
***    (Different type constructors) Found near
***    $( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))
*** 
*** Error: in 'ML', line 14.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
***    $( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))
*** 
*** Error: in 'ML', line 14.
*** Can't unify Term.term with EvalTerm.Generated.boolex
***    (Different type constructors) Found near
***    $( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))
*** 
*** Error: in 'ML', line 19.
*** Can't unify bool with string * Term.typ (Incompatible types) Found near
***    $( $( Const( ...), ...(...)), term_of_boolex(x2))
*** 
*** Error: in 'ML', line 19.
*** Can't unify Term.term with EvalTerm.Generated.boolex
***    (Different type constructors) Found near
***    $( $( Const( ...), ...(...)), term_of_boolex(x2))
*** 
*** At command "value".

If needed: I'm using ProofGeneral-3.7pre071112 and Emacs 22.1 as provided by 
Ubuntu 7.04, in case it makes any difference.

Thanks in advance
-- 
"Doh!" (cit.), I've made another mistake!
Paolo Giarrusso, aka Blaisorblade

Attachment: signature.asc
Description: This is a digitally signed message part.



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