Searched refs:exp (Results 76 - 100 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_FUNCTIONS.sml32 fun mkEnv([], exp) = exp
33 | mkEnv(decs, exp) = Newenv(decs, exp)
79 | codeProps (Newenv(decs, exp)) =
80 List.foldl (fn (d, r) => bindingProps d andb r) (codeProps exp) decs
82 | codeProps (Handle { exp, handler, ... }) =
84 (codeProps exp orb PROPWORD_NORAISE) andb codeProps handler
174 | codeProps(Raise exp) = codeProps exp and
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dlisp_proofScript.sml98 ``!exp x y zstack alist l.
99 (lisp_numberp (exp,x,y,z,stack,alist,l) =
100 (LISP_NUMBERP exp,x,y,z,stack,alist,l)) /\
101 (lisp_symbolp (exp,x,y,z,stack,alist,l) =
102 (LISP_SYMBOLP exp,x,y,z,stack,alist,l)) /\
103 (lisp_consp (exp,x,y,z,stack,alist,l) =
104 (LISP_CONSP exp,x,y,z,stack,alist,l)) /\
105 (lisp_atomp (exp,x,y,z,stack,alist,l) =
106 (LISP_ATOMP exp,x,y,z,stack,alist,l)) /\
337 ``repeat_cdr(exp,Va
[all...]
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dautomation_lemmasScript.sml455 (case_tree (y:exp) xs)
460 case_enum y ((n,x)::xs) = If Equal [y; Const (name n)] x (case_enum (y:exp) xs)
467 val x_tm = ���x:exp���
488 val new_x = mk_var("x_" ^ vn, ���:exp���)
530 val x0 = mk_var("x0",���:exp���)
555 val x = mk_var(s ^ "_exp",���:exp���)
635 (* exp *)
638 exp (Const n) = list [Name "Const"; Num n] ���
639 exp (Var n) = list [Name "Var"; Num n] ���
640 exp (O
[all...]
/seL4-l4v-master/HOL4/src/real/
H A DtranscScript.sml65 (* The three functions we define by series are exp, sin, cos *)
77 val exp = new_definition("exp", value
78 ���exp(x) = suminf(\n. (^exp_ser) n * (x pow n))���);
87 (* Show the series for exp converges, using the ratio test *)
91 ���!x. (\n. (^exp_ser) n * (x pow n)) sums exp(x)���,
95 GEN_TAC THEN REWRITE_TAC[exp] THEN MATCH_MP_TAC SUMMABLE_SUM THEN
222 (* Now at last we can get the derivatives of exp, sin and cos *)
232 ���!x. (exp diffl exp(
[all...]
H A DcomplexScript.sml1432 ``complex_exp (z:complex) = exp(RE z) * (cos (IM z),sin (IM z))``);
1434 val _ = overload_on ("exp", Term`$complex_exp`);
1437 ``!x:real. exp (i * x) = (cos x,sin x)``,
1442 ``!z:complex. modu z * exp (i * arg z) = z``,
1447 ``!z:complex w:complex. exp (z + w) = exp z * exp w``,
1452 ``!z:complex. exp (-z) = inv (exp z)``,
1460 ``!z:complex w:complex. exp (
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_logicScript.sml207 (!fname params exp var sem.
208 fname IN FDOM ctxt /\ (ctxt ' fname = (params,WITNESS_FUN exp var,sem)) ==>
209 term_ok ctxt exp /\ ALL_DISTINCT (var::params) /\
210 LIST_TO_SET (free_vars exp) SUBSET LIST_TO_SET (var::params) /\
212 (?v. isTrue (EvalTerm (FunVarBind (var::params) (v::args),ctxt) exp)) ==>
213 isTrue (EvalTerm (FunVarBind (var::params) ((sem args)::args),ctxt) exp))`;
545 (!f params exp var_name witness ctxt.
546 f IN FDOM ctxt /\ (ctxt ' f = (params,WITNESS_FUN exp var_name,witness)) ==>
547 MilawaTrue ctxt (Or (Equal exp ^nnil)
548 (Not (Equal (mLamApp (var_name::params) exp
[all...]
/seL4-l4v-master/HOL4/src/1/
H A DPmatch.sml579 fun mk_case1 tybase (exp, plist) =
580 case match_info tybase (type_names (type_of exp))
585 val ty' = list_mk_fun (type_of exp::map type_of fns,
588 in list_mk_comb(inst theta c,exp::fns)
591 fun mk_case2 v (exp, plist) =
597 in if aconv v exp then switch
598 else mk_literal_case(mk_abs(v,switch),exp)
601 fun mk_case tybase (exp, plist) =
606 mk_case1 tybase (exp, plist)
608 mk_case2 (last col0) (exp, plis
742 val (exp, cases) = if is_case1 tybase M' value
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_bigopsScript.sml264 exp in x4
546 !exp cs2 x0 x1 x2 x3 x4 x5 xs ys io xbp.
548 ((exp,cs2) = sexp_lex_parse (cs,s,task,mem)) ==>
554 (exp,y1,y2,y3,y4,y5,LIST_UPDATE_NTH xs2 xs ++ ys,REPLACE_INPUT_IO cs2 io,xbp,amnt))) (cs,s,task,mem)``,
571 \\ Q.PAT_X_ASSUM `!exp.bbb` MATCH_MP_TAC
602 \\ `lisp_parse_mem_inv x5 ((x =+ exp) mem) (LENGTH xs + LENGTH ys) amnt (UPDATE_NTH x exp xs) ys` by
606 \\ `LENGTH xs = LENGTH (UPDATE_NTH x exp xs)` by SIMP_TAC std_ss [LENGTH_UPDATE_NTH]
609 \\ Q.PAT_X_ASSUM `!expp.bbb` (MP_TAC o Q.SPECL [`exp'`,`cs2`,`exp`,`Va
[all...]
/seL4-l4v-master/HOL4/src/integer/
H A DIntDP_Munge.sml125 fun elim_div_mod0 exp t = let
130 val (c1, c2) = if exp then (RAND_CONV o LAND_CONV, RAND_CONV o RAND_CONV)
133 (dest_div to_elim, c1, c2, if exp then INT_DIV_P else INT_DIV_FORALL_P)
135 if exp then INT_MOD_P else INT_MOD_FORALL_P)
148 | _ => FIRST_CONV (map elim_t divmods) THENC elim_div_mod0 exp
156 val exp = goal_qtype t = qsEXISTS value
163 (if passed_a_binder then TRY_CONV (elim_div_mod0 exp)
286 fun elim_div_mod0 exp t = let
291 (dest_div to_elim, if exp then (DIV_P, RAND_CONV)
293 handle HOL_ERR _ => (dest_mod to_elim, if exp the
311 val exp = goal_qtype t = qsEXISTS andalso value
[all...]
H A DOmegaMath.sig118 d | exp
119 where exp includes at least one variable from x1 .. xn.
126 ~(d | exp)
127 where exp includes at least one variable from x1 .. xn. It
/seL4-l4v-master/HOL4/examples/algebra/monoid/
H A DsubmonoidScript.sml54 submonoid_exp |- !g h. h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n
191 (* Theorem: h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n *)
193 Base: h.exp x 0 = x ** 0
194 LHS = h.exp x 0
199 Step: h.exp x n = x ** n ==> h.exp x (SUC n) = x ** SUC n
200 LHS = h.exp x (SUC n)
201 = h.op x (h.exp x n) by monoid_exp_SUC
202 = x * (h.exp x n) by submonoid_property
209 ``!(g:'a monoid) h. h << g ==> !x. x IN H ==> !n. h.exp
[all...]
/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DintegralDomainScript.sml60 ## = r.sum.exp
65 ** = r.prod.exp
87 (f*.op = $* ) /\ (f*.exp = $** )
216 For f*.exp = r.prod.exp
222 (F* = R+) /\ (f*.id = #1) /\ (f*.op = r.prod.op) /\ (f*.exp = r.prod.exp)``,
479 = case OLEAST k. 0 < k /\ (f*.exp x k = f*.id) of NONE => 0 | SOME k => k by period_def
512 or ?n. n <> 0 /\ (f*.exp x n = f*.id) by integral_domain_nonzero_mult_property
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A Drefine.sml242 fun lift_cond exp =
243 let val t = dest_C exp (* eliminate the C *)
245 if is_let t then (* exp = LET (\v. N) M *)
260 val th2 = prove (mk_eq(exp,t2),
270 REFL exp
/seL4-l4v-master/HOL4/polyml/basis/
H A DSML90.sml39 val exp : real -> real value
74 fun exp x = let val r = Real.Math.exp x in if Real.isFinite r then r else raise Exp end function
H A DRealSignature.sml80 val toManExp : real -> {man : real, exp : int}
81 val fromManExp : {man : real, exp : int} -> real
H A DIEEE_REAL.sml41 { class : float_class, sign : bool, digits : int list, exp : int }
H A DMATH.sml36 val exp : real -> real value
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DtestTypesScript.sml167 | Let of dec => exp;
169 exp = Exp1 of atexp
170 | Exp2 of exp => atexp
176 rule = Rule of pat => exp;
181 valbind = Single of pat => exp
182 | Multi of pat => exp => valbind
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DcongruencesScript.sml88 ((Zstar p).exp a (CARD (Zstar p).carrier) = (Zstar p).id): thm
158 > val it = |- !p. prime p ==> !x. 0 < x /\ x < p ==> ((Zstar p).inv x = (Zstar p).exp x (order (Zstar p) x - 1)) : thm
173 `(Zstar p).exp a (p-2) = a**(p-2) MOD p` by rw_tac std_ss[Zstar_exp] >>
280 > val it = |- !p. prime p ==> !x. 0 < x /\ x < p ==> ((mult_mod p).inv x = (mult_mod p).exp x (order (mult_mod p) x - 1)) : thm
294 `(mult_mod p).exp a (p-2) = (a**(p-2) MOD p)` by rw_tac std_ss[mult_mod_exp] >>
297 `(mult_mod p).exp a (p-2) IN (mult_mod p).carrier` by rw_tac std_ss[group_exp_element] >>
H A DgroupOrderScript.sml125 generated_exp |- !g a z. a IN G /\ z IN Gen a ==> !n. (gen a).exp z n = z ** n
166 Generated_subset_exp |- !g s. (gen_set s).exp = $**
500 `!x. x IN H ==> !n. h.exp x n = x ** n` by metis_tac[subgroup_exp] >>
590 ((Invertibles g).exp x (order (Invertibles g) x) = (Invertibles g).id): thm
598 (Invertibles g).exp x (order (Invertibles g) x) =
602 and (Invertibles g).exp = $** by Invertibles_property
687 (* Theorem: !a. a IN G ==> (Gen a = IMAGE (g.exp a) univ(:num)) *)
691 ``!(g:'a group) a. a IN G ==> (Gen a = IMAGE (g.exp a) univ(:num))``,
830 (* Theorem: a IN G /\ z IN (Gen a) ==> !n. (gen a).exp z n = z ** n *)
832 (gen a).exp
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DPRINT_PARSETREE.sml214 | printValBind (ValBind{dec, exp, isRecursive, ...} :: rest, depth) =
228 displayParsetree (exp, depth - 1)
251 and printClause (FValClause{dec, exp, ...}, depth) =
258 displayParsetree (exp, depth - 1)
514 | HandleTree {exp, hrules, ...} =>
517 displayParsetree (exp, depth - 1),
639 and displayMatch(MatchTree {vars, exp, ...}, depth) =
646 displayParsetree (exp, depth - 1)
H A DBaseParseTreeSig.sml135 | Localdec of (* Local dec in dec and let dec in exp. *)
179 { exp: parsetree, hrules: matchtree list, location: location, listLocation: location }
212 exp: parsetree,
239 exp: parsetree,
285 exp: parsetree,
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputeRingScript.sml578 Note (ZN n).sum.exp 1 c = c MOD m by ZN_num, 0 < n
579 and (ZN n).sum.op ((ZN n).sum.exp 1 1) ((ZN n).sum.exp 1 c)
580 = ((ZN n).sum.exp 1 1) + (ZN n).sum.exp 1 c)) MOD n by ZN_property
591 = [(ZN n).sum.op ((ZN n).sum.exp 1 1) ((ZN n).sum.exp 1 c)] by above
597 = PAD_RIGHT (ZN n).sum.id [(ZN n).sum.op ((ZN n).sum.exp 1 1) ((ZN n).sum.exp 1 c)] by above
604 ((ZN n).sum.exp
[all...]
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolynomialScript.sml83 ## = (PolyRing r).sum.exp |1|
84 ** = (PolyRing r).prod.exp
90 poly_num r = (PolyRing r).sum.exp (poly_one r)
91 poly_exp r = (PolyRing r).prod.exp
330 val _ = overload_on ("##", ``(PolyRing r).sum.exp |1|``);
331 val _ = overload_on ("**", ``(PolyRing r).prod.exp``);
339 val _ = overload_on("poly_num", ``\r. (PolyRing r).sum.exp (poly_one r)``);
340 val _ = overload_on("poly_exp", ``\r. (PolyRing r).prod.exp``);
/seL4-l4v-master/HOL4/examples/acl2/examples/
H A DtestEncode.sml88 | Let of dec => exp;
90 exp = Exp1 of atexp
91 | Exp2 of exp => atexp
97 rule = Rule of pat => exp;
102 valbind = Single of pat => exp
103 | Multi of pat => exp => valbind
231 ``:One``,``:('a,'b) Term``,``:'a List``,``:('a,'b) Btree``,``:Command``,``:tri``,``:exp``,``:Steve0``,``:('a,'b,'c) TY1``,``:atpat_e``];

Completed in 280 milliseconds

12345678910