55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian MaederDescription : Isabelle instance of class Logic
72186e215ea8bd54f41bde5b792652aa7ca42167Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
72186e215ea8bd54f41bde5b792652aa7ca42167Till MossakowskiStability : provisional
6b8f813c46b719a37e9a61cdfba85339952abbedChristian MaederPortability : non-portable (imports Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederInstance of class Logic for Isabelle (including Pure, HOL etc.).
a5e231ee4359da4667d54016848220c590a77b79Paolo Torrinitype IsabelleMorphism = DefaultMorphism Sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- a dummy datatype for the LogicGraph and for identifying the right
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maederdata Isabelle = Isabelle deriving Show
05ca76b03b6d16bcfb3e7654c31e41a220e85663Till Mossakowskiinstance Language Isabelle where
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder description _ =
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski "logic of the generic theorem prover Isabelle\n" ++
6b8f813c46b719a37e9a61cdfba85339952abbedChristian Maeder "This logic corresponds to the logic of Isabelle,\n" ++
6b8f813c46b719a37e9a61cdfba85339952abbedChristian Maeder "a weak intuitionistic type theory\n" ++
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder "Also, the logics encoded in Isabelle, like FOL, HOL, HOLCF, ZF " ++
6b8f813c46b719a37e9a61cdfba85339952abbedChristian Maeder "are made available\n" ++
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski "See http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiinstance Logic.Logic.Syntax Isabelle () () () ()
6b8f813c46b719a37e9a61cdfba85339952abbedChristian Maeder -- default implementation is fine!
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maederinstance GetRange Sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Sentences Isabelle Sentence Sign IsabelleMorphism () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map_sen Isabelle _ = return
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder print_named Isabelle = printNamedSen
6b8f813c46b719a37e9a61cdfba85339952abbedChristian Maeder -- other default implementations are fine
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian Maederinstance StaticAnalysis Isabelle () Sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsabelleMorphism () () where
72186e215ea8bd54f41bde5b792652aa7ca42167Till Mossakowski empty_signature Isabelle = emptySign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder is_subsig Isabelle = isSubSign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder subsig_inclusion Isabelle = defaultInclusion
72186e215ea8bd54f41bde5b792652aa7ca42167Till Mossakowskiinstance Logic Isabelle () () Sentence () ()
b65e16b9e5652ff341ab0f49be5da51e2c0e10a5Till Mossakowski IsabelleMorphism () () () where
b65e16b9e5652ff341ab0f49be5da51e2c0e10a5Till Mossakowski stability _ = Testing
6b8f813c46b719a37e9a61cdfba85339952abbedChristian Maeder -- again default implementations are fine
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich empty_proof_tree _ = ()
eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder provers Isabelle =
eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder [isabelleProver Emacs, isabelleProver JEdit, isabelleBatchProver]
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich cons_checkers Isabelle = [isabelleConsChecker]
eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaederinstance LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism