isabelle: src/Tools/Metis/src/Proof.sig@e8552cba702d (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 *)
39502 cffceed8e7fa fix license blanchet parents: 39501 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	wenzelm
	Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389	e8552cba702d
parent 39502	cffceed8e7fa
child 72004	913162a47d9f
permissions	-rw-r--r--