Searched refs:subst (Results 1 - 25 of 351) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibMatch.sig11 type subst = mlibSubst.subst type
14 val matchl : subst -> (term * term) list -> subst
15 val match : term -> term -> subst
16 val matchl_literals : subst -> (formula * formula) list -> subst
17 val match_literals : formula -> formula -> subst
20 val unifyl : subst -> (term * term) list -> subst
[all...]
H A DmlibSubst.sig14 type subst type
16 val |<>| : subst
17 val ::> : (string, term) maplet * subst -> subst
18 val @> : subst * subst -> subst
19 val null : subst -> bool
20 val term_subst : subst -> term -> term
21 val formula_subst : subst
[all...]
H A DmlibSubsume.sig13 type subst = mlibSubst.subst type
24 val subsumes : 'a subsume -> formula list -> (subst * 'a) stream
27 val subsumes' : 'a subsume -> formula list -> (subst * 'a) stream
30 val subsumes1 : formula list -> formula list -> subst list
31 val subsumes1' : formula list -> formula list -> subst list
H A DmlibKernel.sig11 type subst = mlibSubst.subst type
24 val INST : subst -> thm -> thm
H A DmlibTermorder.sig11 type subst = mlibSubst.subst type
30 val subst : subst -> termorder -> termorder value
H A DmatchTools.sig9 type ('a, 'b) subst = ('a, 'b) Lib.subst
13 type tySubst = (hol_type, hol_type) subst
14 type Subst = (term, term) subst * tySubst
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DSubst.sig13 type subst type
19 val empty : subst
21 val null : subst -> bool
23 val size : subst -> int
25 val peek : subst -> Term.var -> Term.term option
27 val insert : subst -> Term.var * Term.term -> subst
29 val singleton : Term.var * Term.term -> subst
31 val toList : subst -> (Term.var * Term.term) list
33 val fromList : (Term.var * Term.term) list -> subst
53 val subst : subst -> Term.term -> Term.term value
[all...]
H A DSubsume.sig32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
33 (Thm.clause * Subst.subst * 'a) option
38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
39 (Thm.clause * Subst.subst * 'a) option
47 val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option
49 val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option
H A DAtom.sig81 val subst : Subst.subst -> atom -> atom value
87 val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
93 val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DSubst.sig13 type subst type
19 val empty : subst
21 val null : subst -> bool
23 val size : subst -> int
25 val peek : subst -> Term.var -> Term.term option
27 val insert : subst -> Term.var * Term.term -> subst
29 val singleton : Term.var * Term.term -> subst
31 val toList : subst -> (Term.var * Term.term) list
33 val fromList : (Term.var * Term.term) list -> subst
53 val subst : subst -> Term.term -> Term.term value
[all...]
H A DSubsume.sig32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
33 (Thm.clause * Subst.subst * 'a) option
38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
39 (Thm.clause * Subst.subst * 'a) option
47 val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option
49 val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option
H A DAtom.sig81 val subst : Subst.subst -> atom -> atom value
87 val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
93 val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/
H A DcommonUnifScript.sml12 `!subst source z.
14 (!m n. m < n ==> (subst m) SUBMAP (subst n)) /\
15 (!n. DISJOINT (FDOM (subst n)) (source n)) /\
16 (!n. z < n ==> (FDOM (subst n) UNION (source n) = FDOM (subst z) UNION (source z))))
17 ==> ?x. !n. x < n ==> ((subst n) = (subst x)))`,
32 `?n.m < n /\ subst m <> subst
[all...]
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A DCond_rewrite.sig15 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list)
19 :term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list
21 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DUnify.sig13 term list -> term -> term -> (term,term)subst -> (term,term)subst
14 val simp_unify_terms : term list -> term -> term -> (term,term)subst
18 val deref_tmenv : (term,term)subst -> term -> term
22 val restrict_tmenv :(term -> bool) -> (term,term)subst -> (term,term)subst
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A Dstringfindreplace.sig4 val subst : {redex:string,residue:string} list -> string -> string value
H A DFinalType-sig.sml39 val type_subst : (hol_type,hol_type) Lib.subst -> hol_type -> hol_type
41 val match_type : hol_type -> hol_type -> (hol_type,hol_type) Lib.subst
44 -> (hol_type,hol_type) Lib.subst
47 -> (hol_type,hol_type)Lib.subst
48 -> (hol_type,hol_type)Lib.subst
50 -> (hol_type,hol_type) Lib.subst * hol_type list
51 -> (hol_type,hol_type) Lib.subst * hol_type list
55 val ty_sub : (hol_type,hol_type) Lib.subst -> hol_type ->
H A DFinalTerm-sig.sml6 type ('a,'b)subst = ('a,'b)Lib.subst
64 val subst : (term,term) subst -> term -> term value
65 val inst : (hol_type,hol_type) subst -> term -> term
69 -> (term,term)subst * (hol_type,hol_type)subst
70 -> ((term,term)subst * term set) *
71 ((hol_type,hol_type)subst * hol_type list)
73 -> (term,term)subst * (hol_typ
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DarmLib.sig14 val RES_MP1_TAC : (term frag list, term frag list) subst -> thm -> tactic
15 val RES_MP_TAC : (term frag list, term frag list) subst -> thm -> tactic
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DarmLib.sig12 val RES_MP1_TAC : (term frag list, term frag list) subst -> thm -> tactic
13 val RES_MP_TAC : (term frag list, term frag list) subst -> thm -> tactic
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DRules.sig3 type ('a,'b) subst = ('a,'b)Lib.subst
14 val IT_EXISTS : (term,term) subst -> thm -> thm
H A DwfrecUtils.sig25 val match_type : 'a -> hol_type -> hol_type -> (hol_type,hol_type)subst
27 -> (term,term) subst * (hol_type,hol_type) subst
/seL4-l4v-10.1.1/HOL4/src/1/
H A DAbbrev.sml17 type ('a,'b)subst = ('a,'b) Lib.subst
H A DAbbrev.sig19 type ('a,'b)subst = ('a,'b) Lib.subst
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/
H A DelsaUtils.sig43 val STRONG_INST :{term_substitution:(term,term)Lib.subst, theorem:thm} -> thm
45 :{theorem:thm,type_substitution:(hol_type,hol_type) Lib.subst} -> thm
46 val STRONG_INST_TY_TERM :{term_substitution:(term,term) Lib.subst,
48 type_substitution:(hol_type,hol_type)Lib.subst} ->
53 -> (term,term) Lib.subst * (hol_type,hol_type) Lib.subst

Completed in 153 milliseconds

1234567891011>>