{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

{- |

Module : $Header$

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 _ =

"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 Logic.Logic.Syntax Isabelle () () ()

-- default implementation is fine!

instance GetRange Sentence

instance Sentences Isabelle Sentence Sign IsabelleMorphism () where

map_sen Isabelle _ s = return s

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]

cons_checkers Isabelle = [isabelleConsChecker]

instance LogicFram Isabelle () () Sentence () () Sign IsabelleMorphism () () ()