Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] typecheck a term

view this post on Zulip Email Gateway (Aug 17 2022 at 13:46):

From: Sean McLaughlin <seanmcl@cmu.edu>
Hi,

I needed to create some Isabelle terms by hand, and would like to
make
sure they typecheck as a sanity check. So, eg.

Const ("==", "bool => bool => bool") $ Free ("a", "bool") $
Free ("b", "prop") : Term.term

Doesn't typecheck. What function do I call?

Thanks,

Sean

view this post on Zulip Email Gateway (Aug 17 2022 at 13:46):

From: Lawrence Paulson <lp15@cam.ac.uk>
One way is to call the function cterm_of, which converts a raw term
to a "certified term". Note that typechecking only makes sense in the
context of a theory. The most basic theory is ProtoPure.thy, which
only knows about the meta-logic connectives. Or HOL.thy (for the
basic HOL types) or Main.thy (for everything).

Larry

view this post on Zulip Email Gateway (Aug 17 2022 at 13:46):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Sean McLaughlin wrote:
If I understand you correctly, you have entered the code

Const ("==", "bool => bool => bool") $ Free ("a", "bool") $

Free ("b", "prop") : Term.term

by hand - is that right?

If so you have the problem that the type which is printed as
"bool => bool => bool" isn't actually a string, to create it you
have to do something like

fun ctyp str = Type (str, []) ;
val charT = ctyp "List.char" ; (* was "Main.char" *)
val nibbleT = ctyp "List.nibble" ; (* was "Main.nibble" *)
val boolT = ctyp "bool" ;
fun listT ty = Type ("List.list", [ty]) ;
fun setT ty = Type ("set", [ty]) ;
fun pairT (t1, t2) = Type ("*", [t1, t2]) ;
fun funT (t1, t2) = Type ("fun", [t1, t2]) ;
fun ifunT [] t2 = t2
| ifunT (t :: ts) t2 = funT (t, ifunT ts t2) ;

ifunT [boolT, boolT] boolT ;
val it = "bool => bool => bool" : Term.typ

Then you can do

val t = Free ("==", ifunT [boolT, boolT] boolT) $ Free ("a", boolT) $
Free ("b", boolT) : Term.term ;

cterm_of (the_context ()) t ;

Is this the sort of thing you wanted to do?

Note that you can't use Const except for an already exsiting Const of
the right type,
and "prop" and "bool" are different types.

Jeremy

Last updated: May 03 2024 at 04:19 UTC