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

39348 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	1	(* ========================================================================= *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	2	(* PROOFS IN FIRST ORDER LOGIC *)
39444 beabb8443ee4 MIT license -> BSD License blanchet parents: 39443 diff changeset	3	(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
39348 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	4	(* ========================================================================= *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	5
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	6	signature Proof =
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	7	sig
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	8
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	9	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	10	(* A type of first order logic proofs. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	11	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	12
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	13	datatype inference =
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	14	Axiom of LiteralSet.set
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	15	\| Assume of Atom.atom
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	16	\| Subst of Subst.subst * Thm.thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	17	\| Resolve of Atom.atom * Thm.thm * Thm.thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	18	\| Refl of Term.term
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	19	\| Equality of Literal.literal * Term.path * Term.term
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	20
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	21	type proof = (Thm.thm * inference) list
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	22
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	23	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	24	(* Reconstructing single inferences. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	25	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	26
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	27	val inferenceType : inference -> Thm.inferenceType
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	28
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	29	val parents : inference -> Thm.thm list
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	30
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	31	val inferenceToThm : inference -> Thm.thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	32
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	33	val thmToInference : Thm.thm -> inference
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	34
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	35	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	36	(* Reconstructing whole proofs. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	37	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	38
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	39	val proof : Thm.thm -> proof
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	40
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	41	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	42	(* Free variables. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	43	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	44
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	45	val freeIn : Term.var -> proof -> bool
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	46
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	47	val freeVars : proof -> NameSet.set
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	48
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	49	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	50	(* Printing. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	51	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	52
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	53	val ppInference : inference Print.pp
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	54
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	55	val inferenceToString : inference -> string
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	56
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	57	val pp : proof Print.pp
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	58
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	59	val toString : proof -> string
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	60
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	61	end

author	blanchet
	Thu, 16 Sep 2010 07:30:15 +0200
changeset 39444	beabb8443ee4
parent 39443	e330437cd22a
child 39501	aaa7078fff55
permissions	-rw-r--r--