src/Tools/Haskell/Haskell.thy

 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Term (
   Indexname, Sort, Typ(..), Term(..),
   Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
-  type_op0, type_op1, op0, op1, op2, typed_op1, typed_op2, binder,
+  type_op0, type_op1, op0, op1, op2, typed_op0, typed_op1, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
   aconv, list_comb, strip_comb, head_of
 )
 where
 

   where
     mk t u = App (App (Const (name, []), t), u)
     dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
     dest _ = Nothing
 
+typed_op0 :: Name -> (Typ -> Term, Term -> Maybe Typ)
+typed_op0 name = (mk, dest)
+  where
+    mk ty = Const (name, [ty])
+    dest (Const (c, [ty])) | c == name = Just ty
+    dest _ = Nothing
+
 typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
 typed_op1 name = (mk, dest)
   where
     mk ty t = App (Const (name, [ty]), t)
     dest (App (Const (c, [ty]), t)) | c == name = Just (ty, t)

   mk_setT, dest_setT, mk_mem, dest_mem,
   mk_eq, dest_eq, true, is_true, false, is_false,
   mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
   mk_imp, dest_imp, mk_iff, dest_iff,
   mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
-  mk_all, dest_all, mk_ex, dest_ex
+  mk_all, dest_all, mk_ex, dest_ex,
+  mk_undefined, dest_undefined
 )
 where
 
 import qualified Isabelle.Name as Name
 import Isabelle.Term

 mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_all, dest_all) = binder \<open>\<^const_name>\<open>All\<close>\<close>
 
 mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_ex, dest_ex) = binder \<open>\<^const_name>\<open>Ex\<close>\<close>
+
+mk_undefined :: Typ -> Term; dest_undefined :: Term -> Maybe Typ
+(mk_undefined, dest_undefined) = typed_op0 \<open>\<^const_name>\<open>undefined\<close>\<close>
 \<close>
 
 generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
 {-  Title:      Isabelle/Term_XML/Encode.hs
     Author:     Makarius