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



Hi,

The problem appears to be with the constructor "Const" which is the same name as the constructor "Const" for internal represaentation of Lambda terms in Isabelle.

Your theory works if you change Const into Cst. Maybe the Code generator should rename such constants before emitting ML Code for evaluation?

Hope it helps,
Amine.

Paolo Giarrusso wrote:
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





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