isabelle: src/Tools/Metis/src/Units.sig@58c0636e0ef5 (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	(* A STORE FOR UNIT THEOREMS *)
72004 913162a47d9f Update Metis to 2.4 desharna parents: 39502 diff changeset	3	(* Copyright (c) 2001 Joe Leslie-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 Units =
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 unit store. *)
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	type unitThm = Literal.literal * Thm.thm
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	14
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	15	type units
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	16
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	17	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	18	(* Basic operations. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	19	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	20
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	21	val empty : units
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	22
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	23	val size : units -> int
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	24
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	25	val toString : units -> string
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 pp : units Print.pp
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	28
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	29	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	30	(* Add units into the store. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	31	(* ------------------------------------------------------------------------- *)
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 add : units -> unitThm -> units
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	34
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	35	val addList : units -> unitThm list -> units
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	36
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	37	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	38	(* Matching. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	39	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	40
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	41	val match : units -> Literal.literal -> (unitThm * Subst.subst) option
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	42
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	43	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	44	(* Reducing by repeated matching and resolution. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	45	(* ------------------------------------------------------------------------- *)
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 reduce : units -> Rule.rule
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	48
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	49	end

author	wenzelm
	Thu, 15 Feb 2024 10:15:28 +0100
changeset 79614	58c0636e0ef5
parent 72004	913162a47d9f
permissions	-rw-r--r--