Re: [isabelle] typecheck a term

Sean McLaughlin wrote:

  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?



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.


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