446N/A{- |

4744N/AModule : $Header$

446N/ACopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach, Swansea University 2008

446N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

446N/A

446N/AMaintainer : csliam@swansea.ac.uk

446N/AStability : provisional

446N/APortability : portable

446N/A

446N/AData structures for Isabelle Proofs

446N/A-}

446N/A

446N/Amodule Isabelle.IsaProof where

446N/A

446N/Adata IsaProof = IsaProof

446N/A { proof :: [ProofCommand],

446N/A end :: ProofEnd

446N/A } deriving (Show, Eq, Ord)

446N/A

446N/Adata ProofCommand

873N/A = Apply ProofMethod

446N/A | Using [String]

446N/A | Back

446N/A | Defer Int

446N/A -- | Pr Int -- This proof command simply sets the number of

5073N/A -- goals shown in the display and is not needed

446N/A | Prefer Int

446N/A | Refute

446N/A deriving (Show, Eq, Ord)

4744N/A

4744N/Adata ProofEnd

4744N/A = By ProofMethod

4744N/A | DotDot

4744N/A | Done

4744N/A | Oops

4744N/A | Sorry

4744N/A deriving (Show, Eq, Ord)

4744N/A

4744N/Adata ProofMethod

4744N/A = Auto -- This is a plain auto with no parameters - it is used

4744N/A -- so often it warents its own constructor

4744N/A | Simp -- This is a plain auto with no parameters - it is used

4744N/A -- so often it warents its own constructor

4744N/A | Induct String -- Induction on a variable

4744N/A | CaseTac String -- apply case_tac to a term

4744N/A | SubgoalTac String-- apply subgoal_tac to a term

4744N/A | Insert String -- insert a lemma/theorem name to the assumptions of the first goal

4744N/A | Other String -- used for proof methods that have not been

4744N/A -- implemented yet - including auto and simp

4744N/A -- with parameters

4744N/A deriving (Show, Eq, Ord)

5073N/A

4744N/AtoIsaProof :: ProofEnd -> IsaProof

5073N/AtoIsaProof e = IsaProof [] e

4744N/A

4744N/AmkOops :: IsaProof

4744N/AmkOops = toIsaProof Oops

4744N/A