Re: [isabelle] typecheck a term



Sean McLaughlin wrote:
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


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






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