{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module : ./Isabelle/Logic_Isabelle.hs
Description : Isabelle instance of class Logic
Copyright : (c) Till Mossakowski, Uni Bremen 2002-2004
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : non-portable (imports Logic)
Instance of class Logic for Isabelle (including Pure, HOL etc.).
-}
module Isabelle.Logic_Isabelle where
import Common.DefaultMorphism
import Common.Id
import Logic.Logic
import Isabelle.ATC_Isabelle ()
import Isabelle.IsaSign
import Isabelle.IsaPrint
import Isabelle.IsaProve
type IsabelleMorphism = DefaultMorphism Sign
{- a dummy datatype for the LogicGraph and for identifying the right
instances -}
data Isabelle = Isabelle deriving Show
instance Language Isabelle where
description _ =
"logic of the generic theorem prover Isabelle\n" ++
"This logic corresponds to the logic of Isabelle,\n" ++
"a weak intuitionistic type theory\n" ++
"Also, the logics encoded in Isabelle, like FOL, HOL, HOLCF, ZF " ++
"are made available\n" ++
instance Logic.Logic.Syntax Isabelle () () () ()
-- default implementation is fine!
instance GetRange Sentence
instance Sentences Isabelle Sentence Sign IsabelleMorphism () where
map_sen Isabelle _ = return
print_named Isabelle = printNamedSen
-- other default implementations are fine
instance StaticAnalysis Isabelle () Sentence
() ()
Sign
IsabelleMorphism () () where
empty_signature Isabelle = emptySign
is_subsig Isabelle = isSubSign
subsig_inclusion Isabelle = defaultInclusion
instance Logic Isabelle () () Sentence () ()
Sign
IsabelleMorphism () () () where
stability _ = Testing
-- again default implementations are fine
empty_proof_tree _ = ()
provers Isabelle =
[isabelleProver Emacs, isabelleProver JEdit, isabelleBatchProver]
cons_checkers Isabelle = [isabelleConsChecker]
instance LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism
() () ()