Hets - the Heterogeneous Tool Set

Copyright(c) University of Cambridge Cambridge England
adaption (c) Till Mossakowski Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Isabelle.IsaSign

Description

Data structures for Isabelle signatures and theories. Adapted from Isabelle.

Synopsis

Documentation

type TName = String Source #

type names

data AltSyntax Source #

Constructors

AltSyntax String [Int] Int 

Instances

Eq AltSyntax Source # 

Methods

(==) :: AltSyntax -> AltSyntax -> Bool

(/=) :: AltSyntax -> AltSyntax -> Bool

Data AltSyntax Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AltSyntax -> c AltSyntax

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AltSyntax

toConstr :: AltSyntax -> Constr

dataTypeOf :: AltSyntax -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c AltSyntax)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltSyntax)

gmapT :: (forall b. Data b => b -> b) -> AltSyntax -> AltSyntax

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AltSyntax -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AltSyntax -> r

gmapQ :: (forall d. Data d => d -> u) -> AltSyntax -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AltSyntax -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AltSyntax -> m AltSyntax

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AltSyntax -> m AltSyntax

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AltSyntax -> m AltSyntax

Ord AltSyntax Source # 

Methods

compare :: AltSyntax -> AltSyntax -> Ordering

(<) :: AltSyntax -> AltSyntax -> Bool

(<=) :: AltSyntax -> AltSyntax -> Bool

(>) :: AltSyntax -> AltSyntax -> Bool

(>=) :: AltSyntax -> AltSyntax -> Bool

max :: AltSyntax -> AltSyntax -> AltSyntax

min :: AltSyntax -> AltSyntax -> AltSyntax

Show AltSyntax Source # 

Methods

showsPrec :: Int -> AltSyntax -> ShowS

show :: AltSyntax -> String

showList :: [AltSyntax] -> ShowS

data VName Source #

names for values or constants (non-classes and non-types)

Constructors

VName 

Fields

Instances

Eq VName Source # 

Methods

(==) :: VName -> VName -> Bool

(/=) :: VName -> VName -> Bool

Data VName Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VName -> c VName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VName

toConstr :: VName -> Constr

dataTypeOf :: VName -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c VName)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VName)

gmapT :: (forall b. Data b => b -> b) -> VName -> VName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VName -> r

gmapQ :: (forall d. Data d => d -> u) -> VName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> VName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VName -> m VName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VName -> m VName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VName -> m VName

Ord VName Source # 

Methods

compare :: VName -> VName -> Ordering

(<) :: VName -> VName -> Bool

(<=) :: VName -> VName -> Bool

(>) :: VName -> VName -> Bool

(>=) :: VName -> VName -> Bool

max :: VName -> VName -> VName

min :: VName -> VName -> VName

Show VName Source # 

Methods

showsPrec :: Int -> VName -> ShowS

show :: VName -> String

showList :: [VName] -> ShowS

orig :: VName -> String Source #

the original (Haskell) name

data QName Source #

Constructors

QName 

Fields

Instances

Eq QName Source # 

Methods

(==) :: QName -> QName -> Bool

(/=) :: QName -> QName -> Bool

Data QName Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QName -> c QName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QName

toConstr :: QName -> Constr

dataTypeOf :: QName -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c QName)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)

gmapT :: (forall b. Data b => b -> b) -> QName -> QName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r

gmapQ :: (forall d. Data d => d -> u) -> QName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QName -> m QName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QName -> m QName

Ord QName Source # 

Methods

compare :: QName -> QName -> Ordering

(<) :: QName -> QName -> Bool

(<=) :: QName -> QName -> Bool

(>) :: QName -> QName -> Bool

(>=) :: QName -> QName -> Bool

max :: QName -> QName -> QName

min :: QName -> QName -> QName

Show QName Source # 

Methods

showsPrec :: Int -> QName -> ShowS

show :: QName -> String

showList :: [QName] -> ShowS

mkQName :: String -> QName Source #

data Indexname Source #

Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.

Constructors

Indexname 

Fields

Instances

Eq Indexname Source # 

Methods

(==) :: Indexname -> Indexname -> Bool

(/=) :: Indexname -> Indexname -> Bool

Data Indexname Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Indexname -> c Indexname

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Indexname

toConstr :: Indexname -> Constr

dataTypeOf :: Indexname -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Indexname)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Indexname)

gmapT :: (forall b. Data b => b -> b) -> Indexname -> Indexname

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Indexname -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Indexname -> r

gmapQ :: (forall d. Data d => d -> u) -> Indexname -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Indexname -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Indexname -> m Indexname

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Indexname -> m Indexname

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Indexname -> m Indexname

Ord Indexname Source # 

Methods

compare :: Indexname -> Indexname -> Ordering

(<) :: Indexname -> Indexname -> Bool

(<=) :: Indexname -> Indexname -> Bool

(>) :: Indexname -> Indexname -> Bool

(>=) :: Indexname -> Indexname -> Bool

max :: Indexname -> Indexname -> Indexname

min :: Indexname -> Indexname -> Indexname

Show Indexname Source # 

Methods

showsPrec :: Int -> Indexname -> ShowS

show :: Indexname -> String

showList :: [Indexname] -> ShowS

data IsaClass Source #

Constructors

IsaClass String 

Instances

Eq IsaClass Source # 

Methods

(==) :: IsaClass -> IsaClass -> Bool

(/=) :: IsaClass -> IsaClass -> Bool

Data IsaClass Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsaClass -> c IsaClass

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsaClass

toConstr :: IsaClass -> Constr

dataTypeOf :: IsaClass -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c IsaClass)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsaClass)

gmapT :: (forall b. Data b => b -> b) -> IsaClass -> IsaClass

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsaClass -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsaClass -> r

gmapQ :: (forall d. Data d => d -> u) -> IsaClass -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsaClass -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsaClass -> m IsaClass

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaClass -> m IsaClass

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaClass -> m IsaClass

Ord IsaClass Source # 

Methods

compare :: IsaClass -> IsaClass -> Ordering

(<) :: IsaClass -> IsaClass -> Bool

(<=) :: IsaClass -> IsaClass -> Bool

(>) :: IsaClass -> IsaClass -> Bool

(>=) :: IsaClass -> IsaClass -> Bool

max :: IsaClass -> IsaClass -> IsaClass

min :: IsaClass -> IsaClass -> IsaClass

Show IsaClass Source # 

Methods

showsPrec :: Int -> IsaClass -> ShowS

show :: IsaClass -> String

showList :: [IsaClass] -> ShowS

data Typ Source #

Constructors

Type 

Fields

TFree 

Fields

TVar 

Instances

Eq Typ Source # 

Methods

(==) :: Typ -> Typ -> Bool

(/=) :: Typ -> Typ -> Bool

Data Typ Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Typ -> c Typ

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Typ

toConstr :: Typ -> Constr

dataTypeOf :: Typ -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Typ)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ)

gmapT :: (forall b. Data b => b -> b) -> Typ -> Typ

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r

gmapQ :: (forall d. Data d => d -> u) -> Typ -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Typ -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Typ -> m Typ

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Typ -> m Typ

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Typ -> m Typ

Ord Typ Source # 

Methods

compare :: Typ -> Typ -> Ordering

(<) :: Typ -> Typ -> Bool

(<=) :: Typ -> Typ -> Bool

(>) :: Typ -> Typ -> Bool

(>=) :: Typ -> Typ -> Bool

max :: Typ -> Typ -> Typ

min :: Typ -> Typ -> Typ

Show Typ Source # 

Methods

showsPrec :: Int -> Typ -> ShowS

show :: Typ -> String

showList :: [Typ] -> ShowS

data Continuity Source #

Constructors

IsCont Bool 
NotCont 

Instances

Eq Continuity Source # 

Methods

(==) :: Continuity -> Continuity -> Bool

(/=) :: Continuity -> Continuity -> Bool

Data Continuity Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Continuity -> c Continuity

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Continuity

toConstr :: Continuity -> Constr

dataTypeOf :: Continuity -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Continuity)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Continuity)

gmapT :: (forall b. Data b => b -> b) -> Continuity -> Continuity

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Continuity -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Continuity -> r

gmapQ :: (forall d. Data d => d -> u) -> Continuity -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Continuity -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Continuity -> m Continuity

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Continuity -> m Continuity

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Continuity -> m Continuity

Ord Continuity Source # 
Show Continuity Source # 

Methods

showsPrec :: Int -> Continuity -> ShowS

show :: Continuity -> String

showList :: [Continuity] -> ShowS

data TAttr Source #

Constructors

TFun 
TMet 
TCon 
NA 

Instances

Eq TAttr Source # 

Methods

(==) :: TAttr -> TAttr -> Bool

(/=) :: TAttr -> TAttr -> Bool

Data TAttr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TAttr -> c TAttr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TAttr

toConstr :: TAttr -> Constr

dataTypeOf :: TAttr -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TAttr)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAttr)

gmapT :: (forall b. Data b => b -> b) -> TAttr -> TAttr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAttr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAttr -> r

gmapQ :: (forall d. Data d => d -> u) -> TAttr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TAttr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TAttr -> m TAttr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TAttr -> m TAttr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TAttr -> m TAttr

Ord TAttr Source # 

Methods

compare :: TAttr -> TAttr -> Ordering

(<) :: TAttr -> TAttr -> Bool

(<=) :: TAttr -> TAttr -> Bool

(>) :: TAttr -> TAttr -> Bool

(>=) :: TAttr -> TAttr -> Bool

max :: TAttr -> TAttr -> TAttr

min :: TAttr -> TAttr -> TAttr

Show TAttr Source # 

Methods

showsPrec :: Int -> TAttr -> ShowS

show :: TAttr -> String

showList :: [TAttr] -> ShowS

data DTyp Source #

Constructors

Hide 

Fields

Disp 

Fields

Instances

Eq DTyp Source # 

Methods

(==) :: DTyp -> DTyp -> Bool

(/=) :: DTyp -> DTyp -> Bool

Data DTyp Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DTyp -> c DTyp

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DTyp

toConstr :: DTyp -> Constr

dataTypeOf :: DTyp -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DTyp)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DTyp)

gmapT :: (forall b. Data b => b -> b) -> DTyp -> DTyp

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r

gmapQ :: (forall d. Data d => d -> u) -> DTyp -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DTyp -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DTyp -> m DTyp

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DTyp -> m DTyp

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DTyp -> m DTyp

Ord DTyp Source # 

Methods

compare :: DTyp -> DTyp -> Ordering

(<) :: DTyp -> DTyp -> Bool

(<=) :: DTyp -> DTyp -> Bool

(>) :: DTyp -> DTyp -> Bool

(>=) :: DTyp -> DTyp -> Bool

max :: DTyp -> DTyp -> DTyp

min :: DTyp -> DTyp -> DTyp

Show DTyp Source # 

Methods

showsPrec :: Int -> DTyp -> ShowS

show :: DTyp -> String

showList :: [DTyp] -> ShowS

data Term Source #

Constructors

Const 

Fields

Free 

Fields

Abs 
App 
If 
Case 

Fields

Let 

Fields

IsaEq 

Fields

Tuplex [Term] Continuity 
Set SetDecl 

Instances

Eq Term Source # 

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Data Term Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Ord Term Source # 

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Show Term Source # 

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

data Prop Source #

Constructors

Prop 

Fields

Instances

Eq Prop Source # 

Methods

(==) :: Prop -> Prop -> Bool

(/=) :: Prop -> Prop -> Bool

Data Prop Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Prop -> c Prop

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Prop

toConstr :: Prop -> Constr

dataTypeOf :: Prop -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Prop)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Prop)

gmapT :: (forall b. Data b => b -> b) -> Prop -> Prop

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Prop -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Prop -> r

gmapQ :: (forall d. Data d => d -> u) -> Prop -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Prop -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Prop -> m Prop

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Prop -> m Prop

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Prop -> m Prop

Ord Prop Source # 

Methods

compare :: Prop -> Prop -> Ordering

(<) :: Prop -> Prop -> Bool

(<=) :: Prop -> Prop -> Bool

(>) :: Prop -> Prop -> Bool

(>=) :: Prop -> Prop -> Bool

max :: Prop -> Prop -> Prop

min :: Prop -> Prop -> Prop

Show Prop Source # 

Methods

showsPrec :: Int -> Prop -> ShowS

show :: Prop -> String

showList :: [Prop] -> ShowS

data Props Source #

Constructors

Props 

Fields

Instances

Eq Props Source # 

Methods

(==) :: Props -> Props -> Bool

(/=) :: Props -> Props -> Bool

Data Props Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Props -> c Props

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Props

toConstr :: Props -> Constr

dataTypeOf :: Props -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Props)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Props)

gmapT :: (forall b. Data b => b -> b) -> Props -> Props

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Props -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Props -> r

gmapQ :: (forall d. Data d => d -> u) -> Props -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Props -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Props -> m Props

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Props -> m Props

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Props -> m Props

Ord Props Source # 

Methods

compare :: Props -> Props -> Ordering

(<) :: Props -> Props -> Bool

(<=) :: Props -> Props -> Bool

(>) :: Props -> Props -> Bool

(>=) :: Props -> Props -> Bool

max :: Props -> Props -> Props

min :: Props -> Props -> Props

Show Props Source # 

Methods

showsPrec :: Int -> Props -> ShowS

show :: Props -> String

showList :: [Props] -> ShowS

data Sentence Source #

Constructors

Sentence 

Fields

Instance 

Fields

ConstDef 

Fields

RecDef 

Fields

TypeDef 
Lemmas

Isabelle syntax for grouping multiple lemmas in to a single lemma.

Fields

Locale 
Class 
Datatypes [Datatype] 
Domains [Domain] 
Consts [(String, Maybe Mixfix, Typ)] 
TypeSynonym QName (Maybe Mixfix) [String] Typ 
Axioms [Axiom] 
Lemma 

Fields

Definition 
Fun 

Fields

Primrec 

Fields

Fixrec [(String, Maybe Mixfix, Typ, [FixrecEquation])] 
Instantiation 
InstanceProof 

Fields

InstanceArity 

Fields

InstanceSubclass 

Fields

Subclass 

Fields

Typedef 

Fields

Defs 

Fields

Instances

Eq Sentence Source # 

Methods

(==) :: Sentence -> Sentence -> Bool

(/=) :: Sentence -> Sentence -> Bool

Data Sentence Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sentence -> c Sentence

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sentence

toConstr :: Sentence -> Constr

dataTypeOf :: Sentence -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Sentence)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)

gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r

gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence

Ord Sentence Source # 

Methods

compare :: Sentence -> Sentence -> Ordering

(<) :: Sentence -> Sentence -> Bool

(<=) :: Sentence -> Sentence -> Bool

(>) :: Sentence -> Sentence -> Bool

(>=) :: Sentence -> Sentence -> Bool

max :: Sentence -> Sentence -> Sentence

min :: Sentence -> Sentence -> Sentence

Show Sentence Source # 

Methods

showsPrec :: Int -> Sentence -> ShowS

show :: Sentence -> String

showList :: [Sentence] -> ShowS

Sentences Isabelle Sentence Sign IsabelleMorphism () Source # 
StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source # 

Methods

basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source #

sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source #

stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source #

convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source #

ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source #

qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source #

symbol_to_raw :: Isabelle -> () -> () Source #

id_to_raw :: Isabelle -> Id -> () Source #

matches :: Isabelle -> () -> () -> Bool Source #

empty_signature :: Isabelle -> Sign Source #

add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source #

signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source #

signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source #

intersection :: Isabelle -> Sign -> Sign -> Result Sign Source #

final_union :: Isabelle -> Sign -> Sign -> Result Sign Source #

morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source #

is_subsig :: Isabelle -> Sign -> Sign -> Bool Source #

subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source #

generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source #

cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source #

induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source #

induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source #

is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source #

is_injective :: Isabelle -> IsabelleMorphism -> Bool Source #

theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Methods

base_sig :: Isabelle -> Sign Source #

write_logic :: Isabelle -> String -> String Source #

write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_model :: Isabelle -> String -> IsabelleMorphism -> String Source #

read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source #

write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #

Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Methods

parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source #

stability :: Isabelle -> Stability Source #

data_logic :: Isabelle -> Maybe AnyLogic Source #

top_sublogic :: Isabelle -> () Source #

all_sublogics :: Isabelle -> [()] Source #

bottomSublogic :: Isabelle -> Maybe () Source #

sublogicDimensions :: Isabelle -> [[()]] Source #

parseSublogic :: Isabelle -> String -> Maybe () Source #

proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source #

provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source #

default_prover :: Isabelle -> String Source #

cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source #

conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source #

empty_proof_tree :: Isabelle -> () Source #

syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Isabelle -> Maybe OMCD Source #

export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

data DefEquation Source #

Instances

Eq DefEquation Source # 

Methods

(==) :: DefEquation -> DefEquation -> Bool

(/=) :: DefEquation -> DefEquation -> Bool

Data DefEquation Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefEquation -> c DefEquation

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefEquation

toConstr :: DefEquation -> Constr

dataTypeOf :: DefEquation -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DefEquation)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefEquation)

gmapT :: (forall b. Data b => b -> b) -> DefEquation -> DefEquation

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefEquation -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefEquation -> r

gmapQ :: (forall d. Data d => d -> u) -> DefEquation -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DefEquation -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefEquation -> m DefEquation

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefEquation -> m DefEquation

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefEquation -> m DefEquation

Ord DefEquation Source # 
Show DefEquation Source # 

Methods

showsPrec :: Int -> DefEquation -> ShowS

show :: DefEquation -> String

showList :: [DefEquation] -> ShowS

data FixrecEquation Source #

Instances

Eq FixrecEquation Source # 
Data FixrecEquation Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixrecEquation -> c FixrecEquation

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixrecEquation

toConstr :: FixrecEquation -> Constr

dataTypeOf :: FixrecEquation -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c FixrecEquation)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixrecEquation)

gmapT :: (forall b. Data b => b -> b) -> FixrecEquation -> FixrecEquation

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixrecEquation -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixrecEquation -> r

gmapQ :: (forall d. Data d => d -> u) -> FixrecEquation -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FixrecEquation -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixrecEquation -> m FixrecEquation

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixrecEquation -> m FixrecEquation

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixrecEquation -> m FixrecEquation

Ord FixrecEquation Source # 
Show FixrecEquation Source # 

Methods

showsPrec :: Int -> FixrecEquation -> ShowS

show :: FixrecEquation -> String

showList :: [FixrecEquation] -> ShowS

data Ctxt Source #

Constructors

Ctxt 

Fields

Instances

Eq Ctxt Source # 

Methods

(==) :: Ctxt -> Ctxt -> Bool

(/=) :: Ctxt -> Ctxt -> Bool

Data Ctxt Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ctxt -> c Ctxt

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ctxt

toConstr :: Ctxt -> Constr

dataTypeOf :: Ctxt -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Ctxt)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ctxt)

gmapT :: (forall b. Data b => b -> b) -> Ctxt -> Ctxt

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctxt -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctxt -> r

gmapQ :: (forall d. Data d => d -> u) -> Ctxt -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ctxt -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ctxt -> m Ctxt

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ctxt -> m Ctxt

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ctxt -> m Ctxt

Ord Ctxt Source # 

Methods

compare :: Ctxt -> Ctxt -> Ordering

(<) :: Ctxt -> Ctxt -> Bool

(<=) :: Ctxt -> Ctxt -> Bool

(>) :: Ctxt -> Ctxt -> Bool

(>=) :: Ctxt -> Ctxt -> Bool

max :: Ctxt -> Ctxt -> Ctxt

min :: Ctxt -> Ctxt -> Ctxt

Show Ctxt Source # 

Methods

showsPrec :: Int -> Ctxt -> ShowS

show :: Ctxt -> String

showList :: [Ctxt] -> ShowS

data Mixfix Source #

Constructors

Mixfix 

Fields

Instances

Eq Mixfix Source # 

Methods

(==) :: Mixfix -> Mixfix -> Bool

(/=) :: Mixfix -> Mixfix -> Bool

Data Mixfix Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Mixfix -> c Mixfix

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Mixfix

toConstr :: Mixfix -> Constr

dataTypeOf :: Mixfix -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Mixfix)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Mixfix)

gmapT :: (forall b. Data b => b -> b) -> Mixfix -> Mixfix

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Mixfix -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Mixfix -> r

gmapQ :: (forall d. Data d => d -> u) -> Mixfix -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Mixfix -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Mixfix -> m Mixfix

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Mixfix -> m Mixfix

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Mixfix -> m Mixfix

Ord Mixfix Source # 

Methods

compare :: Mixfix -> Mixfix -> Ordering

(<) :: Mixfix -> Mixfix -> Bool

(<=) :: Mixfix -> Mixfix -> Bool

(>) :: Mixfix -> Mixfix -> Bool

(>=) :: Mixfix -> Mixfix -> Bool

max :: Mixfix -> Mixfix -> Mixfix

min :: Mixfix -> Mixfix -> Mixfix

Show Mixfix Source # 

Methods

showsPrec :: Int -> Mixfix -> ShowS

show :: Mixfix -> String

showList :: [Mixfix] -> ShowS

data MixfixTemplate Source #

Constructors

Arg Int 
Str String 
Break Int 
Block Int [MixfixTemplate] 

Instances

Eq MixfixTemplate Source # 
Data MixfixTemplate Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MixfixTemplate -> c MixfixTemplate

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MixfixTemplate

toConstr :: MixfixTemplate -> Constr

dataTypeOf :: MixfixTemplate -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c MixfixTemplate)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MixfixTemplate)

gmapT :: (forall b. Data b => b -> b) -> MixfixTemplate -> MixfixTemplate

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MixfixTemplate -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MixfixTemplate -> r

gmapQ :: (forall d. Data d => d -> u) -> MixfixTemplate -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MixfixTemplate -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MixfixTemplate -> m MixfixTemplate

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MixfixTemplate -> m MixfixTemplate

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MixfixTemplate -> m MixfixTemplate

Ord MixfixTemplate Source # 
Show MixfixTemplate Source # 

Methods

showsPrec :: Int -> MixfixTemplate -> ShowS

show :: MixfixTemplate -> String

showList :: [MixfixTemplate] -> ShowS

data Datatype Source #

Instances

Eq Datatype Source # 

Methods

(==) :: Datatype -> Datatype -> Bool

(/=) :: Datatype -> Datatype -> Bool

Data Datatype Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Datatype -> c Datatype

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Datatype

toConstr :: Datatype -> Constr

dataTypeOf :: Datatype -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Datatype)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Datatype)

gmapT :: (forall b. Data b => b -> b) -> Datatype -> Datatype

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Datatype -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Datatype -> r

gmapQ :: (forall d. Data d => d -> u) -> Datatype -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Datatype -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Datatype -> m Datatype

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Datatype -> m Datatype

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Datatype -> m Datatype

Ord Datatype Source # 

Methods

compare :: Datatype -> Datatype -> Ordering

(<) :: Datatype -> Datatype -> Bool

(<=) :: Datatype -> Datatype -> Bool

(>) :: Datatype -> Datatype -> Bool

(>=) :: Datatype -> Datatype -> Bool

max :: Datatype -> Datatype -> Datatype

min :: Datatype -> Datatype -> Datatype

Show Datatype Source # 

Methods

showsPrec :: Int -> Datatype -> ShowS

show :: Datatype -> String

showList :: [Datatype] -> ShowS

data DatatypeConstructor Source #

Instances

Eq DatatypeConstructor Source # 
Data DatatypeConstructor Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DatatypeConstructor -> c DatatypeConstructor

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DatatypeConstructor

toConstr :: DatatypeConstructor -> Constr

dataTypeOf :: DatatypeConstructor -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DatatypeConstructor)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DatatypeConstructor)

gmapT :: (forall b. Data b => b -> b) -> DatatypeConstructor -> DatatypeConstructor

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r

gmapQ :: (forall d. Data d => d -> u) -> DatatypeConstructor -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DatatypeConstructor -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DatatypeConstructor -> m DatatypeConstructor

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeConstructor -> m DatatypeConstructor

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeConstructor -> m DatatypeConstructor

Ord DatatypeConstructor Source # 
Show DatatypeConstructor Source # 

Methods

showsPrec :: Int -> DatatypeConstructor -> ShowS

show :: DatatypeConstructor -> String

showList :: [DatatypeConstructor] -> ShowS

data Domain Source #

Instances

Eq Domain Source # 

Methods

(==) :: Domain -> Domain -> Bool

(/=) :: Domain -> Domain -> Bool

Data Domain Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Domain -> c Domain

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Domain

toConstr :: Domain -> Constr

dataTypeOf :: Domain -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Domain)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Domain)

gmapT :: (forall b. Data b => b -> b) -> Domain -> Domain

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Domain -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Domain -> r

gmapQ :: (forall d. Data d => d -> u) -> Domain -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Domain -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Domain -> m Domain

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Domain -> m Domain

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Domain -> m Domain

Ord Domain Source # 

Methods

compare :: Domain -> Domain -> Ordering

(<) :: Domain -> Domain -> Bool

(<=) :: Domain -> Domain -> Bool

(>) :: Domain -> Domain -> Bool

(>=) :: Domain -> Domain -> Bool

max :: Domain -> Domain -> Domain

min :: Domain -> Domain -> Domain

Show Domain Source # 

Methods

showsPrec :: Int -> Domain -> ShowS

show :: Domain -> String

showList :: [Domain] -> ShowS

data DomainConstructor Source #

Instances

Eq DomainConstructor Source # 
Data DomainConstructor Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DomainConstructor -> c DomainConstructor

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DomainConstructor

toConstr :: DomainConstructor -> Constr

dataTypeOf :: DomainConstructor -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DomainConstructor)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DomainConstructor)

gmapT :: (forall b. Data b => b -> b) -> DomainConstructor -> DomainConstructor

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructor -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructor -> r

gmapQ :: (forall d. Data d => d -> u) -> DomainConstructor -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DomainConstructor -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DomainConstructor -> m DomainConstructor

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructor -> m DomainConstructor

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructor -> m DomainConstructor

Ord DomainConstructor Source # 
Show DomainConstructor Source # 

Methods

showsPrec :: Int -> DomainConstructor -> ShowS

show :: DomainConstructor -> String

showList :: [DomainConstructor] -> ShowS

data DomainConstructorArg Source #

Instances

Eq DomainConstructorArg Source # 
Data DomainConstructorArg Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DomainConstructorArg -> c DomainConstructorArg

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DomainConstructorArg

toConstr :: DomainConstructorArg -> Constr

dataTypeOf :: DomainConstructorArg -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DomainConstructorArg)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DomainConstructorArg)

gmapT :: (forall b. Data b => b -> b) -> DomainConstructorArg -> DomainConstructorArg

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructorArg -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DomainConstructorArg -> r

gmapQ :: (forall d. Data d => d -> u) -> DomainConstructorArg -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DomainConstructorArg -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DomainConstructorArg -> m DomainConstructorArg

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructorArg -> m DomainConstructorArg

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DomainConstructorArg -> m DomainConstructorArg

Ord DomainConstructorArg Source # 
Show DomainConstructorArg Source # 

Methods

showsPrec :: Int -> DomainConstructorArg -> ShowS

show :: DomainConstructorArg -> String

showList :: [DomainConstructorArg] -> ShowS

data Axiom Source #

Constructors

Axiom 

Fields

Instances

Eq Axiom Source # 

Methods

(==) :: Axiom -> Axiom -> Bool

(/=) :: Axiom -> Axiom -> Bool

Data Axiom Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Axiom -> c Axiom

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Axiom

toConstr :: Axiom -> Constr

dataTypeOf :: Axiom -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Axiom)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Axiom)

gmapT :: (forall b. Data b => b -> b) -> Axiom -> Axiom

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r

gmapQ :: (forall d. Data d => d -> u) -> Axiom -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Axiom -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom

Ord Axiom Source # 

Methods

compare :: Axiom -> Axiom -> Ordering

(<) :: Axiom -> Axiom -> Bool

(<=) :: Axiom -> Axiom -> Bool

(>) :: Axiom -> Axiom -> Bool

(>=) :: Axiom -> Axiom -> Bool

max :: Axiom -> Axiom -> Axiom

min :: Axiom -> Axiom -> Axiom

Show Axiom Source # 

Methods

showsPrec :: Int -> Axiom -> ShowS

show :: Axiom -> String

showList :: [Axiom] -> ShowS

data FunSig Source #

Constructors

FunSig 

Fields

Instances

Eq FunSig Source # 

Methods

(==) :: FunSig -> FunSig -> Bool

(/=) :: FunSig -> FunSig -> Bool

Data FunSig Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunSig -> c FunSig

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunSig

toConstr :: FunSig -> Constr

dataTypeOf :: FunSig -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c FunSig)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSig)

gmapT :: (forall b. Data b => b -> b) -> FunSig -> FunSig

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunSig -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunSig -> r

gmapQ :: (forall d. Data d => d -> u) -> FunSig -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunSig -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunSig -> m FunSig

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunSig -> m FunSig

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunSig -> m FunSig

Ord FunSig Source # 

Methods

compare :: FunSig -> FunSig -> Ordering

(<) :: FunSig -> FunSig -> Bool

(<=) :: FunSig -> FunSig -> Bool

(>) :: FunSig -> FunSig -> Bool

(>=) :: FunSig -> FunSig -> Bool

max :: FunSig -> FunSig -> FunSig

min :: FunSig -> FunSig -> FunSig

Show FunSig Source # 

Methods

showsPrec :: Int -> FunSig -> ShowS

show :: FunSig -> String

showList :: [FunSig] -> ShowS

data SetDecl Source #

Constructors

SubSet Term Typ Term

Create a set using a subset. First parameter is the variable Second is the type of the variable third is the formula describing the set comprehension e.g. x Nat "even x" would be produce the isabelle code: {x::Nat . even x}

FixedSet [Term]

A set declared using a list of terms. e.g. {1,2,3} would be Set [1,2,3]

Instances

Eq SetDecl Source # 

Methods

(==) :: SetDecl -> SetDecl -> Bool

(/=) :: SetDecl -> SetDecl -> Bool

Data SetDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SetDecl -> c SetDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SetDecl

toConstr :: SetDecl -> Constr

dataTypeOf :: SetDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SetDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SetDecl)

gmapT :: (forall b. Data b => b -> b) -> SetDecl -> SetDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SetDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SetDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> SetDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SetDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SetDecl -> m SetDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SetDecl -> m SetDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SetDecl -> m SetDecl

Ord SetDecl Source # 

Methods

compare :: SetDecl -> SetDecl -> Ordering

(<) :: SetDecl -> SetDecl -> Bool

(<=) :: SetDecl -> SetDecl -> Bool

(>) :: SetDecl -> SetDecl -> Bool

(>=) :: SetDecl -> SetDecl -> Bool

max :: SetDecl -> SetDecl -> SetDecl

min :: SetDecl -> SetDecl -> SetDecl

Show SetDecl Source # 

Methods

showsPrec :: Int -> SetDecl -> ShowS

show :: SetDecl -> String

showList :: [SetDecl] -> ShowS

data MetaTerm Source #

Constructors

Term Term 
Conditional [Term] Term 

Instances

Eq MetaTerm Source # 

Methods

(==) :: MetaTerm -> MetaTerm -> Bool

(/=) :: MetaTerm -> MetaTerm -> Bool

Data MetaTerm Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaTerm -> c MetaTerm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaTerm

toConstr :: MetaTerm -> Constr

dataTypeOf :: MetaTerm -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c MetaTerm)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaTerm)

gmapT :: (forall b. Data b => b -> b) -> MetaTerm -> MetaTerm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaTerm -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaTerm -> r

gmapQ :: (forall d. Data d => d -> u) -> MetaTerm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaTerm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaTerm -> m MetaTerm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaTerm -> m MetaTerm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaTerm -> m MetaTerm

Ord MetaTerm Source # 

Methods

compare :: MetaTerm -> MetaTerm -> Ordering

(<) :: MetaTerm -> MetaTerm -> Bool

(<=) :: MetaTerm -> MetaTerm -> Bool

(>) :: MetaTerm -> MetaTerm -> Bool

(>=) :: MetaTerm -> MetaTerm -> Bool

max :: MetaTerm -> MetaTerm -> MetaTerm

min :: MetaTerm -> MetaTerm -> MetaTerm

Show MetaTerm Source # 

Methods

showsPrec :: Int -> MetaTerm -> ShowS

show :: MetaTerm -> String

showList :: [MetaTerm] -> ShowS

type ClassDecl = ([IsaClass], [(String, Term)], [(String, Typ)]) Source #

type LocaleDecl = ([String], [(String, Term)], [(String, Term)], [(String, Typ, Maybe AltSyntax)]) Source #

type Def = (Typ, [(String, Typ)], Term) Source #

type FunDef = (Typ, [([Term], Term)]) Source #

type Locales = Map String LocaleDecl Source #

type Defs = Map String Def Source #

type Funs = Map String FunDef Source #

type Arities = Map TName [(IsaClass, [(Typ, Sort)])] Source #

type Abbrs = Map TName ([TName], Typ) Source #

data TypeSig Source #

Constructors

TySg 

Instances

Eq TypeSig Source # 

Methods

(==) :: TypeSig -> TypeSig -> Bool

(/=) :: TypeSig -> TypeSig -> Bool

Ord TypeSig Source # 

Methods

compare :: TypeSig -> TypeSig -> Ordering

(<) :: TypeSig -> TypeSig -> Bool

(<=) :: TypeSig -> TypeSig -> Bool

(>) :: TypeSig -> TypeSig -> Bool

(>=) :: TypeSig -> TypeSig -> Bool

max :: TypeSig -> TypeSig -> TypeSig

min :: TypeSig -> TypeSig -> TypeSig

Show TypeSig Source # 

Methods

showsPrec :: Int -> TypeSig -> ShowS

show :: TypeSig -> String

showList :: [TypeSig] -> ShowS

data BaseSig Source #

Constructors

Main_thy

main theory of higher order logic (HOL)

Custom_thy 
MainHC_thy

extend main theory of HOL logic for HasCASL

MainHCPairs_thy

for HasCASL translation to bool pairs

HOLCF_thy

higher order logic for continuous functions

HsHOLCF_thy

HOLCF for Haskell

HsHOL_thy

HOL for Haskell

MHsHOL_thy 
MHsHOLCF_thy 
CspHOLComplex_thy 

Instances

Eq BaseSig Source # 

Methods

(==) :: BaseSig -> BaseSig -> Bool

(/=) :: BaseSig -> BaseSig -> Bool

Ord BaseSig Source # 

Methods

compare :: BaseSig -> BaseSig -> Ordering

(<) :: BaseSig -> BaseSig -> Bool

(<=) :: BaseSig -> BaseSig -> Bool

(>) :: BaseSig -> BaseSig -> Bool

(>=) :: BaseSig -> BaseSig -> Bool

max :: BaseSig -> BaseSig -> BaseSig

min :: BaseSig -> BaseSig -> BaseSig

Show BaseSig Source # 

Methods

showsPrec :: Int -> BaseSig -> ShowS

show :: BaseSig -> String

showList :: [BaseSig] -> ShowS

data Sign Source #

Constructors

Sign 

Fields

Instances

Eq Sign Source # 

Methods

(==) :: Sign -> Sign -> Bool

(/=) :: Sign -> Sign -> Bool

Ord Sign Source # 

Methods

compare :: Sign -> Sign -> Ordering

(<) :: Sign -> Sign -> Bool

(<=) :: Sign -> Sign -> Bool

(>) :: Sign -> Sign -> Bool

(>=) :: Sign -> Sign -> Bool

max :: Sign -> Sign -> Sign

min :: Sign -> Sign -> Sign

Show Sign Source # 

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

Sentences Isabelle Sentence Sign IsabelleMorphism () Source # 
StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source # 

Methods

basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source #

sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source #

stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source #

convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source #

ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source #

qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source #

symbol_to_raw :: Isabelle -> () -> () Source #

id_to_raw :: Isabelle -> Id -> () Source #

matches :: Isabelle -> () -> () -> Bool Source #

empty_signature :: Isabelle -> Sign Source #

add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source #

signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source #

signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source #

intersection :: Isabelle -> Sign -> Sign -> Result Sign Source #

final_union :: Isabelle -> Sign -> Sign -> Result Sign Source #

morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source #

is_subsig :: Isabelle -> Sign -> Sign -> Bool Source #

subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source #

generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source #

cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source #

induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source #

induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source #

is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source #

is_injective :: Isabelle -> IsabelleMorphism -> Bool Source #

theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Methods

base_sig :: Isabelle -> Sign Source #

write_logic :: Isabelle -> String -> String Source #

write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source #

write_model :: Isabelle -> String -> IsabelleMorphism -> String Source #

read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source #

write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #

Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Methods

parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source #

stability :: Isabelle -> Stability Source #

data_logic :: Isabelle -> Maybe AnyLogic Source #

top_sublogic :: Isabelle -> () Source #

all_sublogics :: Isabelle -> [()] Source #

bottomSublogic :: Isabelle -> Maybe () Source #

sublogicDimensions :: Isabelle -> [[()]] Source #

parseSublogic :: Isabelle -> String -> Maybe () Source #

proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source #

provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source #

default_prover :: Isabelle -> String Source #

cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source #

conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source #

empty_proof_tree :: Isabelle -> () Source #

syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Isabelle -> Maybe OMCD Source #

export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

type DomainEntry = (Typ, [(VName, [Typ])]) Source #

isSubSign :: Sign -> Sign -> Bool Source #

data IsaProof Source #

Constructors

IsaProof 

Fields

Instances

Eq IsaProof Source # 

Methods

(==) :: IsaProof -> IsaProof -> Bool

(/=) :: IsaProof -> IsaProof -> Bool

Data IsaProof Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsaProof -> c IsaProof

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsaProof

toConstr :: IsaProof -> Constr

dataTypeOf :: IsaProof -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c IsaProof)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsaProof)

gmapT :: (forall b. Data b => b -> b) -> IsaProof -> IsaProof

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsaProof -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsaProof -> r

gmapQ :: (forall d. Data d => d -> u) -> IsaProof -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsaProof -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsaProof -> m IsaProof

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaProof -> m IsaProof

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsaProof -> m IsaProof

Ord IsaProof Source # 

Methods

compare :: IsaProof -> IsaProof -> Ordering

(<) :: IsaProof -> IsaProof -> Bool

(<=) :: IsaProof -> IsaProof -> Bool

(>) :: IsaProof -> IsaProof -> Bool

(>=) :: IsaProof -> IsaProof -> Bool

max :: IsaProof -> IsaProof -> IsaProof

min :: IsaProof -> IsaProof -> IsaProof

Show IsaProof Source # 

Methods

showsPrec :: Int -> IsaProof -> ShowS

show :: IsaProof -> String

showList :: [IsaProof] -> ShowS

data ProofCommand Source #

Constructors

Apply [ProofMethod] Bool

Apply a list of proof methods, which will be applied in sequence withing the apply proof command. The boolean is if the + modifier should be used at the end of the apply proof method. e.g. Apply(A,B,C) True would represent the Isabelle proof command "apply(A,B,C)+"

Using [String] 
Back 
Defer Int 
Prefer Int 
Refute 

Instances

Eq ProofCommand Source # 

Methods

(==) :: ProofCommand -> ProofCommand -> Bool

(/=) :: ProofCommand -> ProofCommand -> Bool

Data ProofCommand Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofCommand -> c ProofCommand

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofCommand

toConstr :: ProofCommand -> Constr

dataTypeOf :: ProofCommand -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ProofCommand)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofCommand)

gmapT :: (forall b. Data b => b -> b) -> ProofCommand -> ProofCommand

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofCommand -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofCommand -> r

gmapQ :: (forall d. Data d => d -> u) -> ProofCommand -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofCommand -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofCommand -> m ProofCommand

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofCommand -> m ProofCommand

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofCommand -> m ProofCommand

Ord ProofCommand Source # 
Show ProofCommand Source # 

Methods

showsPrec :: Int -> ProofCommand -> ShowS

show :: ProofCommand -> String

showList :: [ProofCommand] -> ShowS

data ProofEnd Source #

Constructors

By ProofMethod 
DotDot 
Done 
Oops 
Sorry 

Instances

Eq ProofEnd Source # 

Methods

(==) :: ProofEnd -> ProofEnd -> Bool

(/=) :: ProofEnd -> ProofEnd -> Bool

Data ProofEnd Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofEnd -> c ProofEnd

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofEnd

toConstr :: ProofEnd -> Constr

dataTypeOf :: ProofEnd -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ProofEnd)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofEnd)

gmapT :: (forall b. Data b => b -> b) -> ProofEnd -> ProofEnd

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofEnd -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofEnd -> r

gmapQ :: (forall d. Data d => d -> u) -> ProofEnd -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofEnd -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofEnd -> m ProofEnd

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofEnd -> m ProofEnd

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofEnd -> m ProofEnd

Ord ProofEnd Source # 

Methods

compare :: ProofEnd -> ProofEnd -> Ordering

(<) :: ProofEnd -> ProofEnd -> Bool

(<=) :: ProofEnd -> ProofEnd -> Bool

(>) :: ProofEnd -> ProofEnd -> Bool

(>=) :: ProofEnd -> ProofEnd -> Bool

max :: ProofEnd -> ProofEnd -> ProofEnd

min :: ProofEnd -> ProofEnd -> ProofEnd

Show ProofEnd Source # 

Methods

showsPrec :: Int -> ProofEnd -> ShowS

show :: ProofEnd -> String

showList :: [ProofEnd] -> ShowS

data Modifier Source #

Constructors

No_asm

No_asm means that assumptions are completely ignored.

No_asm_simp

No_asm_simp means that the assumptions are not simplified but are used in the simplification of the conclusion.

No_asm_use

No_asm_use means that the assumptions are simplified but are not used in the simplification of each other or the conclusion.

Instances

Eq Modifier Source # 

Methods

(==) :: Modifier -> Modifier -> Bool

(/=) :: Modifier -> Modifier -> Bool

Data Modifier Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Modifier -> c Modifier

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Modifier

toConstr :: Modifier -> Constr

dataTypeOf :: Modifier -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Modifier)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Modifier)

gmapT :: (forall b. Data b => b -> b) -> Modifier -> Modifier

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Modifier -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Modifier -> r

gmapQ :: (forall d. Data d => d -> u) -> Modifier -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Modifier -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Modifier -> m Modifier

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Modifier -> m Modifier

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Modifier -> m Modifier

Ord Modifier Source # 

Methods

compare :: Modifier -> Modifier -> Ordering

(<) :: Modifier -> Modifier -> Bool

(<=) :: Modifier -> Modifier -> Bool

(>) :: Modifier -> Modifier -> Bool

(>=) :: Modifier -> Modifier -> Bool

max :: Modifier -> Modifier -> Modifier

min :: Modifier -> Modifier -> Modifier

Show Modifier Source # 

Methods

showsPrec :: Int -> Modifier -> ShowS

show :: Modifier -> String

showList :: [Modifier] -> ShowS

data ProofMethod Source #

Constructors

Auto

This is a plain auto with no parameters - it is used so often it warents its own constructor

Simp

This is a plain auto with no parameters - it is used so often it warents its own constructor

AutoSimpAdd (Maybe Modifier) [String]

This is an auto where the simpset has been temporarily extended with a listof lemmas, theorems and axioms. An optional modifier can also be used to control how the assumptions are used. It is used so often it warents its own constructor

SimpAdd (Maybe Modifier) [String]

This is a simp where the simpset has been temporarily extended with a listof lemmas, theorems and axioms. An optional modifier can also be used to control how the assumptions are used. It is used so often it warents its own constructor

Induct Term

Induction proof method. This performs induction upon a variable

CaseTac Term

Case_tac proof method. This perfom a case distinction on a term

SubgoalTac Term

Subgoal_tac proof method . Adds a term to the local assumptions and also creates a sub-goal of this term

Insert [String]

Insert proof method. Inserts a lemma or theorem name to the assumptions of the first goal

Other String

Used for proof methods that have not been implemented yet. This includes auto and simp with parameters

Instances

Eq ProofMethod Source # 

Methods

(==) :: ProofMethod -> ProofMethod -> Bool

(/=) :: ProofMethod -> ProofMethod -> Bool

Data ProofMethod Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProofMethod -> c ProofMethod

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProofMethod

toConstr :: ProofMethod -> Constr

dataTypeOf :: ProofMethod -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ProofMethod)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProofMethod)

gmapT :: (forall b. Data b => b -> b) -> ProofMethod -> ProofMethod

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProofMethod -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProofMethod -> r

gmapQ :: (forall d. Data d => d -> u) -> ProofMethod -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProofMethod -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProofMethod -> m ProofMethod

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofMethod -> m ProofMethod

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProofMethod -> m ProofMethod

Ord ProofMethod Source # 
Show ProofMethod Source # 

Methods

showsPrec :: Int -> ProofMethod -> ShowS

show :: ProofMethod -> String

showList :: [ProofMethod] -> ShowS