isabelle: src/Tools/Metis/src/Proof.sig@6ee87f67d9cd (annotated)

23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	1	(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	2	(* PROOFS IN FIRST ORDER LOGIC *)
23510 4521fead5609 GPL -> BSD paulson parents: 23442 diff changeset	3	(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	4	(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	5
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	6	signature Proof =
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	7	sig
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	8
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	9	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	10	(* A type of first order logic proofs. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	11	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	12
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	13	datatype inference =
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	14	Axiom of LiteralSet.set
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	15	\| Assume of Atom.atom
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	16	\| Subst of Subst.subst * Thm.thm
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	17	\| Resolve of Atom.atom * Thm.thm * Thm.thm
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	18	\| Refl of Term.term
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	19	\| Equality of Literal.literal * Term.path * Term.term
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	20
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	21	type proof = (Thm.thm * inference) list
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	22
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	23	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	24	(* Reconstructing single inferences. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	25	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	26
25430 372d6749f00e patching in the latest changes from Hurd paulson parents: 23510 diff changeset	27	val inferenceType : inference -> Thm.inferenceType
372d6749f00e patching in the latest changes from Hurd paulson parents: 23510 diff changeset	28
372d6749f00e patching in the latest changes from Hurd paulson parents: 23510 diff changeset	29	val parents : inference -> Thm.thm list
372d6749f00e patching in the latest changes from Hurd paulson parents: 23510 diff changeset	30
23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	31	val inferenceToThm : inference -> Thm.thm
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	32
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	33	val thmToInference : Thm.thm -> inference
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	34
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	35	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	36	(* Reconstructing whole proofs. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	37	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	38
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	39	val proof : Thm.thm -> proof
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	40
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	41	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	42	(* Printing. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	43	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	44
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	45	val ppInference : inference Parser.pp
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	46
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	47	val inferenceToString : inference -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	48
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	49	val pp : proof Parser.pp
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	50
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	51	val toString : proof -> string
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	52
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	53	end

author	wenzelm
	Sat, 28 Feb 2009 14:52:21 +0100
changeset 30165	6ee87f67d9cd
parent 25430	372d6749f00e
child 39353	7f11d833d65b
permissions	-rw-r--r--