/seL4-l4v-10.1.1/l4v/misc/vim/ |
H A D | isabelle.vim | 183 syn keyword IsabelleCommandMethod insert subst hypsubst 228 syn keyword IsabelleCommandRule ssubst subst
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 305 (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 D | Units.sml | 90 val rth = Thm.subst sub rth
|
H A D | Tptp.sml | 608 | Literal l => Literal (Literal.subst sub l); 1006 | Proof.Subst _ => "subst"
|
H A D | Units.sig | 41 val match : units -> Literal.literal -> (unitThm * Subst.subst) option
|
H A D | Thm.sig | 112 (* -------- subst s *) 116 val subst : Subst.subst -> thm -> thm value
|
H A D | Thm.sml | 143 (* -------- subst s *) 147 fun subst sub (th as Thm (cl,inf)) = function 149 val cl' = LiteralSet.subst sub cl
|
H A D | Subsume.sig | 32 (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 D | Subsume.sml | 80 {empty : (Thm.clause * Subst.subst * 'a) list,
|
H A D | Subst.sig | 13 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 D | Subst.sml | 15 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 D | Rule.sml | 85 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 D | Rewrite.sml | 148 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 D | Rule.sig | 262 (* 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 D | selftest.sml | 305 (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 D | Units.sml | 90 val rth = Thm.subst sub rth
|
H A D | Tptp.sml | 608 | Literal l => Literal (Literal.subst sub l); 1006 | Proof.Subst _ => "subst"
|
H A D | Units.sig | 41 val match : units -> Literal.literal -> (unitThm * Subst.subst) option
|
H A D | Thm.sig | 112 (* -------- subst s *) 116 val subst : Subst.subst -> thm -> thm value
|
H A D | Thm.sml | 143 (* -------- subst s *) 147 fun subst sub (th as Thm (cl,inf)) = function 149 val cl' = LiteralSet.subst sub cl
|
H A D | Subsume.sig | 32 (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 D | Subsume.sml | 80 {empty : (Thm.clause * Subst.subst * 'a) list,
|
H A D | Subst.sig | 13 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 D | Subst.sml | 15 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 D | Rule.sml | 85 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)
|