Searched refs:count (Results 151 - 175 of 316) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/pgcl/src/
H A DmeasureScript.sml516 (MP_TAC o Q.SPEC `\n. BIGUNION (IMAGE f (count n))`)
520 BIGUNION (IMAGE (\n. BIGUNION (IMAGE f (count n))) UNIV)`
526 ++ Q.EXISTS_TAC `BIGUNION (IMAGE f (count (SUC x')))`
630 measure m (BIGUNION (IMAGE f (count n))))``,
688 lam (BIGUNION (IMAGE f (count n)) INTER g))``,
840 `(lam g = lam (BIGUNION (IMAGE f (count n)) INTER g) +
841 lam (COMPL (BIGUNION (IMAGE f (count n))) INTER g)) /\
843 lam (COMPL (BIGUNION (IMAGE f (count n))) INTER g)`
846 >> (Suff `BIGUNION (IMAGE f (count n)) IN lambda_system gsig lam`
1185 ++ Q.EXISTS_TAC `\n. f n DIFF (BIGUNION (IMAGE f (count
[all...]
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DgroupInstancesScript.sml70 Zadd_def |- !n. Z n = <|carrier := count n; id := 0; op := (\i j. (i + j) MOD n)|>
75 Zadd_carrier |- !n. (Z n).carrier = count n
84 #! Zadd_eval |- !n. ((Z n).carrier = count n) /\ (!x y. (Z n).op x y = (x + y) MOD n) /\ ((Z n).id = 0)
177 add_mod_carrier_alt |- !n. (add_mod n).carrier = count n
231 <| carrier := count n;
259 ``!n. ((Z n).carrier = count n) /\
283 (* Theorem: (Z n).carrier = count n *)
286 !n. (Z n).carrier = count n
714 `{i | 0 < i /\ i < n /\ coprime n i} SUBSET count n` by rw[SUBSET_DEF] >>
1331 (* Theorem: (add_mod n).carrier = count
[all...]
/seL4-l4v-master/HOL4/src/integer/
H A DjrhCore.sml108 (* count a and b terms, also pair each count with the total number of free
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A DarmLib.sml232 val count = pad 8 o pad0 4 o lower o toHexString value
234 List.app (fn (n,i) => output_code ostrm (count (start + n)) i)
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DElementSet.sml281 fun count p = function
285 fn Set m => KM.count mp m
H A DSet.sml267 fun count p = function
271 fn Set m => Map.count mp m
H A DMap.sig148 val count : ('key * 'a -> bool) -> ('key,'a) map -> int value
H A DUseful.sig107 (* Lists: note we count elements from 0. *)
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DElementSet.sml281 fun count p = function
285 fn Set m => KM.count mp m
H A DSet.sml267 fun count p = function
271 fn Set m => Map.count mp m
H A DMap.sig148 val count : ('key * 'a -> bool) -> ('key,'a) map -> int value
H A DUseful.sig107 (* Lists: note we count elements from 0. *)
/seL4-l4v-master/HOL4/examples/algebra/field/
H A DfieldInstancesScript.sml77 GF_property |- !p. ((GF p).carrier = count p) /\ ((GF p).sum = add_mod p) /\
240 ``!p. ((GF p).carrier = count p) /\
249 (* Proof: by GF_def, i.e. (GF p).carrier = count p. *)
470 > val it = |- !n. ZN n = <|carrier := count n; sum := add_mod n; prod := times_mod n|> : thm
586 Note (ZN n).carrier = count n by ZN_eval
588 Also FINITE (count n) by FINITE_COUNT
598 `(ZN n).carrier = count n` by rw[ZN_eval] >>
737 Since (ZN n).carrier = count n by ZN_def
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dstatistics.cpp524 void Statistics::setCount(int which, POLYUNSIGNED count)
532 counterAddrs[which][length] = (unsigned char)(count & 0xff);
533 count = count >> 8;
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Djedit_resources.scala122 def content(): Bytes = Bytes(this.buf, 0, this.count)
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_resources.scala122 def content(): Bytes = Bytes(this.buf, 0, this.count)
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sml305 "count leading zeroes"
684 fun arm_run trace prog options count =
688 ptree_arm_run trace (prog, state) count
701 val count = input_number (fn i => ~1 <= i) "Enter number of cycles: " value
703 case time (arm_run (int_to_trace trace) prog options) count
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/prog/
H A Dm0_progLib.sml60 [["PSR", "REG", "count", "pcinc"],
61 ["MEM", "REG", "count", "pcinc"],
62 ["REG", "count", "pcinc"]
67 ["PSR.N", "PSR.Z", "PSR.C", "PSR.V", "count", "REG", "MEM"]
307 | "m0_prog$m0_count" => K "count"
/seL4-l4v-master/HOL4/src/sort/
H A DsortingScript.sml370 ?f. (BIJ f (count(LENGTH l1)) (count(LENGTH l1)) /\
886 `PERM (SET_TO_LIST (count n)) (COUNT_LIST n)`,
895 `SIGMA f (count n) = SUM (GENLIST f n)`,
910 `(!m. m < n ==> (g m = SIGMA (\x. f (x + k * m)) (count k))) ==>
911 (SIGMA f (count (k * n)) = SIGMA g (count n))`,
921 `SIGMA (\m. SIGMA (f m) (count a)) (count b) = SIGMA (\m. f (m DIV a) (m MOD a)) (count (
[all...]
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyProductScript.sml300 > EVAL ``POW (count 2)``;
301 val it = |- POW (count 2) = {{1; 0}; {1}; {0}; {}}: thm
310 > EVAL ``IMAGE (\s. SUM_SET s) (POW (count 2))``;
311 val it = |- IMAGE (\s. SUM_SET s) (POW (count 2)) = {1; 0}: thm -- need a BAG when not distinct.
312 > EVAL ``IMAGE (\s. prod s) (POW (count 2))``;
314 val it = |- IMAGE (\s. prod s) (POW (count 2)) = {prod {1; 0}; prod {1}; prod {0}; prod {}}: thm
315 > EVAL ``IMAGE (\s. prod s) (POW (IMAGE SUC (count 2)))``;
317 val it = |- IMAGE (\s. prod s) (POW (IMAGE SUC (count 2))) = {prod {2; 1}; prod {2}; prod {1}; prod {}}: thm
321 EVAL ``IMAGE (\s. IMAGE (\c. X + ###(SUC c)) s) (POW (count 2))``;
324 > EVAL ``IMAGE (\s. IMAGE (\c. Y + (SUC c)) s) (POW (count
[all...]
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DConsThms.sml172 fun mk_def_term ftn_var old_type (app_con::app_con_list) count =
179 rhs = Term.mk_numeral (Arbnum.fromInt count)}
180 (* rhs = mk_const {Name = Lib.int_to_string count,
189 (count + 1)}
397 fun helper count (arg::more_args) =
401 ("_arg"^(Lib.int_to_string count)) type_of_ftn
420 (helper (count + 1) more_args)
/seL4-l4v-master/HOL4/examples/miller/formalize/
H A Dextra_realScript.sml500 (!n. 0 <= f n) /\ INJ j1 (count n1) UNIV /\
501 IMAGE j1 (count n1) SUBSET IMAGE j2 (count n2) ==>
594 Q.SPECL [`h`, `s`, `count N INTER s`] o
597 >> Know `FINITE (count N INTER s)`
668 Q.SPECL [`h`, `s`, `count n INTER s`] o
671 >> Know `FINITE (count n INTER s)`
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffConjugateScript.sml135 !x. x IN R ==> Conj x SUBSET IMAGE (conj x) (count (r <:> s))
203 INJ (conj x) (count (order (ZN (forder x)).prod (CARD B))) (Conj x)
205 SURJ (conj x) (count (order (ZN (forder x)).prod (CARD B))) (Conj x)
207 BIJ (conj x) (count (order (ZN (forder x)).prod (CARD B))) (Conj x)
209 (Conj x = IMAGE (conj x) (count (order (ZN (forder x)).prod (CARD B))))
705 !x. x IN R ==> (Conj x) SUBSET (IMAGE (conj x) (count (r <:> s))) *)
713 so y IN IMAGE (conj x) (count d) by IN_IMAGE, IN_COUNT
714 or (Conj x) SUBSET (IMAGE (conj x) (count d)) by SUBSET_DEF
719 !x. x IN R ==> (Conj x) SUBSET (IMAGE (conj x) (count (r <:> s)))``,
729 Let c = count (
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A DbackgroundLib.sml55 (* count inferences and record time *)
/seL4-l4v-master/HOL4/src/TeX/
H A DmungeTools.sml161 fun recurse count acc =
179 NONE => (warn ((count,0),
188 | SOME _ => (warn ((count,0),
195 recurse (count + 1) acc'

Completed in 169 milliseconds

1234567891011>>