| The "fold" operators defined in the CommunityModules [1] are your friend here. Something along the lines of CMPN == [f \in BVN |-> [g \in BVN |-> FoldFunction(LAMBDA x,y : x /\ y, TRUE, [i \in 0 .. N |-> ~XOR[f][g][i]])] where the operator FoldFunction comes from the modules Functions of the CommunityModules. I have not actually tried this, though. Also, be aware that at this point the standard proof library does not yet contain lemmas about fold operators, so you will want to state (without proof) basic lemmas such as the ones asserted below (copied from [2]). Stephan IsAssociativeOn(op(_,_), S) == \A x,y,z \in S : op(x, op(y,z)) = op(op(x,y), z) IsCommutativeOn(op(_,_), S) == \A x,y \in S : op(x,y) = op(y,x) IsIdentityOn(op(_,_), e, S) == \A x \in S : op(e,x) = x LEMMA FoldFunctionIsFoldFunctionOnSet == ASSUME NEW op(_,_), NEW base, NEW fun PROVE FoldFunction(op, base, fun) = FoldFunctionOnSet(op, base, fun, DOMAIN fun) LEMMA FoldFunctionOnSetEmpty == ASSUME NEW op(_,_), NEW base, NEW fun PROVE FoldFunctionOnSet(op, base, fun, {}) = base LEMMA FoldFunctionOnSetIterate == ASSUME NEW op(_,_), NEW S, IsFiniteSet(S), NEW T, NEW base \in T, NEW fun \in [S -> T], NEW inds \in SUBSET S, NEW e \in inds, IsAssociativeOn(op, T), IsCommutativeOn(op, T), IsIdentityOn(op, base, T) PROVE FoldFunctionOnSet(op, base, fun, inds) = op(fun[e], FoldFunctionOnSet(op, base, fun, inds \ {e}))
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/D7C94004-FFE4-4CCE-A3FC-DEDC8D891F33%40gmail.com. |