/seL4-l4v-master/HOL4/examples/pgcl/src/ |
H A D | measureScript.sml | 516 (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 D | groupInstancesScript.sml | 70 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 D | jrhCore.sml | 108 (* count a and b terms, also pair each count with the total number of free
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | armLib.sml | 232 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 D | ElementSet.sml | 281 fun count p = function 285 fn Set m => KM.count mp m
|
H A D | Set.sml | 267 fun count p = function 271 fn Set m => Map.count mp m
|
H A D | Map.sig | 148 val count : ('key * 'a -> bool) -> ('key,'a) map -> int value
|
H A D | Useful.sig | 107 (* Lists: note we count elements from 0. *)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | ElementSet.sml | 281 fun count p = function 285 fn Set m => KM.count mp m
|
H A D | Set.sml | 267 fun count p = function 271 fn Set m => Map.count mp m
|
H A D | Map.sig | 148 val count : ('key * 'a -> bool) -> ('key,'a) map -> int value
|
H A D | Useful.sig | 107 (* Lists: note we count elements from 0. *)
|
/seL4-l4v-master/HOL4/examples/algebra/field/ |
H A D | fieldInstancesScript.sml | 77 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 D | statistics.cpp | 524 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 D | jedit_resources.scala | 122 def content(): Bytes = Bytes(this.buf, 0, this.count)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_resources.scala | 122 def content(): Bytes = Bytes(this.buf, 0, this.count)
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sml | 305 "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 D | m0_progLib.sml | 60 [["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 D | sortingScript.sml | 370 ?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 D | polyProductScript.sml | 300 > 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 D | ConsThms.sml | 172 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 D | extra_realScript.sml | 500 (!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 D | ffConjugateScript.sml | 135 !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 D | backgroundLib.sml | 55 (* count inferences and record time *)
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | mungeTools.sml | 161 fun recurse count acc = 179 NONE => (warn ((count,0), 188 | SOME _ => (warn ((count,0), 195 recurse (count + 1) acc'
|