0N/A{- |

2105N/AModule : $Header$

0N/ACopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004

0N/ALicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

0N/A

0N/AMaintainer : hets@tzi.de

0N/AStability : provisional

0N/APortability : portable

0N/A

0N/A utilities for the HasCASL to Isabelle comorphism

0N/A-}

0N/A

0N/Amodule Isabelle.IsaConsts where

0N/A

0N/Aimport Isabelle.IsaSign

0N/A

0N/A-- | application

0N/AtermAppl :: Term -> Term -> Term

1472N/AtermAppl t1 t2 = App t1 t2 NotCont

1472N/A

1472N/A-- | apply binary operation to arguments

0N/AbinConst :: String -> Term -> Term -> Term

0N/AbinConst s t1 t2 = termAppl (termAppl (con s) t1) t2

0N/A

91N/A-- | construct a constant

0N/AconT :: String -> Typ -> Term

0N/AconT s t = Const s t isaTerm

0N/A

0N/A-- | construct a constant with no type

0N/Acon :: String -> Term

1879N/Acon s = conT s noType

0N/A

1879N/A-- * some stuff

0N/A

1879N/AsomeS :: String

1879N/AsomeS = "Some"

1879N/A

1879N/AconSomeT :: Typ -> Term

1879N/AconSomeT t = conT someS t

1879N/A

1879N/A-- | some constant with no type

1879N/AconSome :: Term

1879N/AconSome = con someS

1879N/A

1879N/A-- | defOp constant

1879N/AdefOp :: Term

1879N/AdefOp = con "defOp"

0N/A

0N/A-- | not constant

1879N/AnotOp :: Term

2105N/AnotOp = con "Not"

2105N/A

2105N/A-- * quantor strings

2105N/A

1879N/AallS, exS, ex1S :: String

0N/AallS = "All"

0N/AexS = "Ex"

0N/Aex1S = "Ex1"

1879N/A

1879N/A-- * strings of binary ops

1879N/A

1879N/Aconj :: String

1879N/Aconj = "op &"

0N/A

0N/Adisj :: String

1879N/Adisj = "op |"

0N/A

0N/Aimpl :: String

0N/Aimpl = "op -->"

0N/A

0N/Aeqv :: String

1879N/Aeqv = "op <=>"

0N/A

0N/Aeq :: String

0N/Aeq = "op ="

0N/A

0N/A-- * binary junctors

0N/AbinConj, binDisj, binImpl, binEqv, binEq :: Term -> Term -> Term

1879N/AbinConj= binConst conj

0N/AbinDisj = binConst disj

0N/AbinImpl = binConst impl

0N/AbinEq = binConst eq

1879N/AbinEqv = binConst eqv

1879N/A

0N/A-- * boolean constants

1879N/Atrue, false :: Term

0N/Atrue = con "True"

1879N/Afalse = con "False"

2105N/A

0N/A-- | pair stuff

0N/ApairC :: String

0N/ApairC = "pair"

659N/A

1934N/AisaPair :: String

1879N/AisaPair = "Pair"

1879N/A

1879N/A

1879N/A