41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski{- |

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till MossakowskiModule : $Header$

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till MossakowskiMaintainer : maeder@tzi.de

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till MossakowskiStability : provisional

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederPortability : non-portable (imports Logic)

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till MossakowskiInstance of class Logic for Isabelle (including Pure, HOL etc.).

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski-}

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskimodule Isabelle.Logic_Isabelle where

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskiimport Common.DefaultMorphism

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskiimport Logic.Logic

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskiimport Isabelle.ATC_Isabelle()

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskiimport Isabelle.IsaSign

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskiimport Isabelle.IsaPrint

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskiimport Isabelle.IsaProve

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowski

41cff438a611c7aac5b2a2c3e395fc5b88d68230Till Mossakowskitype IsabelleMorphism = DefaultMorphism Sign

4918e2f622cfb96f9a57b7617cd18ca7e4f8b5d4Christian Maeder

-- a dummy datatype for the LogicGraph and for identifying the right

-- instances

data Isabelle = Isabelle deriving (Show)

instance Language Isabelle where

description _ =

"Isabelle - a generic theorem prover\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" ++

"See http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"

instance Category Isabelle Sign IsabelleMorphism where

dom Isabelle = domOfDefaultMorphism

cod Isabelle = codOfDefaultMorphism

ide Isabelle = ideOfDefaultMorphism

comp Isabelle = compOfDefaultMorphism

legal_obj Isabelle = const True

legal_mor Isabelle = legalDefaultMorphism (legal_obj Isabelle)

-- abstract syntax, parsing (and printing)

instance Logic.Logic.Syntax Isabelle () () ()

-- default implementation is fine!

instance Sentences Isabelle Sentence () Sign IsabelleMorphism () where

map_sen Isabelle _ s = return s

print_named Isabelle = printNamedSen

provers Isabelle = [isabelleProver]

cons_checkers Isabelle = [isabelleConsChecker]

-- other default implementations are fine

instance StaticAnalysis Isabelle () Sentence ()

() ()

Sign

IsabelleMorphism () () where

sign_to_basic_spec Isabelle _sigma _sens = ()

empty_signature Isabelle = emptySign

inclusion Isabelle = defaultInclusion (is_subsig Isabelle)

is_subsig Isabelle = const $ const True -- TODO!!

instance Logic Isabelle () () Sentence () ()

Sign

IsabelleMorphism () () () where

stability _ = Testing

-- again default implementations are fine