Searched refs:subst (Results 1 - 25 of 351) sorted by last modified time

1234567891011>>

/seL4-l4v-10.1.1/l4v/misc/vim/
H A Disabelle.vim183 syn keyword IsabelleCommandMethod insert subst hypsubst
228 syn keyword IsabelleCommandRule ssubst subst
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dselftest.sml305 (Formula.subst (S [(NV"y", V"z")]) (F`!x. x = $y`));
310 (Formula.subst (S [(NV"y", V"x")]) (F`!x. x = $y`));
315 (Formula.subst (S [(NV"y", V"x")])
323 Subst.subst (Subst.unify Subst.empty tm1 tm2) tm1;
359 Thm.subst (S [(NV"y0",T`$x`),(NV"y1",T`$y`),(NV"x1",T`$z`),(NV"x0",T`$x`)]) th0;
367 val th1 = Thm.subst (S [(NV"x", Term.Fn (NF"f", [V"y"]))]) th0;
368 val th2 = Thm.subst (S [(NV"y", C"c")]) th1;
1083 Formula.subst sub fm
H A DUnits.sml90 val rth = Thm.subst sub rth
H A DTptp.sml608 | Literal l => Literal (Literal.subst sub l);
1006 | Proof.Subst _ => "subst"
H A DUnits.sig41 val match : units -> Literal.literal -> (unitThm * Subst.subst) option
H A DThm.sig112 (* -------- subst s *)
116 val subst : Subst.subst -> thm -> thm value
H A DThm.sml143 (* -------- subst s *)
147 fun subst sub (th as Thm (cl,inf)) = function
149 val cl' = LiteralSet.subst sub cl
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 DSubsume.sml80 {empty : (Thm.clause * Subst.subst * 'a) list,
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 DSubst.sml15 datatype subst = Subst of Term.term NameMap.map; type
67 fun subst sub = function
109 (* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *)
114 fun f (v,tm,s) = insert s (v, subst sub2 tm)
230 else solve' sub (subst sub tm1) (subst sub tm2) rest
H A DRule.sml85 val symTh = Thm.subst sub symmetry
133 val th = Thm.subst sub transitivity
505 val symTh = Thm.subst sub symmetry
580 | SOME sub => expandAbbrevs (Thm.subst sub th);
607 fun freshVars th = Thm.subst (Subst.freshVars (Thm.freeVars th)) th;
616 (* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *)
634 | Joinable of Subst.subst
707 else raise Bug "Rule.factor.init_edges: empty subst"
781 fun fact sub = removeSym (Thm.subst sub th)
H A DRewrite.sml148 order (tm, Subst.subst (Subst.normalize sub) r) = SOME GREATER
251 val tm' = Subst.subst sub r
257 (tm', Thm.subst sub th)
472 val tm' = Subst.subst (Subst.normalize sub) r
H A DRule.sig262 (* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *)
270 val factor' : Thm.clause -> Subst.subst list
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dselftest.sml305 (Formula.subst (S [(NV"y", V"z")]) (F`!x. x = $y`));
310 (Formula.subst (S [(NV"y", V"x")]) (F`!x. x = $y`));
315 (Formula.subst (S [(NV"y", V"x")])
323 Subst.subst (Subst.unify Subst.empty tm1 tm2) tm1;
359 Thm.subst (S [(NV"y0",T`$x`),(NV"y1",T`$y`),(NV"x1",T`$z`),(NV"x0",T`$x`)]) th0;
367 val th1 = Thm.subst (S [(NV"x", Term.Fn (NF"f", [V"y"]))]) th0;
368 val th2 = Thm.subst (S [(NV"y", C"c")]) th1;
1083 Formula.subst sub fm
H A DUnits.sml90 val rth = Thm.subst sub rth
H A DTptp.sml608 | Literal l => Literal (Literal.subst sub l);
1006 | Proof.Subst _ => "subst"
H A DUnits.sig41 val match : units -> Literal.literal -> (unitThm * Subst.subst) option
H A DThm.sig112 (* -------- subst s *)
116 val subst : Subst.subst -> thm -> thm value
H A DThm.sml143 (* -------- subst s *)
147 fun subst sub (th as Thm (cl,inf)) = function
149 val cl' = LiteralSet.subst sub cl
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 DSubsume.sml80 {empty : (Thm.clause * Subst.subst * 'a) list,
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 DSubst.sml15 datatype subst = Subst of Term.term NameMap.map; type
67 fun subst sub = function
109 (* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *)
114 fun f (v,tm,s) = insert s (v, subst sub2 tm)
230 else solve' sub (subst sub tm1) (subst sub tm2) rest
H A DRule.sml85 val symTh = Thm.subst sub symmetry
133 val th = Thm.subst sub transitivity
505 val symTh = Thm.subst sub symmetry
580 | SOME sub => expandAbbrevs (Thm.subst sub th);
607 fun freshVars th = Thm.subst (Subst.freshVars (Thm.freeVars th)) th;
616 (* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *)
634 | Joinable of Subst.subst
707 else raise Bug "Rule.factor.init_edges: empty subst"
781 fun fact sub = removeSym (Thm.subst sub th)

Completed in 105 milliseconds

1234567891011>>