Searched refs:sum (Results 1 - 25 of 240) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DringIntegerScript.sml66 Z_def |- Z = <|carrier := univ(:int); sum := Z_add; prod := Z_mult|>
77 sum := <|carrier := Z_multiple n; op := Z.sum.op; id := Z.sum.id|>;
82 Z_ideal_sum_group |- !n. Group (Z* n).sum
83 Z_ideal_sum_subgroup |- !n. (Z* n).sum <= Z.sum
84 Z_ideal_sum_normal |- !n. (Z* n).sum << Z.sum
89 Z_sum_cogen |- !n. 0 < n ==> !x. x IN Z.sum
[all...]
H A DringIdealScript.sml56 x o I = coset r.sum x i.carrier
70 i.sum <= r.sum /\ (i.sum.carrier = I) /\
73 ideal_has_subgroup |- !r i. i << r ==> i.sum <= r.sum
74 ideal_carriers |- !r i. i << r ==> (i.sum.carrier = I) /\ (i.prod.carrier = I)
76 ideal_element |- !r i. i << r ==> !x. x IN I ==> x IN r.sum.carrier
77 ideal_ops |- !r i. i << r ==> (i.sum.op = $+) /\ (i.prod.op = $* )
88 ideal_zero |- !r i. Ring r /\ i << r ==> (i.sum
[all...]
H A DringMapScript.sml54 #0_ = (r_:'b ring).sum.id
56 +_ = (r_:'b ring).sum.op
59 neg_ = (r_:'b ring).sum.inv
60 ##_ = (r_:'b ring).sum.exp
76 GroupHom f r.sum s.sum /\ MonoidHomo f r.prod s.prod
171 subring_sum_subgroup |- !r s. subring s r ==> subgroup s.sum r.sum
174 Ring r /\ Ring s /\ subgroup s.sum r.sum /\ submonoi
[all...]
H A DquotientRingScript.sml59 R/I = CosetPartition r.sum i.sum
60 gen x = cogen r.sum i.sum x
78 sum := quotient_ring_add r i;
82 ((r / i).sum = quotient_ring_add r i) /\
125 quotient_ring_homo_kernel |- !r i. Ring r /\ i << r ==> (kernel (\x. x o I) r.sum (r / i).sum = I)
129 <|carrier := kernel f r.sum s.sum;
[all...]
H A DringScript.sml52 r.sum = Addition component of Ring, binary operation overloaded as +.
56 + = r.sum.op
57 #0 = r.sum.id
58 ## = r.sum.exp
59 - = r.sum.inv
74 Ring_def |- !r. Ring r <=> AbelianGroup r.sum /\ AbelianMonoid r.prod /\
75 (r.sum.carrier = R) /\ (r.prod.carrier = R) /\
80 # ring_carriers |- !r. Ring r ==> (r.sum.carrier = R) /\ (r.prod.carrier = R)
81 ring_add_group |- !r. Ring r ==> Group r.sum /\ (r.sum
[all...]
/seL4-l4v-master/HOL4/examples/CCS/
H A DObsCongrLawsScript.sml22 (* Prove OBS_SUM_IDENT_R: |- !E. OBS_CONGR (sum E nil) E *)
27 (* Prove OBS_SUM_IDENT_L: |- !E. OBS_CONGR (sum nil E) E *)
32 (* Prove OBS_SUM_IDEMP: |- !E. OBS_CONGR (sum E E) E *)
37 (* Prove OBS_SUM_COMM: |- !E E'. OBS_CONGR (sum E E') (sum E' E) *)
43 |- !E E' E''. OBS_CONGR (sum (sum E E') E'') (sum E (sum E' E''))
50 |- !E E' E''. OBS_CONGR (sum
[all...]
H A DWeakLawsScript.sml21 (* Prove WEAK_SUM_IDENT_R: |- !E. WEAK_EQUIV (sum E nil) E *)
26 (* Prove WEAK_SUM_IDENT_L: |- !E. WEAK_EQUIV (sum nil E) E *)
31 (* Prove WEAK_SUM_IDEMP: |- !E. WEAK_EQUIV (sum E E) E *)
36 (* Prove WEAK_SUM_COMM: |- !E E'. WEAK_EQUIV (sum E E') (sum E' E) *)
44 (!E''. WEAK_EQUIV (sum E'' E) (sum E'' E'))
58 |- !E E' E''. WEAK_EQUIV (sum (sum E E') E'') (sum
[all...]
H A DCoarsestCongrScript.sml27 |- !E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))
31 ``!E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))``,
34 (SPEC ``sum E' E`` (GEN_ALL (OC_SYM (SPEC_ALL TAU2))))
36 >> OC_LHS_SUBST1_TAC (SPEC ``sum E' E`` TAU2));
192 "SUM_EQUIV", ``SUM_EQUIV = (\p q. !r. WEAK_EQUIV (sum p r) (sum
[all...]
H A DStrongLawsScript.sml17 (* Basic laws of strong equivalence for the sum operator (sum_strong_laws) *)
21 (* Prove STRONG_SUM_IDENT_R: |- !E. STRONG_EQUIV (sum E nil) E *)
23 "STRONG_SUM_IDENT_R",``!E. STRONG_EQUIV (sum E nil) E``,
27 ``\x y. (x = y) \/ (?E'. (x = sum E' nil) /\ (y = E'))``
45 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = sum E'' nil``]
56 (* Prove STRONG_SUM_IDEMP: |- !E. STRONG_EQUIV (sum E E) E *)
58 "STRONG_SUM_IDEMP", ``!E. STRONG_EQUIV (sum E E) E``,
62 ``\x y. (x = y) \/ (?E'. (x = sum E' E') /\ (y = E'))``
80 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = sum E'' E''``]
90 (* Prove STRONG_SUM_COMM: |- !E E'. STRONG_EQUIV(sum
[all...]
/seL4-l4v-master/HOL4/src/coretypes/
H A DsumSyntax.sml11 mk_thy_type {Tyop = "sum", Thy = "sum", Args = [ty1, ty2]}
15 SOME {Tyop = "sum", Thy = "sum", Args = [ty1, ty2]} => (ty1, ty2)
16 | other => raise ERR "dest_sum" "not a sum type"
25 Thy = "sum",
38 val monop = HolKernel.syntax_fns1 "sum"
53 "sum" "INL"
63 "sum" "INR"
69 datatype ('a,'b) sum
[all...]
H A DsumSimps.sml11 val SUM_ss = BasicProvers.thy_ssfrag "sum"
H A DsumScript.sml4 (* the sum type operator. The sum type is defined and *)
38 val _ = new_theory "sum";
46 (* The sum of types `:'a` and `:'b` will be represented by a certain *)
77 val sum_TY_DEF = new_type_definition ("sum", EXISTS_SUM_REP);
78 val _ = add_infix_type {Prec = 60, ParseName = SOME "+", Name = "sum",
83 (* Define a representation function, REP_sum, from the type ('a,'b)sum to *)
103 (* Define the injection function INL:'a->('a,'b)sum *)
105 ���!e.(INL:'a->(('a,'b)sum)) e = ABS_sum(\b x (y:'b). (x = e) /\ b)���);
107 (* Define the injection function INR:'b->( 'a,'b )sum *)
[all...]
H A DsumSyntax.sig40 datatype ('a, 'b) sum = INL of 'a | INR of 'b
44 -> ('a,'b)sum
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Dhalfaddn.ml25 "HALFADD_IMP (a:^wire,cin:^wire,sum:^wire,cout:^wire) =
26 AND_IMP (a,cin,cout) /\ XOR_IMP (a,cin,sum)");;
30 "(HALFADDn_IMP 0 (a:^bus) (cin:^wire) (sum:^bus) (cout:^wire) =
31 HALFADD_IMP (DEST_BUS a 0,cin,DEST_BUS sum 0,cout)) /\
32 (HALFADDn_IMP (SUC n) a cin sum cout =
34 HALFADDn_IMP n a cin sum c /\
35 HALFADD_IMP (DEST_BUS a (SUC n),c,DEST_BUS sum (SUC n),cout))");;
52 "!i cin sum cout.
53 HALFADD_IMP (i,cin,sum,cout)
57 Def (sum
[all...]
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyModuloRingScript.sml65 #0z = (PolyModRing r z).sum.id
67 p +z q = (PolyModRing r z).sum.op p q
70 negz p = (PolyModRing r z).sum.inv p
72 x ##z n = (PolyModRing r z).sum.exp x n
85 sum := <|carrier := poly_remainders r z; op := (\x y. (x + y) % z); id := |0||>;
91 ((PolyModRing r z).sum.carrier = Rz) /\
95 poly_mod_ring_carriers |- !r z. ((PolyModRing r z).sum.carrier = Rz) /\ ((PolyModRing r z).prod.carrier = Rz)
97 poly_mod_ring_sum_abelian_group |- !r. Ring r ==> !z. ulead z ==> AbelianGroup (PolyModRing r z).sum
107 coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier IN
111 ((coset (PolyRing r).sum
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A Dadder-in-Model.ml14 % PART ADDER_IMP (n) [a(0:n),b(0:n),cin] -> sum(0:n),cout %
19 % ADD1[a(i),b(i),c(i)] -> sum(i),c(i+1) %
31 % ADDER_IMP n (a,b,cin,sum,cout) = %
34 % ITERATE (0,n) (\i. ADD1(a i, b i, c i, sum i, c(i+1))) /\ %
40 % ADDER 0 (a,b,cin,sum,cout) = ADD1(a(0),b(0),cin,sum(0),cout) %
42 % ADDER (SUC n) (a,b,cin,sum,cout) = %
43 % ?c.ADDER n (a,b,cin,sum,c) /\ %
44 % ADD1(a(SUC n),b(SUC n),c,sum(SUC n),cout)) %
192 "ADDER_IMP n (a,b,cin,sum,cou
[all...]
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffInstancesScript.sml82 # GF_2_zero |- (GF 2).sum.id = 0
98 (\x. coset (PolyRing (GF 2)).sum x (principal_ideal (PolyRing (GF 2)) h).carrier)
105 # GF_4_sum_id |- GF_4.sum.id = []
119 GF_4_sum_1_1 |- GF_4.sum.op [1] [1] = []
120 GF_4_sum_1_a |- GF_4.sum.op [1] [0; 1] = [1; 1]
121 GF_4_sum_1_b |- GF_4.sum.op [1] [1; 1] = [0; 1]
122 GF_4_sum_a_b |- GF_4.sum.op [0; 1] [1; 1] = [1]
132 GF_4_sum_x_x |- !x. x IN GF_4.carrier ==> (GF_4.sum.op x x = GF_4.sum.id)
133 GF_4_neg |- !x. x IN GF_4.carrier ==> (GF_4.sum
[all...]
H A DffBasicScript.sml46 val _ = overload_on ("ring_numr", ``r.sum.exp #1``); (* for fallback *)
47 val _ = overload_on ("##", ``r.sum.exp #1``); (* current use *)
53 val _ = overload_on ("##", ``(PolyRing r).sum.exp |1|``);
71 sum := <|carrier := IMAGE $## univ(:num); op := $+; id := #0|>;
75 ((PF r).sum.carrier = IMAGE $## univ(:num)) /\
76 ((PF r).sum.op = $+) /\ ((PF r).sum.id = #0) /\
82 prime_field_sum_abelian_group |- !r. Field r /\ 0 < char r ==> AbelianGroup (PF r).sum
97 prime_field_neg |- !r. FiniteField r ==> !x. x IN Fp ==> ((PF r).sum.inv x = -x)
111 scalar_ring_sum_abelian_group |- !r. Ring r /\ 0 < char r ==> AbelianGroup (PF r).sum
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A DTEA.sml76 let (cipheredtxt,keys,sum) = Rounds(32w,(txt,keys,0w)) in
90 `InvRound(y,z,k0,k1,k2,k3,sum) =
91 (y - ShiftXor(z - ShiftXor(y, sum, k2, k3), sum, k0, k1),
92 z - ShiftXor(y, sum, k2, k3),
94 sum-DELTA)`;
116 let (plaintxt,keys,sum) = InvRounds(32w,(txt,keys,DELTA << 5))
/seL4-l4v-master/HOL4/examples/algebra/field/
H A DfieldMapScript.sml55 f_* = (r_:'b field).prod excluding r_.sum.id
175 subgroup s.sum r.sum /\ submonoid s.prod r.prod
180 subfield_zero |- !r s. s <<= r ==> (s.sum.id = #0)
182 subfield_ids |- !r s. s <<= r ==> (s.sum.id = #0) /\ (s.prod.id = #1)
186 (s.sum.op x y = x + y) /\ (s.prod.op x y = x * y)
187 subfield_add |- !r s. s <<= r ==> !x y. x IN B /\ y IN B ==> (s.sum.op x y = x + y)
189 subfield_neg |- !r s. s <<= r ==> !x. x IN B ==> (s.sum.inv x = -x)
191 subfield_num |- !r s. s <<= r ==> !n. s.sum.exp s.prod.id n = ##n
199 (s.sum
[all...]
H A DfieldIdealScript.sml64 (* The carrier of Ideal = carrier of group i.sum *)
66 (* The carrier of Ideal = carrier of group j.sum *)
104 (2) (r / i).prod.id <> (r / i).sum.id
111 (3) x IN (r / i).carrier /\ x <> (r / i).sum.id ==> ?y. y IN (r / i).carrier /\ ((r / i).prod.op x y = (r / i).prod.id)
181 (r/r).sum.id = R by field_zero_element, IN_SING
190 `(r/r).sum.id IN (r/r).carrier /\ (r/r).prod.id IN (r/r).carrier` by rw[] >>
198 (r/r).sum.id = R by field_zero_element, IN_SING
218 `(homo_ideal (\x. x o I) r (r/i) j = principal_ideal (r / i) (r / i).sum.id) \/
220 `(principal_ideal (r / i) (r / i).sum.id).carrier = {(r / i).sum
[all...]
/seL4-l4v-master/HOL4/src/probability/
H A DiterateScript.sml2600 val _ = overload_on ("sum",``Sum``);
2621 ``!f s. ~(FINITE {x | x IN s /\ ~(f x = &0)}) ==> (sum s f = &0)``,
2626 ``(!f. sum {} f = &0) /\
2628 ==> ((sum (x INSERT s) f =
2629 if x IN s then sum s f else f(x) + sum s f)))``,
2636 ==> ((sum (s UNION t) f = sum s f + sum t f))``,
2640 ``!f s t. FINITE s /\ t SUBSET s ==> (sum (
[all...]
/seL4-l4v-master/HOL4/examples/Crypto/TEA/
H A DteaScript.sml53 `(!x:state. P x) = !v0 v1 k0 k1 k2 k3 sum. P((v0,v1),(k0,k1,k2,k3),sum)`,
102 let (cipheredtxt,keys,sum) = Rounds(32w,(txt,keys,0w)) in
116 `InvRound((y,z),(k0,k1,k2,k3),sum) =
117 let z' = z - ShiftXor(y, sum, k2, k3) in
118 let y' = y - ShiftXor(z',sum, k0, k1) in
119 let sum' = sum-DELTA
121 ((y',z'), (k0,k1,k2,k3), sum')`;
139 let (plaintxt,keys,sum)
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/MISC/
H A Dmk_adders.old.ml29 p4|---------+-------| |--sum p1|------------+--------| |--cout
80 "ADD1_IMP(a,b,cin,sum,cout) =
90 PWR(p0) /\ PTRAN(p4,p0,sum) /\ NTRAN(p4,sum,p11) /\
189 "ADD2_IMP(a,b,cin,sum,cout) =
192 PTRAN(cin,p0,p1) /\ NTRAN(cin,p1,p5) /\ PTRAN(p3,p1,sum) /\
193 NTRAN(p2,p1,sum) /\ PTRAN(p2,cin,sum) /\ NTRAN(p3,cin,sum) /\
/seL4-l4v-master/HOL4/examples/hardware/hol88/cmos/
H A Dmk_adders.ml29 p4|---------+-------| |--sum p1|------------+--------| |--cout
80 "ADD1_IMP(a,b,cin,sum,cout) =
90 PWR(p0) /\ PTRAN(p4,p0,sum) /\ NTRAN(p4,sum,p11) /\
193 "ADD2_IMP(a,b,cin,sum,cout) =
196 PTRAN(cin,p0,p1) /\ NTRAN(cin,p1,p5) /\ PTRAN(p3,p1,sum) /\
197 NTRAN(p2,p1,sum) /\ PTRAN(p2,cin,sum) /\ NTRAN(p3,cin,sum) /\

Completed in 228 milliseconds

12345678910