/seL4-l4v-master/HOL4/examples/algebra/ring/ |
H A D | ringIntegerScript.sml | 66 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 D | ringIdealScript.sml | 56 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 D | ringMapScript.sml | 54 #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 D | quotientRingScript.sml | 59 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 D | ringScript.sml | 52 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 D | ObsCongrLawsScript.sml | 22 (* 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 D | WeakLawsScript.sml | 21 (* 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 D | CoarsestCongrScript.sml | 27 |- !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 D | StrongLawsScript.sml | 17 (* 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 D | sumSyntax.sml | 11 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 D | sumSimps.sml | 11 val SUM_ss = BasicProvers.thy_ssfrag "sum"
|
H A D | sumScript.sml | 4 (* 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 D | sumSyntax.sig | 40 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 D | halfaddn.ml | 25 "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 D | polyModuloRingScript.sml | 65 #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 D | adder-in-Model.ml | 14 % 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 D | ffInstancesScript.sml | 82 # 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 D | ffBasicScript.sml | 46 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 D | TEA.sml | 76 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 D | fieldMapScript.sml | 55 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 D | fieldIdealScript.sml | 64 (* 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 D | iterateScript.sml | 2600 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 D | teaScript.sml | 53 `(!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 D | mk_adders.old.ml | 29 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 D | mk_adders.ml | 29 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) /\
|