Searched refs:chain (Results 1 - 25 of 57) sorted by relevance

123

/seL4-l4v-master/HOL4/examples/miller/prob/
H A Dprob_trichotomyTools.sml24 fun chain f seq 0 = [] function
25 | chain f seq n =
30 th :: chain f seq (n - 1)
36 Count.apply (chain ``prob_trichotomy`` ``prob_pseudo 103 95 75 0``) 10;
/seL4-l4v-master/HOL4/src/tfl/examples/sorting/
H A DsortingScript.sml20 * a "chain" predicate that holds just when the relation R holds between *
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DProof.h33 // (offline mode) this class. Each call to 'root()' or 'chain()' produces a new clause. The first
34 // clause has ID 0, the next 1 and so on. These are the IDs passed to 'chain()'s 'cs' parameter.
38 virtual void chain (const vec<ClauseId>& cs, const vec<Var>& xs) {} function in struct:ProofTraverser
H A DProof.C142 trav->chain(chain_id, chain_var);
273 case -2 : // a chain that has been visited before. write it out now
302 case -1 : // this root/chain has not been visited before
317 } else { // if chain, process antecedent clauses first
324 c2c[id] = -2; // means a chain that has been visited but not written out yet
405 trav.chain(chain_id, chain_var);
H A DMain.C149 void chain (const vec<ClauseId>& cs, const vec<Var>& xs) { function in struct:Checker
/seL4-l4v-master/HOL4/src/metis/
H A DmatchTools.sml46 fun chain [] = [] function
47 | chain [_] = []
48 | chain (x :: (xs as y :: _)) = (x, y) :: chain xs;
146 fun vunify_type tyvarP = vunifyl_type tyvarP [] o chain;
212 fun vunify varP = vunifyl varP ([], []) o chain;
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODESIG.sml52 val defaultTypeVarMap: (int->int) * level -> typeVarMap (* The end of the chain. *)
57 (* Mark in the cache chain that some type constructors are new. *)
H A DTYPETREESIG.sml65 (* Follow a chain of unified type variables *)
/seL4-l4v-master/HOL4/src/HolSat/
H A DminisatParse.sml80 (* parse resolution chain *)
94 (* parse and resolve a chain : assumes all dependencies already calculated *)
155 in if isch then readTrace lfn cl sva vc clauseth fin (id+1) (* chain*)
162 (*build the clause/chain list *)
/seL4-l4v-master/HOL4/src/num/reduce/src/
H A DArithconv.sml251 and chain = INST [xv |-> xn, yv |-> yn, pv |-> pn, value
254 MP (MP (MP chain p1) p2) p3
283 and chain = INST [xv |-> xn, yv |-> yn, pv |-> pn, value
286 MP (MP (MP chain p1) p2) p3
/seL4-l4v-master/seL4/manual/tools/
H A Dgen_invocations.py34 arch_types = list(itertools.chain(*syscall_stub_gen.init_arch_types(WORD_SIZE).values()))
/seL4-l4v-master/HOL4/src/coretypes/
H A DposetScript.sml92 ``chain ((s,r) : 'a poset) c <=>
267 chain (s,r) c /\ lub (s,r) c x ==>
274 chain (s,r) c /\ glb (s,r) c x ==>
/seL4-l4v-master/HOL4/src/finite_maps/
H A DwotScript.sml70 `chain (C:'x set set) = !a b. a IN C /\ b IN C ==> a cpl b`;
89 `uncl (c:'x set set) = !w. w SUBSET c /\ chain w ==> BIGUNION w IN c`;
104 (* We will prove, in imitation of Halmos/Zermelo/Zorn, chain (t0) . *)
130 (* We set out to prove that t0 is a chain. *)
217 (* "Since the union of a chain of comparable sets is comparable... ." *)
242 val chain_t0 = prove (``chain (t0:'x set set)``,
254 (* Imitation of gAC_lem for t0, now known to be a chain: *)
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/
H A DwellorderScript.sml1084 `!c. chain c R ==> upper_bounds c R <> {}`
1445 val chain = new_definition ("chain", value
1448 val _ = overload_on ("chain",``Chain``);
1464 ``!r:'a#'a->bool s:'a->bool. chain r s = chain s r``,
1465 REWRITE_TAC [chain, chain_def] THEN SET_TAC []);
1476 (!P. chain P r ==> upper_bounds P r <> {}) ==>
1479 (!P. chain(r) P ==> (?y. fl(r) y /\ !x. P x ==> r(x,y))) ==>
1485 (!t. chain
[all...]
/seL4-l4v-master/HOL4/examples/logic/folcompactness/
H A DfolPropScript.sml99 >- ((* upper bounds of chain t *)
100 rename [���chain t _���, ���upper_bounds t _ ��� ������] >>
/seL4-l4v-master/HOL4/examples/set-theory/vbg/
H A DordinalScript.sml16 chain A R C ��� C ��� A ��� ���x y. x ��� C ��� y ��� C ��� R x y ��� R y x
/seL4-l4v-master/isabelle/src/HOL/SPARK/Manual/document/
H A Dintro.tex117 \caption{\SPARK{} program verification tool chain}
121 tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
/seL4-l4v-master/l4v/isabelle/src/HOL/SPARK/Manual/document/
H A Dintro.tex117 \caption{\SPARK{} program verification tool chain}
121 tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
/seL4-l4v-master/HOL4/src/pred_set/src/
H A Dset_relationScript.sml1346 chain s r =
1368 { k | chain k r /\ k <> {} /\
1369 !C. chain C r /\ C SUBSET k /\
1377 `!x s r. chain s r /\ x IN s ==> x IN domain r /\ x IN range r`,
1399 `chain C r /\ C SUBSET k2 /\ C SUBSET k1`
1445 chain (BIGUNION (fchains r)) r /\
1477 chain C r /\
1611 (!t. chain t r ==> upper_bounds t r <> {})
/seL4-l4v-master/graph-refine/
H A Dstack_logic.py880 chain = []
896 chain.append (fname)
897 tag = 'fun%d' % len (chain)
901 if chain == []:
903 recursion_trace.append (' created fun chain %s' % chain)
/seL4-l4v-master/HOL4/src/unwind/
H A DunwindLib.sml493 fun loops_containing_line line graph chain =
495 (filter (fn (_,predecs) => tmem (Lib.trye hd chain) predecs) graph)
496 val not_in_chain = filter (fn line => not (tmem line chain)) successors
497 val new_chains = map (fn line => line::chain) not_in_chain
501 in if tmem line successors then (rev chain)::new_loops
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp152 void chain (const vec<ClauseId>& cs, const vec<Var>& xs) { function in struct:Checker
308 // create minisat chain for a "CL" line of zChaff proof trace
327 // create minisat chain for a "VAR" line of zChaff proof trace
351 // create minisat chain for "CONF" line of zChaff proof trace
/seL4-l4v-master/HOL4/src/datatype/record/
H A DRecordType.sml446 1. that a complete chain of updates over any value is
447 equivalent to a chain of updates over ARB. This particular
/seL4-l4v-master/HOL4/polyml/basis/
H A DForeignMemory.sml152 (* It would be possible to chain the free list in the C memory
/seL4-l4v-master/HOL4/examples/imperative/
H A Dnecec2010.sml267 Given a list of assumptions, converts them into a chain of refinements.

Completed in 243 milliseconds

123