/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_FUNCTIONS.sml | 32 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 D | lisp_proofScript.sml | 98 ``!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 D | automation_lemmasScript.sml | 455 (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 D | transcScript.sml | 65 (* 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 D | complexScript.sml | 1432 ``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 D | milawa_logicScript.sml | 207 (!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 D | Pmatch.sml | 579 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 D | lisp_bigopsScript.sml | 264 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 D | IntDP_Munge.sml | 125 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 D | OmegaMath.sig | 118 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 D | submonoidScript.sml | 54 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 D | integralDomainScript.sml | 60 ## = 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 D | refine.sml | 242 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 D | SML90.sml | 39 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 D | RealSignature.sml | 80 val toManExp : real -> {man : real, exp : int} 81 val fromManExp : {man : real, exp : int} -> real
|
H A D | IEEE_REAL.sml | 41 { class : float_class, sign : bool, digits : int list, exp : int }
|
H A D | MATH.sml | 36 val exp : real -> real value
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | testTypesScript.sml | 167 | 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 D | congruencesScript.sml | 88 ((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 D | groupOrderScript.sml | 125 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 D | PRINT_PARSETREE.sml | 214 | 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 D | BaseParseTreeSig.sml | 135 | 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 D | computeRingScript.sml | 578 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 D | polynomialScript.sml | 83 ## = (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 D | testEncode.sml | 88 | 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``];
|